ImpAlg.Adequacy
Set Implicit Arguments.
Set Contextual Implicit.
Require Import Utf8.
Require Import Setoid.
Require Import Morphisms.
Require Import Relation_Definitions.
Require Import TLC.LibLN.
Require Import Arith.
Require Import Omega.
Require Import Program.
(* Notation "a ~ A" := (single a A). *)
Require Import Sets.Ensembles.
Require Import ImpAlg.Lattices.
Require Import ImpAlg.ImplicativeStructures.
Require Import ImpAlg.Lambda.
Set Contextual Implicit.
Require Import Utf8.
Require Import Setoid.
Require Import Morphisms.
Require Import Relation_Definitions.
Require Import TLC.LibLN.
Require Import Arith.
Require Import Omega.
Require Import Program.
(* Notation "a ~ A" := (single a A). *)
Require Import Sets.Ensembles.
Require Import ImpAlg.Lattices.
Require Import ImpAlg.ImplicativeStructures.
Require Import ImpAlg.Lambda.
The goal of this file is to prove the adequacy of the interpretation of λ-terms in implicative structures.
Namely, writting - the intepretations of terms and types, we want to prove the following implication:
⊢ t: T => t ≤ T
From now on, we assume that an implicative structure is fixed, we shall refer to it as IS.
Section Adequacy.
Context `{IS:ImplicativeStructure}.
Infix "@" := (app ) (at level 59, left associativity):ia_scope.
Notation "λ- f":= (abs f) (at level 60):ia_scope.
Definition cc `{IS:ImplicativeStructure} :=⋂[a] (⋂[b] (((a ↦ b) ↦ a) ↦ a)).
Proof tactics
Ltac gather_vars :=
let A := gather_vars_with (fun x : vars => x) in
let B := gather_vars_with (fun x : var => \{x}) in
let C := gather_vars_with (fun x : env => (dom x)\u (@codom X x)) in
let D := gather_vars_with (fun x : trm => @fv_trm X x) in
let E := gather_vars_with (fun x : typ => @fv_typ X x) in
constr:(A \u B \u C \u D \u E).
let A := gather_vars_with (fun x : vars => x) in
let B := gather_vars_with (fun x : var => \{x}) in
let C := gather_vars_with (fun x : env => (dom x)\u (@codom X x)) in
let D := gather_vars_with (fun x : trm => @fv_trm X x) in
let E := gather_vars_with (fun x : typ => @fv_typ X x) in
constr:(A \u B \u C \u D \u E).
Tactic pick_fresh x adds to the context a new variable x
and a proof that it is fresh from all of the other variables
gathered by tactic gather_vars.
Ltac pick_fresh Y :=
let L := gather_vars in (pick_fresh_gen L Y).
Tactic apply_fresh T as y takes a lemma T of the form
forall L ..., (forall x, x \notin L, P x) -> ... -> Q.
instanciate L to be the set of variables occuring in the
context (by gather_vars), then introduces for the premise
with the cofinite quantification the name x as "y" (the second
parameter of the tactic), and the proof that x is not in L.
Tactic Notation "apply_fresh" constr(T) "as" ident(x) :=
apply_fresh_base T gather_vars x.
Tactic Notation "apply_fresh" "*" constr(T) "as" ident(x) :=
apply_fresh T as x; auto_star.
Tactic Notation "apply_fresh" constr(T) :=
apply_fresh_base T gather_vars ltac_no_arg.
Tactic Notation "apply_fresh" "*" constr(T) :=
apply_fresh T; auto_star.
We define some tactics to automatize the resolution of goals
involving simple inequalities and arbitrary meet
Ltac adjunction_mon:=
repeat
match goal with
| |- (_ ↦ ?a ≤ _ ↦ ?a) => apply arrow_mon_l
| |- (?a ↦ _ ≤ ?a ↦ _ )=> apply arrow_mon_r
| |- _@?a ≤ _@?a => apply app_mon_l
| |- _ ≤ ?a ↦ (_@?a)=> apply adjunction
| |- ?a ≤ _ ↦ (?a@_)=> apply adjunction
| |- (?a ↦ _)@?a ≤ _ => apply adjunction
| |- (_ ↦ ?a)@_ ≤ ?a => apply adjunction
end;try (apply ord_refl); auto.
Ltac repeat_meet_intro :=
repeat
(apply meet_intro;intros ?x ?Hx;
repeat (
match goal with
| Ha: exists x, _ |- _ => destruct Ha as (?x,?Hx)
| Ha: ?a = _ |- _ ≤ ?a => rewrite Ha
| Ha: _ ∧ _ |- _ => destruct Ha as (?Ha1,?Ha2)
end)
).
Ltac auto_meet_elim :=
apply meet_elim;
match goal with
| |- (exists !a, ?b ↦ _ = ?a ↦ _ )=> exists ?b;reflexivity
| |- _ => auto
end.
Embedding of λ-terms and types into implicative structures
Definition substitution := var → X.
Definition update σ v c:var → X :=
fun a => If v=a then c else σ a.
Application of a substitution to a pre-term:
Fixpoint subst_trm (t:trm) (σ:substitution) {struct t} :=
match t with
|trm_bvar n => trm_bvar n
|trm_fvar a => trm_cvar (σ a)
|trm_cvar a => trm_cvar a
|trm_abs t0 => trm_abs (subst_trm t0 σ)
|trm_app t u => trm_app (subst_trm t σ) (subst_trm u σ)
|trm_cc => trm_cc
end.
Application of a substitution to a pre-type:
Fixpoint subst_typ (T:typ) (σ:substitution) {struct T} :=
match T with
|typ_bvar n => typ_bvar n
|typ_fvar X => typ_cvar (σ X)
|typ_cvar a => typ_cvar a
|typ_fall T => typ_fall (subst_typ T σ)
|typ_arrow T U => typ_arrow (subst_typ T σ) (subst_typ U σ)
end.
Notation "{ k ~> u } t" := (open_rec_trm k t u) (at level 67).
Notation "t ^^ u" := (open_trm t u) (at level 67).
Notation "t ^c a" := (open_trm t (trm_cvar a)) (at level 67).
Notation "t ^v a" := (open_trm t (trm_fvar a)) (at level 67).
Notation "{ k ~t> U } T" := (open_rec_typ k T U) (at level 67).
Notation "T ^t^ U" := (open_typ T U) (at level 67).
Notation "T ^tc a" := (open_typ T (typ_cvar a)) (at level 67).
Notation "T ^t X" := (open_typ T (typ_fvar X)) (at level 67).
Properties of the substitutions wrt free variables
Lemma subst_trm_var: ∀ t u x σ τ , u \notin fv_trm(t) → τ u = x → (∀ y, y ≠ u→ τ y=σ y)
→ subst_trm (t ^v u) τ = subst_trm t σ ^c x.
Proof.
intro t.
unfold open_trm.
generalize 0.
induction t;intros k u a σ τ Hu Ha H;simpl in *;auto.
- case_nat;simpl;auto. now rewrite Ha.
- f_equal; now apply H, not_eq_sym, notin_singleton.
- rewrite (IHt _ _ a σ);auto.
- rewrite (IHt1 _ _ a σ);auto.
rewrite (IHt2 _ _ a σ);auto.
Qed.
→ subst_trm (t ^v u) τ = subst_trm t σ ^c x.
Proof.
intro t.
unfold open_trm.
generalize 0.
induction t;intros k u a σ τ Hu Ha H;simpl in *;auto.
- case_nat;simpl;auto. now rewrite Ha.
- f_equal; now apply H, not_eq_sym, notin_singleton.
- rewrite (IHt _ _ a σ);auto.
- rewrite (IHt1 _ _ a σ);auto.
rewrite (IHt2 _ _ a σ);auto.
Qed.
Translation of terms
Inductive translated : trm → X → Prop :=
|tr_cvar: ∀ x, translated (trm_cvar x) x
|tr_abs: ∀ t f, (∀ x, translated (t ^c x) (f x)) → translated (trm_abs t) (λ- (fun x => f x))
|tr_app: ∀ t u x y, translated t x → translated u y → translated (trm_app t u) (x@y)
|tr_cc : translated trm_cc (cc )
.
We now define the translation of pre-types as a fixpoint.
To prove that this fixpoint terminates,
we need to define it with an extra parameter (the fioul)
which will be taken as the size of the pre-type we translate.
Fixpoint trans_trm_aux (σ:substitution) (t:@trm X) fioul {struct fioul}: X :=
match fioul with
| 0 => (top)
| Datatypes.S f =>
(match t:trm with
|trm_cvar x => x
|trm_fvar x => σ x
|trm_cc => cc
|trm_app t1 t2 => (trans_trm_aux σ t1 f) @ (trans_trm_aux σ t2 f)
|trm_abs t' => (λ- (λ x,trans_trm_aux σ (t' ^c x) f))
| _ => (top)
end)
end.
Definition trans_trm σ t:=trans_trm_aux σ t (size t).
We prove the soundness of the fixpoint with respect to the function "translated".
The function trans_trm is intrinsically limited by the size of the pre-term in argument,
that is to say that if the amount of fioul is superior to the size of the argument, the result is unchanged.
Lemma trans_trm_fioul_aux:
∀ n p t σ, p<= n → size t <= p → trans_trm_aux σ t p = trans_trm_aux σ t (size t).
Proof.
intro n;induction n;intros p t σ Hp Size;[exfalso;apply (size_not_0 t);omega|].
destruct t; destruct p;simpl in *;trivial;try omega.
- apply ord_antisym;apply meet_intro;intros z (y,Hy) ;apply meet_elim;exists y;rewrite Hy;
rewrite <- (size_open_c t y 0) in *;[symmetry | ];f_equal;apply* IHn; omega.
- assert (H1:=size_le_1 t1). assert (H2:=size_le_1 t2). omega.
- assert (size t1 + size t2 <= S n) as H by omega.
destruct (size_plus_S t1 t2) as (m,(Hm,(Hm1,Hm2))).
rewrite Hm. simpl.
f_equal;symmetry; rewrite IHn;try omega;symmetry;apply IHn;omega.
Qed.
Lemma trans_trm_fioul:
∀ p t σ, size t <= p → trans_trm_aux σ t p = trans_trm_aux σ t (size t).
Proof.
intros p t σ Size; apply (@trans_trm_fioul_aux p);trivial.
Qed.
Lemma trans_trm_fold:
∀ t σ n, size t <= n → trans_trm_aux σ t n = trans_trm σ t.
Proof.
intros t σ n Size. unfold trans_trm.
apply trans_trm_fioul;trivial.
Qed.
Properties of the translation function
Translation of application
Lemma trans_trm_app:
∀ t u σ, trans_trm σ (trm_app t u) = (trans_trm σ t) @ (trans_trm σ u).
Proof.
intros.
unfold trans_trm.
simpl.
destruct (size_plus_S t u) as (p,(Hp,(Hp1,Hp2))).
rewrite Hp. simpl.
rewrite~ trans_trm_fioul.
f_equal.
rewrite~ trans_trm_fioul.
Qed.
∀ t u σ, trans_trm σ (trm_app t u) = (trans_trm σ t) @ (trans_trm σ u).
Proof.
intros.
unfold trans_trm.
simpl.
destruct (size_plus_S t u) as (p,(Hp,(Hp1,Hp2))).
rewrite Hp. simpl.
rewrite~ trans_trm_fioul.
f_equal.
rewrite~ trans_trm_fioul.
Qed.
Translation of abstraction
Lemma trans_trm_abs:
∀ t σ, trans_trm (σ:substitution) (trm_abs t) = (λ- (λ x, trans_trm σ (t ^c x))).
Proof.
intros.
unfold trans_trm,open_trm.
simpl.
apply ord_antisym.
- apply meet_intro;intros x (y,Hy) ;apply meet_elim;exists y; rewrite~ (@size_open_c X) in Hy.
- apply meet_intro;intros x (y,Hy) ;apply meet_elim;exists y; rewrite~ (@size_open_c X).
Qed.
∀ t σ, trans_trm (σ:substitution) (trm_abs t) = (λ- (λ x, trans_trm σ (t ^c x))).
Proof.
intros.
unfold trans_trm,open_trm.
simpl.
apply ord_antisym.
- apply meet_intro;intros x (y,Hy) ;apply meet_elim;exists y; rewrite~ (@size_open_c X) in Hy.
- apply meet_intro;intros x (y,Hy) ;apply meet_elim;exists y; rewrite~ (@size_open_c X).
Qed.
The most technical lemma, to prove that if t is a pre-term,
v a fresh variable, σ a substitution and a an element of IS, then
the translation of t{0:=v} with the subsitution σv:=a is equal
to the translation of t{0:=a} with the substitution σ .
Hint Resolve term_cvar term_var term_abs term_app.
Lemma trans_trm_var: ∀ t v x (σ:substitution) τ, v \notin fv_trm(t) → τ v = x → (∀ y, y ≠ v→ τ y=σ y)
→ trans_trm τ (t ^v v) = trans_trm σ (t ^c x).
Proof.
intro t. unfold open_trm. generalize 0.
apply (size_ind (fun t => ∀ (n:nat) (v : var) (x : X) (σ τ : var → X),
v \notin fv_trm t → τ v = x → (∀ y : var, y ≠ v → τ y = σ y)
→ trans_trm τ ({n ~> trm_fvar v} t) = trans_trm σ ({n ~> trm_cvar x} t)));auto.
intros n IHn t0 Size k v a σ τ Hv Ha H.
destruct t0;simpl;auto.
- case_nat;compute;auto.
- compute. simpl in Hv.
now apply H, not_eq_sym, notin_singleton.
- do 2 (rewrite trans_trm_abs).
unfold open_trm.
apply ord_antisym;apply meet_intro; intros x (y,Hy);
apply meet_elim; exists y; rewrite Hy;f_equal;
rewrite (@open_trm_com_ct X);auto.
+ rewrite (@open_trm_com_ct X _ (trm_fvar v));auto.
assert (size ({0 ~> trm_cvar y} t0) <= n).
rewrite size_open_c;simpl in Size; now inversion Size.
rewrite (IHn _ H0 _ _ a σ τ);auto.
simpl in Hv. now rewrite fv_trm_subst.
+ rewrite (@open_trm_com_ct X _ (trm_cvar a));auto.
assert (size ({0 ~> trm_cvar y} t0) <= n).
rewrite size_open_c;simpl in Size; now inversion Size.
rewrite (IHn _ H0 _ _ a σ τ);auto.
simpl in Hv. now rewrite fv_trm_subst.
- repeat (rewrite trans_trm_app).
simpl in *.
rewrite~ (IHn _ (size_app_le_l _ _ (Nat.eq_le_incl _ _ Size)) k v a σ τ).
rewrite~ (IHn _ (size_app_le_r _ _ (Nat.eq_le_incl _ _ Size)) k v a σ τ).
Qed.
We can finally prove the correction of the translation of terms :
Lemma trans_correct:
∀ (t:trm) (σ:substitution), term (t:trm) → translated (subst_trm (t:trm) σ ) (trans_trm σ t).
Proof.
intros t σ Term; generalize σ;induction Term;intros.
- compute;simpl. apply tr_cvar.
- compute;simpl. apply tr_cvar.
- simpl. rewrite trans_trm_abs.
apply tr_abs. pick_fresh v.
specialize (H0 v (notin_union_r1 Fr)). intro c.
rewrite~ <-(@subst_trm_var t v c σ0 (update σ0 v c));
try(now intros;compute;try(apply~ If_l);try(apply~ If_r)).
rewrite~ <- (@trans_trm_var t v c σ0 (update σ0 v c));
now intros;compute;try(apply~ If_l);try(apply~ If_r).
- rewrite trans_trm_app. simpl. now apply tr_app.
- simpl;apply tr_cc.
Qed.
Lemma subst_closed: ∀ t σ, fv_trm t = \{} → subst_trm t σ = t.
Proof.
intros t σ H;generalize σ;clear σ;induction t;intros σ.
- reflexivity.
- inversion H. simpl in H1. exfalso.
apply (@notin_empty _ v). rewrite <- H1. apply in_singleton_self.
- reflexivity.
- simpl. rewrite IHt;trivial.
- simpl. rewrite IHt1;[rewrite IHt2|];trivial;simpl in H;
now destruct (union_empty H).
- reflexivity.
Qed.
Lemma translated_closed: ∀ t, closed t → ∃ a, translated t a.
Proof.
intros t (Term,Fv).
pose (σ:=(λ _,top):substitution).
exists (trans_trm σ t).
rewrite <- (subst_closed σ Fv) at 1.
now apply trans_correct.
Qed.
The translation of a term is unique, ie "translated"
is a functional relation in P(term * X):
Lemma translated_unique:
∀ t y z, translated t y → translated t z → y = z.
Proof.
apply (size_ind (fun x => ∀ (y z : X), translated x y → translated x z → y = z)).
intros.
- destruct t.
+ inversion H1.
+ inversion H1.
+ inversion H1. inversion H2.
rewrite <- H3,H5.
reflexivity.
+ inversion H1. inversion H2.
apply ord_antisym; apply meet_intro;
intros a [b Ha]; rewrite Ha;apply meet_elim;
exists b;replace (f0 b) with (f b);auto;
apply (H (t^c b));auto;
inversion H0;unfold open_trm;
rewrite size_open_c;
reflexivity.
+ inversion H1. inversion H2.
replace x with x0.
replace y0 with y1;auto.
apply (H t2 (size_app_le_r t1 t2 (Nat.eq_le_incl _ _ H0)) _ _ H12 H7);auto.
now apply (H t1 (size_app_le_l t1 t2 (Nat.eq_le_incl _ _ H0)) _ _ H10 H5).
+ inversion H1. now inversion H2.
Qed.
Inversion of the property (translated λt a)
Lemma translated_abs_inv :
∀ t a, translated (trm_abs t) a → ∃ f,(a = λ- (λ x : X, f x) ∧ ∀x, translated (t ^c x) (f x)).
Proof.
intros t a H.
inversion H.
exists f;split;trivial.
Qed.
∀ t a, translated (trm_abs t) a → ∃ f,(a = λ- (λ x : X, f x) ∧ ∀x, translated (t ^c x) (f x)).
Proof.
intros t a H.
inversion H.
exists f;split;trivial.
Qed.
If a preterm has a translated element in an IS, then it is term
Lemma translated_term_n: ∀ n (u:@trm X) a, size u<=n → translated u a → term u.
Proof.
intro n; induction n; intros u a Size H;[exfalso; apply (size_not_0 u); omega|].
inversion H.
- apply term_cvar.
- apply_fresh (@term_abs X).
apply (term_subst t _ a).
apply (IHn _ (f a));trivial.
unfold open_trm;rewrite size_open_c.
subst. simpl in Size. omega.
- subst. inversion H. subst. simpl in Size. apply term_app;eapply IHn.
+ now apply size_app_le_l in Size.
+ exact H0.
+ now apply size_app_le_r in Size.
+ exact H1.
- apply term_cc.
Qed.
Lemma translated_term: ∀ (u:@trm X) a, translated u a → term u.
Proof.
intros u a Hu.
now apply (@translated_term_n (size u) u a).
Qed.
Proof.
intro n; induction n; intros u a Size H;[exfalso; apply (size_not_0 u); omega|].
inversion H.
- apply term_cvar.
- apply_fresh (@term_abs X).
apply (term_subst t _ a).
apply (IHn _ (f a));trivial.
unfold open_trm;rewrite size_open_c.
subst. simpl in Size. omega.
- subst. inversion H. subst. simpl in Size. apply term_app;eapply IHn.
+ now apply size_app_le_l in Size.
+ exact H0.
+ now apply size_app_le_r in Size.
+ exact H1.
- apply term_cc.
Qed.
Lemma translated_term: ∀ (u:@trm X) a, translated u a → term u.
Proof.
intros u a Hu.
now apply (@translated_term_n (size u) u a).
Qed.
Compatibility of the translation with substitution
Lemma translated_subst_n: ∀ n t u v a k, size t <= n →
translated u a → translated v a -> ∀ z, (translated ({k~> u} t ) z → translated ({k~> v} t ) z).
Proof.
intro n; induction n; intros t u v a k Size Hu Hv c Ht;[exfalso;apply (size_not_0 t);omega|].
destruct t;cbn in *;trivial.
- case_nat;trivial.
now destruct (translated_unique Hu Ht).
- inversion Ht.
apply tr_abs. intros x.
unfold open_trm. rewrite open_trm_com_ct;[|apply (translated_term Hv)|omega].
apply (IHn _ u _ a);auto.
+ rewrite size_open_c. omega.
+ rewrite <- open_trm_com_ct;[|apply (translated_term Hu)|omega]. apply H0.
- inversion Ht. apply tr_app;apply (IHn _ u _ a);auto;
[now apply size_app_le_l in Size| now apply size_app_le_r in Size].
Qed.
Lemma translated_subst: ∀ t u v a k,
translated u a → translated v a -> ∀ z, (translated ({k~> u} t ) z → translated ({k~> v} t ) z).
Proof.
intros t u v a k Hu Hv c Ht.
now apply (@translated_subst_n (size t) t u v a k).
Qed.
Lemma imp_betared_n:
∀ n t t' a a', size t<= n → size t' <= n → translated t a → translated t' a' → betared t t' → a ≤ a'.
Proof.
intro n; induction n; intros t t' a a' St St' Ht Ht' Hred;[exfalso;apply (size_not_0 t);omega|].
inversion Hred;intros .
- subst. inversion Ht. subst.
destruct (translated_abs_inv H3) as [f [H1 H2]].
subst. apply beta_red.
apply by_refl. symmetry.
apply (translated_unique (Ht')).
apply (@translated_subst _ (trm_cvar y) _ y);[ apply tr_cvar| assumption | apply H2].
- subst. inversion Ht. inversion Ht'. subst.
destruct (translated_unique H5 H10). simpl in *.
apply app_mon_l. apply (IHn t1 t1');trivial;
eapply size_app_le_l; [exact St|exact St'].
- subst. inversion Ht. inversion Ht'. subst.
destruct (translated_unique H3 H8).
apply app_mon_r. apply (IHn t2 t2');trivial;
eapply size_app_le_r; [exact St|exact St'].
- subst. simpl in *. inversion Ht;inversion Ht'.
auto_meet_intro. auto_meet_elim_trans. apply arrow_mon_r.
apply (IHn (t1 ^c a0) (t1' ^c a0));try(unfold open_trm;rewrite size_open_c;omega);trivial.
apply (beta_cvar) with L0;trivial.
Qed.
Lemma imp_betared:
∀ t t' a a', translated t a → translated t' a' → betared t t' → a ≤ a'.
Proof.
intros t t' a a' Ht Ht' Bred.
apply (@imp_betared_n (max (size t) (size t')) t t');auto with arith.
Qed.
Translation of types
Inductive translated_typ : typ → X → Prop :=
|tr_typ_var: ∀ x, translated_typ (typ_cvar x) x
|tr_typ_arrow: ∀ T U x y, (translated_typ T x)
→ (translated_typ U y)
→ translated_typ (typ_arrow T U) (x ↦ y)
|tr_typ_fall: ∀ T f, (∀ x, translated_typ (T ^tc x) (f x))
→ translated_typ (typ_fall T) (⊓ (fun x => ∃ y, x=f y)) .
Fixpoint trans_typ_aux (σ:substitution) (T: typ) fioul {struct fioul}: X :=
match fioul with
| 0 => (top)
| Datatypes.S f =>
(match T with
|typ_cvar x => x
|typ_fvar x => σ x
|typ_arrow T U => (trans_typ_aux σ T (f)) ↦ (trans_typ_aux σ U (f))
|typ_fall T => (⊓ (fun x => ∃ y, x=trans_typ_aux σ (T ^tc y) (f)))
| _ => (top)
end)
end.
Definition trans_typ σ T:=trans_typ_aux σ T (size_typ T).
We prove the soundness of the fixpoint with respect to the function "translated".
Lemma trans_typ_fall: ∀ T σ,
trans_typ (σ:substitution) (typ_fall T) = (⊓ (fun x => ∃ y, x=trans_typ σ (T ^tc y))).
Proof.
intros.
unfold trans_typ,open_typ.
simpl.
apply ord_antisym.
- apply meet_intro;intros x (y,Hy) ;apply meet_elim;exists y; rewrite~ (@size_typ_open X) in Hy.
- apply meet_intro;intros x (y,Hy) ;apply meet_elim;exists y; rewrite~ (@size_typ_open X).
Qed.
(* TODO : REMOVE ? *)
Ltac rewrite_S:=
match goal with
| H:_>=1 |- _ => let HS:= fresh H in destruct (geq_1_S H) as (?,HS);rewrite HS;simpl;try tauto
| H:_>= S _ |- _ => let HS:= fresh H in destruct (geq_S_S H) as (?,(HS,?));rewrite HS;simpl;try tauto
| H:_>= Datatypes.S _ |- _ => let HS:= fresh H in destruct (Datatypes.S H) as (?,(HS,?));rewrite HS;simpl;try tauto
end.
The function trans_typ is intrinsically limited by the size of the pre-type in argument,
that is to say that if the amount of fioul is superior to the size of the argument, the result is unchanged.
Lemma trans_typ_fioul:
∀ T σ n, size_typ T <= n → trans_typ_aux σ T n = trans_typ_aux σ T (size_typ T).
Proof.
apply (size_typ_ind (fun T => ∀ (σ : substitution) (n : nat),
n ≥ size_typ T → trans_typ_aux σ T n = trans_typ_aux σ T (size_typ T))). intros n IH T Size σ m Hm.
- destruct T; simpl in *;try rewrite_S.
+ apply eq_add_S in Size. apply ord_antisym;apply meet_intro;intros z (y,Hy) ;apply meet_elim;exists y;rewrite Hy;
rewrite <- (size_typ_open T y 0) in *;[symmetry | ];apply* IH;rewrite~ Size.
+ destruct (size_typ_plus_S T1 T2) as (p,(Hp,(Hp1,Hp2))).
rewrite Hp in *.
destruct m;try omega.
inversion Size;subst.
inversion Hm;subst;trivial.
simpl.
rewrite~ (IH T1);[|omega].
rewrite~ (IH T2);[|omega].
f_equal;symmetry;apply* IH.
Qed.
Lemma trans_typ_fold:
∀ T σ n, size_typ T <= n → trans_typ_aux σ T n = trans_typ σ T.
Proof.
intros.
unfold trans_typ.
apply~ trans_typ_fioul.
Qed.
Lemma trans_typ_arrow: ∀ T U σ,
trans_typ σ (typ_arrow T U) = (trans_typ σ T) ↦ (trans_typ σ U).
Proof.
intros.
unfold trans_typ.
simpl.
destruct (size_typ_plus_S T U) as (p,(Hp,(Hp1,Hp2))).
rewrite Hp.
simpl.
rewrite~ trans_typ_fioul.
f_equal.
rewrite~ trans_typ_fioul.
Qed.
Lemma subst_typ_var: ∀ T U x σ τ , U \notin fv_typ(T) → τ U = x → (∀ y, y ≠ U→ τ y=σ y)
→ subst_typ (T ^t U) τ = subst_typ T σ ^tc x.
Proof.
intro T.
unfold open_typ.
generalize 0.
induction T;intros k U a σ τ HU Ha H;simpl in *;auto.
- unfold open_typ.
unfold open_rec_typ.
case_nat;simpl;auto.
rewrite~ Ha.
- f_equal; now apply H, not_eq_sym, notin_singleton.
- rewrite (IHT _ _ a σ);auto.
- rewrite (IHT1 _ _ a σ);auto.
rewrite (IHT2 _ _ a σ);auto.
Qed.
Lemma fv_typ_subst: ∀ (T:@typ X) y, fv_typ ({0 ~t> typ_cvar y} T) = fv_typ T.
Proof.
intro T.
generalize 0.
induction T;simpl;intros;auto.
- case_nat;simpl;auto.
- rewrite IHT1.
rewrite~ IHT2.
Qed.
∀ T σ n, size_typ T <= n → trans_typ_aux σ T n = trans_typ_aux σ T (size_typ T).
Proof.
apply (size_typ_ind (fun T => ∀ (σ : substitution) (n : nat),
n ≥ size_typ T → trans_typ_aux σ T n = trans_typ_aux σ T (size_typ T))). intros n IH T Size σ m Hm.
- destruct T; simpl in *;try rewrite_S.
+ apply eq_add_S in Size. apply ord_antisym;apply meet_intro;intros z (y,Hy) ;apply meet_elim;exists y;rewrite Hy;
rewrite <- (size_typ_open T y 0) in *;[symmetry | ];apply* IH;rewrite~ Size.
+ destruct (size_typ_plus_S T1 T2) as (p,(Hp,(Hp1,Hp2))).
rewrite Hp in *.
destruct m;try omega.
inversion Size;subst.
inversion Hm;subst;trivial.
simpl.
rewrite~ (IH T1);[|omega].
rewrite~ (IH T2);[|omega].
f_equal;symmetry;apply* IH.
Qed.
Lemma trans_typ_fold:
∀ T σ n, size_typ T <= n → trans_typ_aux σ T n = trans_typ σ T.
Proof.
intros.
unfold trans_typ.
apply~ trans_typ_fioul.
Qed.
Lemma trans_typ_arrow: ∀ T U σ,
trans_typ σ (typ_arrow T U) = (trans_typ σ T) ↦ (trans_typ σ U).
Proof.
intros.
unfold trans_typ.
simpl.
destruct (size_typ_plus_S T U) as (p,(Hp,(Hp1,Hp2))).
rewrite Hp.
simpl.
rewrite~ trans_typ_fioul.
f_equal.
rewrite~ trans_typ_fioul.
Qed.
Lemma subst_typ_var: ∀ T U x σ τ , U \notin fv_typ(T) → τ U = x → (∀ y, y ≠ U→ τ y=σ y)
→ subst_typ (T ^t U) τ = subst_typ T σ ^tc x.
Proof.
intro T.
unfold open_typ.
generalize 0.
induction T;intros k U a σ τ HU Ha H;simpl in *;auto.
- unfold open_typ.
unfold open_rec_typ.
case_nat;simpl;auto.
rewrite~ Ha.
- f_equal; now apply H, not_eq_sym, notin_singleton.
- rewrite (IHT _ _ a σ);auto.
- rewrite (IHT1 _ _ a σ);auto.
rewrite (IHT2 _ _ a σ);auto.
Qed.
Lemma fv_typ_subst: ∀ (T:@typ X) y, fv_typ ({0 ~t> typ_cvar y} T) = fv_typ T.
Proof.
intro T.
generalize 0.
induction T;simpl;intros;auto.
- case_nat;simpl;auto.
- rewrite IHT1.
rewrite~ IHT2.
Qed.
The most technical lemma, to prove that if T is a pre-type,
X a fresh variable, σ a substitution and a an element of IS, then
the translation of T{0:=X} with the subsitution σX:=a is equal
to the translation of T{0:=a} with the substitution σ .
Lemma trans_typ_var: ∀ T U x (σ:substitution) τ, U \notin fv_typ(T) → τ U = x → (∀ y, y ≠ U→ τ y=σ y)
→ trans_typ τ (T ^t U) = trans_typ σ (T ^tc x).
Proof.
intro T.
unfold open_typ.
generalize 0.
apply (size_typ_ind (fun T => ∀ (n:nat) (U : var) (x : X) (σ τ : var → X),
U \notin fv_typ T
→ τ U = x
→ (∀ y : var, y ≠ U → τ y = σ y)
→ trans_typ τ ({n ~t> typ_fvar U} T) =
trans_typ σ ({n ~t> typ_cvar x} T)));auto.
intros n IHn T0 Size k U a σ τ HU Ha H.
destruct T0;simpl;auto.
- case_nat;compute;auto.
- compute. simpl in HU.
now apply H, not_eq_sym, notin_singleton.
- rewrite trans_typ_fall.
rewrite trans_typ_fall.
unfold open_typ.
apply ord_antisym;apply meet_intro; intros x (y,Hy);
apply meet_elim;exists y; rewrite Hy;
rewrite~ (@open_typ_com_cf X); rewrite~ (@open_typ_com_cc X).
+ symmetry.
assert (size_typ ({0 ~t> typ_cvar y} T0) <= n) as S0;
[rewrite size_typ_open;simpl in Size; now inversion Size|].
apply (IHn _ S0 _ _ a σ τ);auto; simpl in HU;rewrite~ fv_typ_subst.
+ assert (size_typ ({0 ~t> typ_cvar y} T0) <= n) as S0.
rewrite size_typ_open;simpl in Size; now inversion Size.
apply (IHn _ S0 _ _ a σ τ);auto; simpl in HU;rewrite~ fv_typ_subst.
- repeat (rewrite trans_typ_arrow).
simpl in *.
rewrite~ (IHn _ (size_typ_arrow_le_l _ _ (Nat.eq_le_incl _ _ Size)) k U a σ τ).
rewrite~ (IHn _ (size_typ_arrow_le_r _ _ (Nat.eq_le_incl _ _ Size)) k U a σ τ).
Qed.
We can finally prove the correction of the translation of types :
Lemma trans_typ_correct:
∀ T (σ:substitution), type T → translated_typ (subst_typ T σ ) (trans_typ σ T).
Proof.
intros T σ Typ; generalize σ;induction Typ;intros.
- compute;simpl.
apply tr_typ_var.
- compute;simpl.
apply tr_typ_var.
- simpl.
rewrite trans_typ_fall.
apply tr_typ_fall.
pick_fresh U.
specialize (H0 U (notin_union_r1 Fr)).
intro x.
rewrite~ <- (@subst_typ_var T U x σ0 (update σ0 U x));
try(now intros;compute;try(apply~ If_l);try(apply~ If_r)).
rewrite~ <- (@trans_typ_var T U x σ0 (update σ0 U x));
try(now intros;compute;try(apply~ If_l);try(apply~ If_r)).
- rewrite trans_typ_arrow. simpl.
apply~ tr_typ_arrow.
Qed.
The translation of a type is unique:
Lemma translated_typ_unique:
∀ T y z, translated_typ T y → translated_typ T z → y = z.
Proof.
apply (size_typ_ind (fun x => ∀ (y z : X), translated_typ x y → translated_typ x z → y = z)).
intros.
- destruct T.
+ inversion H1.
+ inversion H1.
+ inversion H1. inversion H2.
rewrite <- H3,H5. reflexivity.
+ inversion H1. inversion H2.
apply ord_antisym; apply meet_intro;
intros a [b Ha]; rewrite Ha;
apply meet_elim; exists b;
replace (f0 b) with (f b);auto.
* apply (H (T ^tc b));auto;
inversion H0; unfold open_typ;
rewrite size_typ_open; reflexivity.
* apply (H (T^tc b));auto;
inversion H0; unfold open_typ;
rewrite size_typ_open; reflexivity.
+ inversion H1. inversion H2.
f_equal;symmetry.
* apply (H T1 (size_typ_arrow_le_l _ _ (Nat.eq_le_incl _ _ H0)) _ _ H10 H5);auto.
* apply (H T2 (size_typ_arrow_le_r _ _ (Nat.eq_le_incl _ _ H0)) _ _ H12 H7);auto.
Qed.
We say that a substitution σ "realize" an environement Γ
if for each hypothesis (a:A) ∈ Γ, σ(a) = A^σ :
Inductive realize : substitution → env → Prop:=
|real_empty : ∀ σ, realize σ empty
|real_push : ∀ σ a A Γ b, σ a ≤ b → translated_typ (subst_typ A σ) b → realize σ Γ → realize σ (Γ & (single a A))
.
Lemma realize_inv:
∀ σ x T Γ a, binds x T Γ → realize σ Γ
→ translated_typ (subst_typ T σ) a → σ x ≤ a.
Proof.
intros σ x T Γ.
induction Γ;intros.
- contradict H.
rewrite <- empty_def .
intro.
apply (binds_empty_inv H).
- destruct a as (v,A).
inversion H0.
+ rewrite <- cons_to_push in H2.
inversion H2.
subst v;subst A0;subst Γ0.
clear H2.
rewrite cons_to_push in *.
destruct (@var_eq_dec x a) as [Hx | Hx].
* subst. apply binds_push_eq_inv in H.
subst. rewrite H3.
now destruct (translated_typ_unique H4 H1).
* apply IHΓ;try assumption.
apply (binds_push_neq_inv H Hx).
Qed.
Lemma subst_typ_update:
∀ U σ c y, c \notin (fv_typ U) → subst_typ U (update σ c y) =subst_typ U σ.
Proof.
intro U.
induction U;simpl;intros;auto.
- unfold update. rewrite If_r;[reflexivity|apply (notin_singleton_r H)].
- rewrite IHU;auto.
- rewrite IHU1;auto.
rewrite IHU2;auto.
Qed.
Lemma realize_update:
∀ Γ σ c y, c \notin ((dom Γ)\u (codom Γ)) → realize σ Γ → realize (update σ c y) Γ.
Proof.
intro Γ.
induction Γ;intros.
- apply real_empty.
- destruct a as (v,A).
rewrite cons_to_push in *.
inversion H0.
+ apply real_empty.
+ repeat (rewrite <- cons_to_push in H1).
inversion H1.
rewrite <- H7,H8,H9 in *.
clear H4 H7 H8 H9 H1.
apply (@real_push _ _ _ _ b).
* rewrite <- H2. apply by_refl.
apply If_r. rewrite dom_push in H.
do 2 (apply notin_union_r1 in H).
apply (notin_singleton_r H).
* rewrite subst_typ_update;auto.
rewrite codom_push in H. apply notin_union_r2 in H.
apply notin_union_r1 in H. auto.
* apply IHΓ;auto. rewrite dom_push,codom_push in H.
auto.
Qed.
Lemma subst_trm_update_open: ∀ t σ x v k, v \notin fv_trm t →
({k ~> trm_cvar x} subst_trm t σ) = (subst_trm ({k ~> trm_fvar v} t) (update σ v x)) .
Proof.
intro t.
induction t;intros;simpl.
- destruct (Nat.eq_dec n k); subst;simpl.
+ unfold update;repeat (rewrite~ If_l;simpl).
+ unfold update;repeat (rewrite~ If_r;simpl).
- simpl in H; apply notin_singleton in H.
unfold update; rewrite~ If_r.
- simpl;reflexivity.
- simpl. f_equal.
apply IHt. now simpl in H.
- simpl in H.
apply notin_union in H as (H1,H2).
f_equal;[apply~ IHt1|apply~ IHt2].
- reflexivity.
Qed.
Lemma subst_trm_update: ∀ t σ x v, v \notin fv_trm t →
(subst_trm t σ) = (subst_trm t (update σ v x)).
Proof.
intro t.
induction t;intros;simpl;try intuition.
- simpl in H; apply notin_singleton in H.
unfold update; rewrite~ If_r.
- f_equal;apply IHt. now simpl in H.
- simpl in H. apply notin_union in H as (H1,H2).
f_equal;[apply~ IHt1|apply~ IHt2].
Qed.
Hint Unfold open_typ.
Lemma trans_typ_update:∀ T U σ y k, y \notin (fv_typ T) → trans_typ σ ({k ~t> typ_cvar (trans_typ σ U)} T) =
trans_typ (update σ y (trans_typ σ U)) ({k ~t> typ_cvar (trans_typ σ U)} T).
Proof.
apply (size_typ_ind (fun T => ∀ U σ y k, y \notin (fv_typ T) → trans_typ σ ({k ~t> typ_cvar (trans_typ σ U)} T) = trans_typ (update σ y (trans_typ σ U)) ({k ~t> typ_cvar (trans_typ σ U)} T))).
intros n IH T Size U σ y k Fr.
destruct T;simpl;intros.
- destruct (Nat.eq_dec n0 k); subst;simpl.
+ unfold update;repeat (rewrite~ If_l;simpl).
+ unfold update;repeat (rewrite~ If_r;simpl).
- simpl in Size; apply notin_singleton in Fr.
cbn. unfold update; rewrite~ If_r.
- simpl;reflexivity.
- cbn. apply ord_antisym;
apply meet_intro;intros x (z,Hx);subst;
apply meet_elim; exists z; simpl in Fr;
do 2 (rewrite trans_typ_fold;[|unfold open_typ;rewrite~ (@size_typ_open X)]);
unfold open_typ; rewrite~ (@open_typ_com_cc X);
[symmetry|]; apply IH.
+ rewrite size_typ_open;simpl in Size;now inversion Size.
+ now rewrite fv_typ_subst.
+ rewrite size_typ_open;simpl in Size;now inversion Size.
+ now rewrite fv_typ_subst.
- simpl. do 2 (rewrite trans_typ_arrow).
apply size_typ_arrow in Size as (Hn1,Hn2).
simpl in Fr.
apply notin_union in Fr as (Hy1,Hy2).
rewrite~ (IH T1 Hn1 U σ y k Hy1).
rewrite~ (IH T2 Hn2 U σ y k Hy2).
Qed.
Lemma trans_typ_open: ∀ T U σ k, type(U) → trans_typ σ ({k ~t> U} T) = (trans_typ σ ({k ~t> typ_cvar(trans_typ σ U)} T)).
Proof.
apply (size_typ_ind (fun T => ∀ U σ k, type(U) → trans_typ σ ({k ~t> U} T) = (trans_typ σ ({k ~t> typ_cvar(trans_typ σ U)} T)))).
intros n IH T Size U σ k.
destruct T;unfold open_typ;simpl;try intuition.
- case_nat*.
- cbn.
apply ord_antisym;apply meet_intro; intros x (y,Hx);rewrite Hx;apply meet_elim;exists y.
+ unfold open_typ. rewrite~ (@open_typ_com_cc X).
rewrite~ <- (@open_typ_com_ct _ T U).
repeat (rewrite trans_typ_fold).
* symmetry. apply~ IH.
rewrite size_typ_open;simpl in Size;now inversion Size.
* rewrite~ (@open_typ_com_ct _ T U).
now rewrite size_typ_open.
* rewrite~ (@open_typ_com_cc X).
now rewrite size_typ_open.
+ unfold open_typ.
rewrite~ (@open_typ_com_cc X).
rewrite~ <- (@open_typ_com_ct _ T U).
rewrite trans_typ_fold.
rewrite trans_typ_fold.
* apply* IH.
rewrite size_typ_open;simpl in Size;now inversion Size.
* rewrite~ (@open_typ_com_cc X).
now rewrite size_typ_open.
* rewrite~ (@open_typ_com_ct _ T U).
now rewrite size_typ_open.
- do 2 (rewrite trans_typ_arrow).
apply size_typ_arrow in Size as (Hn1,Hn2).
rewrite~ (IH T1 Hn1 U σ k).
rewrite~ (IH T2 Hn2 U σ k).
Qed.
A small tactic to automatize the proof of goals of the shape "translated_typ T a" :
Ltac find_translated_typ :=
repeat (
match goal with
| |- translated_typ (typ_fall _ ) _ =>
apply tr_typ_fall;intros;unfold open_typ;unfold open_rec_typ
| |- translated_typ (typ_arrow _ _) _ => apply tr_typ_arrow
| |- translated_typ (typ_cvar _) _ => apply tr_typ_var
| |- translated_typ (If ?a = ?a then _ else _ ) _ => rewrite~ If_l
| |- translated_typ (_ _ (If S ?a = 0 then _ else _ ) _ ) _ => rewrite~ If_r
end
).
Lemma translated_peirce : ∀ T U t u, translated_typ T t → translated_typ U u →
translated_typ (typ_peirce T U) (((t ↦ u) ↦ t) ↦ t).
Proof.
intros.
unfold typ_peirce.
find_translated_typ;intuition.
Qed.
Adequacy
Theorem adequacy:
∀ t T x Γ σ a, typing_trm Γ t T → realize σ Γ → translated (subst_trm t σ) x
→ translated_typ (subst_typ T σ) a → x ≤ a.
Proof.
intros t T x Γ σ a Typ.
generalize x σ a.
clear x σ a.
induction Typ;intros.
- inversion H3.
rewrite (@realize_inv _ _ _ _ a0 H0 H2 H4).
apply ord_refl.
- inversion H4. inversion H5.
unfold abs. apply (ord_trans _ (x0 ↦ f x0)).
apply meet_elim. exists x0;reflexivity.
apply arrow_mon_r.
pick_fresh c. assert (Fr2:=Fr).
repeat (apply notin_union_r1 in Fr).
apply (H0 c Fr _ (update σ c x0)).
+ apply (@real_push _ _ _ _ x0).
* apply by_refl. apply If_l. reflexivity.
* rewrite subst_typ_update;auto.
* apply realize_update;auto.
+ unfold open_trm;rewrite <- subst_trm_update_open;auto;
apply H7.
+ rewrite subst_typ_update;auto.
- simpl in H0. inversion H0.
specialize (IHTyp2 y σ (trans_typ σ T) H H6).
specialize (IHTyp1 x0 σ ((trans_typ σ T) ↦ a ) H H4).
apply adjunction. apply (ord_trans _ (trans_typ σ T ↦ a) _).
apply IHTyp1. simpl. apply tr_typ_arrow.
+ apply trans_typ_correct.
apply (typing_type Typ2).
+ assumption.
+ apply arrow_mon_l. apply IHTyp2.
apply trans_typ_correct.
apply (typing_type Typ2).
- inversion H4.
apply meet_intro.
intros x0 (y,Hy).
pick_fresh U.
assert (Fr2:=Fr).
repeat (apply notin_union_r1 in Fr).
specialize (H0 _ Fr x (update σ U y) x0).
apply H0. apply~ realize_update.
rewrite~ <- subst_trm_update.
specialize (H6 y). rewrite <- Hy in H6.
rewrite~ (@subst_typ_var T U y σ (update σ U y)).
compute;apply~ If_l.
intros;compute;apply~ If_r.
- pick_fresh y.
pose (τ:=(update σ y (trans_typ σ U))).
apply (ord_trans _ (trans_typ τ (typ_fall T)) _).
+ apply~ (IHTyp x τ).
* apply* realize_update.
* unfold τ.
rewrite~ <- subst_trm_update.
* apply trans_typ_correct.
apply (typing_type Typ).
+ rewrite trans_typ_fall.
unfold τ. apply meet_elim.
exists (trans_typ σ U).
apply (translated_typ_unique H3).
apply notin_union in Fr as (Fr,_).
apply notin_union in Fr as (_,Fr).
unfold open_typ; rewrite <- (@trans_typ_update T U σ y _ Fr).
rewrite~ <- trans_typ_open.
apply~ trans_typ_correct.
- intros. unfold typ_peirce in H3.
simpl in *. inversion H2;subst.
apply (translated_typ_unique (translated_peirce (trans_typ_correct σ H) (trans_typ_correct σ H0))) in H3;subst.
unfold cc. apply meet_elim_trans;auto.
later. split;[later;reflexivity|].
apply meet_elim. later. reflexivity.
Qed.
Consequence in the case of an empty typing context
If t doesn't have free variables, any substitution leaves it unchanged
Lemma empty_fv_trm_subst: ∀ t σ , fv_trm t = \{} → subst_trm t σ = t.
Proof.
intro t.
induction t;intros;auto.
- simpl in H. exfalso.
assert (bli:=@notin_empty var v).
rewrite <- H in bli.
apply notin_singleton in bli.
auto.
- simpl in H. simpl.
now rewrite (IHt _ H).
- simpl in H.
apply union_empty in H as (H1,H2).
simpl. rewrite IHt1,IHt2;auto.
Qed.
Proof.
intro t.
induction t;intros;auto.
- simpl in H. exfalso.
assert (bli:=@notin_empty var v).
rewrite <- H in bli.
apply notin_singleton in bli.
auto.
- simpl in H. simpl.
now rewrite (IHt _ H).
- simpl in H.
apply union_empty in H as (H1,H2).
simpl. rewrite IHt1,IHt2;auto.
Qed.
If t is typed in an empty context, any substitution leaves it unchanged
Lemma typing_subst_trm: ∀ t σ T, typing_trm empty t T → subst_trm t σ = t.
Proof.
intros t σ T H.
apply empty_fv_trm_subst.
eapply (typing_fv_trm H).
Qed.
Proof.
intros t σ T H.
apply empty_fv_trm_subst.
eapply (typing_fv_trm H).
Qed.
If a type T doesn't have free variables, any substitution leaves it unchanged
Lemma empty_fv_typ_subst: ∀ T σ , fv_typ T = \{} → subst_typ T σ = T.
Proof.
intro T.
induction T;intros;auto.
- simpl in H. exfalso.
assert (bli:=@notin_empty var v).
rewrite <- H in bli.
apply notin_singleton in bli.
auto.
- simpl in H. simpl.
now rewrite (IHT _ H).
- simpl in H. apply union_empty in H as (H1,H2).
simpl. rewrite IHT1,IHT2;auto.
Qed.
Proof.
intro T.
induction T;intros;auto.
- simpl in H. exfalso.
assert (bli:=@notin_empty var v).
rewrite <- H in bli.
apply notin_singleton in bli.
auto.
- simpl in H. simpl.
now rewrite (IHT _ H).
- simpl in H. apply union_empty in H as (H1,H2).
simpl. rewrite IHT1,IHT2;auto.
Qed.
Corollary 17: Adequacy in an empty context.
Theorem adequacy_empty:
∀ t T x a, typing_trm empty t T → translated t x
→ fv_typ T = \{} → translated_typ T a → x ≤ a.
Proof.
intros.
eapply (adequacy H).
apply (@real_empty (fun x => ⊥)).
- now rewrite (typing_subst_trm _ H).
- now rewrite (empty_fv_typ_subst _ H1).
Qed.
End Adequacy.