ImpAlg.ParAlgebras

Set Implicit Arguments.
Set Contextual Implicit.

Require Import Utf8.
Require Import RelationClasses.
Require Import Morphisms.
Require Import Setoid.
Require Import ImpAlg.Ens.
Require Import ImpAlg.Lattices.
Require Export ImpAlg.ImplicativeStructures.
Require Export ImpAlg.Adequacy.
Require Export ImpAlg.Combinators.
Require Export ImpAlg.ImplicativeAlgebras.

We first define the lifting of a binary law ⅋ : X×X → X to sets on the right of left operands

Definition par_set_r {X:Set} {par:X → X → X} (a:X) (B:Ens):Ens :=
    fun x => ∃b, B b ∧ x = par a b.
Definition par_set_l {X:Set} {par:X → X → X} (A:Ens) (b:X):Ens :=
    fun x => ∃a, A a ∧ x = par a b.
Definition par_set {X:Set} {par:X → X → X} (A:Ens) (B:Ens):Ens :=
    fun x => ∃a,∃b, A a ∧ B b ∧ x = par a b.

Global Instance par_set_r_Proper `{X:Set} `{par:X → X → X} a:
  Proper ((@same_set X) ==> (@same_set X)) ((@par_set_r X par) a).
Proof.
  intros A B HAB.
  split;intros Hx; destruct Hx as [b [Hb Hx]];
  exists b;
  split;[apply HAB,Hb| assumption|apply HAB,Hb| assumption].
Qed.

Global Instance par_set_l_Proper `{X:Set} `{par:X → X → X} a:
  Proper ((@same_set X) ==> (@same_set X)) (fun A => (@par_set_l X par) A a).
Proof.
  intros A B HAB.
  split;intros Hx; destruct Hx as [b [Hb Hx]];
  exists b;
  split;[apply HAB,Hb| assumption|apply HAB,Hb| assumption].
Qed.

Disjunctive Structures


Class ParStructure `{CL:CompleteLattice} :=
  {
    par:X → X → X;
    pneg: X → X;

    par_mon: ∀ a a' b b', a ≤ a' → b ≤ b' -> par a b ≤ par a' b';

    pneg_mon: ∀ a a', ord a a' -> ord (pneg a') (pneg a);

    par_meet_l: ∀ A b, par (meet_set A) b = meet_set (@par_set_l X par A b);
    par_meet_r: ∀ a B, par a (meet_set B) = meet_set (@par_set_r X par a B);

    pneg_meet: ∀ A, pneg (meet_set A) = join_set (image_set pneg A)
  }.

Generalizable Variables X ord join meet pneg par L meet_set join_set.
Hint Resolve meet_elim meet_intro join_elim join_intro par_mon pneg_mon.
Hint Resolve par_meet_l par_meet_r pneg_meet.

Infix "⅋":= par (at level 76, right associativity):pa_scope.
Global Open Scope pa_scope.
Notation "¬ a":=(pneg a):pa_scope.
Notation "a ⅋↦ b":= (¬ a ⅋ b) (at level 60, right associativity):pa_scope.
Definition parrow `{PS:ParStructure} a b:= (a ⅋↦ b).

Hint Unfold parrow.

(* 
Section About_ParStructure.
  Context `{PS:ParStructure}. *)

Properties of the ⅋ operator


Lemma par_mon_l `{PS:ParStructure}:
  ∀ a a' b, ord a a' -> ord (par a b ) (par a' b ).
Proof.
intros a a' b H.
apply par_mon;intuition.
Qed.

Lemma par_mon_r `{PS:ParStructure}:
  ∀ a b b', b ≤ b' -> par a b ≤ par a b'.
Proof.
intros a b b' H.
apply par_mon;intuition.
Qed.

Lemma par_top_l `{PS:ParStructure}:
  ∀ a:X, (⊤ ⅋ a) = ⊤.
Proof.
  intros a.
  rewrite <- meet_emptyset.
  rewrite par_meet_l.
  apply meet_same_set.
  intros x;split;[intros (y,(H,_))| intros H];contradict H.
Qed.

Lemma par_top_r `{PS:ParStructure}:
   ∀ a:X, (a⅋⊤) = ⊤.
Proof.
  intros a.
  rewrite <- meet_emptyset.
  rewrite par_meet_r.
  apply meet_same_set.
  intros x;split;[intros (y,(H,_))| intros H];contradict H.
Qed.

Properties of the ¬ operator


Lemma pneg_top `{PS:ParStructure}:
   (¬⊤) = ⊥.
Proof.
  rewrite <- meet_emptyset.
  rewrite pneg_meet.
  rewrite <- join_emptyset.
  apply join_same_set.
  intros x;split;[intros (y,(H,_))| intros H];contradict H.
Qed.

Properties of the arrow


Lemma parrow_mon_l `{PS:ParStructure}:
   ∀ a a' b : X, a ≤ a' → a' ⅋↦ b ≤ a ⅋↦ b.
Proof.
  intros.
  apply par_mon_l.
  apply pneg_mon.
  intuition.
Qed.

Lemma parrow_mon_r `{PS:ParStructure}:
   ∀ a b b' : X, b ≤ b' → a ⅋↦ b ≤ a ⅋↦ b'.
Proof.
  intros.
  apply par_mon_r.
  intuition.
Qed.

Lemma parrow_mon `{PS:ParStructure}:
  ∀ a a' b b' , a' ≤ a -> b ≤ b' -> parrow a b ≤ parrow a' b'.
Proof.
  intros.
  apply (@ord_trans _ _ _ (a' ⅋↦ b)).
  - apply parrow_mon_l; auto.
  - apply parrow_mon_r; auto.
Qed.

Lemma parrow_meet `{PS:ParStructure}:
  ∀ (a : X) (B : Ens), a ⅋↦ (meet_set B) = meet_set (@arrow_set_r X parrow a B).
Proof.
  intros.
  apply par_meet_r.
Qed.

Induced implicative structure

Any disjunctive structure induces an implicative structure

Global Instance PS_IS `{PS:ParStructure}:ImplicativeStructure:=
{arrow:=parrow; arrow_mon_l:=parrow_mon_l; arrow_mon_r:=parrow_mon_r; arrow_meet:=parrow_meet}.

Lemma inf_pneg `{PS:ParStructure}:
   ∀ (f:X→X), ⋂[a] (f a) ≤ ⋂[a] (f (¬a)).
Proof.
intro f.
auto_meet_leq.
Qed.

We can transfer all the properties of application and abstraction obtained in implicative structures. We only recall the main one here.

Lemma ps_app_mon `{PS:ParStructure}:
  ∀ a a' b b', a≤ a' → b ≤ b' → a @ b ≤ a' @ b'.
Proof.
    apply (@app_mon _ _ _ _ PS_IS).
Qed.

Lemma ps_abs_mon `{PS:ParStructure}:
  ∀ f g, (∀a, f a ≤ g a) → (λ- f) ≤ (λ- g).
Proof.
  apply (@abs_mon _ _ _ _ PS_IS).
Qed.

Lemma ps_betarule `{PS:ParStructure}:
  ∀ f a, (λ- f) @ a ≤ f a.
Proof.
  apply (@betarule _ _ _ _ PS_IS).
Qed.

Lemma ps_etarule `{PS:ParStructure}:
   ∀ a, a ≤ (λ- (eta a)).
Proof.
    apply (@etarule _ _ _ _ PS_IS).
Qed.

Lemma ps_app_min `{PS:ParStructure}:
  ∀ a b, min (fun x => a ≤ b ⅋↦ x) (a@b).
Proof.
    apply (@app_min _ _ _ _ PS_IS).
Qed.

Lemma ps_adjunction `{PS:ParStructure}:
  ∀ a b c, a @ b ≤ c ↔ a ≤ b ⅋↦ c.
Proof.
  apply (@adjunction _ _ _ _ PS_IS).
Qed.

Definition ps_upwards_closure `{PS:ParStructure} (A:Ens):= ∀ a b, a≤ b → A a → A b .
Definition ps_app_closure `{PS:ParStructure} (A:Ens):= ∀ a b, A a → A b → A (a@b).
Definition ps_mod_pon_closure `{PS:ParStructure} (A:Ens):= ∀ a b, A a → A (a⅋↦b) → A b.
Remark mod_pon_app `{PS:ParStructure}:∀ A:Ens, ps_upwards_closure A → (ps_app_closure A <-> ps_mod_pon_closure A).
Proof.
  apply (@mod_pon_app _ _ _ _ PS_IS).
Qed.


Hint Resolve par_mon_l par_mon_r parrow_mon_l parrow_mon_r parrow_mon.

We define some tactics which we use to prove that two meets are equal from the fact that the corresponding sets are extensionally equals.

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_stepX X:=
  match goal with
  |[ |- _ ≅ _ ] => let x:=fresh "x" in let a := fresh "a" in let H:=fresh "H" in
              intro x; unfold image_set,par_set_r,par_set_l; split;try (intros [a H]);intros
  |[ 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)
   |[ H: ∃ _: X, (_ ∧ ?x = _) |- _] =>
    let b:=fresh "a" in let Ha:=fresh "H" in let Hb:=fresh "H" in
    destruct H as (b,(Hb,Ha));try(subst b);auto
  |[ H: ∃ _: X,_ |- _] =>
    let b:=fresh "a" in let Ha:=fresh "H" in
    destruct H as (b,Ha);try(subst);auto
  |[ H: _ ∧ _ |- _] =>
    let Ha:=fresh "H" in let Hb:=fresh "H" in
    destruct H as (Ha,Hb);try(subst);auto
(*  
 *)(*
 *)
   |[ H: ?x = _ |- ∃ _ : X, ((∃ _ : X, _ = _) ∧ ?x = _ )] =>
      try(later;split;[later;reflexivity|]);try(rewrite H;now reflexivity)
   |[ H: ?x = _ |- ∃ _ : X,( _ ∧ ?x = _ )] =>
    later;split;[|reflexivity];try(now auto)
    |[ H: ?x = _ |- ∃ _ : X, ?x = _] => later;repeat(auto_rewrite)
   |[ H: ?A ?x |- ∃ a : X,( ?A a ∧ ?x = a )] =>
      try(later;split;[|reflexivity]);try(now auto)
  |[ |- ⊓ _ = ⊓ _] => apply meet_same_set
  |[ |- _ = _] => now reflexivity
  end.



Ltac auto_same_setX X:=repeat (auto_same_set_stepX X).

Commutations of par and meets
  Lemma par_meet_f_r `{PS:ParStructure}:
    ∀ (b:X) (f:X→X),( b ⅋ (⋂[a] f a)) = ⋂[a] (b ⅋ ( f a)).
  Proof.
  intros b f.
  rewrite par_meet_r.
  apply meet_same_set.
  auto_same_setX X.
  Qed.

  Lemma arrow_meet_r `{PS:ParStructure}:
    ∀ (b:X) (f:X→X),( b ⅋↦ (⋂[a] f a)) = ⋂[a] (b ⅋↦ ( f a)).
  Proof.
  intros b f.
  apply par_meet_f_r.
  Qed.

  Lemma arrow_meet_r_aux `{PS:ParStructure}: ∀ (f:X→X→X) (g:X→X→X→X),
  ⋂[a] (⋂[b] ((f a b) ⅋↦ (⋂[c] (g a b c)))) = ⋂[a] ⋂[b] ⋂[c] ((f a b ) ⅋↦ (g a b c)).
  Proof.
  intros f g.
  apply ord_antisym.
  - auto_meet_leq. apply parrow_mon_r. auto_meet_leq.
  - do 2 auto_meet_intro. apply ps_adjunction. auto_meet_intro.
  apply ps_adjunction. auto_meet_elim_trans.
  Qed.

Disjunctive Algebras

We define the combinators which will axiomatize disjunctive separators. These combinators corresponds to Bourbaki logical axioms in Eléments de mathématique. Théorie des ensembles. I§3, p25

Definition PS1 `{PS:ParStructure}:= ⋂[ a ] ((a ⅋ a) ⅋↦ a).
Definition PS2 `{PS:ParStructure}:= ⋂[ a ] (⋂[ b ] (a ⅋↦ (a ⅋ b))).
Definition PS3 `{PS:ParStructure}:= ⋂[ a ] (⋂[ b ] ((a ⅋ b) ⅋↦ (b ⅋ a))).
Definition PS4 `{PS:ParStructure}:= ⋂[ a ] ⋂[ b ] ⋂[ c ] ((a ⅋↦ b) ⅋↦ (c ⅋ a) ⅋↦ (c ⅋ b)).
Definition PS5 `{PS:ParStructure}:= ⋂[ a ] ⋂[ b ] ⋂[ c ] ((a ⅋ (b ⅋ c)) ⅋↦ ((a ⅋ b) ⅋ c)).

Definition PK `{PS:ParStructure}:= ⋂[a] ⋂[b] (a ⅋↦ b ⅋↦ a).
Definition PS `{PS:ParStructure}:= ⋂[a] ⋂[b] ⋂[c] ((a ⅋↦ b ⅋↦ c) ⅋↦ (a ⅋↦ b) ⅋↦ a ⅋↦ c).
Definition Pcc `{PS:ParStructure}:= ⋂[a] ⋂[b](((a ⅋↦ b) ⅋↦ a) ⅋↦ a).

Class ParAlgebra `{PS:ParStructure}:=
  {
    psep: X → Prop;
    pmodus_ponens: ∀ a b, psep a → psep (¬ a ⅋ b) → psep b;
    pup_closed: ∀ a b, ord a b → psep a → psep b;
    psep_PS1 : psep PS1;
    psep_PS2 : psep PS2;
    psep_PS3 : psep PS3;
    psep_PS4 : psep PS4;
    psep_PS5 : psep PS5;
  }.

Notation "a '∈ʆ'":= (psep a) (at level 80,no associativity):pa_scope.
Hint Resolve psep_PS1 psep_PS2 psep_PS3 psep_PS4 psep_PS5.

(* * Tactics  *)

Ltac step ax:= eapply pup_closed;[|apply ax]; repeat auto_meet_intro; auto_meet_elim_trans.
Ltac auto_empty_meet_elim := apply meet_elim_trans ;later;split;[later;[assumption|reflexivity]|auto_meet_leq].
Ltac auto_add_inf_X X:=
match goal with
  |[ |- psep ?p ]=>
  apply pup_closed with (meet_set (fun x => ∃(b:X), x=(p))) ;auto_meet_leq;[repeat auto_empty_meet_elim|]
end.

Section About_ParAlg.
  Context `{PA:ParAlgebra}.
  Definition IS:=PS_IS.
  Ltac auto_add_inf:=auto_add_inf_X X.
  Ltac auto_same_set_step:=auto_same_set_stepX X.
  Ltac auto_same_set:=auto_same_set X.

Properties of the separator


  Lemma modus_ponens_parrow: ∀ a b, psep a → psep (a ⅋↦ b) → psep b.
  Proof.
    intros a b Sa Sab.
    apply (pmodus_ponens a b Sa).
    intuition.
  Qed.

  Definition entails a b := psep (a ⅋↦ b).
  Infix "⊢":= entails (at level 75).
  Definition equivalence a b := a ⊢ b ∧ b ⊢ a.

  Lemma S1_p : ∀ (a:X), (a ⅋ a) ⊢ a.
  Proof.
    intros.
    apply (pup_closed PS1);auto.
    auto_meet_elim_trans.
  Qed.

  Lemma S2_p : ∀ a b, a ⊢ (a ⅋ b).
  Proof.
    intros.
    apply (pup_closed PS2);auto.
    auto_meet_elim_trans.
  Qed.

  Lemma S3_p : ∀ a b, (a ⅋ b) ⊢ (b ⅋ a).
  Proof.
    intros.
    apply (pup_closed PS3);auto.
    auto_meet_elim_trans.
  Qed.

  Lemma S4_p : ∀ a b c,(a ⅋↦ b) ⊢ (c ⅋ a) ⅋↦ (c ⅋ b).
  Proof.
    intros.
    apply (pup_closed PS4);auto.
    auto_meet_elim_trans.
  Qed.

  Hint Resolve S1_p S2_p S3_p S4_p.

  Lemma app_closed : ∀ a b, psep a → psep b → psep (a@b).
  Proof.
  intros.
  apply (pmodus_ponens b (a@b)).
  - assumption.
  - apply (pup_closed a).
   + apply ps_adjunction.
     apply ord_refl.
   + assumption.
  Qed.

  Hint Resolve app_closed adjunction etarule betarule.


We define some other useful terms and lemma. The names, which might seem a bit cryptic, are borrowed from Bourbaki.

  Lemma C6_p a b c: (a ⊢ b) → (b ⊢ c) → (a ⊢ c).
  Proof.
    intros Sab Sbc.
    apply (pmodus_ponens (a ⅋↦ b) _ Sab).
    apply (pmodus_ponens (b ⅋↦ c) _ Sbc).
    apply S4_p.
  Qed.

Technical lemmas

We define a bunch of lemmas that will be useful in the sequel to obtain properties about separators. This section only contains boring technical lemmas, and is not of great interest. Logical properties of separators are given in the next section.
Generalized modus ponens, compatible with meets

  Lemma mod_pon_inf:
     ∀ (f g:X→X→X), psep (⋂[a] ⋂[b] ((f a b) ⅋↦ (g a b)))
              → psep (⋂[a] ⋂[b] (f a b)) → psep (⋂[a] ⋂[b] (g a b)).
  Proof.
    intros f g Hfg Hf.
    remember (⋂[a] ⋂[b] ((f a b) ⅋↦ (g a b))) as Ifg.
    remember (⋂[a] ⋂[b] (f a b)) as If.
    apply pup_closed with (Ifg@If);auto.
    repeat auto_meet_intro.
    apply adjunction.
    rewrite HeqIfg.
    auto_meet_elim_trans.
    apply parrow_mon_l.
    rewrite HeqIf.
    auto_meet_elim_trans.
  Qed.

  Lemma mod_pon_inf_ter:
     ∀ (f g:X→X→X→X), psep (⋂[a] ⋂[b] ⋂[c] ((f a b c) ⅋↦ (g a b c)))
     → psep (⋂[a] ⋂[b] ⋂[c] (f a b c)) → psep (⋂[a] ⋂[b] ⋂[c] (g a b c)).
  Proof.
    intros f g Hfg Hf.
    remember (⋂[a] ⋂[b] ⋂[c] ((f a b c) ⅋↦ (g a b c))) as Ifg.
    remember (⋂[a] ⋂[b] ⋂[c](f a b c)) as If.
    apply pup_closed with (Ifg@If);auto.
    repeat auto_meet_intro.
    apply adjunction.
    rewrite HeqIfg.
    auto_meet_elim_trans.
    apply parrow_mon_l.
    rewrite HeqIf.
    auto_meet_elim_trans.
  Qed.

The following lemmas allow us to deduce that a given arrow of the shape:
⋂a ( bli ⅋↦ blo )
in the separator by using intermediate steps, like
⋂a ( bli ⅋↦ bla ) and ⋂a ( bla ⅋↦ blo )
We call it the generalized transitivity.

  Definition PC6 (f g:X→X→X):=(⋂[a] ⋂[b]((f a b) ⅋↦ (g a b))).
  Definition PC6_ter (f g:X→X→X→X):=(⋂[a] ⋂[b] ⋂[c] ((f a b c) ⅋↦ (g a b c))).

  Lemma psep_PC6:
    forall f g h, psep (PC6 f g) → psep (PC6 g h) → psep (PC6 f h).
  Proof.
    intros f g h Hfg Hgh.
    apply pup_closed with ((PS4 @(PC6 g h))@(PC6 f g));auto.
    repeat auto_meet_intro.
    do 2 apply adjunction.
    auto_meet_elim_trans.
    apply parrow_mon;[auto_meet_elim_trans|].
    apply parrow_mon;[auto_meet_elim_trans|].
    reflexivity.
  Qed.

  Lemma psep_PC6_ter: ∀ f g h, psep (PC6_ter f g) → psep (PC6_ter g h) → psep (PC6_ter f h).
  Proof.
    intros f g h Hfg Hgh.
    apply pup_closed with ((PS4 @(PC6_ter g h))@(PC6_ter f g));auto.
    repeat auto_meet_intro.
    do 2 apply adjunction.
    auto_meet_elim_trans.
    apply parrow_mon;[auto_meet_elim_trans|].
    apply parrow_mon;[auto_meet_elim_trans|].
    reflexivity.
  Qed.

a⅋b is implied by b (dual to PS2 for a)

  Definition PC7:= ⋂[a] ⋂[b] (b ⅋↦ (a ⅋ b)).
  Lemma psep_C7: psep PC7.
  Proof.
    apply psep_PC6 with (g:=fun a b => b ⅋ a).
    - eapply pup_closed.
      apply inf_comm_aux.
      apply psep_PS2.
    - unfold PC6.
      eapply pup_closed.
      apply inf_comm_aux.
      apply psep_PS3.
  Qed.

  Hint Resolve psep_C7.

  Lemma C7: ∀ a b, psep (b ⅋↦ (a ⅋ b)).
  Proof.
    intros a b.
    apply (pup_closed PC7);[auto_meet_elim_trans|exact psep_C7].
  Qed.

The following tactic is very convenient: it automatizes a step by generealized transitivity with the axiom "ax". The argument "p" is here to help the tactic determin the shape of the intermediate step.

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

⅋ is associative on both sides (under meets)

  Definition par_assoc_l:=psep_PS5.
  Lemma par_assoc_r: psep (⋂[a] (⋂[b] (⋂[c] (((a ⅋ b) ⅋ c) ⅋↦ (a ⅋ (b ⅋ c)))))).
  Proof.
    auto_step_ter (fun a b c => c ⅋ (a ⅋ b)) psep_PS3.
    auto_step_ter (fun a b c => (c ⅋ a) ⅋ b) psep_PS5.
    auto_step_ter (fun a b c => b ⅋ (c ⅋ a)) psep_PS3.
    auto_step_ter (fun a b c => (b ⅋ c) ⅋ a) psep_PS5.
    step psep_PS3.
  Qed.

We can swap operands of a disjunction (under meets)

  Definition Pswap_r:=(⋂[a] (⋂[b] (⋂[c] ((a ⅋ ( b ⅋ c)) ⅋↦ (a ⅋ (c ⅋ b)))))).
  Lemma swap_r: psep Pswap_r.
  Proof.
    eapply mod_pon_inf_ter with (f:= fun a b c => (b ⅋ c) ⅋↦ (c ⅋ b)).
    step psep_PS4.
    step psep_PS3.
  Qed.

  Definition Pswap_l:=⋂[a] (⋂[b] (⋂[c] ((a ⅋ ( b ⅋ c)) ⅋↦ (b ⅋ (a ⅋ c))))).

  Lemma swap_l: psep Pswap_l.
  Proof.
    auto_step_ter (fun a b c => (b ⅋ c) ⅋ a) psep_PS3.
    auto_step_ter (fun a b c => b ⅋ (c ⅋ a)) par_assoc_r.
    step swap_r.
  Qed.

A useful tactics which allows to automatize intermediate step by modus ponens

  Ltac auto_mod_pon_ter ax:=
    match ax with
    | psep (⋂[a] (⋂[b] (⋂[c] ( ?p a b c)))) =>
        try(eapply mod_pon_inf_ter with (f:=fun a b c => p a b c);[try(step ax)|try assumption]);
        try(eapply mod_pon_inf_ter with (g:=fun a b c => p a b c);[try assumption|try(step ax)])
    end.

  Ltac step_mod_pon_ter g ax := eapply mod_pon_inf_ter with (f:=g);[step ax|try assumption].


The separator is somewhat closed by commutativity/associativity/etc... of ⅋ (under meets)

  Lemma par_comm_psep:∀ (f g :X→X→X→X),
  psep (⋂[a] ⋂[b] ⋂[c] ((f a b c) ⅋ (g a b c)))
    <-> psep (⋂[a] ⋂[b] ⋂[c] ((g a b c) ⅋ (f a b c))).
  Proof.
  intros f g .
  split;intro H.
  - step_mod_pon_ter (fun a b c => (f a b c) ⅋ (g a b c)) psep_PS3.
  - step_mod_pon_ter (fun a b c => (g a b c) ⅋ (f a b c)) psep_PS3.
  Qed.

  Lemma par_assoc_psep:∀ (f g h:X→X→X→X),
  psep (⋂[a] (⋂[b] (⋂[c] (((f a b c) ⅋ ( (g a b c) ⅋ (h a b c)))))))
    <-> psep (⋂[a] (⋂[b] (⋂[c] ((((f a b c) ⅋ (g a b c)) ⅋ (h a b c)))))).
  Proof.
  intros f g h.
  split;intro H.
  - step_mod_pon_ter (fun a b c => (f a b c) ⅋ (g a b c) ⅋ (h a b c)) par_assoc_l.
  - step_mod_pon_ter (fun a b c => ((f a b c) ⅋ (g a b c)) ⅋ (h a b c)) par_assoc_r.
  Qed.

  Lemma par_swap_psep:∀ (f g h:X→X→X→X),
  psep (⋂[a] (⋂[b] (⋂[c] (((f a b c) ⅋ ( (g a b c) ⅋ (h a b c)))))))
    <-> psep (⋂[a] (⋂[b] (⋂[c] ((g a b c) ⅋ (f a b c) ⅋ (h a b c))))).
  Proof.
  intros f g h.
  split;intro H.
  - step_mod_pon_ter (fun a b c => (f a b c) ⅋ (g a b c) ⅋ (h a b c)) swap_l.
  - step_mod_pon_ter (fun a b c => (g a b c) ⅋ (f a b c) ⅋ (h a b c)) swap_l.
  Qed.

  Lemma arrow_swap_psep:∀ (f g h:X→X→X→X), psep (⋂[a] (⋂[b] (⋂[c] (((f a b c) ⅋↦ (g a b c) ⅋↦ (h a b c))))))
    <-> psep (⋂[a] (⋂[b] (⋂[c] (((g a b c) ⅋↦ (f a b c) ⅋↦ (h a b c)))))).
  Proof.
  intros f g h.
  rewrite par_swap_psep.
  intuition.
  Qed.


  Hint Resolve swap_r swap_l par_assoc_r.


Some more lemmas to be used with the modus_ponens or similar pre-compositions

  Lemma S6_gen:psep (⋂[a] ⋂[b] ⋂[c] ((a ⅋↦ b) ⅋↦ (b ⅋↦ c) ⅋↦ (a ⅋↦ c))).
  Proof.
    apply pup_closed with (Pswap_l @ PS4);[|apply app_closed;auto].
    repeat auto_meet_intro.
    apply adjunction.
    auto_meet_elim_trans;auto.
    apply parrow_mon.
    - auto_meet_elim_trans.
    - reflexivity.
  Qed.


  Lemma pre_comp_arr_bi: ∀ f g h k,
  psep ( ⋂[a] ⋂[b] ⋂[c] ((f a b c) ⅋↦ (g a b c) ⅋↦ (h a b c))) →
      psep (PC6_ter h k ) → psep ( ⋂[a] ⋂[b] ⋂[c] ((f a b c) ⅋↦ (g a b c) ⅋↦ (k a b c))).
  Proof.
    intros f g h k Ifg Ih.
    rewrite par_assoc_psep in Ifg.
    rewrite par_assoc_psep.
    apply pup_closed with ((PS4 @(PC6_ter h k))@(⋂[a] ⋂[b] ⋂[c] (((¬(f a b c)) ⅋ ¬(g a b c)) ⅋ (h a b c))));auto.
    repeat auto_meet_intro.
    do 2 apply adjunction;auto_meet_elim_trans.
    apply parrow_mon;[auto_meet_elim_trans|].
    apply parrow_mon_l; auto_meet_elim_trans.
  Qed.

  Hint Unfold PC6 PC6_ter.

  Lemma swap_imp: ∀ (f g:X→X→X→X), psep (⋂[a] ⋂[b] ⋂[c] ((c⅋ (f a b c)) ⅋↦ (c ⅋ (g a b c))))
      → psep (⋂[a] ⋂[b] ⋂[c] (((f a b c)⅋ c) ⅋↦ ((g a b c) ⅋c))).
  Proof.
    intros f g H.
    auto_step_ter (fun a b c => (c ⅋ (f a b c))) psep_PS3.
    auto_step_ter (fun a b c => (c ⅋ (g a b c))) H.
    step psep_PS3.
  Qed.

  Lemma mod_pon_cong:
     ∀ (f g:X→X→X), psep (⋂[a] ⋂[b] ⋂[c] (((f a b) ⅋↦ (g a b))⅋c))
     → psep (⋂[a] ⋂[b] ⋂[c] ((f a b)⅋c)) → psep (⋂[a] ⋂[b] ⋂[c] ((g a b)⅋c)).
  Proof.
    intros f g Hfg Hf.
    eapply mod_pon_inf_ter ; [|exact Hf].
    simpl.
    eapply psep_PC6_ter with (g:= (fun a b c => ((g a b) ⅋ c) ⅋ c)).
    - apply swap_imp.
      step_mod_pon_ter (fun a b c => ((f a b) ⅋↦ ( (g a b) ⅋ c))) psep_PS4.
      step_mod_pon_ter (fun a b c => (((f a b) ⅋↦ (g a b)) ⅋ c)) par_assoc_r.
    - auto_step_ter (fun a b c => ((g a b) ⅋ (c ⅋ c))) par_assoc_r.
      step_mod_pon_ter (fun (a b c:X) => ((c ⅋ c) ⅋↦ (c))) psep_PS4.
      step psep_PS1.
  Qed.




A few more combinators

The identity is in any separator

  Definition PI:=(⋂[a] (a ⅋↦ a)).
  Lemma psep_PI : psep PI.
  Proof.
    apply (pup_closed (⊓ (fun x => ∃(b:X), x= PI))).
    - auto_meet_intro. eapply meet_elim_trans.
      later. split;[later;[auto|reflexivity]| auto_meet_elim_trans].
    - eapply psep_PC6 with (g:= (fun b a => a ⅋ a)).
     + step psep_PS2.
     + step psep_PS1.
  Qed.

  Definition PS2_l := ⋂[ a ] ⋂[ b ] (a ⅋↦ (b ⅋ a)).
  Lemma psep_PS2_l: psep PS2_l.
  Proof.
  eapply psep_PC6 with (g:= (fun a b=> a ⅋ b)).
  step psep_PS2.
  step psep_PS3.
  Qed.

  Definition PS4_r := ⋂[ a ] ⋂[ b ] ⋂[ c ] ((a ⅋↦ b) ⅋↦ (a ⅋ c) ⅋↦ (b ⅋ c)).
  Lemma psep_PS4_r: psep PS4_r.
  Proof.
    auto_step_ter (fun a b c => (c ⅋ a) ⅋↦ (c ⅋ b)) psep_PS4.
    eapply psep_PC6_ter with (g:=fun a b c => (c ⅋ a) ⅋↦ (b ⅋ c)).
    - step_mod_pon_ter (fun (a b c:X) => (c ⅋ b) ⅋↦ (b ⅋ c)) psep_PS4.
      step psep_PS3.
    - unfold PC6_ter.
      rewrite par_swap_psep.
      auto_step_ter (fun (a b c:X) => (c ⅋ a)) psep_PS3.
      unfold PC6_ter; rewrite <- par_swap_psep.
      apply (pup_closed PI);[| apply psep_PI].
      auto_meet_leq.
  Qed.



Extra-hypothesis

This lemma is fundamental in Bourbaki, it is used to add extra non-necessary hypotheses in order to generalize a term.

  Lemma extra_hyp: forall (f g h:X→X→X), psep (⋂[a] ⋂[b] ((f a b ) ⅋↦ (g a b))) →
  psep (⋂[a] ⋂[b] ((h a b) ⅋↦ (f a b) ⅋↦ (g a b ))).
  Proof.
  intros f g h Hfg.
  eapply mod_pon_inf with (fun a b => (f a b ) ⅋↦ (g a b));auto.
  step psep_PS2_l.
  Qed.

  Lemma extra_hyp_ter: forall (f g h:X→X→X→X), psep (⋂[a] ⋂[b] ⋂[c] ((f a b c) ⅋↦ (g a b c))) →
  psep (⋂[a] ⋂[b] ⋂[c] ((h a b c) ⅋↦ (f a b c) ⅋↦ (g a b c))).
  Proof.
  intros f g h Hfg.
  step_mod_pon_ter (fun a b c => (f a b c) ⅋↦ (g a b c)) psep_PS2_l.
  Qed.

  Lemma half_pmodus_ponens: ∀ (f g:X→X→X), psep (⋂[a] ⋂[b] (f a b))
  → psep (⋂[a] ⋂[b] (((f a b ) ⅋↦ (g a b)) ⅋↦ (g a b))).
  Proof.
  intros f g Hf.
  eapply mod_pon_inf;[|exact Hf].
  auto_add_inf.
  rewrite arrow_swap_psep.
  step psep_PI.
  Qed.


Logical properties

We are now equipped to give some logical properties of the separator. In particular, we prove that some elements (which correpond to meaningful formulas) always belong to separators.

Sum type


  Definition or a b:= ⋂[c] ((a ⅋↦ c) ⅋↦ (b ⅋↦ c) ⅋↦ c).
  Infix "+":=or.

  Lemma par_or_gen : psep (⋂[a] ⋂[b]( (a ⅋ b) ⅋↦ a + b)).
  Proof.
  unfold or.
  rewrite arrow_meet_r_aux.
  assert (⋂[ a] (⋂[ b] (⋂[ c] ( (b ⅋↦ c) ⅋↦ (a ⅋ b) ⅋↦ (a ⅋↦ c) ⅋↦ c))) ∈ʆ).
  - apply (pre_comp_arr_bi (fun a b c => b ⅋↦ c) (fun a b c => a ⅋ b )
          (fun (a b c:X) => a ⅋ c) (fun (a b c:X) => (¬ a ⅋↦ c) ⅋ c)).
    step psep_PS4.
    auto_step_ter (fun (a b c:X) => c⅋a) psep_PS3.
    unfold PC6_ter.
    rewrite arrow_swap_psep.
    apply pre_comp_arr_bi with (h:=fun (a b c:X) => c⅋c);[step psep_PS4|step psep_PS1].
  - rewrite par_assoc_psep .
    rewrite par_swap_psep.
    auto_step_ter (fun (a b c:X) => (a ⅋ b) ⅋↦ (a ⅋↦ c) ⅋↦ c) H.
    step psep_PS5.
  Qed.

  Lemma par_or : ∀ a b, (a ⅋ b) ⊢ (a + b).
  Proof.
  intros a b. step par_or_gen.
  Qed.

  Lemma or_par_gen : psep (⋂[a] ⋂[b]( a + b ⅋↦ (a ⅋ b))).
  Proof.
  apply psep_PC6 with (g:= fun a b => ((a ⅋↦ (a⅋b))⅋↦ (b ⅋↦ (a⅋b)) ⅋↦ (a⅋b))).
  - step psep_PI.
    apply parrow_mon_r. auto_meet_elim_trans.
  - apply psep_PC6 with (g:= fun a b => ((b ⅋↦ (a⅋b)) ⅋↦ (a⅋b))).
    + apply half_pmodus_ponens. step psep_PS2.
    + apply half_pmodus_ponens. step psep_PS2_l.
  Qed.

  Lemma or_par : ∀ a b, (a + b) ⊢ (a ⅋ b).
  Proof.
  intros a b. step or_par_gen.
  Qed.




Properties of the negation


  Lemma ex_falso: psep (⋂[a] ( bot ⅋↦ a )).
  Proof.
    apply (pup_closed PI);[|apply psep_PI].
    auto_meet_leq.
    apply parrow_mon_r.
    auto.
  Qed.

  Lemma dni: psep (⋂[a] (a ⅋↦ ¬¬a)).
  Proof.
    do 2 auto_add_inf.
    rewrite <- par_comm_psep.
    apply pup_closed with (⋂[a](a ⅋↦ a));[auto_meet_leq|exact psep_PI].
  Qed.

  Lemma dni_entails: forall a, a ⊢ ¬¬a.
  Proof.
  intro a.
  eapply pup_closed;[|exact dni];auto_meet_elim_trans.
  Qed.



  Lemma pneg_arrow: psep (⋂[a] ((¬a) ⅋↦ (a ⅋↦ ⊥))).
  Proof.
  auto_add_inf.
  rewrite inf_comm.
  step psep_PS2.
  Qed.

  Lemma pneg_imp_bot: ∀ a, (¬ a) ⊢ a ⅋↦ ⊥.
  Proof.
  intro a. step pneg_arrow.
  Qed.

  Lemma arrow_pneg: psep (⋂[a] ((a ⅋↦ ⊥) ⅋↦ (¬a))).
  Proof.
  auto_add_inf.
  apply psep_PC6 with (g:= fun a b=> (b ⅋↦ ¬ b));unfold PC6;simpl.
  - step psep_PI. apply parrow_mon_r. intuition.
  - apply mod_pon_inf with (f:=fun a b => (¬b) ⅋↦ ¬b);[|step psep_PI].
    apply mod_pon_inf with (f:=fun (a b:X) => (¬ b) ⅋ b);[|step psep_PI].
    step par_or_gen.
    apply parrow_mon_r.
    auto_meet_elim_trans.
  Qed.

  Lemma imp_bot_pneg: ∀ a, (a ⅋↦ ⊥) ⊢ ¬ a.
  Proof.
  intro a. step arrow_pneg.
  Qed.

  Lemma absurd_aux_ter:
  ∀ (f:X→X→X→X), psep (⋂[a] (⋂[b] ⋂[c] (((¬ (f a b c)) ⅋↦ (f a b c)) ⅋↦ (f a b c)))).
  Proof.
  intros f.
  eapply mod_pon_inf_ter with (f:=fun (a b c:X)=> (f a b c) ⅋↦ (f a b c));[|step psep_PI].
  eapply mod_pon_inf_ter with (f:=fun (a b c:X)=> (f a b c)⅋ ¬(f a b c)).
  - eapply pup_closed;[|exact par_or_gen].
    unfold or.
    rewrite arrow_meet_r_aux.
    auto_meet_leq.
  - step_mod_pon_ter (fun (a b c:X) => (¬ (f a b c))⅋ (f a b c)) psep_PS3.
    step psep_PI.
  Qed.

  Lemma absurd_aux: psep (⋂[a] (((¬ a) ⅋↦ a) ⅋↦ a)).
  Proof.
  eapply pup_closed;[|exact (absurd_aux_ter (fun (a b c:X)=> a))].
  auto_meet_leq.
  do 2 auto_empty_meet_elim.
  Qed.

  Lemma absurd: ∀ (f:X→X→X→X), psep (⋂[a] (⋂[b] ⋂[c] (((¬ (f a b c)) ⅋↦ ⊥) ⅋↦ f a b c))).
  Proof.
  intros f.
  apply psep_PC6_ter with (g:=fun (a b c:X) => (¬ (f a b c)) ⅋↦ (f a b c));[|step absurd_aux].
  step psep_PI. apply parrow_mon_r. now apply parrow_mon_r.
  Qed.

  Lemma reductio_ad_absurdum:∀a, (¬ a) ⅋↦ ⊥ ⊢ a.
  Proof.
  intros a.
  step (absurd (fun a b c => c)).
  do 2 auto_empty_meet_elim.
  Qed.

  Lemma dne: psep (⋂[a] ((¬¬a) ⅋↦ a)).
  Proof.
  do 2 auto_add_inf.
  auto_step_ter (fun (a b c:X) => ((¬c) ⅋↦ ⊥) ) pneg_arrow.
  step (absurd (fun a b c => c)).
  do 2 auto_empty_meet_elim.
  Qed.

  Lemma dne_entails: forall a, (¬ ¬ a) ⊢ a.
  Proof.
  intro a.
  eapply pup_closed;[|exact dne];auto_meet_elim_trans.
  Qed.

Combinator K


  Lemma psep_K : psep PK.
  Proof.
    apply (pup_closed PC7);auto.
    unfold PC7,PK.
    eapply ord_trans.
    - apply inf_comm_aux.
    - cbn. auto_meet_leq.
  Qed.

  Lemma arrow_precomp_par_assoc:forall (f g h k:X→X→X→X), psep (⋂[a] (⋂[b] (⋂[c] (((f a b c ) ⅋ (g a b c) ⅋ (h a b c)) ⅋↦ (k a b c)))))
  <-> psep (⋂[a] (⋂[b] (⋂[c] ((((f a b c ) ⅋ (g a b c)) ⅋ (h a b c)) ⅋↦ (k a b c))))).
  Proof.
  intros f g h k;split;intro H.
  - auto_step_ter (fun a b c => ((f a b c ) ⅋ (g a b c) ⅋ (h a b c))) par_assoc_r;assumption.
  - auto_step_ter (fun a b c => (((f a b c ) ⅋ (g a b c)) ⅋ (h a b c))) psep_PS5;assumption.
  Qed.

  Lemma psep_S : psep PS.
  Proof.
    auto_step_ter (fun a b c => b ⅋↦ a ⅋↦ c) swap_l.
    auto_step_ter (fun a b c => ((a ⅋↦ b) ⅋↦ a ⅋↦ a ⅋↦ c)) psep_PS4.
    step_mod_pon_ter (fun (a b c:X) => (a ⅋↦ a ⅋↦ c) ⅋↦ ( a ⅋↦ c)) psep_PS4.
    auto_step_ter (fun (a b c:X) => ((¬ a ) ⅋ (¬ a)) ⅋ c) psep_PS5.
    step_mod_pon_ter (fun (a b c:X) => ((¬ a) ⅋ (¬a)) ⅋↦ ¬a) psep_PS4_r.
    step psep_PS1.
  Qed.

Combinator cc


  Lemma psep_cc : psep Pcc.
  Proof.
  eapply psep_PC6 with (g:=fun a b => ((¬ a) ⅋↦ a ⅋↦ b) ⅋↦ (¬ a) ⅋↦ a);[step psep_PS4|].
  apply psep_PC6 with (g:=fun (a b:X) => ((¬ a) ⅋↦ a));[|step absurd_aux].
  apply half_pmodus_ponens.
  eapply psep_PC6 with (g:=fun (a b:X) => (a ⅋↦ ⊥));unfold PC6.
  step pneg_arrow. step psep_PI.
  apply parrow_mon;[reflexivity|];intuition.
  Qed.

  Lemma ImpK : (@K _ _ _ _ IS)= PK .
  Proof.
    intuition.
  Qed.
  Lemma ImpS : (@S _ _ _ _ IS) = PS .
  Proof.
    intuition.
  Qed.
  Lemma Impcc : (@cc _ _ _ _ IS) = Pcc.
  Proof.
    intuition.
  Qed.

  Lemma psep_ImpK : psep (@K _ _ _ _ IS).
  Proof.
    rewrite ImpK.
    apply psep_K.
  Qed.
  Lemma psep_ImpS : psep (@S _ _ _ _ IS).
  Proof.
    rewrite ImpS.
    apply psep_S.
  Qed.
  Lemma psep_Impcc : psep (@cc _ _ _ _ IS).
  Proof.
    rewrite Impcc.
    apply psep_cc.
  Qed.
End About_ParAlg.

 Global Instance PA_IA `{PA:ParAlgebra}:ImplicativeAlgebra:=
 {separator:=psep; modus_ponens:=modus_ponens_parrow;
  up_closed:= pup_closed; sep_K:=psep_ImpK; sep_S:=psep_ImpS;sep_cc:=psep_Impcc}.