ImpAlg.TensorAlgebras

Set Implicit Arguments.
Set Contextual Implicit.

Require Import Utf8.
Require Import Setoid.
Require Import ImpAlg.Ens.
Require Import ImpAlg.Lattices.
Require Export ImpAlg.ImplicativeStructures.
Require Export ImpAlg.ParAlgebras.

Tensor Structures

Definition tensor_set_l `{X:Set} `{tensor:X → X → X} (A:Ens) (b:X):Ens :=
    fun x => ∃a, A a ∧ x = tensor a b.
Definition tensor_set_r `{X:Set} `{tensor:X → X → X} (a:X) (B:Ens):Ens :=
    fun x => ∃b, B b ∧ x = tensor a b.
Definition tensor_set `{X:Set} `{tensor:X → X → X} (A:Ens) (B:Ens):Ens :=
    fun x => ∃a,∃b, A a ∧ B b ∧ x = tensor a b.
Notation "a ◃ b":= (rev a b) (at level 70).

Class TensorStructure `{CL:CompleteLattice} :=
  {
    tensor:X → X → X;
    tneg: X → X;
    
    tensor_mon: ∀ a a' b b', a ≤ a' -> b ≤ b' -> (tensor a b ) ≤ (tensor a' b');

    tneg_mon: ∀ a a', ord a a' -> ord (tneg a') (tneg a);
   
    tensor_join_l: ∀ A b, tensor (join_set A) b = join_set (@tensor_set_l X tensor A b);
    tensor_join_r: ∀ a B, tensor a (join_set B) = join_set (@tensor_set_r X tensor a B);
    
    tneg_join: ∀ A, tneg (join_set A) = meet_set (image_set tneg A)
  }.

Generalizable Variables X ord join meet tneg par L meet_set join_set.
Infix " ⨂ ":= tensor (at level 76, right associativity):ta_scope.
Notation "a ⨂↦ b":= (tneg( tensor a (tneg b))) (at level 60, right associativity):ta_scope.
Global Open Scope ta_scope.
Definition tarrow `{TS:TensorStructure} a b:= (a ⨂↦ b).

Properties of conjunctive structures

Section About_TensorStruct.
Context `{TS:TensorStructure}.

Properties of the ⨂ operator


  Lemma tensor_mon_l: ∀ a a' b, a ≤ a' -> (a ⨂ b) ≤ (a' ⨂ b).
  Proof.
  intros a a' b H.
  apply tensor_mon;intuition.
  Qed.

  Lemma tensor_mon_r: ∀ a b b', b ≤ b' -> (a ⨂ b) ≤ (a ⨂ b').
  Proof.
  intros a b b' H.
  apply tensor_mon;intuition.
  Qed.

  Lemma tensor_bot_l: ∀ a:X, (⊥ ⨂ a) = ⊥.
  Proof.
    intros a.
    rewrite <- join_emptyset.
    rewrite tensor_join_l.
    apply join_same_set.
    intros x;split;[intros (y,(H,_))| intros H];contradict H.
  Qed.

  Lemma tensor_bot_r: ∀ a:X, (a ⨂ ⊥) = ⊥.
  Proof.
    intros a.
    rewrite <- join_emptyset.
    rewrite tensor_join_r.
    apply join_same_set.
    intros x;split;[intros (y,(H,_))| intros H];contradict H.
  Qed.

Properties of the ¬ operator


  Lemma tneg_bot: (tneg ⊥) = ⊤.
  Proof.
    rewrite <- join_emptyset.
    rewrite tneg_join.
    rewrite <- meet_emptyset.
    apply meet_same_set.
    intros x;split;[intros (y,(H,_))| intros H];contradict H.
  Qed.

End About_TensorStruct.

Hint Resolve tensor_mon tneg_mon tensor_join_l tensor_join_r tneg_join.

From ⅋-structures to ⨂-structures

We show that starting from a disjunctive structure, the structure based on the reversed underlying complete lattice with the same negation and a⨂b := a⅋b defines a conjunctive structure.

Section ReversePS.
  Context `{PS:ParStructure}.


  Definition tens a b:=par a b.

  Ltac autorev:=intros;unfold tens,rev,reverse;auto.


 Lemma rev_tensor_mon: ∀ a a' b b', a ◃ a' -> b ◃ b' -> tens a b ◃ tens a' b'.
  Proof.
    autorev.
  Qed.

  Lemma rev_tneg_mon: ∀ a a', a ◃ a' -> (¬ a') ◃ (¬ a).
  Proof.
    autorev.
  Qed.

  Lemma rev_tensor_join_l: ∀ A b, tens (meet_set A) b = meet_set (@tensor_set_l X tens A b).
  Proof.
    unfold tensor_set_l.
    apply par_meet_l.
  Qed.

  Lemma rev_tensor_join_r: ∀ a B, tens a (meet_set B) = meet_set (@tensor_set_r X tens a B).
  Proof.
    unfold tensor_set_l.
    apply par_meet_r.
  Qed.

  Lemma rev_tneg_join: ∀ A, pneg (meet_set A) = join_set (image_set pneg A).
  Proof.
    apply pneg_meet.
  Qed.
End ReversePS.

Global Instance PS_TS `{PS:ParStructure}:@TensorStructure _ _ _ RevCompleteLattice:=
  {tensor:=par; tneg:= pneg; tensor_mon:=rev_tensor_mon;
   tneg_mon:=rev_tneg_mon;tensor_join_l:=rev_tensor_join_l;
   tensor_join_r:=rev_tensor_join_r; tneg_join:=rev_tneg_join}.

From ⨂-structures to ⅋-structures

Conversly, we show that strating from a conjunctive structure, the structure based on the reversed underlying complete lattice with the same negation and a⅋b := a⨂b defines a disjunctive structure.

Section ReverseTS.
  Context `{TS:TensorStructure}.

  Notation "¬ a":=(tneg a).

  Ltac autorev:=intros;unfold rev,reverse;auto.

  Lemma rev_par_mon: ∀ a a' b b', a ◃ a' -> b ◃ b' -> tensor a b ◃ tensor a' b'.
  Proof.
    autorev.
  Qed.

  Lemma rev_pneg_mon: ∀ a a', a ◃ a' -> (¬ a') ◃ (¬ a).
  Proof.
    autorev.
  Qed.

  Lemma rev_par_meet_l: ∀ A b, tensor (join_set A) b = join_set (@par_set_l X tensor A b).
  Proof.
    unfold par_set_l.
    apply tensor_join_l.
  Qed.

  Lemma rev_par_meet_r: ∀ a B, tensor a (join_set B) = join_set (@par_set_r X tensor a B).
  Proof.
    unfold par_set_l.
    apply tensor_join_r.
  Qed.

  Lemma rev_pneg_meet: ∀ A, tneg (join_set A) = meet_set (image_set tneg A).
  Proof.
    apply tneg_join.
  Qed.

End ReverseTS.

Global Instance TS_PS `{TS:TensorStructure}:@ParStructure _ _ _ RevCompleteLattice:=
  {par:=tensor; pneg:=tneg; par_mon:=rev_par_mon;
   pneg_mon:=rev_pneg_mon; par_meet_l:=rev_par_meet_l; par_meet_r:=rev_par_meet_r;
   pneg_meet:=rev_pneg_meet}.

Conjunctive algebras

We define conjunctive algebras as the given of a conjunctive structure together with a separator which contains at least the following combinators.

Definition TS1 `{TS:TensorStructure}:= ⋂[ a ] (a ⨂↦ (a ⨂ a)).
Definition TS2 `{TS:TensorStructure}:= ⋂[ a ] (⋂[ b ] ((a ⨂ b) ⨂↦ a )).
Definition TS3 `{TS:TensorStructure}:= ⋂[ a ] (⋂[ b ] ((a ⨂ b) ⨂↦ (b ⨂ a))).
Definition TS4 `{TS:TensorStructure}:= ⋂[ a ] ⋂[ b ] ⋂[ c ] ((a ⨂↦ b) ⨂↦ (c ⨂ a) ⨂↦ (c ⨂ b)).
Definition TS5 `{TS:TensorStructure}:= ⋂[ a ] ⋂[ b ] ⋂[ c ] ((a ⨂ (b ⨂ c)) ⨂↦ ((a ⨂ b) ⨂ c)).

Class TensorAlgebra `{TS:TensorStructure}:=
  {
    tsep: X → Prop;
    tmodus_ponens: ∀ a b, tsep a → tsep (a ⨂↦ b) → tsep b;
    tup_closed: ∀ a b, ord a b → tsep a → tsep b;
    tsep_TS1 : tsep TS1;
    tsep_TS2 : tsep TS2;
    tsep_TS3 : tsep TS3;
    tsep_TS4 : tsep TS4;
    tsep_TS5 : tsep TS5;
  }.

Notation "a '∈ʆ'":= (tsep a) (at level 80,no associativity):ta_scope.
Global Open Scope ta_scope.
Hint Resolve tsep_TS1 tsep_TS2 tsep_TS3 tsep_TS4 tsep_TS5.

Section ReverseParAlg.
  Context `{PA:ParAlgebra}.

  Definition pre_pneg := preimage (fun a => pneg a).
  Definition pre_pneg_set:= preimage_set (fun a => ¬ a).
  Notation "¬⁻¹ a":=(pre_pneg a) (at level 75):ia_scope.
  Notation "a ◃ b":= (rev Ord a b) (at level 70):ia_scope.



  Definition TS:=PS_TS.
  Definition revsep := pre_pneg_set (psep).

  Notation "a ⨂ b":= (@tensor _ _ _ _ TS a b).

  Lemma in_pre_pneg : ∀ A a, pre_pneg_set A a ↔ A (¬a).
  Proof.
    intros;split;intro H.
    - destruct H as (b,(Ab,Hb));subst;intuition.
    - exists (¬ a); auto.
  Qed.

  Lemma in_revsep : ∀ a, revsep a ↔ psep (¬a).
  Proof.
    intro a;unfold revsep.
    rewrite in_pre_pneg.
    intuition.
  Qed.

  Lemma up_closed_tsep: ∀ a b, a ◃ b → revsep a → revsep b.
  Proof.
    intros a b Hab Ha.
    rewrite in_revsep;rewrite in_revsep in Ha.
    apply pup_closed with (¬ a);intuition.
  Qed.

  Definition tarr:=(@tarrow _ _ _ _ TS).
  Infix "⨂↦":=(tarr) (at level 60, right associativity).

  Ltac PAstep ax:= eapply pup_closed;[|apply ax]; repeat auto_meet_intro; auto_meet_elim_trans.

  Lemma arrow_tsep_psep: ∀ a b, (revsep ( a ⨂↦ b) ↔ psep ((¬a) ⅋↦ (¬b))).
  Proof.
    intros a b ;split;intro H.
    - eapply pmodus_ponens with ((a⅋ ¬b)).
      + eapply pmodus_ponens with (¬¬(a⅋ ¬b)).
        * apply in_revsep;assumption.
        * apply dne_entails.
      + eapply pmodus_ponens;[exact (dni_entails a)|].
        eapply pup_closed;[|apply psep_PS4_r].
        apply (meet_elim_trans);later.
        split;[exists a;reflexivity|].
        apply (meet_elim_trans);later.
        split;[exists (¬¬a);reflexivity|].
        apply (meet_elim);exists (¬b).
        reflexivity.
    - apply in_revsep.
       eapply pmodus_ponens with ((a⅋ ¬b)).
       + eapply pmodus_ponens with ((¬¬a)⅋ ¬b).
         * assumption.
         * eapply pmodus_ponens;[exact (dne_entails a)|].
           eapply pup_closed;[|apply psep_PS4_r].
           apply (meet_elim_trans);later.
           split;[exists (¬¬a);reflexivity|].
           apply (meet_elim_trans);later.
           split;[exists (a);reflexivity|].
           apply (meet_elim);exists (¬b).
           reflexivity.
       + apply dni_entails.
  Qed.


  Lemma modus_ponens_revsep: ∀ a b, revsep a → revsep (a ⨂↦ b) → revsep b.
  Proof.
    intros a b Ha Hab.
    rewrite in_revsep.
    rewrite in_revsep in Ha.
    rewrite arrow_tsep_psep in Hab.
    eapply pmodus_ponens;[exact Ha|exact Hab].
Qed.

  Ltac auto_step_ter p ax:= eapply psep_PC6_ter with (g:= p);[step ax|].

  Ltac auto_rewrite:=
    match goal with
      |[ H: ?x = _ |- ?x = _] => rewrite H; try (reflexivity)
      |[ H: ?x = _ |- ?f ?x = _] => rewrite H; try (reflexivity)
    end.

  Ltac auto_same_set_step:=
    match goal with
      |[ |- _ ≅ _ ] => let x:=fresh "x" in let a := fresh "a" in let H:=fresh "H" in
                                                                 intro x; unfold image_set; split;intros (a,H)
      |[ H: (∃ _: X, _ = _ ) ∧ ?x = _ |- ∃ _:X, ?x = _] =>
       let b:=fresh "a" in let Ha:=fresh "H" in let Hb:=fresh "H" in
                                                destruct H as ((b,Hb),Ha);try(later; rewrite Ha,Hb) (* ,neg_join in ;try(now reflexivity) *)
      |[ H: ?x = _ |- ∃ _ : X, ((∃ _ : X, _ = _) ∧ ?x = _ )] =>
       try(later;split;[later;reflexivity|]);try(rewrite H;now reflexivity)
      |[ H: ?x = _ |- ∃ _ : X, ?x = _] => later;repeat(auto_rewrite)
      |[ |- (tneg (join_set _)) = _] => rewrite tneg_join
      |[ |- _ = (tneg (join_set _))] => rewrite tneg_join;repeat(auto_rewrite)
      |[ |- ⊓ _ = ⊓ _] => apply meet_same_set
      |[ |- _ = _] => now reflexivity
    end.
  Ltac auto_same_set:=repeat (auto_same_set_step).


  Lemma revsep_TS1: revsep (@TS1 _ _ _ _ TS).
  Proof.
    unfold TS1.
    rewrite meet_same_set with (B:=(image_set (@tneg _ _ _ _ TS) (λ x : X, ∃ a : X, x= (a ⨂ (¬ (a ⨂ a)))))).
    - rewrite <- tneg_join.
      rewrite in_revsep.
      unfold meet_set,tensor,TS,PS_TS,psep;simpl.
      eapply pmodus_ponens;[|exact (dni_entails _)].
      do 2 (auto_add_inf_X X).
      eapply mod_pon_inf_ter with (f:= fun (c b a :X) => (¬(a⅋a) ⅋ a)).
      + step psep_PS3.
      + step psep_PS1.
    - auto_same_set.
  Qed.

  Lemma revsep_TS2: revsep (@TS2 _ _ _ _ TS).
  Proof.
    unfold TS2.
    rewrite meet_same_set
    with (B:=image_set (@tneg _ _ _ _ TS) (λ x : X, ∃ a : X, x = @join_set _ _ _ RevCompleteLattice (λ x0 : X, ∃ b : X, x0 = ((a ⨂ b) ⨂ ¬ a)))).
    - rewrite <- tneg_join,in_revsep.
      unfold meet_set,tensor,TS,PS_TS,psep;simpl.
      eapply pmodus_ponens;[|exact (dni_entails _)].
      auto_add_inf_X X.
      eapply mod_pon_inf_ter with (f:= fun (c a b :X) => ((¬a ) ⅋ (a⅋b))).
      + step psep_PS3.
      + step psep_PS2.
    - auto_same_set.
  Qed.

  Lemma revsep_TS3: revsep (@TS3 _ _ _ _ TS).
  Proof.
    unfold TS3.
    rewrite meet_same_set with (B:=image_set (@tneg _ _ _ _ TS)
                                             (λ x : X, ∃ a : X, x = @join_set _ _ _ RevCompleteLattice (λ x0 : X, ∃ b : X, x0 = ((a ⨂ b) ⨂ ¬ (b⨂a))))).
    - rewrite <- tneg_join,in_revsep.
      unfold meet_set,tensor,TS,PS_TS,psep;simpl.
      eapply pmodus_ponens;[|exact (dni_entails _)].
      auto_add_inf_X X.
      eapply mod_pon_inf_ter with (f:= fun (c a b :X) => (b ⅋ a) ⅋↦ (a⅋b)).
      + step psep_PS3.
      + step psep_PS3.
    - auto_same_set.
  Qed.

  Lemma revsep_TS4: revsep (@TS4 _ _ _ _ TS).
  Proof.
    unfold TS4.
    rewrite meet_same_set with (B:=image_set (@tneg _ _ _ _ TS)
                                             (λ x : X, ∃ a : X, x = @join_set _ _ _ RevCompleteLattice
                                                                              (λ x0 : X, ∃ b : X, x0 = @join_set _ _ _ RevCompleteLattice
                                                                                                                  (λ x1 : X, ∃ c : X, x1 = (a ⅋ ¬ b) ⅋↦ (¬ ¬ ((c ⅋ a) ⅋ ¬ (c ⅋ b))))))).
    - rewrite <- tneg_join,in_revsep.
      unfold meet_set,tensor,TS,PS_TS,psep;simpl.
      eapply pmodus_ponens;[|exact (dni_entails _)].
      auto_step_ter (fun (a b c:X) => (b ⅋↦a)) psep_PS3.
      auto_step_ter (fun (a b c:X) => (c ⅋ b) ⅋↦ (c ⅋ a)) psep_PS4.
      auto_step_ter (fun (a b c:X) => (c ⅋ a) ⅋ ¬(c ⅋ b)) psep_PS3.
      step dni.
    - auto_same_set.
  Qed.

  Lemma revsep_TS5: revsep (@TS5 _ _ _ _ TS).
  Proof.
    unfold TS5.
    rewrite meet_same_set with (B:=image_set (@tneg _ _ _ _ TS)
                                             (λ x : X, ∃ a : X, x = @join_set _ _ _ RevCompleteLattice
                                                                              (λ x0 : X, ∃ b : X, x0 = @join_set _ _ _ RevCompleteLattice
                                                                                                                  (λ x1 : X, ∃ c : X, x1 = ((a ⅋ b ⅋ c) ⅋ ¬ ((a ⅋ b) ⅋ c)))))).
    - rewrite <- tneg_join,in_revsep.
      unfold meet_set,tensor,TS,PS_TS,psep;simpl.
      eapply pmodus_ponens;[|exact (dni_entails _)].
      rewrite par_comm_psep.
      step par_assoc_r.
    - auto_same_set.
  Qed.

Global Instance PA_TA:@TensorAlgebra _ _ _ _ TS:=
  {tsep:=revsep;tmodus_ponens:=modus_ponens_revsep;
   tup_closed:= up_closed_tsep; tsep_TS1:=revsep_TS1;
   tsep_TS2:=revsep_TS2;tsep_TS3:=revsep_TS3;tsep_TS4:=revsep_TS4;tsep_TS5:=revsep_TS5}.
End ReverseParAlg.

Section About_TensorAlg.
Context `{TA:TensorAlgebra}.
Notation "¬ a":=(tneg a).
Definition ts_abs t:= ⊓(λ x:X, ∃ a:X, x= ⊓ (λ y : X, ∃ b :X, y = (¬(a ⨂ ¬b)) ∧ t a ≤ b)).
Definition antiapp t u:= (⊔(λ x:X, ∃ a:X, x= a ∧ (t ≤ ¬ (u ⨂ a) ))).
Definition ts_app t u:= (⊓(λ x:X, ∃ a:X, x= a ∧ (t ≤ ⊔ ((λ y : X, ∃ b :X, y = (¬ b) ∧ (u ⨂ ¬a) ≤ b))))).
Notation "λ⨂ t":=(abs t) (at level 60).
Notation "t @⨂ u":=(ts_app t u) (at level 59, left associativity).
Definition eta a:= fun x => a @⨂ x.

Lemma semi_adjunction: ∀ t u r, (¬ r) ≤ antiapp t u <-> t ≤ u ⨂↦ r.
Proof.
intros t u r;split; intro H.
- apply ord_trans with (¬(u ⨂ antiapp t u)).
  + unfold antiapp in *.
    rewrite tensor_join_r,tneg_join.
    apply meet_intro.
    intros x (a,(Ha,Hx)).
    subst x. unfold tensor_set_r in Ha.
    destruct Ha as (b,((c,(Hc,Hd)),Ha)).
    subst. intuition.
  + apply tneg_mon.
    apply tensor_mon;[reflexivity|assumption].
- apply join_elim.
  now later;split;[reflexivity|].
Qed.

Lemma ts_half_adjunction: ∀ t u r, t ≤ u ⨂↦ r → t@⨂u ≤ r .
Proof.
  intros t u r H.
  auto_meet_elim_risky.
  auto_join_elim_risky.
  assumption.
Qed.

End About_TensorAlg.