ImpAlg.ImplicativeAlgebras

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.
Require Import ImpAlg.Combinators.

Implicative Algebras


Class ImplicativeAlgebra `{IS:ImplicativeStructure}:=
  {
    separator: X → Prop;
    modus_ponens: ∀ a b, separator a → separator (arrow a b) → separator b;
    up_closed: ∀ a b, ord a b → separator a → separator b;
    sep_K : separator K;
    sep_S : separator S;
    sep_cc : separator cc
  }.

Generalizable Variables separator.

Notation "a ∈ʆ":= (separator a) (at level 80,no associativity).
Infix "@" := (app) (at level 59, left associativity).
Notation "λ- f":= (abs f) (at level 60).

Hint Resolve arrow_meet modus_ponens sep_K sep_S sep_cc.
Hint Unfold arrow_set_l arrow_set_r arrow_set.

Section IA.
  Context `{IA:ImplicativeAlgebra}.

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

A convenient notation for λ-terms.

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

  Definition neg a:=a ↦ ⊥.
  Definition closed_typ (T:typ):= fv_typ T = \{}.

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);
      try (cbn)
    ).

Bunch of tactics to automatize typing, etc..

  Ltac autofv := cbn;repeat (try rewrite union_empty_l;try rewrite union_empty_r);reflexivity.
  Ltac autoclosed:=split;[autoterm|autofv].
  Ltac translated_closed:=split;[find_translated|autoclosed].
  Ltac exists_term t:= exists t;translated_closed.
  Ltac autoclosed_typ:=unfold closed_typ;cbn;repeat (rewrite union_empty_l);auto.

  Ltac typ_from_translated:=
    unfold neg;
    repeat (
        match goal with
          | |- translated_typ _ (⊓ (_)) => apply tr_typ_fall;intros
          | |- translated_typ _ (_ ↦ _) => apply tr_typ_arrow
          | |- translated_typ _ ?a => apply tr_typ_var
        end
      ).


  Ltac autotype :=
    repeat (
        try (apply type_fvar);
        try (apply type_cvar);
        try (apply_fresh type_fall);
        try (apply type_arrow)
      ).

  Ltac simplIf:=repeat (try (rewrite If_l;[|reflexivity]);try (rewrite If_r;[|auto])).

  Ltac autoget:=
    repeat(
        match goal with
          | |- _ # _ => apply get_none_inv
          | |- get _ empty = None => apply get_empty
          | |- get _ (_ & _ ) = None => rewrite get_push;simplIf
        end
      ).
  Ltac autook:=repeat (apply ok_push);try (apply ok_empty); autoget.

  Ltac autobinds:=
    match goal with
      | |- binds ?y _ (?E & ?y ~ _) => apply* binds_push_eq
      | |- binds ?y _ (?E & ?z ~ _) => apply* binds_push_neq
    end.

  Ltac autotyping:=
    repeat (
      match goal with
        | H: _ \notin _ \u _ |- _ => rewrite_all notin_union in *
        | H: _ \notin \{_} |- _ => rewrite_all notin_singleton in *
        | H: _ \notin \{} |- _ => clear H
        | H: _ ∧ _ |- _ => destruct H
        | |- ok _ => autook
        | |- typing_trm _ (λ+ _) (typ_arrow _ _) => fresh_typing_abs;autotype;unfold open_trm;simpl;simplIf
        | |- typing_trm _ ([ _ ] _ ) _ => eapply typing_app
        | |- typing_trm _ (trm_fvar _) ?a => apply typing_prf_var;[autook|autobinds|autotype]
        | |- type _ => autotype
        end
      ).
   Ltac exX a:=exists (a X).


Properties

Separators are closed under application.

  Lemma app_closed : ∀ a b, a ∈ʆ → b ∈ʆ → a@b ∈ʆ.
  Proof.
    intros.
    apply (modus_ponens b (a@b)).
    - assumption.
    - apply (up_closed a).
      + apply adjunction.
        apply ord_refl.
      + assumption.
  Qed.

We show that any separator contains the interpretation of all closed λ-terms.

  Hint Resolve sep_S sep_K.
  Lemma sep_Id: Id ∈ʆ.
  Proof.
    apply (up_closed _ _ Id_SK).
    repeat (apply app_closed);auto.
  Qed.

  Hint Resolve sep_Id.

  Lemma sep_comb: ∀ A, combinator A → A ∈ʆ.
  Proof.
    intros.
    induction H;auto.
    apply app_closed;auto.
  Qed.

  Lemma sep_SK: ∀ C, (exists t, translated t C ∧ termSK t) → C ∈ʆ.
  Proof.
    intros.
    apply sep_comb.
    destruct H as [t [HC Ht]].
    apply (combinator_translated Ht HC).
  Qed.

  Lemma sep_term: ∀ C, (exists t, translated t C ∧ closed t) → C ∈ʆ.
  Proof.
    intros.
    apply sep_comb.
    destruct H as [t [HC Ht]].
    apply (combinator_trm_translated Ht HC).
  Qed.

  Lemma sep_typ: ∀ C, (exists t T, translated_typ T C ∧ closed_typ T ∧ typing_trm empty t T) → C ∈ʆ.
  Proof.
    intros C (t,(T,(Tr,(Cl,Typ)))).
    destruct (combinatorLambda (typing_empty_closed Typ) ) as (u,(Comb,Htu)).
    eapply up_closed.
    apply (adequacy_empty Typ Htu Cl Tr).
    now apply sep_comb.
  Qed.

  Lemma sep_W: W ∈ʆ.
  Proof.
    apply sep_term.
    exX @lambdaW.
    split.
    apply translated_W.
    autoclosed.
  Qed.

  Lemma sep_Easy: Easy ∈ʆ.
  Proof.
    apply sep_term.
    exX @lambdaEasy.
    split.
    apply translated_Easy.
    autoclosed.
  Qed.

  Hint Resolve sep_Id sep_W sep_Easy.

Entailment

We define an entailment relation.

  Definition entails a b := (a ↦ b) ∈ʆ .
  Infix "⊢":= entails (at level 75).
  Definition equivalence a b := a ⊢ b ∧ b ⊢ a.
  Infix "≈":= equivalence (at level 80).
  Notation "¬ a":=(neg a).

The ordering relation is including in the entailment relation

  Lemma subtyping : ∀ a b, a ≤ b → a ⊢ b.
  Proof.
    intros.
    apply (up_closed (a ↦ a)).
    + apply arrow_mon_r.
      assumption.
    + apply (up_closed (Id)); auto.
      apply meet_elim. exists a;reflexivity.
  Qed.

We define a tactic "realizer" to automatize to proof that a given a∈A element belongs to the separator. This tactics takes a λ-terms t as input and try to show that t ≤ a. It might go to far in trying to find the translation of t, in which case realizer_step is useful.

  Lemma realizer_later: ∀ a, (exists b, b ∈ʆ ∧ b ≤ a) → a ∈ʆ.
  Proof.
    intros a (b,(Hb,Ha)).
    apply (modus_ponens b _ Hb).
    apply* (subtyping).
  Qed.

  Ltac in_sep_term t:= apply sep_term;exists t;split;[find_translated|autoclosed].
  Ltac emeet_elim:=apply (meet_elim_trans);later;split;[later;reflexivity|].
  Ltac hnform:=repeat (emeet_elim;apply arrow_mon_r);adjunction_mon.
  Ltac realizer t:= apply realizer_later;later;split;[in_sep_term t| hnform].
  Ltac realizer_step t:= apply realizer_later;later;split;[in_sep_term t|].


The entailment relation is a preorder

  Lemma entails_refl : reflexive X entails.
  Proof.
    unfold entails,reflexive.
    intro a.
    realizer (λ+ $0).
  Qed.

  Lemma entails_trans : transitive X entails.
  Proof.
    unfold entails,transitive.
    intros a b c Ha Hb.
    apply (modus_ponens (b ↦ c));auto.
    apply (modus_ponens (a ↦ b));auto.
    realizer (λ+ λ+ λ+ ([$1] ([$2] $0))).
  Qed.

  Lemma equiv_sep: ∀ a b, a ≈ b → (a ∈ʆ ↔ b ∈ʆ).
  Proof.
    intros a b (Hab,Hba).
    split;intro H;
    [apply (modus_ponens _ _ H Hab)|
     apply (modus_ponens _ _ H Hba)].
  Qed.


  Lemma entails_half_adj:
    ∀a b c, a ⊢ b ↦ c → a ⋀ b ⊢ c .
  Proof.
  intros a b c H.
  apply modus_ponens with (a0:=a ↦ b ↦ c);auto.
  apply (up_closed W);auto. unfold W.
  apply (ord_trans _ (((a ⋀ b) ↦ (a ⋀ b) ↦ c) ↦ (a ⋀ b) ↦ c)).
  - auto_meet_elim_trans.
  - repeat apply arrow_mon;intuition.
  Qed.

  Lemma mod_ponens : ∀ a b, (a ↦ b) ⋀ a ⊢ b.
  Proof.
    intros.
    apply entails_half_adj.
    apply entails_refl.
  Qed.

  Lemma modus_ponens_later: ∀ a, (exists b, b ∈ʆ ∧ b ⊢ a ) → a ∈ʆ.
  Proof.
    intros a (b,(Hb,Ha)).
    apply* (modus_ponens b).
  Qed.

This example is only given to illustrate the utility of some tactics. Actually, this formula is realized by λxyz.y(xz) and the following is enough to prove the lemma:
realizer ((λ+ λ+ λ+ ( $ 1 ($ 2

  Lemma contraposition_l: ∀ a b, a ↦ b ⊢ (¬ b) ↦ ¬ a.
  Proof.
    intros.
    unfold entails,neg.
(*    realizer ((λ+ λ+ λ+ ( $ 1  ($ 2 *)
    apply sep_typ.
    exists ((λ+ λ+ λ+ ([ $ 1 ] ([$ 2] $ 0)))).
    later.
    repeat split.
    + typ_from_translated.
    + autoclosed_typ.
    + autotyping.
  Qed.

Ex falso quod libet:

  Lemma exfalso_S: ∀ a, ⊥ ⊢ a.
  Proof.
    intro.
    apply (subtyping _ _ (bot_min a)).
  Qed.

  Lemma true_S: ∀ a, a ⊢ ⊤.
  Proof.
    intro.
    apply (subtyping _ _ (top_max a)).
  Qed.

Double-negation elimination:

  Lemma dni: ∀ a, a ⊢ ¬ (¬ a).
  Proof.
    intro.
    unfold neg.
    realizer (λ+ λ+ ([$0] $1)).
  Qed.

  Lemma dne: ∀ a, (¬ (¬ a)) ⊢ a.
  Proof.
    intro.
    unfold entails,neg.
    apply (up_closed (((a ↦ ⊥ ) ↦ a) ↦ a)).
    - adjunction_mon.
    - apply (up_closed cc);auto.
      auto_meet_elim_trans.
  Qed.

  Lemma dn: ∀ a, a ≈ ¬ ¬ a.
  Proof.
    intros;split;[apply dni|apply dne].
  Qed.

The relation of entailment is compatible with the arrow:

  Lemma arrow_entails_mon_r: ∀ a b b', b ⊢ b' → a ↦ b ⊢ a ↦ b'.
  Proof.
    intros a b b' H.
    apply modus_ponens_later. exists (b ↦ b'). split;auto.
    realizer (λ+ λ+ λ+ ([ $2 ] ([ $1 ] $0))).
  Qed.

  Lemma arrow_entails_mon_l: ∀ a a' b, a ⊢ a' → a' ↦ b ⊢ a ↦ b.
  Proof.
    intros a a' b H.
    apply modus_ponens_later. exists (a ↦ a'). split;auto.
    realizer (λ+ λ+ λ+ ([ $1 ] ([ $2 ] $0))).
  Qed.

  Lemma arrow_entails_mon: ∀ a a' b b', a' ⊢ a → b ⊢ b' → a ↦ b ⊢ a' ↦ b'.
  Proof.
    intros a a' b b' Ha Hb.
    apply modus_ponens_later. exists (b ↦ b'). split;auto.
    apply modus_ponens_later. exists (a' ↦ a). split;auto.
    realizer (λ+ λ+ λ+ λ+ ([ $2 ] ([ $1 ] ([ $3 ] $0)))).
  Qed.

  Lemma contraposition_r: ∀ a b, (¬ a) ↦ (¬ b) ⊢ b ↦ a.
  Proof.
    intros.
    apply (@entails_trans ((¬ a) ↦ ¬ b) ((¬ ¬ b) ↦ ¬ ¬ a)).
    - apply contraposition_l.
    - apply arrow_entails_mon.
      + apply dni.
      + apply dne.
  Qed.

Internal logic

We define simple tactics to automatize the proof by beta reduction for goals of the shape λ- f ≤ a ↦ b or λ- f ≤ ⋂_ t

  Ltac lam_leq:=apply adjunction,beta_red;try (adjunction_mon).
  Ltac lam_meet:=auto_meet_intro;apply adjunction,beta_red.

Quantifiers


  Definition forallt:=meet_family.
  Definition existst `{I:Type} (a:I→X):=⋂[c](meet_family (fun (i:I)=> a i ↦ c) ↦ c).
  Definition ex_term t := λ- (fun x => x@t).

  Notation "[∀] a":=(forallt a) (at level 69).
  Notation "[∃] a":=(existst a) (at level 69).

We prove the semantic typing rules for the × type

  Lemma type_fa_intro:
    ∀ I (a:I→X) t, (∀ i, t ≤ a i) → t ≤ [∀] a.
  Proof.
  intros I a t H.
  now auto_meet_intro.
  Qed.

  Lemma type_fa_elim:
    ∀ I (a:I→X) t, t ≤ [∀] a → ∀i, t≤ a i.
  Proof.
  intros I a t H i.
  eapply ord_trans;[exact H|].
  auto_meet_elim_trans.
  Qed.

  Lemma type_ex_intro:
    ∀ I (a:I→X) t, (∃ i, t ≤ a i) → λ- (fun x => x@t) ≤ [∃] a.
  Proof.
  intros I a t [i H].
  lam_meet.
  apply adjunction.
  auto_meet_elim_trans.
  apply arrow_mon_l;exact H.
  Qed.

  Lemma type_ex_elim:
    ∀ I (a:I→X) t u c, t ≤ [∃] a → (∀i x, x≤ a i → u x≤ c) → (t@λ- (fun x => u x))≤ c.
  Proof.
  intros I a t u c H Hu.
  apply adjunction. eapply ord_trans;[exact H|].
  auto_meet_elim_trans. apply arrow_mon_l.
  apply meet_intro. intros x [i Hx]. subst.
  lam_leq. now apply (Hu i).
  Qed.



Meet: ×


  Definition prodt a b :=(⋂[c] ((a ↦ b ↦ c) ↦c)).
  Notation "a × b":=(prodt a b) (at level 69).
  Definition pair a b :=λ- (fun x => x@ a @ b).
  Definition proj1:= λ- (fun x => λ- (fun y => x)).
  Definition proj2:= λ- (fun x => λ- (fun y => y)).

We prove the semantic typing rules for the × type

  Lemma type_pair:
    ∀ a b t u, t ≤ a → u ≤ b → pair t u ≤ a × b .
  Proof.
  intros a b t u Ha Hb.
  apply meet_intro.
  intros x [c H]. subst.
  lam_leq.
  do 2 apply adjunction.
  do 2 (apply arrow_mon;intuition).
  Qed.

  Lemma type_proj1:
    ∀ a b t , t ≤ a × b → t@proj1 ≤ a.
  Proof.
  intros a b t Ha.
  apply adjunction.
  eapply ord_trans;[exact Ha|].
  auto_meet_elim_trans. apply arrow_mon_l.
  now do 2 lam_leq.
  Qed.

  Lemma type_proj2:
    ∀ a b t , t ≤ a × b → t@proj2 ≤ b.
  Proof.
  intros a b t Ha.
  apply adjunction.
  eapply ord_trans;[exact Ha|].
  auto_meet_elim_trans. apply arrow_mon_l.
  now do 2 lam_leq.
  Qed.

We prove the adjunction for × and ↦ in the induced Heyting prealgebra:

  Lemma ha_adjunction:
    ∀ a b c, a ⊢ b ↦ c <-> a × b ⊢ c.
  Proof.
    intros a b c;split;intro H.
    - apply modus_ponens_later.
      exists (a ↦ b ↦ c);split;auto.
      realizer (λ+ λ+ [$0] $1).
      apply adjunction.
      auto_meet_elim_trans.
    - apply modus_ponens_later.
      exists ((a × b) ↦ c);split;auto.
      unfold entails.
      realizer_step (λ+ λ+ λ+ [$2] (λ+ ([[$0] $2] $1))).
      do 3 lam_leq.
      lam_meet.
      apply adjunction. adjunction_mon.
  Qed.

We prove that × is indeed a meet in the induced Heyting prealgebra:

  Lemma prodt_l:
      ∀ a b, a × b ⊢ a.
  Proof.
  intros a b.
  realizer (λ+ [$0] (λ+ λ+ $1)).
  apply adjunction.
  auto_meet_elim_trans. apply arrow_mon_l.
  now do 2 lam_leq.
  Qed.

  Lemma prodt_r:
      ∀ a b, a × b ⊢ b.
  Proof.
  intros a b.
  realizer (λ+ [$0] (λ+ λ+ $0)).
  apply adjunction.
  auto_meet_elim_trans. apply arrow_mon_l.
  now do 2 lam_leq.
  Qed.

  Lemma prodt_intro:
      ∀ a b c, c ⊢ a → c ⊢ b → c ⊢ a × b.
  Proof.
  intros a b c Ha Hb.
  apply modus_ponens with (a0:=c↦b);auto.
  apply modus_ponens with (a0:=c↦a);auto.
  (* λtucz.z(tc)(uc) *)
  realizer (λ+ λ+ λ+ λ+ [[$0] ([$3] $1)] ([$2] $1)).
  lam_meet.
  do 2 apply adjunction.
  apply arrow_mon;adjunction_mon.
  Qed.



Join: +


  Definition sumt a b :=(⋂[c] ((a ↦ c) ↦ (b ↦ c) ↦c)).
  Notation "a ⊕ b":=(sumt a b) (at level 69).
  Definition inj1 t:= λ- (fun x => λ- (fun y => x@t )).
  Definition inj2 t:= λ- (fun x => λ- (fun y => y@t)).
  Definition case t u v := (t@λ- (fun x => u x)) @ λ- (fun x => v x).


We prove the semantic typing rules for the + type

  Lemma type_inj1:
    ∀ a b t , t ≤ a → inj1 t ≤ a ⊕ b.
  Proof.
  intros a b t Ha.
  lam_meet. lam_leq.
  Qed.

  Lemma type_inj2:
    ∀ a b t , t ≤ b → inj2 t ≤ a ⊕ b.
  Proof.
  intros a b t Ha.
  lam_meet. lam_leq.
  Qed.


  Lemma type_case:
    ∀ a b c t u v, t ≤ a ⊕ b → (∀x,x≤a → u x≤ c) → (∀x,x≤b → v x≤ c)
    → case t u v ≤ c.
  Proof.
  intros a b c t u v Ht Hu Hv.
  do 2 apply adjunction.
  eapply ord_trans;[exact Ht|].
  auto_meet_elim_trans.
  apply arrow_mon;[|apply arrow_mon_l];lam_leq;intuition.
  Qed.

We prove that + is indeed a join in the induced Heyting prealgebra:

  Lemma sumt_l:
      ∀ a b, a ⊢ a ⊕ b.
  Proof.
  intros a b.
  realizer (λ+ λ+ λ+ [$1] $2). (* λxyz.yx *)
  lam_meet. lam_leq.
  Qed.

  Lemma sumt_r:
      ∀ a b, b ⊢ a ⊕ b.
  Proof.
  intros a b.
  realizer (λ+ λ+ λ+ [$0] $2). (* λxyz.zx *)
  lam_meet. lam_leq.
  Qed.

  Lemma sumt_elim:
      ∀ a b c, a ⊢ c → b ⊢ c → a ⊕ b ⊢ c.
  Proof.
  intros a b c Ha Hb.
  apply modus_ponens with (a0:=b↦c);auto.
  apply modus_ponens with (a0:=a↦c);auto.
  realizer (λ+ λ+ λ+ [[$0] $2] $1). (* λxyz.zxy *)
  do 2 apply adjunction.
  auto_meet_elim_trans.
  Qed.

End IA.