ImpAlg.Lambda
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 ImpAlg.Lattices.
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 ImpAlg.Lattices.
λc-calculus in localy nameless representation
Section Definitions.
Context `{X:Type}.
Lemma geq_1_S:∀ n, n>=1 → ∃ m, n=S m.
Proof.
intros.
destruct n.
- inversion H.
- exists n.
reflexivity.
Qed.
Lemma geq_S_S:∀ n p, n>=S p → ∃ m, n=S m /\ m >= p.
Proof.
intros.
destruct n.
- inversion H.
- exists n;split;auto.
apply Nat.succ_le_mono. auto.
Qed.
Equality of variables is decidable
Lemma var_eq_dec: ∀ (x y:var), { x = y} + { x ≠ y}.
Proof.
intros x y.
destruct (Bool.bool_dec (var_compare x y) true) as [Hx|Hx];rewrite var_compare_eq in Hx.
- rewrite LibReflect.isTrue_eq_true_eq in Hx. now left.
- apply Bool.not_true_is_false in Hx.
rewrite LibReflect.isTrue_eq_false_eq in Hx. now right.
Qed.
Terms
- n is a natural number, for De Bruijn indices,
- v is a variable, ie a name,
- a is an element of the career X of an implicative structure,
- λt,tu,cc are the usual terms of the λc-calculus (with De Bruijn indices)
Inductive trm : Type :=
| trm_bvar : nat → trm
| trm_fvar : var → trm
| trm_cvar : X → trm
| trm_abs : trm → trm
| trm_app : trm → trm → trm
| trm_cc : trm.
Substitution of the index k by q in the pre-term p, we write it { k ~> q}p
Fixpoint open_rec_trm (k : nat) (p : trm) (q : trm) {struct p} : trm :=
match p with
| trm_bvar i => If k=i then q else trm_bvar i
| trm_fvar a => trm_fvar a
| trm_cvar a => trm_cvar a
| trm_abs t => trm_abs (open_rec_trm (S k) t q)
| trm_app t u => trm_app (open_rec_trm k t q) (open_rec_trm k u q)
| trm_cc => trm_cc
end.
Definition open_trm t u := open_rec_trm 0 t u.
Definition open_trm_var t x := open_rec_trm 0 t (trm_fvar x).
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).
Hint Unfold open_trm open_rec_trm.
Lemma open_trm_def p q: p ^^q = {0 ~> q} p.
Proof. unfolds* open_trm. Qed.
Free-variables of a pre-term
Fixpoint fv_trm (t : trm) {struct t} : vars :=
match t with
| trm_bvar i => \{}
| trm_fvar a => \{a}
| trm_cvar x => \{}
| trm_abs t => (fv_trm t)
| trm_app t u => (fv_trm t) \u (fv_trm u)
| trm_cc => \{}
end.
Free De Bruijn indices of a pre-term
Definition map_pred U := LibList.map (fun x => x-1) U.
Fixpoint remove_0 l {struct l}:=
match l with
| nil => nil
| cons 0 l => remove_0 l
| cons n l => cons n (remove_0 l)
end.
Fixpoint remove (k:nat) l {struct l}:=
match l with
| nil => nil
| cons n l => If (n=k) then remove k l else cons n (remove k l)
end.
Fixpoint fn_trm_aux (t : trm) {struct t} :=
match t with
| trm_bvar i => cons i nil
| trm_fvar a => nil
| trm_cvar x => nil
| trm_abs t => map_pred (remove_0 (fn_trm_aux t))
| trm_app t u => LibList.app (fn_trm_aux t) (fn_trm_aux u)
| trm_cc => nil
end.
Definition fn_trm t:=from_list (fn_trm_aux t).
Fixpoint remove_0 l {struct l}:=
match l with
| nil => nil
| cons 0 l => remove_0 l
| cons n l => cons n (remove_0 l)
end.
Fixpoint remove (k:nat) l {struct l}:=
match l with
| nil => nil
| cons n l => If (n=k) then remove k l else cons n (remove k l)
end.
Fixpoint fn_trm_aux (t : trm) {struct t} :=
match t with
| trm_bvar i => cons i nil
| trm_fvar a => nil
| trm_cvar x => nil
| trm_abs t => map_pred (remove_0 (fn_trm_aux t))
| trm_app t u => LibList.app (fn_trm_aux t) (fn_trm_aux u)
| trm_cc => nil
end.
Definition fn_trm t:=from_list (fn_trm_aux t).
Substitution for names
Fixpoint subst_trm (z : var) (u : trm) (t : trm) {struct t} : trm :=
match t with
| trm_bvar i => trm_bvar i
| trm_fvar x => If x = z then u else (trm_fvar x)
| trm_cvar x => trm_cvar x
| trm_abs t1 => trm_abs (subst_trm z u t1)
| trm_app t1 t2 => trm_app (subst_trm z u t1) (subst_trm z u t2)
| trm_cc => trm_cc
end.
Notation "[ z ~> u ] t" := (subst_trm z u t) (at level 68).
Terms are locally-closed pre-terms
Inductive term : trm -> Prop :=
| term_var : forall a, term (trm_fvar a)
| term_cvar : forall a, term (trm_cvar a)
| term_abs : forall L t,
(forall a, a\notin L -> term (t ^v a)) ->
term (trm_abs t)
| term_app : ∀ t u, term t → term u → term (trm_app t u)
| term_cc : term trm_cc
.
Hint Resolve term_var term_cvar term_abs term_app term_cc.
| term_var : forall a, term (trm_fvar a)
| term_cvar : forall a, term (trm_cvar a)
| term_abs : forall L t,
(forall a, a\notin L -> term (t ^v a)) ->
term (trm_abs t)
| term_app : ∀ t u, term t → term u → term (trm_app t u)
| term_cc : term trm_cc
.
Hint Resolve term_var term_cvar term_abs term_app term_cc.
Closed terms are terms without free variables
Definition of the body of an abstraction
Types
- n is a natural number, for De Bruijn indices,
- v is a type variable, ie a name,
- a is an element of the career X of an implicative structure,
- ∀T and T→U are the usual second-order types of system F (with De Bruijn indices for types)
Inductive typ : Type :=
| typ_bvar : nat → typ
| typ_fvar : var → typ
| typ_cvar : X → typ
| typ_fall : typ → typ
| typ_arrow : typ → typ → typ
.
Substitution for type De Bruijn indicies
Fixpoint open_rec_typ (k : nat) (T : typ) (U : typ) {struct T} : typ :=
match T with
| typ_bvar i => If k=i then U else typ_bvar i
| typ_fvar T => typ_fvar T
| typ_cvar a => typ_cvar a
| typ_arrow V W => typ_arrow (open_rec_typ k V U) (open_rec_typ k W U)
| typ_fall T => typ_fall (open_rec_typ (S k) T U)
end.
Definition open_typ T U := open_rec_typ 0 T U.
Definition open_typ_fvar T X:= open_rec_typ 0 T (typ_fvar X).
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).
Types are defined as pre-types without free De Bruijn indices (but with variables).
Being a type is defined as a proposition (typ → Prop).
Inductive type : typ → Prop:=
| type_fvar : ∀ v, type (typ_fvar v)
| type_cvar : ∀ x, type (typ_cvar x)
| type_fall : ∀ L T, (∀ v, v \notin L → type (T ^t v)) → type (typ_fall T)
| type_arrow : ∀ T U, type T → type U → type (typ_arrow T U).
Hint Resolve type_fvar type_fall @type_cvar type_arrow type_cvar.
Inductive stype : typ → Prop:=
| stype_fvar : ∀ v, stype (typ_fvar v)
| stype_fall : ∀ L T, (∀ v, v \notin L → stype (T ^t v)) → stype (typ_fall T)
| stype_arrow : ∀ T U, stype T → stype U → stype (typ_arrow T U).
Hint Resolve type_fvar type_fall @type_cvar type_arrow type_cvar.
Fixpoint fv_typ (T:typ) {struct T} :=
match T with
| typ_fvar U => \{U}
| typ_cvar _ => \{}
| typ_bvar _ => \{}
| typ_fall U => fv_typ U
| typ_arrow T U => (fv_typ T) \u (fv_typ U)
end.
Definition closed_typ (T:typ):= fv_typ T = \{}.
Free De Bruijn indices of a pre-type
(* TODO: transformer en \{} directement *)
Fixpoint fn_typ_aux (T:typ) {struct T}:=
match T with
| typ_fvar _ => nil
| typ_cvar _ => nil
| typ_bvar n => cons n nil
| typ_fall U => map_pred (remove_0 (fn_typ_aux U ))
| typ_arrow T U => LibList.app (fn_typ_aux T) (fn_typ_aux U)
end.
Definition fn_typ T:=from_list (fn_typ_aux T).
Environment are list of the shape:
Γ ::= ε | Γ,(x:A)
where x is a variable and A a pre-type.
Peirce's law is a valid type
Definition typ_peirce T U:= typ_arrow (typ_arrow (typ_arrow T U) T ) T.
Lemma type_peirce : ∀ T U, type T → type U → type (typ_peirce T U).
Proof.
unfold typ_peirce.
auto.
Qed.
Hint Resolve type_peirce.
Inductive typing_trm : env -> trm -> typ -> Prop :=
| typing_prf_var : ∀ Γ a T,
ok Γ ->
binds a T Γ ->
type T →
typing_trm Γ (trm_fvar a) T
| typing_abs : forall L Γ U T t,
(forall a, a \notin L -> typing_trm (Γ & a ~ U) (t ^v a) T) ->
type U → type T →
typing_trm Γ (trm_abs t) (typ_arrow U T)
| typing_app : ∀ Γ U T t u,
typing_trm Γ t (typ_arrow T U) →
typing_trm Γ u T →
typing_trm Γ (trm_app t u) U
| typing_fallI : ∀ L Γ T t, (∀ U, U \notin L → typing_trm Γ t (T ^t U))
→ type (typ_fall T)
→ typing_trm Γ t (typ_fall T)
| typing_fallE : ∀ Γ T t U, typing_trm Γ t (typ_fall T)
→ type (T ^t^ U) → type U
→ typing_trm Γ t (T ^t^ U)
| typing_cc : ∀ Γ T U, type T → type U → typing_trm Γ trm_cc (typ_peirce T U).
Notation "Γ |= t : T":= (typing_trm Γ t T) (at level 69).
Instanciation of tactics
Definition codom (Γ:env):=
LibList.fold_right (fun p E => (fv_typ (snd p)) \u E) \{} Γ.
Definition empty:env := nil.
Lemma empty_eq: EnvOps.empty = empty.
Proof. unfold empty; rewrite empty_def; reflexivity. Qed.
Lemma codom_empty :
(codom empty) = \{}.
Proof. (*rew_env_defs.*) auto. Qed.
Lemma codom_single : forall x v,
codom (x ~ v) = fv_typ v.
Proof.
intros. rew_env_defs.
unfold codom.
simpl.
rewrite~ union_empty_r.
Qed.
Lemma codom_push : forall (x:var) (v:typ) (E:list (var * typ)),
codom (E & x ~ v) = fv_typ v \u codom E.
Proof.
intros.
unfold codom.
rewrite <- cons_to_push.
simpl.
auto.
Qed.
Lemma codom_concat : forall E F,
codom (E & F) = codom E \u codom F.
Proof.
intros. rew_env_defs.
gen E. induction F as [|(x,v)]; intros.
unfold codom at 3. simpl.
rewrite LibList.app_nil_l.
rewrite~ union_empty_r.
rewrite LibList.app_cons_l.
do 2 (rewrite cons_to_push).
do 2 (rewrite codom_push).
rewrite IHF.
rewrite~ union_comm_assoc.
Qed.
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)) in
let D := gather_vars_with (fun x : trm => fv_trm x) in
let E := gather_vars_with (fun x : typ => fv_typ 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.
Hint Constructors trm.
Ltac autoterm :=
repeat (
try (apply term_cc); try (apply term_var);
try (apply_fresh term_abs); try (apply term_app); try (case_nat)
).
If we can derive Γ ⊢ t:T then T is a type and t is a term
Lemma typing_type: ∀ Γ t T, typing_trm Γ t T → type(T).
Proof.
intros.
induction H;intuition.
- inversion IHtyping_trm1.
assumption.
Qed.
Lemma typing_term: ∀ Γ t T, typing_trm Γ t T → term t.
Proof.
intros.
induction H;intuition.
- autoterm.
apply H0.
now repeat (apply notin_union_r1 in Fry).
- pick_fresh v.
apply (H0 v).
now repeat (apply notin_union_r1 in Fr).
Qed.
Call/cc is typed as usual:
ε ⊢ cc: ∀A.∀B.(((A → B) → A) → A)
Lemma cc_polymorph: typing_trm empty trm_cc (typ_fall (typ_fall (typ_peirce (typ_bvar 1) (typ_bvar 0)))).
Proof.
apply_fresh typing_fallI.
- unfold open_typ.
simpl.
rewrite If_l,If_r;auto.
apply_fresh typing_fallI.
+ unfold open_typ.
simpl.
rewrite If_l;auto.
apply typing_cc;auto.
+ apply_fresh type_fall.
apply~ type_peirce.
now rewrite If_l.
- apply_fresh type_fall.
unfold open_typ;simpl;rewrite If_l,If_r;auto.
apply_fresh type_fall.
unfold open_typ;simpl;rewrite If_l;auto.
Qed.
Infrastructures
We need to prove several lemmas on substitutions for terms and types, and about the primitive we introduced to manipulate lists
About remove and map_pred
Lemma remove_0_cons_0: ∀ l, remove_0 (0::l) = remove_0 l.
Proof.
intro l.
cbn.
reflexivity.
Qed.
Lemma map_pred_cons: ∀ a l, map_pred (a :: l) = cons (a-1) (map_pred l).
Proof.
intro l.
cbn.
reflexivity.
Qed.
Lemma remove_0_incl: ∀ k l, k\notin from_list l → k\notin from_list (remove_0 l).
Proof.
intros k l; generalize k;induction l;intros.
- simpl.
rewrite from_list_nil.
apply notin_empty.
- rewrite from_list_cons in H.
apply notin_union in H as (Ha,Hl).
destruct a;subst;simpl.
+ now apply IHl.
+ rewrite from_list_cons.
apply notin_union;split;[|apply IHl];now intuition.
Qed.
Lemma remove_app: ∀ l1 l2 k, remove k (LibList.app l1 l2)=
(LibList.app (remove k l1) (remove k l2)).
Proof.
intros l1.
induction l1;intros;auto.
destruct (Nat.eq_dec a k);simpl.
- do 2 (rewrite~ If_l).
apply~ IHl1.
- do 2 (rewrite~ If_r).
rewrite LibList.app_cons_l.
rewrite <- IHl1.
reflexivity.
Qed.
Lemma map_pred_app: ∀ l1 l2, map_pred (LibList.app l1 l2)=
(LibList.app (map_pred l1) (map_pred l2)).
Proof.
intros l1.
induction l1;intros;auto.
rewrite LibList.app_cons_l.
do 2 (rewrite map_pred_cons).
rewrite LibList.app_cons_l.
now rewrite IHl1.
Qed.
Definition compat_app (f:list nat → list nat):=
∀l1 l2, f (LibList.app l1 l2)=(LibList.app (f l1) (f l2)).
Definition in_list (A:Type) (a:A) l:= (a \in from_list l).
Lemma remove_0_def: ∀ l, remove_0 l = remove 0 l.
Proof.
intros.
induction l;intros;auto.
destruct a.
- simpl;rewrite~ If_l.
- simpl;rewrite~ If_r.
now rewrite IHl.
Qed.
Lemma remove_comm: ∀ k m, k ≠ m → ∀ l, remove k (remove m l) = remove m (remove k l).
Proof.
intros k m H l.
induction l.
- now cbn.
- destruct (Nat.eq_dec a m);destruct (Nat.eq_dec a k);simpl.
+ now rewrite If_l,If_l,IHl.
+ rewrite If_l,If_r,IHl;auto. simpl. now rewrite If_l.
+ rewrite If_r,If_l;auto. simpl. now rewrite If_l,IHl.
+ rewrite If_r,If_r;auto. simpl. now rewrite If_r,If_r,IHl.
Qed.
Lemma remove_pred: ∀ k, k ≠ 0 → ∀ l, remove k (map_pred l) = map_pred (remove (S k) l).
Proof.
intros k H l.
induction l.
- now cbn.
- destruct (Nat.eq_dec a (S k));simpl.
+ rewrite If_l,If_l;auto.
subst;simpl. apply Nat.sub_0_r.
+ rewrite If_r,If_r;auto.
now rewrite map_pred_cons,<- IHl.
intro. subst;simpl. apply n.
destruct a;intuition.
Qed.
Lemma remove_pred_0: ∀ l, remove 0 (map_pred (remove_0 l)) = map_pred (remove_0 (remove 1 l)).
Proof.
intros l.
induction l.
- now cbn.
- repeat (rewrite remove_0_def in*).
destruct a as [ | a];[|destruct a].
+ simpl. rewrite If_l,If_r;auto. simpl. rewrite If_l;auto.
+ simpl. rewrite If_r,If_l;auto. simpl. rewrite If_l;auto.
+ simpl. rewrite If_r,If_r;auto. simpl. rewrite If_r,If_r;auto. now rewrite map_pred_cons,<- IHl.
Qed.
Lemma from_list_app:∀A L M, (@from_list A (LibList.app L M)) = (from_list L) \u (from_list M).
Proof.
intros A l M.
induction l.
- now rewrite LibList.app_nil_l,from_list_nil,union_empty_l.
- rewrite LibList.app_cons_l.
do 2 (rewrite from_list_cons).
now rewrite <- union_assoc,IHl.
Qed.
Lemma map_pred_S: ∀ k l, k ≠ 0 → S k \notin from_list l → k \notin from_list (map_pred l).
Proof.
intros k l; generalize k;induction l;intros.
- simpl.
rewrite from_list_nil.
apply notin_empty.
- rewrite from_list_cons in H0.
apply notin_union in H0 as (Ha,Hl).
destruct (Nat.eq_dec a (S k0));subst;simpl.
+ apply notin_singleton in Ha; now contradict Ha.
+ cbn.
apply notin_union;split.
* apply notin_singleton;intro.
apply notin_singleton in Ha; apply Ha.
subst.
destruct a.
simpl in H;now contradict H.
simpl.
now rewrite Nat.sub_0_r.
* now apply IHl.
Qed.
About fv_trm
Lemma fv_trm_subst: ∀ (t:trm) y, fv_trm ({0 ~> trm_cvar y} t) = fv_trm t.
Proof.
intro t.
generalize 0.
induction t;simpl;intros;auto.
- case_nat;simpl;auto.
- rewrite IHt1.
now rewrite IHt2.
Qed.
About fn_trm
Lemma fn_trm_app:
∀ t u, fn_trm (trm_app t u) = (fn_trm t) \u (fn_trm u).
Proof.
intros.
apply from_list_app.
Qed.
Lemma fn_trm_abs_Aux: ∀ t v k (f:list nat → list nat), f nil = nil → compat_app f
→ f (fn_trm_aux ({k ~> trm_fvar v} t )) = nil → f (remove k (fn_trm_aux t)) = nil.
Proof.
intro T.
induction T;intros;auto.
- destruct (Nat.eq_dec k n);subst.
+ cbn;rewrite~ If_l.
+ cbn in *.
rewrite~ If_r in H1.
rewrite~ If_r.
- simpl in H0.
simpl.
apply (IHT v (S k) (fun l => f (map_pred (remove_0 l)))) in H1;[ |now cbn| ].
+ destruct k.
* now rewrite remove_pred_0.
* rewrite~ remove_pred.
rewrite remove_0_def in *.
rewrite~ remove_comm.
+ intros l1 l2.
rewrite remove_0_def,remove_app,map_pred_app,H0.
now do 2 (rewrite remove_0_def).
- simpl in *.
rewrite remove_app.
rewrite H0 in *.
symmetry in H1.
apply LibList.nil_eq_app_inv in H1 as (HT1,HT2).
rewrite~ (IHT1 v k).
rewrite~ (IHT2 v k).
Qed.
Lemma fn_trm_abs_aux: ∀ (t:trm) v, fn_trm_aux (t ^v v) = nil → (remove_0 (fn_trm_aux t)) = nil.
Proof.
intros T v H.
rewrite remove_0_def.
apply~ (@fn_trm_abs_Aux T v 0 (fun l => l)).
intros l1 l2;reflexivity.
Qed.
By definition of De Bruijn indices, k isn't in fn_trm (∀.T) iff Sk isn't in fn_trm (T)
Lemma fn_trm_abs: ∀ T k, (k \notin fn_trm (trm_abs T) <->
S k \notin fn_trm T).
Proof.
intros;split;intros.
- cbn in H.
unfold fn_trm.
induction (fn_trm_aux T);try (cbn;now intuition).
cbn;apply notin_union;split.
+ destruct a;subst;auto.
* apply notin_singleton.
apply Nat.neq_succ_0.
* subst.
simpl in H.
apply notin_union in H as (H,_).
rewrite notin_singleton in *.
rewrite Nat.sub_0_r in H.
now apply not_eq_S.
+ apply IHl.
destruct a;subst;auto.
simpl in H.
now apply notin_union in H as (_,H).
- unfold fn_trm in *.
simpl.
induction (fn_trm_aux T);try (cbn;now intuition).
rewrite from_list_cons in H.
apply notin_union in H as (Ha,Hl).
destruct a;subst.
+ rewrite remove_0_cons_0.
now apply IHl.
+ cbn.
rewrite Nat.sub_0_r.
apply notin_union;split.
apply notin_singleton.
rewrite notin_singleton in Ha.
intro;subst;now apply Ha.
fold from_list.
destruct k.
now apply IHl.
apply~ map_pred_S.
now apply remove_0_incl.
Qed.
Lemma open_trm_fn: ∀ t n u, (∀ k, n <= k → k \notin fn_trm t) → {n ~> u} t = t.
Proof.
intro t. induction t;simpl;intros;try intuition.
- case_nat.
+ specialize (H n (le_refl n)). cbn in H.
apply notin_union in H as (H1,H2).
apply notin_singleton in H1 .
contradict H1.
reflexivity.
+ reflexivity.
- f_equal.
apply IHt.
intros k Hk.
destruct k;try omega.
apply fn_trm_abs,H;omega.
- rewrite~ IHt1;[rewrite~ IHt2|];
intros k Hk;specialize (H k Hk);
rewrite fn_trm_app, notin_union in H;destruct H as [H1 H2];trivial.
Qed.
If t is a term, then it doesn't have free De Bruijn indices
Lemma fn_trm_term_aux: ∀ t, term t → fn_trm_aux t = nil.
Proof.
intros t Trm.
induction Trm;intros;simpl;auto.
- cbn.
pick_fresh v.
rewrite (fn_trm_abs_aux t v)
;[|rewrite (H0 v (notin_union_r1 Fr))];
now simpl.
- rewrite IHTrm1,IHTrm2.
now cbn.
Qed.
Lemma fn_trm_term: ∀ t n, term t → (∀ k, n <= k → k \notin fn_trm t).
Proof.
intros t _ Trm k _.
apply fn_trm_term_aux in Trm.
unfold fn_trm.
rewrite Trm,from_list_nil.
apply notin_empty.
Qed.
Lemma open_term: ∀ t n u, term t → {n ~> u} t = t.
Proof.
intros.
apply open_trm_fn.
apply~ fn_trm_term.
Qed.
Lemma open_trm_com_ct: ∀ t u n m c, term (u) → n ≠ m →
({ m~> trm_cvar c} ({ n~> u} t)) = ({ n~> u} ({ m~> trm_cvar c}t)).
Proof.
intro t.
induction t;intros u k m c Hu Hk;simpl;auto.
- case_nat.
+ rewrite~ If_r. simpl. rewrite~ If_l. now apply open_term.
+ case_nat.
* simpl;rewrite~ If_l.
* simpl;repeat (rewrite~ If_r).
- rewrite~ IHt.
- rewrite~ IHt1.
rewrite~ IHt2.
Qed.
Lemma open_trm_com_v: ∀ t n m x y, n ≠ m →
({ m~> trm_fvar x} ({ n~> trm_fvar y} t)) = ({ n~> trm_fvar y} ({ m~> trm_fvar x}t)).
Proof.
intro t.
induction t;intros k m z y H;simpl;auto.
- case_nat.
+ rewrite~ If_r. simpl. rewrite~ If_l.
+ case_nat.
* simpl;rewrite~ If_l.
* simpl;repeat (rewrite~ If_r).
- rewrite~ IHt.
- rewrite~ IHt1.
rewrite~ IHt2.
Qed.
About fn_typ
Lemma fn_typ_fall_bvar:
∀ k, fn_typ (typ_fall (typ_bvar (S k))) = \{k}.
Proof.
intros.
cbn.
rewrite union_empty_r.
now rewrite Nat.sub_0_r.
Qed.
Lemma fn_typ_arrow:
∀ T U, fn_typ (typ_arrow T U) = (fn_typ T) \u (fn_typ U).
Proof.
intros.
unfold fn_typ.
simpl.
apply from_list_app.
Qed.
About fn_typ_fall
Lemma fn_typ_fall_Aux: ∀ T v k (f:list nat → list nat), f nil = nil → compat_app f → f (fn_typ_aux ({k ~t> typ_fvar v} T )) = nil → f (remove k (fn_typ_aux T)) = nil.
Proof.
intro T.
induction T;intros;auto.
- destruct (Nat.eq_dec k n);subst.
+ cbn;rewrite~ If_l.
+ cbn in *.
rewrite~ If_r in H1.
rewrite~ If_r.
- simpl in H0.
simpl.
apply (IHT v (S k) (fun l => f (map_pred (remove_0 l)))) in H1;[ |now cbn| ].
+ destruct k.
* now rewrite remove_pred_0.
* rewrite~ remove_pred.
rewrite remove_0_def in *.
rewrite~ remove_comm.
+ intros l1 l2.
rewrite remove_0_def,remove_app,map_pred_app,H0.
now do 2 (rewrite remove_0_def).
- simpl in *.
rewrite remove_app.
rewrite H0 in *.
symmetry in H1.
apply LibList.nil_eq_app_inv in H1 as (HT1,HT2).
rewrite~ (IHT1 v k).
rewrite~ (IHT2 v k).
Qed.
Lemma fn_typ_fall_aux: ∀ T v, fn_typ_aux (T ^t v) = nil → (remove_0 (fn_typ_aux T)) = nil.
Proof.
intros T v H.
rewrite remove_0_def.
apply~ (@fn_typ_fall_Aux T v 0 (fun l => l)).
intros l1 l2;reflexivity.
Qed.
By definition of De Bruijn indices, k isn't in fn_typ (∀.T) iff Sk isn't in fn_typ (T)
Lemma fn_typ_fall: ∀ T k, (k \notin fn_typ (typ_fall T) <->
S k \notin fn_typ T).
Proof.
intros;split;intros.
- cbn in H.
unfold fn_typ.
induction (fn_typ_aux T);try (cbn;now intuition).
cbn;apply notin_union;split.
+ destruct a;subst;auto.
* apply notin_singleton.
apply Nat.neq_succ_0.
* subst.
simpl in H.
apply notin_union in H as (H,_).
rewrite notin_singleton in *.
rewrite Nat.sub_0_r in H.
now apply not_eq_S.
+ apply IHl.
destruct a;subst;auto.
simpl in H.
now apply notin_union in H as (_,H).
- unfold fn_typ in *.
simpl.
induction (fn_typ_aux T);try (cbn;now intuition).
rewrite from_list_cons in H.
apply notin_union in H as (Ha,Hl).
destruct a;subst.
+ rewrite remove_0_cons_0.
now apply IHl.
+ cbn.
rewrite Nat.sub_0_r.
apply notin_union;split.
apply notin_singleton.
rewrite notin_singleton in Ha.
intro;subst;now apply Ha.
fold from_list.
destruct k.
now apply IHl.
apply~ map_pred_S.
now apply remove_0_incl.
Qed.
Lemma open_typ_fn: ∀ T n U, (∀ k, n <= k → k \notin fn_typ T) → {n ~t> U} T = T.
Proof.
intro T. induction T; unfold open_typ;simpl;intros;try intuition.
- case_nat.
+ specialize (H n (le_refl n)).
cbn in H.
simpl.
apply notin_union in H as (H,_).
apply notin_singleton in H .
contradict H.
reflexivity.
+ reflexivity.
- f_equal.
apply IHT.
intros k Hk.
apply geq_S_S in Hk as (m,(Hk,Hm)).
subst.
unfold ge in Hm.
specialize (H m Hm).
now apply fn_typ_fall.
- rewrite~ IHT1;[rewrite~ IHT2|];
intros k Hk;specialize (H k Hk);rewrite fn_typ_arrow in H;
apply notin_union in H ;destruct~ H.
Qed.
If T is a type, then it doesn't have free De Bruijn indices
Lemma fn_typ_type_aux: ∀ T, type T → fn_typ_aux T = nil.
Proof.
intros T Typ.
induction Typ;intros;simpl;auto.
- cbn.
pick_fresh v.
rewrite (fn_typ_fall_aux T v)
;[|rewrite (H0 v (notin_union_r1 Fr))];
now simpl.
- rewrite IHTyp1,IHTyp2.
now cbn.
Qed.
Lemma fn_typ_type: ∀ T n, type T → (∀ k, n <= k → k \notin fn_typ T).
Proof.
intros T _ Typ k _.
apply fn_typ_type_aux in Typ.
unfold fn_typ.
rewrite Typ,from_list_nil.
apply notin_empty.
Qed.
If T is a type, then any substitution on T leaves it unchanged
Lemma open_typ_type: ∀ T n U, type T → {n ~t> U} T = T.
Proof.
intros.
apply open_typ_fn.
apply~ fn_typ_type.
Qed.
Commutations for substitution on types
Lemma open_typ_com_cf: ∀ T n m y U, n ≠ m →
{n ~t> typ_cvar y} ({m ~t> typ_fvar U} T) = {m ~t> typ_fvar U} ({n ~t> typ_cvar y} T).
Proof.
intro T.
induction T;intros;simpl;auto.
- case_nat.
+ rewrite~ If_r.
simpl.
rewrite~ If_l.
+ case_nat.
* simpl;rewrite~ If_l.
* simpl;repeat (rewrite~ If_r).
- rewrite~ IHT.
- rewrite~ IHT1.
rewrite~ IHT2.
Qed.
Lemma open_typ_com_cc: ∀ T n m y z, n ≠ m →
{n ~t> typ_cvar y} ({m ~t> typ_cvar z} T) = {m ~t> typ_cvar z} ({n ~t> typ_cvar y} T).
Proof.
intro T.
induction T;intros;simpl;auto.
- case_nat.
+ rewrite~ If_r.
simpl.
rewrite~ If_l.
+ case_nat.
* simpl;rewrite~ If_l.
* simpl;repeat (rewrite~ If_r).
- rewrite~ IHT.
- rewrite~ IHT1.
rewrite~ IHT2.
Qed.
Lemma open_typ_com_ff: ∀ T n m y U, n ≠ m →
{n ~t> typ_fvar y} ({m ~t> typ_fvar U} T) = {m ~t> typ_fvar U} ({n ~t> typ_fvar y} T).
Proof.
intro T.
induction T;intros;simpl;auto.
- case_nat.
+ rewrite~ If_r.
simpl.
rewrite~ If_l.
+ case_nat.
* simpl;rewrite~ If_l.
* simpl;repeat (rewrite~ If_r).
- rewrite~ IHT.
- rewrite~ IHT1.
rewrite~ IHT2.
Qed.
Lemma open_typ_com_ct: ∀ T U n m y, n ≠ m → type (U) →
({m ~t> U} ({n ~t> typ_cvar y} T)) = ({n ~t> typ_cvar y} ({m ~t> U} T)).
Proof.
intro T.
induction T;intros;simpl;auto.
- case_nat.
+ rewrite~ If_r.
simpl.
rewrite~ If_l.
+ case_nat.
* simpl;rewrite~ If_l.
rewrite~ open_typ_type.
* simpl;repeat (rewrite~ If_r).
- rewrite~ IHT.
- rewrite~ IHT1.
rewrite~ IHT2.
Qed.
We define size to do induction on the size of a pre-term in the sequel
Fixpoint size t:nat :=
match t with
|trm_bvar n => 1
|trm_fvar a => 1
|trm_cvar a => 1
|trm_abs t0 => S (size t0 )
|trm_app t u => (size t) + (size u)
|trm_cc => 1
end.
Lemma size_not_0: ∀ t, size t <= 0 → False.
Proof.
intros;induction t;inversion H.
apply PeanoNat.Nat.eq_add_0 in H1.
destruct H1.
apply IHt1.
rewrite H0.
auto with arith.
Qed.
Lemma size_induction :
∀ (P:trm → Prop), (∀ n, (∀ t, size t <= n → P t) → (∀ t, size t=S n → P t ))
→ ∀ n, (∀ t, size t <= n → P t).
Proof.
intros P H n.
induction n.
- intros t Ht.
exfalso.
apply (size_not_0 t).
rewrite Ht;reflexivity.
- intros t Ht.
destruct (Compare_dec.le_lt_eq_dec _ _ Ht).
* apply IHn;auto with arith.
* apply (H n);auto.
Qed.
Lemma size_ind_gen :
∀ (P:trm → Prop), (∀ n, (∀ t, size t <= n → P t)) → ∀ t, P t.
Proof.
intros.
apply (H (size t)).
auto.
Qed.
Lemma size_ind :
∀ (P:trm → Prop), (∀ n, (∀ t, size t <= n → P t) → (∀ t, size t=S n → P t))
→ ∀ t, P t.
Proof.
intros.
apply size_ind_gen.
apply size_induction;auto.
Qed.
Lemma size_le_1: ∀ t, 1 <= size t.
Proof.
intro t.
induction t;simpl;auto with arith.
Qed.
Lemma size_open_c: ∀ t y k , size ({k ~> trm_cvar y} t) = size t.
Proof.
intros t y.
unfold open_trm.
induction t;intro m;simpl;auto.
- case_nat;simpl;reflexivity.
Qed.
Lemma size_open_v: ∀ t y k, size ({k~> trm_fvar y} t) = size t.
Proof.
intros t y.
induction t;intro k;simpl;auto.
- case_nat;simpl;reflexivity.
Qed.
Lemma size_app_le_l: ∀ t u n, size t + size u <= S n → size t <= n.
Proof.
intros t u n Size.
simpl in Size.
apply Nat.le_add_le_sub_r in Size.
apply (le_trans _ _ _ Size);apply Nat.le_sub_le_add_r;apply Nat.le_sub_le_add_l.
replace (S n - n) with 1;try (omega); apply size_le_1.
Qed.
Lemma size_app_le_r: ∀ t u n, size t + size u <= S n → size u <= n.
Proof.
intros t u n Size.
simpl in Size.
apply Nat.le_add_le_sub_l in Size.
apply (le_trans _ _ _ Size);apply Nat.le_sub_le_add_r;apply Nat.le_sub_le_add_l.
replace (S n - n) with 1;try (omega); apply size_le_1.
Qed.
Lemma size_S:∀ t,∃ m,size t = Datatypes.S m.
Proof.
intros.
apply geq_1_S.
apply size_le_1.
Qed.
Lemma size_plus_S:∀ t1 t2,∃ m,(size t1+size t2 = Datatypes.S m ∧ m >= size t1 ∧ m >= size t2).
Proof.
intros t1 t2.
destruct (size_S t1) as (m,Hm).
destruct (size_S t2) as (p,Hp).
rewrite Hm,Hp.
exists (m+Datatypes.S p);repeat split;auto;omega.
Qed.
If a preterm where a De Bruijn is replaced by a constant is term, then
it is still a term when replacing it with a free variable.
Lemma term_subst_n: ∀ n t k y c, size t <= n → term ({k ~> trm_cvar c} t) → term ({k ~> trm_fvar y} t).
Proof.
intro n;induction n;intros t k y c Size Ht;[exfalso; apply (size_not_0 t); omega|].
destruct t;cbn in *;auto.
- case_nat;trivial.
- inversion Ht. subst.
apply_fresh term_abs .
unfold open_trm.
rewrite open_trm_com_v;[|omega].
apply (IHn _ _ _ c).
+ rewrite size_open_v;omega.
+ rewrite open_trm_com_ct;[|apply term_var |omega].
apply H0.
now repeat (apply notin_union in Fry0 as [Fry0 _]).
- inversion Ht. apply term_app;apply (IHn _ k y c);auto.
+ now apply size_app_le_l in Size.
+ now apply size_app_le_r in Size.
Qed.
Lemma term_subst: ∀ t y c, term (t ^c c) → term (t ^v y).
Proof.
intros t y c Ht.
now apply (@term_subst_n (size t) t 0 y c).
Qed.
Similarly, we define size_typ to be able to do induction on the size of a pre-type
Fixpoint size_typ T:nat :=
match T with
|typ_bvar n => 1
|typ_fvar a => 1
|typ_cvar a => 1
|typ_fall T => S (size_typ T )
|typ_arrow T U => (size_typ T) + (size_typ U)
end.
Lemma size_typ_not_0: ∀ T, size_typ T <= 0 → False.
Proof.
intros;induction T;inversion H.
apply PeanoNat.Nat.eq_add_0 in H1.
destruct H1.
apply IHT1.
rewrite H0.
auto with arith.
Qed.
Lemma size_typ_induction :
∀ (P:typ → Prop), (∀ n, (∀ T, size_typ T <= n → P T) → (∀ T, size_typ T =S n → P T ))
→ ∀ n, (∀ T, size_typ T <= n → P T).
Proof.
intros P H n.
induction n.
- intros T HT.
exfalso.
apply (size_typ_not_0 T).
rewrite HT;reflexivity.
- intros T HT.
destruct (Compare_dec.le_lt_eq_dec _ _ HT).
* apply IHn;auto with arith.
* apply (H n);auto.
Qed.
Lemma size_typ_ind_gen :
∀ (P:typ → Prop), (∀ n, (∀ T, size_typ T <= n → P T)) → ∀ T, P T.
Proof.
intros.
apply (H (size_typ T)).
auto.
Qed.
Lemma size_typ_ind :
∀ (P:typ → Prop), (∀ n, (∀ T, size_typ T <= n → P T) → (∀ T, size_typ T=S n → P T))
→ ∀ T, P T.
Proof.
intros.
apply size_typ_ind_gen.
apply size_typ_induction;auto.
Qed.
Lemma size_typ_le_1: ∀ T, 1 <= size_typ T.
Proof.
intro T.
induction T;simpl;auto with arith.
Qed.
Lemma size_typ_open: ∀ T y k, size_typ ({k ~t> typ_cvar y} T) = size_typ T.
Proof.
intros T y.
induction T;intro m;simpl;auto.
- case_nat;simpl;reflexivity.
Qed.
Lemma size_typ_open_f: ∀ T y k, size_typ ({k ~t> typ_fvar y} T) = size_typ T.
Proof.
intros T y .
induction T;intro m;simpl;auto.
- case_nat;simpl;reflexivity.
Qed.
Hint Resolve size_typ_not_0 size_typ_le_1 size_typ_open size_typ_open_f.
Hint Resolve size_not_0 size_le_1 size_open_c size_open_v.
match T with
|typ_bvar n => 1
|typ_fvar a => 1
|typ_cvar a => 1
|typ_fall T => S (size_typ T )
|typ_arrow T U => (size_typ T) + (size_typ U)
end.
Lemma size_typ_not_0: ∀ T, size_typ T <= 0 → False.
Proof.
intros;induction T;inversion H.
apply PeanoNat.Nat.eq_add_0 in H1.
destruct H1.
apply IHT1.
rewrite H0.
auto with arith.
Qed.
Lemma size_typ_induction :
∀ (P:typ → Prop), (∀ n, (∀ T, size_typ T <= n → P T) → (∀ T, size_typ T =S n → P T ))
→ ∀ n, (∀ T, size_typ T <= n → P T).
Proof.
intros P H n.
induction n.
- intros T HT.
exfalso.
apply (size_typ_not_0 T).
rewrite HT;reflexivity.
- intros T HT.
destruct (Compare_dec.le_lt_eq_dec _ _ HT).
* apply IHn;auto with arith.
* apply (H n);auto.
Qed.
Lemma size_typ_ind_gen :
∀ (P:typ → Prop), (∀ n, (∀ T, size_typ T <= n → P T)) → ∀ T, P T.
Proof.
intros.
apply (H (size_typ T)).
auto.
Qed.
Lemma size_typ_ind :
∀ (P:typ → Prop), (∀ n, (∀ T, size_typ T <= n → P T) → (∀ T, size_typ T=S n → P T))
→ ∀ T, P T.
Proof.
intros.
apply size_typ_ind_gen.
apply size_typ_induction;auto.
Qed.
Lemma size_typ_le_1: ∀ T, 1 <= size_typ T.
Proof.
intro T.
induction T;simpl;auto with arith.
Qed.
Lemma size_typ_open: ∀ T y k, size_typ ({k ~t> typ_cvar y} T) = size_typ T.
Proof.
intros T y.
induction T;intro m;simpl;auto.
- case_nat;simpl;reflexivity.
Qed.
Lemma size_typ_open_f: ∀ T y k, size_typ ({k ~t> typ_fvar y} T) = size_typ T.
Proof.
intros T y .
induction T;intro m;simpl;auto.
- case_nat;simpl;reflexivity.
Qed.
Hint Resolve size_typ_not_0 size_typ_le_1 size_typ_open size_typ_open_f.
Hint Resolve size_not_0 size_le_1 size_open_c size_open_v.
If two types are equal when performing any posible substitution, then they are the same
Lemma typ_eq_subst: ∀ T U k,
(∀ v , { k ~t> typ_fvar v} T = { k ~t> typ_fvar v} U) → T = U.
Proof.
intro T.
induction T;intros;simpl in H.
- destruct U; [destruct (Nat.eq_dec n n0);auto| |
| pick_fresh v;specialize (H v);simpl in H;case_nat
| pick_fresh v;specialize (H v);simpl in H;case_nat ];
try (contradict H;intro H;pick_fresh u; pick_fresh v;assert (Hu:= H u);assert (Hv:= H v);simpl in *; apply notin_singleton in Fr0;repeat case_nat
).
case_nat.
+ pick_fresh u; specialize (H u);simpl in H;contradict H;intro H;inversion H.
apply notin_singleton in Fr.
now apply Fr.
+ simpl in H.
now apply H.
- destruct U;try (pick_fresh u; assert (Hu:=H u);simpl in Hu;now (inversion Hu;try case_nat)).
pick_fresh u;specialize (H u).
simpl in H. case_nat. inversion H.
apply notin_singleton in Fr. exfalso. now apply Fr.
- pick_fresh u; specialize (H u).
destruct U;simpl in H;inversion H;auto.
case_nat.
- destruct U;try (pick_fresh u; assert (Hu:=H u);simpl in Hu;now (inversion Hu;try case_nat)).
simpl in H. f_equal.
apply (IHT _ (S k)). intros. specialize (H v). now inversion H.
- destruct U;try (pick_fresh u; assert (Hu:=H u);simpl in Hu;now (inversion Hu;try case_nat)).
rewrite~ (IHT1 U1 k);
[rewrite~ (IHT2 U2 k)| ];
intro v; specialize (H v); now inversion H.
Qed.
The pre-type T{0:=U} is a type iff T{0:= y} is
Lemma type_subst: ∀ T U y, type (T ^t U) <-> type (T ^tc y).
Proof.
intro T.
unfold open_typ; generalize 0.
apply (size_typ_ind (fun T =>
∀ (n : nat) (U : var) (y : X),
type ({n ~t> typ_fvar U} T) ↔ type ({n ~t> typ_cvar y} T))).
intros.
split;induction T0;intros;auto.
- simpl. case_nat.
+ apply type_cvar.
+ simpl in H1.
rewrite~ If_r in H1.
- simpl in *. inversion H1.
apply (@type_fall L). intros.
specialize (H3 v H4). unfold open_typ.
rewrite~ <- open_typ_com_cf.
specialize (H (({0 ~t> typ_fvar v} T0))).
assert (le (size_typ ({0 ~t> typ_fvar v} T0)) n).
assert (Bli:=size_typ_open_f T0 v).
unfold open_typ in Bli.
rewrite Bli. inversion H0;auto.
apply (H H5 (S n0) U y).
rewrite~ <- open_typ_com_ff.
- simpl in *. inversion H1.
inversion H0.
assert (size_typ T0_1 <= n).
apply (plus_le_reg_l _ _ 1).
replace (1+n) with (S n);auto.
rewrite <- H7. rewrite plus_comm.
apply plus_le_compat_l, size_typ_le_1.
assert (size_typ T0_2 <= n).
apply (plus_le_reg_l _ _ 1).
replace (1+n) with (S n);auto.
rewrite <- H7.
apply plus_le_compat_r.
apply size_typ_le_1.
apply type_arrow.
rewrite~ <- (H _ H6 n0 U).
rewrite~ <- (H _ H8 n0 U).
- simpl. case_nat.
+ apply type_fvar.
+ simpl in H1.
rewrite~ If_r in H1.
- simpl in *. inversion H1.
apply (@type_fall L). intros.
specialize (H3 v H4).
unfold open_typ.
rewrite~ <- open_typ_com_ff.
specialize (H (({0 ~t> typ_fvar v} T0))).
assert (le (size_typ ({0 ~t> typ_fvar v} T0)) n).
assert (Bli:=size_typ_open_f T0 v).
unfold open_typ in Bli.
rewrite Bli.
inversion H0;auto.
apply (H H5 (S n0) U y).
rewrite~ open_typ_com_cf.
- simpl in *. inversion H1.
inversion H0.
assert (size_typ T0_1 <= n).
apply (plus_le_reg_l _ _ 1).
replace (1+n) with (S n);auto.
rewrite <- H7.
rewrite plus_comm.
apply plus_le_compat_l.
apply size_typ_le_1.
assert (size_typ T0_2 <= n).
apply (plus_le_reg_l _ _ 1).
replace (1+n) with (S n);auto.
rewrite <- H7.
apply plus_le_compat_r.
apply size_typ_le_1.
apply type_arrow.
rewrite~ (H _ H6 n0 U y).
rewrite~ (H _ H8 n0 U y).
Qed.
About size_typ
Lemma size_typ_S:∀ T,∃ m,size_typ T = Datatypes.S m.
Proof.
intros.
apply* geq_1_S.
Qed.
Lemma size_typ_plus_S:∀ T1 T2,
(∃ m,size_typ T1+size_typ T2 = Datatypes.S m /\ m >= size_typ T1 /\ m >= size_typ T2 ).
Proof.
intros T1 T2.
destruct (size_typ_S T1) as (m,Hm).
destruct (size_typ_S T2) as (p,Hp).
rewrite Hm,Hp.
exists (m+Datatypes.S p); repeat split;trivial;omega.
Qed.
Lemma size_typ_arrow:∀ T1 T2 m,
size_typ (typ_arrow T1 T2) = Datatypes.S m → m >= size_typ T1 /\ m >= size_typ T2.
Proof.
intros.
simpl in H.
destruct (size_typ_plus_S T1 T2).
replace m with x by intuition.
intuition.
Qed.
Lemma size_typ_arrow_le_l: ∀ T U n, size_typ T + size_typ U <= S n → size_typ T <= n.
Proof.
intros T U n Size.
simpl in Size.
apply Nat.le_add_le_sub_r in Size.
apply (le_trans _ _ _ Size);apply Nat.le_sub_le_add_r;apply Nat.le_sub_le_add_l.
replace (S n - n) with 1;try (omega); apply size_typ_le_1.
Qed.
Lemma size_typ_arrow_le_r: ∀ T U n, size_typ T + size_typ U <= S n → size_typ U <= n.
Proof.
intros T U n Size.
simpl in Size.
apply Nat.le_add_le_sub_l in Size.
apply (le_trans _ _ _ Size);apply Nat.le_sub_le_add_r;apply Nat.le_sub_le_add_l.
replace (S n - n) with 1;try (omega); apply size_typ_le_1.
Qed.
Properties on lists
Lemma from_list_nil_inv: ∀ T (l:list T), from_list l = \{} → l=nil.
Proof.
intros;destruct l;auto.
rewrite from_list_cons in H.
exfalso.
assert (bli:=@notin_empty T t).
rewrite <- H in bli.
apply notin_union in bli as (bli,_).
apply notin_singleton in bli.
now apply bli.
Qed.
Lemma union_empty : ∀ T (E F:fset T), E \u F = \{} → E = \{} ∧ F = \{}.
Proof.
intros.
destruct (fset_finite E).
destruct (fset_finite F).
subst.
rewrite <- from_list_app in H.
apply from_list_nil_inv in H.
symmetry in H.
apply LibList.nil_eq_app_inv in H as (H1,H2).
subst.
split;apply from_list_nil.
Qed.
We have the inclusion FV(t) ⊆ FV(t{n:=v}) where v is variable
Lemma fv_open_trm: ∀ (t:trm) a n, fv_trm(t) \c fv_trm ({n ~> trm_fvar a} t).
Proof.
intro t.
induction t; intros.
- cbn.
intros x Hx.
contradict (notin_empty Hx).
- simpl; apply subset_refl.
- simpl; apply subset_refl.
- cbn. apply IHt.
- cbn.
apply* subset_union_2.
- cbn;apply subset_refl.
Qed.
Lemma subset_trans: ∀ (E F G:fset var), E \c F → F \c G → E \c G.
Proof.
intros E F G HE HF x Hx.
apply (HF x (HE x Hx)).
Qed.
Key property for the proof of adequacy:
if Γ ⊢ t:T then FV(t) ⊆ dom(Γ)
In particular, if Γ is the empty list, then FV(t) = {}
Lemma typing_fv_trm_aux: ∀ Γ (t:trm) T, typing_trm Γ t T → fv_trm t \c dom Γ .
Proof.
intros Γ t T H; induction H.
- simpl.
apply binds_get,get_some_inv in H0.
unfold subset.
intros x Hx.
rewrite in_singleton in Hx;now subst.
- pick_fresh a.
simpl.
assert (La:=Fr);
repeat (apply notin_union_r1 in La).
do 2 (apply notin_union_r1 in Fr); apply notin_union_r2 in Fr.
specialize (H0 a La).
apply (subset_trans (@fv_open_trm t a 0)) in H0.
rewrite dom_push in H0.
intros x Hx.
specialize (H0 x Hx).
rewrite in_union in H0.
destruct H0;intuition.
rewrite in_singleton in H0;subst.
contradict (Fr Hx).
- simpl .
intros x Hx.
rewrite in_union in Hx; destruct Hx as [Hx|Hu];
[apply* IHtyping_trm1|apply* IHtyping_trm2].
- pick_fresh U.
repeat (apply notin_union_r1 in Fr).
apply (H0 U Fr).
- assumption.
- simpl.
intros x Hx; contradict (notin_empty Hx).
Qed.
Lemma typing_fv_trm: ∀ (t:trm) T, typing_trm empty t T → fv_trm t = \{}.
Proof.
intros.
apply typing_fv_trm_aux in H.
unfold empty in H.
rewrite <- empty_def, dom_empty in H.
apply~ fset_extens.
apply subset_empty_l.
Qed.
As a corollary, we get that any term typed in the empty context is closed
Lemma typing_empty_closed: ∀ t T, typing_trm empty t T → closed t.
Proof.
intros t T H;split.
apply (typing_term H).
apply (typing_fv_trm H).
Qed.
Proof.
intros t T H;split.
apply (typing_term H).
apply (typing_fv_trm H).
Qed.
Inductive betared : trm -> trm -> Prop :=
| betared_red : forall t1 t2,
body t1 ->
term t2 ->
betared (trm_app (trm_abs t1) t2) (t1 ^^ t2)
| betared_app1 : forall t1 t1' t2,
term t2 ->
betared t1 t1' ->
betared (trm_app t1 t2) (trm_app t1' t2)
| betared_app2 : forall t1 t2 t2',
term t1 ->
betared t2 t2' ->
betared (trm_app t1 t2) (trm_app t1 t2')
| betared_abs : forall L t1 t1',
(forall x, x \notin L -> betared (t1 ^v x) (t1' ^v x)) ->
betared (trm_abs t1) (trm_abs t1')
.
Fixpoint subst (z : var) (u : trm) (t : trm) {struct t} : trm :=
match t with
| trm_bvar i => trm_bvar i
| trm_cvar c => trm_cvar c
| trm_fvar x => If x = z then u else (trm_fvar x)
| trm_abs t1 => trm_abs (subst z u t1)
| trm_app t1 t2 => trm_app (subst z u t1) (subst z u t2)
| trm_cc => trm_cc
end.
Notation "[ z ~> u ] t" := (subst z u t) (at level 68).
Substitution for a fresh name is identity.
Lemma subst_fresh : forall x t u,
x \notin fv_trm t -> [x ~> u] t = t.
Proof.
intros. induction t; simpls; f_equal*.
case_var*.
Qed.
Substitution distributes on the open operation.
Lemma subst_open : forall x u t1 t2, term u ->
[x ~> u] (t1 ^^ t2) = ([x ~> u]t1) ^^ ([x ~> u]t2).
Proof.
intros. unfold open_trm. generalize 0.
induction t1; intros; simpl; f_equal*.
case_nat*. case_var*. rewrite* open_term.
Qed.
Substitution and open_var for distinct names commute.
Lemma subst_open_var : forall x y u t, y <> x -> term u ->
([x ~> u]t) ^v y = [x ~> u] (t ^v y).
Proof.
introv Neq Wu. rewrite* subst_open.
simpl. case_var*.
Qed.
Lemma subst_intro : forall x t u,
x \notin (fv_trm t) -> term u ->
t ^^ u = [x ~> u](t ^v x).
Proof.
introv Fr Wu. rewrite* subst_open.
rewrite* subst_fresh. simpl. case_var*.
Qed.
Lemma subst_term : forall t z u,
term u -> term t -> term ([z ~> u]t).
Proof.
induction 2; simpl;auto.
case_var*.
apply_fresh term_abs as y. rewrite* subst_open_var.
Qed.
Hint Resolve subst_term.
Lemma open_trm_term : forall t u,
body t -> term u -> term (t ^^ u).
Proof.
intros. destruct H. pick_fresh y. rewrite* (@subst_intro y).
Qed.
Lemma beta_subst_n: ∀ n x t u v, size t <= n → size u <= n → term v →
betared t u → betared ([x ~> v] t) ([x ~> v] u).
Proof.
intro n; induction n;intros x t u v St Su Tv Beta;[exfalso;apply (size_not_0 t);omega|].
inversion Beta;subst;simpl in *.
- rewrite* subst_open. apply* betared_red. destruct H as [L H].
exists (L \u \{x}). intros z Hz. rewrite* subst_open_var.
- apply* betared_app1. apply* IHn; apply size_app_le_l with t2;auto.
- apply* betared_app2. apply* IHn; apply size_app_le_r with t1;auto.
- apply betared_abs with (L \u \{x}).
intros z Fr. apply notin_union in Fr as [Fr Hz].
do 2 (rewrite subst_open_var;auto). apply* IHn; unfold open_trm;rewrite size_open_v;omega.
Qed.
Lemma beta_subst: ∀ x t u v, term v →
betared t u → betared ([x ~> v] t) ([x ~> v] u).
Proof.
intros x t u v Term Beta. apply (@beta_subst_n (size t + size u));auto with arith.
Qed.
Lemma beta_cvar: ∀ t u L c,
(∀ x : var, x \notin L → betared (t ^v x) (u ^v x)) → betared (t ^c c) (u ^c c).
Proof.
intros t u L c H.
pick_fresh x.
apply notin_union in Fr as [Fr Fru].
apply notin_union in Fr as [Fr Frt].
rewrite (@subst_intro x t);auto.
rewrite (@subst_intro x u);auto.
apply beta_subst;auto.
Qed.
End Definitions.