ImpAlg.LTensor

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

Section LTensor.
  Context `{TS:TensorStructure}.

  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):lt_scope.
Global Open Scope lt_scope.

  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

  Notation "¬ a":=(tneg a).
  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_meet_leq.
    auto_meet_elim_risky.
    now apply H.
  Qed.

The β-reduction is again 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:

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

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

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

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

  Lemma mup_eta: ∀ t, t = µ+.(λ a, (t ,a )) .
  Proof.
    intros t.
    unfold mup.
    apply ord_antisym.
    -now auto_meet_intro.
    -auto_meet_elim_risky.
  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_join_leq.
    auto_join_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_join_leq.
    auto_join_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_join_leq.
    auto_join_elim_risky.
    now apply H.
  Qed.

η-expansion

  Lemma mun_eta: ∀ e, e = mun (λ a,(a ,e )) .
  Proof.
    intros e.
    unfold mun.
    apply ord_antisym.
    -auto_join_elim_risky.
    -now auto_join_intro.
  Qed.

  Lemma mu_pair_eta: ∀ e, µ{}.(λ a b, ({a ,b },e )) ≤ e.
  Proof.
    intros e.
    now repeat auto_join_intro.
  Qed.

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

ß-reduction

Again, the β-reduction is reflected through the pre-order ◃ as the property of subject reduction.

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

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

  Lemma mu_neg_beta: ∀ c a, ([a ],µ[].c ) ◃ (c a ).
  Proof.
    intros c a H.
    unfold mu_neg.
    auto_join_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, (x,µ.(λ z, c z y))).
  Proof.
    intros.
    unfold mu_abs,mu_pair.
    rewrite join_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 LTensor.