ImpAlg.Combinators

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.
Require Import ImpAlg.ImplicativeStructures.
Require Import ImpAlg.Ens.
Require Import ImpAlg.Lambda.
Require Import ImpAlg.Adequacy.

We start by defining some tactics that are useful in the sequel.
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.

Definition Succ := Datatypes.S.
Ltac find_translated :=
  repeat (
  match goal with
    | |- translated (trm_abs _ ) _ =>
      apply tr_abs;intros;unfold open_trm;simpl;unfold open_rec_trm;simpl;unfold Succ;repeat case_nat
    | |- translated (trm_app _ _) _ => apply tr_app
    | |- translated (trm_cvar _) _ => apply tr_var
  end
    ).

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 Succ ?a = 0 then _ else _ ) _ ) _ => rewrite~ If_r
  end).

Combinators

We define some usual combinators (S,K,I,etc...) and we study the relation between the interpretation (as λ-terms) in an implicative structures and their principal types.

Section Combinators.
  Context `{IS:ImplicativeStructure}.

  Definition env:=@env X.
  Definition codom:=@codom X.
  Definition fv_trm:=@fv_trm X.
  Definition fv_typ:=@fv_typ X.

We define again the tactis 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)) 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).

  Ltac pick_fresh Y :=
    let L := gather_vars in (pick_fresh_gen L Y).

  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 a simple tactic to automatize the proof that a pre-term is a term, when it is the case.

  Ltac fresh_term_abs :=
    let L0:=gather_vars in let L1 := beautify_fset L0 in
                           apply (@term_abs _ L1);intros.
  Ltac fresh_typing_abs :=
    let L0:=gather_vars in let L1 := beautify_fset L0 in
                           apply (@typing_abs _ L1);intros.
  Ltac autoterm :=
  repeat (
      try (apply term_cc);
      try (apply term_var);
      try (fresh_term_abs);
      try (apply term_app);
      try (unfold Succ);
      try (case_nat)
    ).

A convenient notation for λ-terms.

  Notation "λ+ t":= (trm_abs (t:trm)) (at level 69, right associativity).
  Notation "[ t ] u":= (trm_app (t:trm) u ) (at level 69, right associativity).
  Notation "$ n":= (@trm_bvar X n) (at level 69, right associativity).

I (λx.x)

Id is the principal type of I, namely ⊓ (a ↦ a), while lambdaId is the usual λ-term λx.x

  Definition Id:= ⊓ (fun y => ∃ a, y = a ↦ a).
  Definition lambdaId:= (λ+ $0).

We prove that I^A is equal to its principal type. Note that we use the tactic "find_translated" to automatize the proof that I^A = λ(fun x=>x).

  Lemma translated_Id : translated lambdaId Id.
  Proof.
    unfold lambdaId.
    find_translated.
  Qed.

  Lemma lambda_Id: Id = λ- (fun x => x).
  Proof.
    unfold abs.
    reflexivity.
  Qed.


K (λxy.x)

Similarly, we prove that λxy.x^A = ⊓ ⊓ (a ↦ b ↦ a)

  Definition K:= ⋂[a] (⋂[b] (a ↦ b ↦ a)).
  Definition lambdaK:= (λ+ λ+ $1).

  Lemma lambda_K:
    K = λ- (fun x=> λ- (fun y => x)).
  Proof.
    unfold abs.
    apply meet_same_set.
    split;intros Hx;
    destruct Hx as [a Ha];
    exists a;
    rewrite Ha,arrow_meet in *;
    apply meet_same_set;
    [ | apply same_set_sym];
    apply arrow_prenex with (f:=fun x => (fun y => y ↦ x)).
  Qed.

  Lemma translated_K : translated lambdaK K.
  Proof.
    rewrite lambda_K.
    unfold lambdaK.
    find_translated.
  Qed.



S (λxyz.xy(zy)

We prove S^A = ⊓ ⊓ ((a ↦ b ↦ c) ↦ (a ↦ b) ↦ a ↦ c)

  Definition S:= ⋂[a] (⋂[b] ⋂[c] ((a ↦ b ↦ c) ↦ (a ↦ b) ↦ a ↦ c)).
  Definition lambdaS:=λ+ λ+ λ+ [[$2] $0] ([$1] $0).

  Lemma lambda_S: S = λ- (fun x => λ- (fun y => λ- (fun z => (x@z)@(y@z)))).
  Proof.
    unfold S.
    apply (ord_antisym).
    - apply meet_intro;intros x [a Ha].
      unfold abs in Ha at 1.
      rewrite arrow_meet in Ha.
      rewrite Ha.
      apply meet_intro;intros y [z [[b Hb] Hy]]. subst.
      unfold abs.
      do 2 (rewrite arrow_meet).
      apply meet_intro;intros w [v [[u [[c Hc] Hv]] Hw]]. subst.
      apply (ord_trans _ (⊓ (λ z : X, ∃ d : X, z = (c ↦ (b@c) ↦ d) ↦ (c ↦ (b@c)) ↦ c ↦ d))).
      + apply (double_meet_elim (fun c => fun b => ⊓ (λ z : X, ∃ d : X, z = (c ↦ b ↦ d) ↦ (c ↦ (b)) ↦ c ↦ d))).
      + unfold app at 3.
        repeat (rewrite arrow_meet).
        apply meet_intro;intros z [y [[w [[d [Hd Hw]] Hy]] Hz]]. subst.
        apply meet_elim_trans. later;split;[exists d;reflexivity|].
        apply arrow_mon;adjunction_mon.
        apply adjunction.
        apply Hd.
    - repeat_meet_intro.
      unfold abs.
      apply (ord_trans _ ((a ↦ b ↦ c) ↦ ⊓(λ x1 : X,∃ a1 : X,
                                                          x1 = a1 ↦ ⊓ (λ x2 : X, ∃ a2 : X, x2 = a2 ↦ (a ↦ b ↦ c) @ a2 @ (a1 @ a2))))).
      + apply meet_elim.
        exists (a ↦ b ↦ c).
        reflexivity.
      + apply arrow_mon_r.
        apply (ord_trans _ ((a ↦ b) ↦ ⊓ (λ x2 : X, ∃ a2 : X, x2 = a2 ↦ (a ↦ b ↦ c) @ a2 @ ((a ↦ b) @ a2)))).
        * apply meet_elim.
          exists (a ↦ b).
          reflexivity.
        * apply arrow_mon_r.
          apply (ord_trans _ (a ↦ (a ↦ b ↦ c) @ a @ ((a ↦ b) @ a))).
          apply meet_elim;exists a;reflexivity.
          repeat (try (apply arrow_mon_r);try (apply arrow_mon_l);apply adjunction).
          apply ord_refl.
  Qed.

  Lemma translated_S: translated lambdaS S.
  Proof.
    rewrite lambda_S.
    unfold lambdaS.
    find_translated.
  Qed.

S K K ≤ I

We prove that I^A = S K K^A

  Lemma Id_SK : (S @ K) @ K ≤ Id.
  Proof.
    rewrite lambda_S.
    apply (ord_trans _ ((λ- (λ y : X, λ- (λ z : X, K @ z @ (y @ z)))) @ K )).
    - apply app_mon_l.
      apply (betarule (fun x => (λ- (λ y : X, λ- (λ z : X, x @ z @ (y @ z))))) K).
    - apply (ord_trans _ (λ- (λ z : X, K @ z @ (K @ z)))).
      apply (betarule (fun y => λ- (λ z : X, K @ z @ (y @ z))) K).
      rewrite lambda_Id.
      repeat_meet_intro.
      apply adjunction.
      apply (ord_trans _ (K @ a @ (K @ a))).
      apply (betarule (fun z => K @ z @ (K @ z)) a).
      unfold K at 1.
      do 2 (apply adjunction).
      apply (double_meet_elim (fun x => fun y => x ↦ y ↦ x)).
  Qed.

W (λxy.xyy)


  Definition lambdaW:= λ+ λ+ [[$1] $0] $0.
  Definition W := ⋂[ a] (⋂[ b] ( (a ↦ a ↦ b) ↦ a ↦ b)).
  Lemma lambda_W:
    W = λ- (fun x => λ- (fun y => (x @ y) @ y)).
  Proof.
    unfold abs,W.
    apply ord_antisym.
    - repeat_meet_intro.
      rewrite arrow_meet.
      apply meet_intro.
      intros y [z [[c Hz] Hy]].
      rewrite Hy,Hz.
      clear y z Hy Hz x Hx.
      unfold app.
      do 2 (rewrite arrow_meet).
      apply meet_intro; intros w [y [[z [Hz Hy]] Hw]].
      rewrite Hw,Hy.
      rewrite (double_meet).
      apply (ord_trans _ ((c ↦ c ↦ z) ↦ c ↦ z)).
      + apply (double_meet_elim (fun x => fun y => (x ↦ x ↦ y) ↦ x ↦ y)).
      + apply arrow_mon_l.
        apply adjunction.
        apply Hz.
    - repeat_meet_intro.
      apply (ord_trans _ ((a ↦ a ↦ b) ↦ ⊓ (λ x0 : X, ∃ a0 : X, x0 = a0 ↦ (a ↦ a ↦ b)@ a0 @ a0))).
      + apply meet_elim.
        exists (a ↦ a ↦ b).
        reflexivity.
      + apply arrow_mon_r.
        apply (ord_trans _ (a ↦ (a ↦ a ↦ b) @ a @ a)).
        * apply meet_elim.
          exists a;reflexivity.
        * adjunction_mon.
          apply adjunction.
          adjunction_mon.
  Qed.


  Lemma translated_W: translated lambdaW W.
  Proof.
    unfold lambdaW.
    rewrite lambda_W.
    find_translated.
  Qed.


  (* C ≡ λxyz . xzy*)

λxy.xy

We prove one more equality, namely that:
λxy.xy = ⊓ ⊓ ((a ↦ b) ↦ a ↦ b)).
We call the combinator Easy because we didn't have any better idea, but note that in fact, Easy := S@(S@(K@S)@(S@(K@K)@I))@(K@I)

  Definition Easy:= ⊓ (λ x:X, ∃ a, x= ⊓ (λ y:X, ∃ b, y = ( (a ↦ b) ↦ a ↦ b))).
  Lemma lambda_Easy:
    Easy = λ- (fun x => λ- (fun y => x @ y)).
  Proof.
    unfold abs,Easy.
    apply ord_antisym.
    - apply meet_intro;intros x (a,Ha). subst.
       rewrite arrow_meet.
       apply meet_intro;intros b [x [[c Hx] H]]. subst.
       unfold app.
       do 2 (rewrite arrow_meet).
       apply meet_intro; intros w [y [[z [Hz Hy]] Hw]]. subst.
       rewrite (double_meet ).
       apply (ord_trans _ ((c ↦ z) ↦ c ↦ z)).
       + apply (double_meet_elim (fun x => fun y => (x ↦ y) ↦ x ↦ y)).
       + apply arrow_mon_l.
       apply Hz.

    - apply meet_intro;intros.
      destruct H as [a Ha]. subst.
      apply meet_intro;intros b [c Hb]. subst.
      apply (ord_trans _ ((a ↦ c) ↦ ⊓ (λ x0 : X, ∃ a0 : X, x0 = a0 ↦ (a ↦ c) @ a0))).
      + apply meet_elim.
        exists (a ↦ c).
        reflexivity.
      + apply arrow_mon_r.
        apply (ord_trans _ (a ↦ (a ↦ c) @ a)).
        * apply meet_elim.
          exists a;reflexivity.
        * apply arrow_mon_r.
          apply meet_elim.
          apply ord_refl.
  Qed.

  Definition lambdaEasy:= λ+ λ+ [$1] $0.
  Lemma translated_Easy: translated lambdaEasy Easy.
  Proof.
    unfold lambdaEasy.
    rewrite lambda_Easy.
    find_translated.
  Qed.

B (λxyz . x(yz))


  Definition lambdaB:= λ+ λ+ λ+ [$2] ([$1] $0).
  Definition B := ⋂[ a] (⋂[ b] (⋂[ c] ((a ↦ b) ↦ (c ↦ a) ↦ c ↦ b))).

  Lemma lambda_B:
    B = λ- (fun x => λ- (fun y => λ- (fun z => x@ (y @ z)))).
  Proof.
    unfold abs,B.
    apply ord_antisym.
    - repeat_meet_intro.
      rewrite arrow_meet.
      apply meet_intro. intros y [z [[d Hz] Hy]]. subst.
      do 2 (rewrite arrow_meet).
      apply meet_intro; intros x [b [[z [[c Hz] Hy]] Hw]]. subst.
      unfold app. do 3 (rewrite arrow_meet).
      apply meet_intro. intros z [x [[x' [[b [Hz Hy]] H']] H]]. subst.
      eapply ord_trans;[|apply arrow_mon_l;exact Hz].
      apply meet_elim_trans.
      later;split;[exists (⊓ (λ x : X, d ≤ c ↦ x));reflexivity|].
      clear Hz a.
      eapply meet_elim_trans. later;split;[exists b;reflexivity|].
      eapply meet_elim_trans. later;split;[exists c;reflexivity|].
      adjunction_mon.
      apply adjunction.
      reflexivity.
    - repeat_meet_intro.
      auto_meet_elim_trans. apply arrow_mon_r.
      auto_meet_elim_trans. apply arrow_mon_r.
      auto_meet_elim_trans. apply arrow_mon_r.
      adjunction_mon.
  Qed.

  Hint Resolve lambda_S lambda_K lambda_Id translated_Id translated_S translated_K.

Combinatorial terms

We define combinatorial terms as terms that are obtained by combination of S,K and I.

  Inductive combinator : X → Prop :=
  | comb_S : combinator S
  | comb_K : combinator K
  | comb_Id : combinator Id
  | comb_app: ∀ A B, combinator A → combinator B → combinator (A@B).

We define "termSK" (or SK-terms) as the property for pre_terms to be obtainable by combination of (K=λxy.x) and (S=λxyz.xz(yz).

  Inductive termSK : trm → Prop :=
  |term_S : termSK lambdaS
  |term_K : termSK lambdaK
  |termSK_app: ∀ t u, termSK t → termSK u → termSK (trm_app t u).

  Hint Resolve comb_S comb_K comb_Id comb_app term_S term_K termSK_app.

Any SK-term is a combinator:

  Lemma combinator_translated: ∀ t C, termSK t → translated t C → combinator C.
  Proof.
    intros t C SK.
    generalize C.
    clear C.
    induction SK;intros C Tr.
    - replace C with S.
      auto.
      apply (@translated_unique X _ _ _ _ lambdaS _ C);auto.
    - replace C with K.
      auto.
      apply (@translated_unique _ _ _ _ _ lambdaK _ C);auto.
    - inversion Tr;auto.
  Qed.

  Lemma combinatorSK: ∀ t, termSK t → ∃ u, combinator u ∧ translated t u.
  Proof.
    intros t SK.
    induction SK.
    - exists S;auto.
    - exists K;auto.
    - destruct IHSK1 as [Ct [HCt HTt]].
      destruct IHSK2 as [Cu [HCu HTu]].
      exists (Ct@Cu).
      split;auto.
      apply tr_app;auto.
  Qed.

  Definition neg a:=a ↦ ⊥.
  Definition closed_typ (T:typ):= fv_typ T = \{}.
  Definition closed (t:trm):= term t ∧ fv_trm t = \{}.

  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.

This is our only axiom, to avoid the definition of the compilation functions from λ-terms to combinator. To be exact, the axiom should be:
closed t → ∃ c, termSK c ∧ (c -ß→ t).
We abuse the fact that we know that through the translation, c ≤ t

  Axiom lambdaSK : ∀ t, closed t → termSK t.

(*   Axiom combinatory_completeness:
        ∀ t a, closed t → translated t a → ∃ u b, termSK u ∧ translated u b ∧ b ≤ a.
 *)
  Lemma combinatorLambda: ∀ t, closed t → ∃ u, combinator u ∧ translated t u.
  Proof.
    intros.
    apply combinatorSK.
    apply lambdaSK.
    assumption.
  Qed.

  Lemma combinator_trm_translated: ∀ t C, closed t → translated t C → combinator C.
  Proof.
    intros t C SK Tr.
    apply (@combinator_translated t);auto.
    apply lambdaSK;auto.
  Qed.

End Combinators.