ImpAlg.LPar

Set Implicit Arguments.
Set Contextual Implicit.

Require Import Utf8.
Require Import RelationClasses.
Require Import Logic.
Require Import Notations.
Require Import ImpAlg.Ens.
Require Import ImpAlg.Lattices.
Require Export ImpAlg.ParAlgebras.

Section LPar_Encoding.
  Context `{PS:ParStructure}.

  Definition ok c := fst c ≤ snd c.
  Global Instance ok_Reflexive : Reflexive (fun x y=> ok (x ,y )):=ord_refl.

  Notation "c '∈(≤)'":=(ok c) (at level 60,no associativity).
  Notation "'<' t '|' u '>'":=(pair t u) (at level 60,no associativity).

  Definition cord p p':= ok p' → ok p.

  Infix "◃":=(cord) (at level 70).
  Global Instance cord_Reflexive : Reflexive cord.
  Proof. intros x H. exact H. Qed.
  Global Instance cord_Transitive : Transitive cord.
  Proof. intros x y z Hx Hy H. apply (Hx (Hy H)). Qed.

  Hint Resolve cord_Reflexive cord_Transitive.

  Global Instance cord_preOrder: PreOrder cord.
  Proof. split;auto. Qed.

  Lemma cord_mon: ∀ t u t' u', t ≤ t' → u' ≤ u → (t , u ) ◃ (t',u').
  Proof.
    intros t u t' u' Ht Hu H.
    apply (ord_trans _ _ _ Ht);simpl.
    apply (ord_trans _ _ _ H Hu).
  Qed.

  Lemma cord_subset: ∀ c c', (∀ a, c' a ◃ c a ) → subset (λ x:X , ∃a, x = a ∧ ok (c a)) (λ x, ∃a, x = a ∧ ok (c' a)).
  Proof.
    intros c c' H x (a,(Hx,Ha)).
    subst x.
    exists a;intuition.
    now apply H.
  Qed.

  Lemma cord_meet: ∀ c c', (∀ a, c' a ◃ c a ) → ⊓(λ x, ∃ a, x =a ∧ ok (c' a)) ≤ ⊓(λ x, ∃a, x = a ∧ ok (c a)).
  Proof.
  intros c c' H.
  apply meet_subset.
  now apply cord_subset.
  Qed.

  Lemma cord_join: ∀ c c', (∀ a, c' a ◃ c a ) → ⊔(λ x, ∃ a, x =a ∧ ok (c a)) ≤ ⊔(λ x, ∃a, x = a ∧ ok (c' a)).
  Proof.
  intros c c' H.
  apply join_subset.
  now apply cord_subset.
  Qed.

Encodings of positives contexts of the L⅋-calculus

  Definition box (t:X):= ¬ t.
  Definition pairing a b:= a⅋b.
  Definition mup c:= ⊔(λ x, ∃ a, x = a ∧ ok (c a )).
  Notation "'µ+.' c":= (mup c) (at level 60,no associativity).
  Notation "'{' t ',' u '}'":= (pairing t u) (at level 60,no associativity).
  Notation "'[' t ']'":= (box t) (at level 60,no associativity).

Properties of the encoding of µ+

  Lemma mup_mon: ∀ c c', (∀ a, (c' a )◃ (c a )) → µ+.c ≤ µ+.c'.
  Proof.
    intros c c' H. unfold mup.
    auto_join_leq.
    auto_join_elim_risky.
    now apply H.
  Qed.

As such, the β-reduction is reflected through the pre-order ◃ as the property of subject reduction, that is to say that the "pole" is closed under reduction. Indeed, we have the β-reduction rule:

<V|µx.c> → cV/x

and the property of safety of the reduction, that is that if <V|µx.c> ∈ ⫫, then cV/x ∈ ⫫ , or with the notations: <V|µx.c> ◃ cV/x

  Lemma mup_beta: ∀ c a, (a ,µ+.c ) ◃ (c a ) .
  Proof.
    intros c a H.
    unfold mup.
    auto_join_elim_risky.
    now apply H.
  Qed.

The following is the usual property of η-expansion: t → µx.<x|t> which is reflected as in implicative structures by: t ≤ µx.<x|t>

  Lemma mup_eta: ∀ e, e = µ+.(λ a, (a ,e )) .
  Proof.
    intros e.
    unfold mup.
    apply ord_antisym.
    - auto_join_elim_risky.
    - now auto_join_intro.
  Qed.

Encodings of negative terms of the L⅋-calculus

  Definition mun c:= ⊓(λ x, ∃ a, x = a ∧ ok (c a ) ).
  Definition mu_pair c:= ⊓(λ x, ∃ a, x =⊓(λ y, ∃ b, y = (a ⅋ b ) ∧ ok (c a b))).
  Definition mu_neg c:= ⊓(λ x, ∃ a, x = (¬ a ) ∧ ok (c a )).

  Notation "'µ-.' c":= (mun c) (at level 60,no associativity).
  Notation "'µ[].' c":= (mu_neg c) (at level 60,no associativity).
  Notation "'µ{}.' c":= (mu_pair c) (at level 60,no associativity).

Variance properties

  Lemma mun_mon: ∀ c c', (∀ a, (c' a ) ◃ (c a )) → µ-.c' ≤ µ-.c.
  Proof.
    intros c c' H. unfold mun.
    auto_meet_leq.
    auto_meet_elim_risky.
    now apply H.
  Qed.

  Lemma mu_pair_mon: ∀ c c', (∀ a b, (c' a b )◃ (c a b )) → µ{}.c' ≤ µ{}.c.
  Proof.
    intros c c' H. unfold mu_pair.
    auto_meet_leq.
    auto_meet_elim_risky.
    now apply H.
  Qed.

   Lemma mu_neg_mon: ∀ c c', (∀ a, (c' a )◃ (c a )) → µ[].c' ≤ µ[].c.
  Proof.
    intros c c' H. unfold mu_neg.
    auto_meet_leq.
    auto_meet_elim_risky.
    now apply H.
  Qed.

η-expansion

    Lemma mun_eta: ∀ t, t = mun (λ a,(t ,a )) .
  Proof.
    intros t.
    apply ord_antisym.
    - now auto_meet_leq.
    - auto_meet_elim_risky.
  Qed.

  Lemma mu_pair_eta: ∀ t, t ≤ µ{}.(λ a b, (t ,{a ,b })) .
  Proof.
    intros t.
    unfold mu_pair.
    auto_meet_leq.
    now assumption.
  Qed.

  Lemma mu_neg_eta: ∀ t, t ≤ µ[].(λ a, (t ,[a ])) .
  Proof.
    intros t.
    unfold mu_neg.
    auto_meet_leq.
    now assumption.
  Qed.

ß-reduction

  Lemma mun_beta: ∀ c t, (µ-.c ,t ) ◃ (c t ).
  Proof.
    intros c t H.
    unfold mun.
    auto_meet_elim_risky.
  Qed.

  Lemma mu_pair_beta: ∀ c a b, (µ{}.c ,{a ,b }) ◃ (c a b ).
  Proof.
    intros c a b H.
    unfold mun.
    auto_meet_elim_risky.
    now apply H.
    reflexivity.
  Qed.

  Lemma mu_neg_beta: ∀ c a, (µ[].c ,[a ]) ◃ (c a ).
  Proof.
    intros c a H.
    unfold mu_neg.
    auto_meet_elim_risky.
    now apply H.
    reflexivity.
  Qed.

Encodings of µ(α,x).c

  Definition mu_abs c:= ⊓(λ x, ∃ (a:X ), x =⊓(λ y, ∃ b, y = ((¬a ) ⅋ b ) ∧ ok (c a b))).
  Notation "'µ{[],}.' c":= (mu_abs c) (at level 62,no associativity).

  Lemma mu_abs_char: ∀ c, µ{[],}.c = µ{}.(λ x y, (µ[].(λ z, c z y ),x )).
  Proof.
    intros.
    unfold mu_abs,mu_pair.
    rewrite meet_comm.
    rewrite (meet_comm _ (fun a b => a⅋b)).
    apply meet_same_set.
    split;intros (b,Hx);exists b;subst x.
    - apply ord_antisym.
      + auto_meet_intro.
        eapply ord_trans;[|apply par_mon_l; apply H0].
        simpl.
        unfold mu_neg.
        rewrite par_meet_l.
        auto_meet_intro.
        intros y (d,((e,(He,Hf)),Hd)).
        subst d. subst y.
        auto_meet_elim_risky.
      + auto_meet_intro.
        auto_meet_elim_risky.
        * exact H0.
        * reflexivity.
    - apply ord_antisym; auto_meet_intro.
      + auto_meet_elim_risky.
        * exact H0.
        * reflexivity.
      + eapply ord_trans;[|apply par_mon_l; apply H0].
        simpl.
        unfold mu_neg.
        rewrite par_meet_l.
        auto_meet_intro.
        intros y (d,((e,(He,Hf)),Hd)).
        subst d. subst y.
        auto_meet_elim_risky.
  Qed.

Combinators

Combinators S1,S2,S3,S4 & S5 expressed as encodings of L⅋-terms are equal to their principal types

  Lemma PS1_lpar: PS1 = µ{[],}.(λ x y, (x ,{y ,y })).
  Proof.
  apply ord_antisym.
  - auto_meet_leq.
    apply parrow_mon_l.
    apply H1.
  - auto_meet_leq.
    auto_meet_elim.
    later;split;[reflexivity|].
    reflexivity.
  Qed.

  Lemma PS2_lpar_aux: ∀(x:X ), µ{}.(λ w z, (x ,w ))= (x⅋⊥).
  Proof.
  intros x.
  apply ord_antisym.
  - auto_meet_leq. auto_meet_elim_risky.
  - auto_meet_leq. apply par_mon ;intuition.
  Qed.

  Lemma PS2_lpar: PS2 = µ{[],}.(λ x y, (µ{}.(λ w z, (x ,w )),y )).
  Proof.
  apply meet_same_set.
  split; intros (a,Ha);exists a;subst x;rewrite PS2_lpar_aux.
  - apply ord_antisym.
    + auto_meet_leq. apply parrow_mon_r; apply H0.
    + auto_meet_leq. auto_meet_elim_risky. apply parrow_mon_r. now apply par_mon_r.
  - apply ord_antisym.
    + auto_meet_leq. auto_meet_elim_risky. apply parrow_mon_r. now apply par_mon_r.
    + auto_meet_leq. apply parrow_mon_r; apply H0.
  Qed.

  Lemma PS3_lpar: PS3 = µ{[],}.(λ x y, (µ{}.(λ w z, (x ,{z ,w })),y )).
  Proof.
  apply ord_antisym.
  - do 2 auto_meet_intro.
    eapply ord_trans;[|apply parrow_mon_r;apply H1].
    simpl.
    apply ps_adjunction.
    do 2 auto_meet_intro.
    apply adjunction.
    auto_meet_elim_trans.
    apply parrow_mon;[apply H4|reflexivity].
  - do 2 auto_meet_intro.
    auto_meet_elim_risky.
    reflexivity.
  Qed.

Terms on the right is exactly µ(α,x).< µ(ß,y).<µ(c,b).< ß |(c,µγ.< α | (γ,b)>) > | y > | x >

  Lemma PS4_lpar_aux:
  µ{[],}.(λ α x,(µ{[],}.(λ ß y,(µ{}.(λ c b,(ß ,{c ,µ+.(λ γ,(α ,{[γ ],b }))})),y )),x ))
  = ⋂[x] ⋂[b] ⋂[c] (x ⅋↦ (c ⅋ ⊔ (fun z => x ≤ z ⅋↦ b) ) ⅋↦ (c ⅋ b)).
  Proof.
  apply ord_antisym.
  - do 3 auto_meet_intro. subst.
      auto_meet_elim_risky;simpl.
      reflexivity.
      apply parrow_mon;[|reflexivity].
      apply par_mon_r.
      apply join_intro; intros.
      eapply ord_trans;[ reflexivity|apply join_elim;
                           later;split;[reflexivity|]].
      intuition.
   - do 2 auto_meet_intro. subst.
    eapply ord_trans;[|apply parrow_mon_r;exact H1].
    simpl. clear H1.
    apply ps_adjunction.
    do 2 auto_meet_intro. subst.
    eapply ord_trans;[|apply parrow_mon_r;exact H1].
    simpl. clear H1.
    apply ps_adjunction with (b:=a1).
    do 2 auto_meet_intro. subst.
    apply ps_adjunction.
    eapply ord_trans;[|apply parrow_mon_l;exact H1].
    simpl. clear H1.
    apply ps_adjunction.
    auto_meet_elim_risky;simpl.
    apply parrow_mon;[reflexivity|].
    apply parrow_mon;[|reflexivity].
    apply par_mon_r.
    apply join_intro; intros b [c [H H2]]. subst.
    now apply join_elim.
  Qed.

The missing part, which can not be proved without extra commutations We drive the proof forward as far a possible, in order to exhibit the blocking point

(*  Lemma PS4_lpar:
   µ{,}.(λ α x,(µ{,}.(λ ß y,(µ{}.(λ c b,(ß,{c,µ+.(λ γ,(α,{γ,b}))})),y)),x)) = PS4.
  Proof.
    rewrite PS4_lpar_aux.
    apply ord_antisym.
    - do 3 auto_meet_intro. subst.
    auto_meet_elim_risky.
    apply parrow_mon_r,parrow_mon_l.
    apply par_mon_r. now apply join_elim.
    - do 3 auto_meet_intro. subst.
      auto_meet_elim_risky.
      apply parrow_mon;|apply parrow_mon_l;apply par_mon_l;reflexivity.
      (** Here we are stuck, because we would have needed to
      make some commutation with the join to introduce sooner (as in the previous proof) *)
   Qed.
      *)

  Lemma PS5_lpar: PS5 = µ{[],}.(λ α x,(µ{}.(λ y x3 ,(µ{}.(λ x1 x2,(α ,{x1 ,{x2 ,x3 }})),y )),x )).
  Proof.
   apply ord_antisym.
  - do 2 auto_meet_intro.
    clear H0 H.
    eapply ord_trans;[|apply parrow_mon_r;apply H1];simpl.
    apply ps_adjunction.
    do 2 auto_meet_intro.
    clear H0 H.
    eapply ord_trans;[|apply par_mon_l;apply H2];simpl.
    unfold mu_pair. rewrite par_meet_l. unfold par_set_l.
    auto_meet_intro.
    intros x3 (a3,((a4,H4),H)). subst x3 a3.
    rewrite par_meet_l. unfold par_set_l.
    auto_meet_intro.
    intros x3 (a3,((a5,(H4,H5)),H)). subst x3 a3.
    apply adjunction.
    auto_meet_leq.
    apply parrow_mon;[apply H5|reflexivity].
  - do 3 auto_meet_intro.
    auto_meet_elim_risky.
    + apply ord_refl.
    + simpl. now apply par_mon_l.
  Qed.

End LPar_Encoding.