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 Sets.Ensembles.
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_cvar
  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.

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

Proposition 18.2
  Lemma lambda_K:
    K = λ- (fun x=> λ- (fun y => x)).
  Proof.
    unfold abs.
    apply meet_same_set.
    split;intros x [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).

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

Proposition 18.4

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

Combinatory terms

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

  Inductive comb :=
  | combS : comb
  | combK : comb
  | combCC : comb
  | combApp: comb → comb → comb
  .

  Fixpoint trm_comb c:=
    match c with
    | combS => lambdaS
    | combK => lambdaK
    | combCC => trm_cc
    | combApp c d => trm_app (trm_comb c) (trm_comb d)
    end.

  Fixpoint imp_comb c:=
    match c with
    | combS => S
    | combK => K
    | combCC => cc
    | combApp c d => (imp_comb c)@(imp_comb d)
    end.



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

  Hint Resolve comb_S comb_K comb_Id comb_cc comb_app.

  Lemma translated_comb: ∀ c, translated (trm_comb c) (imp_comb c).
  Proof.
    intro c; induction c;simpl;auto.
    apply* tr_app.
  Qed.

  Lemma combinator_comb: ∀ c, combinator (imp_comb c).
  Proof.
    intro c; induction c;simpl;auto.
  Qed.

For the combinatory completeness, we need to consider closed terms without parameters. We thus define strict terms (sterms) are terms without constants
  Inductive sterm : @trm X -> Prop :=
  | sterm_var : forall a, sterm (trm_fvar a)
  | sterm_abs : forall L t,
      (forall a, a\notin L -> sterm (open_rec_trm 0 t (trm_fvar a))) ->
      sterm (trm_abs t)
  | sterm_app : ∀ t u, sterm t → sterm u → sterm (trm_app t u)
  | sterm_cc : sterm trm_cc
  .

  Hint Resolve term_var term_abs term_app term_cc.
  Hint Resolve sterm_var sterm_abs sterm_app sterm_cc.


  Lemma sterm_term: ∀t, sterm t → term t.
  Proof.
    intros t H; induction H; auto.
    apply term_abs with L0;trivial.
  Qed.
  Definition sclosed (t:trm):= sterm t ∧ fv_trm t = \{}.

This is our only axiom, to avoid the definition of the compilation functions from λ-terms to combinator. It simply states the well-known fact that any closed λ-term can be expressed as a combination of K and S modulo ß-reduction. Observe that we consider here λc-term, i.e. λ-terms extended with call/cc, and consequently the combinatorial basis K,S,cc. Since we didn't give reduction rules to call/cc, it plays the role of an inert constant and it is obvious that it doesn't affect the result.


  Axiom combinatory_completeness:
        ∀ t, sclosed t → ∃ c, betared (trm_comb c) t.

 Lemma combinator_trm_translated:
    ∀ t a, sclosed t → translated t a → ∃ c, (combinator c ∧ c ≤ a).
  Proof.
    intros t a Ht Tr.
    destruct (combinatory_completeness Ht) as (c,Beta).
    exists (imp_comb c);split.
    + apply combinator_comb.
    + apply (imp_betared (translated_comb _) Tr Beta).
  Qed.

End Combinators.