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 ImpAlg.Ens.
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

Because tactics do not survive to sections, we need to redefine the tactic from LibLN to pick fresh variables.
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).

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

We define a substitution as a function mapping variables to elements of the implicative structure IS.

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).

The function "translated t a" returns True iff a is the interpretation of the term t in IS:

Inductive translated : trm → X → Prop :=
|tr_var: ∀ 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 )
.

The function "translated_typ T a" returns True iff a is the interpretation of the type T in IS:
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)) .

We 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_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.

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 (geq_S_S Hm) as (x,(Hmx,Hx)).
      rewrite Hmx.
      simpl.
      apply eq_add_S in Size.
      subst.
      assert (size_typ T1 <= x).
      transitivity n;auto.
      assert (size_typ T2 <= x).
      transitivity n;auto.
      rewrite~ (IH T1).
      rewrite~ (IH T2).
      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.
  - unfold open_typ.
    unfold open_rec_typ.
    assert (Hv:= var_comp).
    destruct Hv as [Hv ].
    destruct (Hv v U) as [dec Hx].
    destruct dec.
    * rewrite LibReflect.true_eq_isTrue in Hx.
      symmetry in Hx.
      contradict Hx.
      apply (notin_singleton).
      assumption.
    * rewrite LibReflect.false_eq_isTrue in Hx.
      rewrite~ (H v Hx).
  - 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.
    assert (Hv:= var_comp).
    destruct Hv as [Hv ].
    destruct (Hv v U) as [dec Hx].
    destruct dec.
    * rewrite LibReflect.true_eq_isTrue in Hx.
      symmetry in Hx.
      contradict Hx.
      simpl in *.
      apply (notin_singleton).
      assumption.
    * rewrite LibReflect.false_eq_isTrue in Hx.
      compute.
      rewrite~ (H v Hx).
  - 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).
      assert (Bli:=@size_typ_open X).
      assert (size_typ ({0 ~t> typ_cvar y} T0) <= n).
      rewrite size_typ_open.
      simpl in Size. inversion Size. auto.
      rewrite (IHn _ H0 _ _ a σ τ);auto.
      simpl in HU. rewrite~ fv_typ_subst.
    + 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).
      assert (Bli:=@size_typ_open X).
      assert (size_typ ({0 ~t> typ_cvar y} T0) <= n).
      rewrite size_typ_open.
      simpl in Size. inversion Size. auto.
      rewrite (IHn _ H0 _ _ a σ τ);auto.
      simpl in HU.
      rewrite~ fv_typ_subst.
  - repeat (rewrite trans_typ_arrow).
    simpl in *.
    assert (size_typ T0_1 <= n).
    apply (plus_le_reg_l _ _ 1).
    replace (1+n) with (S n);auto.
    rewrite <- Size.
    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 <- Size.
    apply plus_le_compat_r.
    apply size_typ_le_1.
    rewrite~ (IHn _ H0 k U a σ τ).
    rewrite~ (IHn _ H1 k U a σ τ).
Qed.

We can finally prove the correstion of the translation of types :

Lemma trans_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));auto.
  rewrite~ <- (@trans_typ_var T U x σ0 (update σ0 U x));auto.
  compute. apply~ If_l. intros.
  compute. apply~ If_r.
  compute. apply~ If_l. intros.
  compute. apply~ If_r.
- rewrite trans_typ_arrow.
  simpl.
  apply~ tr_typ_arrow.
Qed.

The translation of a term (resp. a type) is unique, ie "translated" (resp. "translated_typ") is a functional relation in P(typ * 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;
        rewrite size_open;
        reflexivity.
      * apply (H (t^c b));auto;
        inversion H0;
        rewrite size_open;
        reflexivity.
    + inversion H1.
      inversion H2.
      assert (size t2 <= n).
        inversion H0.
        apply (le_trans _ (S n - (size t1))).
        apply Nat.le_add_le_sub_l.
        rewrite H14;reflexivity.
        apply Nat.le_sub_le_add_l.
        apply Nat.le_sub_le_add_r.
        replace (S n - n) with 1.
        apply size_le_1.
        apply plus_minus.
        replace n with (n+0) at 1.
        apply plus_n_Sm.
        auto with arith.
      assert (size t1 <= n).
        inversion H0.
        apply (le_trans _ (S n - (size t2))).
        apply Nat.le_add_le_sub_r.
        rewrite H15;reflexivity.
        apply Nat.le_sub_le_add_r.
        apply Nat.le_sub_le_add_l.
        replace (S n - n) with 1.
        apply size_le_1.
        apply plus_minus.
        replace n with (n+0) at 1.
        apply plus_n_Sm.
        auto with arith.
      * replace x with x0.
        replace y0 with y1;auto.
        apply (H t2 H13 _ _ H12 H7);auto.
        apply (H t1 H14 _ _ H10 H5);auto.
    + inversion H1.
      now inversion H2.
Qed.

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.
      assert (size_typ T2 <= n).
        inversion H0.
        apply (le_trans _ (S n - (size_typ T1))).
        apply Nat.le_add_le_sub_l.
        rewrite H14;reflexivity.
        apply Nat.le_sub_le_add_l.
        apply Nat.le_sub_le_add_r.
        replace (S n - n) with 1.
        apply size_typ_le_1.
        apply plus_minus.
        replace n with (n+0) at 1.
        apply plus_n_Sm.
        auto with arith.
      assert (size_typ T1 <= n).
        inversion H0.
        apply (le_trans _ (S n - (size_typ T2))).
        apply Nat.le_add_le_sub_r.
        rewrite H15;reflexivity.
        apply Nat.le_sub_le_add_r.
        apply Nat.le_sub_le_add_l.
        replace (S n - n) with 1.
        apply size_typ_le_1.
        apply plus_minus.
        replace n with (n+0) at 1.
        apply plus_n_Sm.
        auto with arith.
      * replace x with x0.
        replace y0 with y1;auto.
        apply (H T2 H13 _ _ H12 H7);auto.
        apply (H T1 H14 _ _ H10 H5);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 σ (Γ & (a ~ A))
.

We prove a few properties about the previous definition:

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.
    + contradict H4.
      rewrite empty_def.
      intro.
      apply (@LibList.nil_eq_last_val_app_inv _ (v,A) nil Γ).
      rewrite LibList.app_nil_l.
      rewrite LibList.app_cons_one.
      assumption.
    + rewrite <- cons_to_push in H2.
      inversion H2.
      subst v;subst A0;subst Γ0.
      clear H2.
      rewrite cons_to_push in *.
      assert (Hv:= var_comp).
      destruct Hv as [Hv ].
      destruct (Hv x a) as [dec Hx].
      destruct dec.
      * rewrite LibReflect.true_eq_isTrue in Hx.
        subst a.
        apply binds_push_eq_inv in H.
        subst A.
        rewrite H3.
        now destruct (translated_typ_unique H4 H1).
      * rewrite LibReflect.false_eq_isTrue in Hx.
        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.
  - rewrite <- empty_def.
    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).
      rewrite trans_typ_fold.
      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.


Proof of 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).
    do 8 (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_correct.
      apply (typing_type Typ2).
    + assumption.
    + apply arrow_mon_l.
      apply IHTyp2.
      apply trans_correct.
      apply (typing_type Typ2).
  - inversion H4.
    apply meet_intro.
    intros x0 (y,Hy).
    pick_fresh U.
    assert (Fr2:=Fr).
    do 5 (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.
(*    remember (update σ y (trans_typ σ U)) as τ.*)
    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_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_correct.
  - intros.
    unfold typ_peirce in H3.
    simpl in H3.
    simpl in H2.
    inversion H2;subst.
    apply (translated_typ_unique (translated_peirce (trans_correct σ H) (trans_correct σ H0))) in H3;subst.
    unfold cc.
    apply meet_elim_trans;auto.
    later.
    split.
    later.
    reflexivity.
    apply meet_elim.
    later.
    reflexivity.
Qed.

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.

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.

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.

The main result

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.