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.

λc-calculus in localy nameless representation

This is an adaptation of the localy nameless representation for Krivine's λc-calculus. For further details on the localy nameless representation, see the original paper:
A. Charguéraud - The Locally Nameless Representation
http://doi.org/10.1007/s10817-011-9225-2

Section Definitions.
  Context `{X:Set}.

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.

Terms

Pre-terms (trm) are defined by the BNF:
t,u ::= bvar n | fvar v | cvar a | λt | tu | cc
where:
  • 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 : Set :=
| 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.

Terms are locally-closed pre-terms

Inductive term : trm -> Prop :=
| term_var : forall a, term (trm_fvar 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
.

Types

Similarly, pre-terms are defined by the BNF:
t,u ::= bvar n | fvar v | cvar a | ∀T | T → U
where:
  • 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 : Set :=
  | 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.

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.

We define some useful functions for list manipulations

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.

Free De Bruijn indicies of a pre-type

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.append (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.

Definition env := LibEnv.env typ.

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.

Type system


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

Tactic gather_vars returns a set of variables occurring in the context of proofs, including domain of environments and free variables in terms mentionned in the context.

Definition codom (Γ:env):=
  LibList.fold_right (fun p E => (fv_typ (snd p)) \u E) \{} Γ.

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.
  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.
  - autoterm.
    apply H0.
    now repeat (apply notin_union_r1 in Fry).
  - now autoterm.
  - pick_fresh v.
    apply (H0 v).
    now repeat (apply notin_union_r1 in Fr).
  - autoterm.
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 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 from_list_append:∀A L M, (@from_list A (LibList.append 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.
    do 2 (rewrite from_list_cons).
    now rewrite <- union_assoc,IHl.
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_append.
Qed.

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_append: ∀ l1 l2 k, remove k (LibList.append l1 l2)=
                                (LibList.append (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.
    rewrite <- IHl1.
    reflexivity.
Qed.

Lemma map_pred_append: ∀ l1 l2, map_pred (LibList.append l1 l2)=
                                (LibList.append (map_pred l1) (map_pred l2)).
Proof.
  intros l1.
  induction l1;intros;auto.
  rewrite LibList.app_cons.
  do 2 (rewrite map_pred_cons).
  rewrite LibList.app_cons.
  now rewrite IHl1.
Qed.

Definition compat_append (f:list nat → list nat):=
  ∀l1 l2, f (LibList.append l1 l2)=(LibList.append (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.

About fn_typ_fall

Lemma fn_typ_fall_Aux: ∀ T v k (f:list nat → list nat), f nil = nil → compat_append 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_append,map_pred_append,H0.
      now do 2 (rewrite remove_0_def).
  - simpl in *.
    rewrite remove_append.
    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.

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.

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.

Hint Resolve term_var term_abs term_app.

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: ∀ t y, size (t ^c y) = size t.
Proof.
  intros t y.
  unfold open_trm.
  generalize 0.
  induction t;intro m;simpl;auto.
  - case_nat;simpl;reflexivity.
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.

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;auto.
  rewrite <- plus_Snm_nSm.
  unfold ge.
  apply le_plus_l.
  unfold ge.
  apply le_plus_r.
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.

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_append 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.
  rewrite dom_empty in H.
  apply~ fset_extens.
  apply subset_empty_l.
Qed.

End Definitions.