Classical.Phase: phase semantics and soundness for CLL

        X^⊥ = { y | ∀ x ∈ X, x · y ∈ ⫫ }      the "counter-bags" of X

        Γ ⊨ Δ   iff   ⟦A₁⟧ ⊙ … ⊙ ⟦Aₙ⟧ ⊙ ⟦B₁⟧^⊥ ⊙ … ⊙ ⟦Bₘ⟧^⊥  ⊆  ⫫

From stdpp Require Export propset.
[Loading ML file rocq-runtime.plugins.ring ... done]
[Loading ML file rocq-runtime.plugins.zify ... done]
[Loading ML file rocq-runtime.plugins.micromega_core ... done]
[Loading ML file rocq-runtime.plugins.micromega ... done]
[Loading ML file rocq-runtime.plugins.ssrmatching ... done]
[Loading ML file rocq-runtime.plugins.ssreflect ... done]
[Loading ML file rocq-runtime.plugins.btauto ... done]
[Loading ML file rocq-runtime.plugins.nsatz_core ... done]
[Loading ML file rocq-runtime.plugins.nsatz ... done]
From LinearLogic.Classical Require Export Sequent.

Record cphase_space : Type := {
  ccarrier :> Type;
  cph_equiv : Equiv ccarrier;
  cph_op : ccarrier -> ccarrier -> ccarrier;
  cph_e  : ccarrier;
  cph_pole : propset ccarrier;
  cph_J  : propset ccarrier;

  cph_equivalence : Equivalence (@equiv _ cph_equiv);
  cph_op_proper : Proper (@equiv _ cph_equiv ==> @equiv _ cph_equiv ==>
                          @equiv _ cph_equiv) cph_op;
  cph_assoc  : ∀ x y z, @equiv _ cph_equiv (cph_op x (cph_op y z))
                                           (cph_op (cph_op x y) z);
  cph_comm   : ∀ x y, @equiv _ cph_equiv (cph_op x y) (cph_op y x);
  cph_unit_l : ∀ x, @equiv _ cph_equiv (cph_op cph_e x) x;

  cph_pole_proper : ∀ x y, @equiv _ cph_equiv x y -> x ∈ cph_pole -> y ∈ cph_pole;

  cph_J_proper : ∀ x y, @equiv _ cph_equiv x y -> x ∈ cph_J -> y ∈ cph_J;
  cph_J_unit   : cph_e ∈ cph_J;
  cph_J_op     : ∀ x y, x ∈ cph_J -> y ∈ cph_J -> cph_op x y ∈ cph_J;
  cph_J_weak   : ∀ j y, j ∈ cph_J -> y ∈ cph_pole -> cph_op j y ∈ cph_pole;
  cph_J_contr  : ∀ j y, j ∈ cph_J ->
      cph_op (cph_op j j) y ∈ cph_pole -> cph_op j y ∈ cph_pole;
}.

Arguments cph_op {_}. Arguments cph_e {_}. Arguments cph_pole {_}.
Arguments cph_J {_}. Arguments cph_assoc {_}. Arguments cph_comm {_}.
Arguments cph_unit_l {_}. Arguments cph_pole_proper {_}.
Arguments cph_J_proper {_}. Arguments cph_J_unit {_}. Arguments cph_J_op {_}.
Arguments cph_J_weak {_}. Arguments cph_J_contr {_}.

#[export] Existing Instance cph_equiv.
#[export] Instance cph_equivalence' (P : cphase_space) : Equivalence (≡@{P})
  := cph_equivalence P.
#[export] Instance cph_op_proper' (P : cphase_space)
  : Proper ((≡) ==> (≡) ==> (≡)) (@cph_op P) := cph_op_proper P.

Declare Scope cll_phase_scope.
Open Scope cll_phase_scope.

Notation "x · y" := (cph_op x y) (at level 40, left associativity)
  : cll_phase_scope.
Notation "⫫" := cph_pole : cll_phase_scope.

Section SetFormers.
  Context {P : cphase_space}.
  Implicit Types (X Y : propset P) (x y z : P).

  Definition one_set : propset P := {[ z | z ≡ cph_e ]}.
  Definition prod_set X Y : propset P := {[ z | ∃ a b, a ∈ X ∧ b ∈ Y ∧ z ≡ a · b ]}.
  Definition orth X : propset P := {[ y | ∀ x, x ∈ X -> x · y ∈ ⫫ ]}.
  Definition full_set : propset P := {[ _ | True ]}.

  Lemma elem_of_one z : z ∈ one_set ↔ z ≡ cph_e.
P: cphase_space
z: P
z ∈ one_set ↔ z ≡ cph_e
  Proof.
P: cphase_space
z: P
z ∈ one_set ↔ z ≡ cph_e unfold one_set.
P: cphase_space
z: P
z ∈ {[ z0 | z0 ≡ cph_e ]} ↔ z ≡ cph_e by rewrite elem_of_PropSet. Qed.
  Lemma elem_of_prod X Y z : z ∈ prod_set X Y ↔ ∃ a b, a ∈ X ∧ b ∈ Y ∧ z ≡ a · b.
P: cphase_space
X, Y: propset P
z: P
z ∈ prod_set X Y ↔ ∃ a b : P, a ∈ X ∧ b ∈ Y ∧ z ≡ a · b
  Proof.
P: cphase_space
X, Y: propset P
z: P
z ∈ prod_set X Y ↔ ∃ a b : P, a ∈ X ∧ b ∈ Y ∧ z ≡ a · b unfold prod_set.
P: cphase_space
X, Y: propset P
z: P
z ∈ {[ z0 | ∃ a b : P, a ∈ X ∧ b ∈ Y ∧ z0 ≡ a · b ]}
↔ ∃ a b : P, a ∈ X ∧ b ∈ Y ∧ z ≡ a · b by rewrite elem_of_PropSet. Qed.
  Lemma elem_of_orth X y : y ∈ orth X ↔ ∀ x, x ∈ X -> x · y ∈ ⫫.
P: cphase_space
X: propset P
y: P
y ∈ orth X ↔ ∀ x, x ∈ X → x · y ∈ ⫫
  Proof.
P: cphase_space
X: propset P
y: P
y ∈ orth X ↔ ∀ x, x ∈ X → x · y ∈ ⫫ unfold orth.
P: cphase_space
X: propset P
y: P
y ∈ {[ y0 | ∀ x, x ∈ X → x · y0 ∈ ⫫ ]} ↔ ∀ x, x ∈ X → x · y ∈ ⫫ by rewrite elem_of_PropSet. Qed.
  Lemma elem_of_full z : z ∈ full_set.
P: cphase_space
z: P
z ∈ full_set
  Proof.
P: cphase_space
z: P
z ∈ full_set unfold full_set.
P: cphase_space
z: P
z ∈ {[ _ | True ]} by rewrite elem_of_PropSet. Qed.
End SetFormers.

Infix "⊙" := prod_set (at level 40, left associativity) : cll_phase_scope.
Notation "X ^⊥" := (orth X) (at level 20, format "X ^⊥") : cll_phase_scope.

Section Orth.
  Context {P : cphase_space}.
  Implicit Types (X Y Z F R : propset P) (x y z : P).

  Lemma cph_unit_r x : x · cph_e ≡ x.
P: cphase_space
x: P
x · cph_e ≡ x
  Proof.
P: cphase_space
x: P
x · cph_e ≡ x rewrite cph_comm.
P: cphase_space
x: P
cph_e · x ≡ x apply cph_unit_l. Qed.

  Lemma orth_proper X y y' : y ≡ y' -> y ∈ X^⊥ -> y' ∈ X^⊥.
P: cphase_space
X: propset P
y, y': P
y ≡ y' → y ∈ X^⊥ → y' ∈ X^⊥
  Proof.
P: cphase_space
X: propset P
y, y': P
y ≡ y' → y ∈ X^⊥ → y' ∈ X^⊥
    rewrite !elem_of_orth.
P: cphase_space
X: propset P
y, y': P
y ≡ y' → (∀ x, x ∈ X → x · y ∈ ⫫) → ∀ x, x ∈ X → x · y' ∈ ⫫ intros Hy H x Hx.
P: cphase_space
X: propset P
y, y': P
Hy: y ≡ y'
H: ∀ x, x ∈ X → x · y ∈ ⫫
x: P
Hx: x ∈ X
x · y' ∈ ⫫
    apply (cph_pole_proper (x · y)); [by rewrite Hy | auto].
  Qed.

  Lemma orth_anti X Y : X ⊆ Y -> Y^⊥ ⊆ X^⊥.
P: cphase_space
X, Y: propset P
X ⊆ Y → Y^⊥ ⊆ X^⊥
  Proof.
P: cphase_space
X, Y: propset P
X ⊆ Y → Y^⊥ ⊆ X^⊥ intros H y.
P: cphase_space
X, Y: propset P
H: X ⊆ Y
y: P
y ∈ Y^⊥ → y ∈ X^⊥ rewrite !elem_of_orth.
P: cphase_space
X, Y: propset P
H: X ⊆ Y
y: P
(∀ x, x ∈ Y → x · y ∈ ⫫) → ∀ x, x ∈ X → x · y ∈ ⫫ naive_solver. Qed.

  Lemma biorth X : X ⊆ X^⊥^⊥.
P: cphase_space
X: propset P
X ⊆ (X^⊥)^⊥
  Proof.
P: cphase_space
X: propset P
X ⊆ (X^⊥)^⊥
    intros x Hx.
P: cphase_space
X: propset P
x: P
Hx: x ∈ X
x ∈ (X^⊥)^⊥ apply elem_of_orth.
P: cphase_space
X: propset P
x: P
Hx: x ∈ X
∀ x0, x0 ∈ X^⊥ → x0 · x ∈ ⫫ intros y Hy.
P: cphase_space
X: propset P
x: P
Hx: x ∈ X
y: P
Hy: y ∈ X^⊥
y · x ∈ ⫫ rewrite elem_of_orth in Hy.
P: cphase_space
X: propset P
x: P
Hx: x ∈ X
y: P
Hy: ∀ x, x ∈ X → x · y ∈ ⫫
y · x ∈ ⫫
    apply (cph_pole_proper (x · y)); [apply cph_comm | auto].
  Qed.

  Lemma triorth X : X^⊥^⊥^⊥ ⊆ X^⊥.
P: cphase_space
X: propset P
((X^⊥)^⊥)^⊥ ⊆ X^⊥
  Proof.
P: cphase_space
X: propset P
((X^⊥)^⊥)^⊥ ⊆ X^⊥ apply orth_anti, biorth. Qed.

  Lemma biorth_mono X Y : X ⊆ Y -> X^⊥^⊥ ⊆ Y^⊥^⊥.
P: cphase_space
X, Y: propset P
X ⊆ Y → (X^⊥)^⊥ ⊆ (Y^⊥)^⊥
  Proof.
P: cphase_space
X, Y: propset P
X ⊆ Y → (X^⊥)^⊥ ⊆ (Y^⊥)^⊥ intros H.
P: cphase_space
X, Y: propset P
H: X ⊆ Y
(X^⊥)^⊥ ⊆ (Y^⊥)^⊥ by apply orth_anti, orth_anti. Qed.

  Definition fact F : Prop := F^⊥^⊥ ⊆ F.

  Lemma fact_orth X : fact (X^⊥).
P: cphase_space
X: propset P
fact (X^⊥)
  Proof.
P: cphase_space
X: propset P
fact (X^⊥) apply triorth. Qed.

  Lemma fact_inter X Y : fact X -> fact Y -> fact (X ∩ Y).
P: cphase_space
X, Y: propset P
fact X → fact Y → fact (X ∩ Y)
  Proof.
P: cphase_space
X, Y: propset P
fact X → fact Y → fact (X ∩ Y)
    intros HX HY z Hz.
P: cphase_space
X, Y: propset P
HX: fact X
HY: fact Y
z: P
Hz: z ∈ ((X ∩ Y)^⊥)^⊥
z ∈ X ∩ Y apply elem_of_intersection.
P: cphase_space
X, Y: propset P
HX: fact X
HY: fact Y
z: P
Hz: z ∈ ((X ∩ Y)^⊥)^⊥
z ∈ X ∧ z ∈ Y
    split; [apply HX | apply HY]; revert z Hz; apply biorth_mono; set_solver.
  Qed.

  Lemma fact_full : fact full_set.
P: cphase_space
fact full_set
  Proof.
P: cphase_space
fact full_set intros z _.
P: cphase_space
z: P
z ∈ full_set apply elem_of_full. Qed.

  Lemma fact_proper F x y : fact F -> x ≡ y -> x ∈ F -> y ∈ F.
P: cphase_space
F: propset P
x, y: P
fact F → x ≡ y → x ∈ F → y ∈ F
  Proof.
P: cphase_space
F: propset P
x, y: P
fact F → x ≡ y → x ∈ F → y ∈ F intros HF Hxy Hx.
P: cphase_space
F: propset P
x, y: P
HF: fact F
Hxy: x ≡ y
Hx: x ∈ F
y ∈ F apply HF.
P: cphase_space
F: propset P
x, y: P
HF: fact F
Hxy: x ≡ y
Hx: x ∈ F
y ∈ (F^⊥)^⊥ apply (orth_proper _ x); [done | by apply biorth]. Qed.

  Lemma prod_pole X Y : X ⊙ Y ⊆ ⫫ ↔ Y ⊆ X^⊥.
P: cphase_space
X, Y: propset P
X ⊙ Y ⊆ ⫫ ↔ Y ⊆ X^⊥
  Proof.
P: cphase_space
X, Y: propset P
X ⊙ Y ⊆ ⫫ ↔ Y ⊆ X^⊥
    split.
P: cphase_space
X, Y: propset P
X ⊙ Y ⊆ ⫫ → Y ⊆ X^⊥
P: cphase_space
X, Y: propset P
Y ⊆ X^⊥ → X ⊙ Y ⊆ ⫫
    -
P: cphase_space
X, Y: propset P
X ⊙ Y ⊆ ⫫ → Y ⊆ X^⊥ intros H y Hy.
P: cphase_space
X, Y: propset P
H: X ⊙ Y ⊆ ⫫
y: P
Hy: y ∈ Y
y ∈ X^⊥ apply elem_of_orth.
P: cphase_space
X, Y: propset P
H: X ⊙ Y ⊆ ⫫
y: P
Hy: y ∈ Y
∀ x, x ∈ X → x · y ∈ ⫫ intros x Hx.
P: cphase_space
X, Y: propset P
H: X ⊙ Y ⊆ ⫫
y: P
Hy: y ∈ Y
x: P
Hx: x ∈ X
x · y ∈ ⫫ apply H, elem_of_prod.
P: cphase_space
X, Y: propset P
H: X ⊙ Y ⊆ ⫫
y: P
Hy: y ∈ Y
x: P
Hx: x ∈ X
∃ a b : P, a ∈ X ∧ b ∈ Y ∧ x · y ≡ a · b by exists x, y.
    -
P: cphase_space
X, Y: propset P
Y ⊆ X^⊥ → X ⊙ Y ⊆ ⫫ intros H z (a & b & Ha & Hb & Hz)%elem_of_prod.
P: cphase_space
X, Y: propset P
H: Y ⊆ X^⊥
z, a, b: P
Ha: a ∈ X
Hb: b ∈ Y
Hz: z ≡ a · b
z ∈ ⫫
      apply (cph_pole_proper (a · b)); [by symmetry |].
P: cphase_space
X, Y: propset P
H: Y ⊆ X^⊥
z, a, b: P
Ha: a ∈ X
Hb: b ∈ Y
Hz: z ≡ a · b
a · b ∈ ⫫
      specialize (H b Hb).
P: cphase_space
X, Y: propset P
b: P
H: b ∈ X^⊥
z, a: P
Ha: a ∈ X
Hb: b ∈ Y
Hz: z ≡ a · b
a · b ∈ ⫫ rewrite elem_of_orth in H.
P: cphase_space
X, Y: propset P
b: P
H: ∀ x, x ∈ X → x · b ∈ ⫫
z, a: P
Ha: a ∈ X
Hb: b ∈ Y
Hz: z ≡ a · b
a · b ∈ ⫫ auto.
  Qed.

  Lemma prod_mono X X' Y Y' : X ⊆ X' -> Y ⊆ Y' -> X ⊙ Y ⊆ X' ⊙ Y'.
P: cphase_space
X, X', Y, Y': propset P
X ⊆ X' → Y ⊆ Y' → X ⊙ Y ⊆ X' ⊙ Y'
  Proof.
P: cphase_space
X, X', Y, Y': propset P
X ⊆ X' → Y ⊆ Y' → X ⊙ Y ⊆ X' ⊙ Y'
    intros HX HY z (a & b & Ha & Hb & Hz)%elem_of_prod.
P: cphase_space
X, X', Y, Y': propset P
HX: X ⊆ X'
HY: Y ⊆ Y'
z, a, b: P
Ha: a ∈ X
Hb: b ∈ Y
Hz: z ≡ a · b
z ∈ X' ⊙ Y'
    apply elem_of_prod.
P: cphase_space
X, X', Y, Y': propset P
HX: X ⊆ X'
HY: Y ⊆ Y'
z, a, b: P
Ha: a ∈ X
Hb: b ∈ Y
Hz: z ≡ a · b
∃ a0 b0 : P, a0 ∈ X' ∧ b0 ∈ Y' ∧ z ≡ a0 · b0 exists a, b.
P: cphase_space
X, X', Y, Y': propset P
HX: X ⊆ X'
HY: Y ⊆ Y'
z, a, b: P
Ha: a ∈ X
Hb: b ∈ Y
Hz: z ≡ a · b
a ∈ X' ∧ b ∈ Y' ∧ z ≡ a · b auto.
  Qed.

  Lemma prod_assoc_l X Y Z : X ⊙ (Y ⊙ Z) ⊆ (X ⊙ Y) ⊙ Z.
P: cphase_space
X, Y, Z: propset P
X ⊙ (Y ⊙ Z) ⊆ X ⊙ Y ⊙ Z
  Proof.
P: cphase_space
X, Y, Z: propset P
X ⊙ (Y ⊙ Z) ⊆ X ⊙ Y ⊙ Z
    intros z (a & w & Ha & (b & c & Hb & Hc & Hw)%elem_of_prod & Hz)%elem_of_prod.
P: cphase_space
X, Y, Z: propset P
z, a, w: P
Ha: a ∈ X
b, c: P
Hb: b ∈ Y
Hc: c ∈ Z
Hw: w ≡ b · c
Hz: z ≡ a · w
z ∈ X ⊙ Y ⊙ Z
    apply elem_of_prod.
P: cphase_space
X, Y, Z: propset P
z, a, w: P
Ha: a ∈ X
b, c: P
Hb: b ∈ Y
Hc: c ∈ Z
Hw: w ≡ b · c
Hz: z ≡ a · w
∃ a0 b0 : P, a0 ∈ X ⊙ Y ∧ b0 ∈ Z ∧ z ≡ a0 · b0 exists (a · b), c.
P: cphase_space
X, Y, Z: propset P
z, a, w: P
Ha: a ∈ X
b, c: P
Hb: b ∈ Y
Hc: c ∈ Z
Hw: w ≡ b · c
Hz: z ≡ a · w
a · b ∈ X ⊙ Y ∧ c ∈ Z ∧ z ≡ a · b · c rewrite elem_of_prod.
P: cphase_space
X, Y, Z: propset P
z, a, w: P
Ha: a ∈ X
b, c: P
Hb: b ∈ Y
Hc: c ∈ Z
Hw: w ≡ b · c
Hz: z ≡ a · w
(∃ a0 b0 : P, a0 ∈ X ∧ b0 ∈ Y ∧ a · b ≡ a0 · b0) ∧ c ∈ Z ∧ z ≡ a · b · c split_and!; auto.
P: cphase_space
X, Y, Z: propset P
z, a, w: P
Ha: a ∈ X
b, c: P
Hb: b ∈ Y
Hc: c ∈ Z
Hw: w ≡ b · c
Hz: z ≡ a · w
∃ a0 b0 : P, a0 ∈ X ∧ b0 ∈ Y ∧ a · b ≡ a0 · b0
P: cphase_space
X, Y, Z: propset P
z, a, w: P
Ha: a ∈ X
b, c: P
Hb: b ∈ Y
Hc: c ∈ Z
Hw: w ≡ b · c
Hz: z ≡ a · w
z ≡ a · b · c
    -
P: cphase_space
X, Y, Z: propset P
z, a, w: P
Ha: a ∈ X
b, c: P
Hb: b ∈ Y
Hc: c ∈ Z
Hw: w ≡ b · c
Hz: z ≡ a · w
∃ a0 b0 : P, a0 ∈ X ∧ b0 ∈ Y ∧ a · b ≡ a0 · b0 by exists a, b.
    -
P: cphase_space
X, Y, Z: propset P
z, a, w: P
Ha: a ∈ X
b, c: P
Hb: b ∈ Y
Hc: c ∈ Z
Hw: w ≡ b · c
Hz: z ≡ a · w
z ≡ a · b · c rewrite Hz, Hw.
P: cphase_space
X, Y, Z: propset P
z, a, w: P
Ha: a ∈ X
b, c: P
Hb: b ∈ Y
Hc: c ∈ Z
Hw: w ≡ b · c
Hz: z ≡ a · w
a · (b · c) ≡ a · b · c apply cph_assoc.
  Qed.

  Lemma prod_assoc_r X Y Z : (X ⊙ Y) ⊙ Z ⊆ X ⊙ (Y ⊙ Z).
P: cphase_space
X, Y, Z: propset P
X ⊙ Y ⊙ Z ⊆ X ⊙ (Y ⊙ Z)
  Proof.
P: cphase_space
X, Y, Z: propset P
X ⊙ Y ⊙ Z ⊆ X ⊙ (Y ⊙ Z)
    intros z (w & c & (a & b & Ha & Hb & Hw)%elem_of_prod & Hc & Hz)%elem_of_prod.
P: cphase_space
X, Y, Z: propset P
z, w, c, a, b: P
Ha: a ∈ X
Hb: b ∈ Y
Hw: w ≡ a · b
Hc: c ∈ Z
Hz: z ≡ w · c
z ∈ X ⊙ (Y ⊙ Z)
    apply elem_of_prod.
P: cphase_space
X, Y, Z: propset P
z, w, c, a, b: P
Ha: a ∈ X
Hb: b ∈ Y
Hw: w ≡ a · b
Hc: c ∈ Z
Hz: z ≡ w · c
∃ a0 b0 : P, a0 ∈ X ∧ b0 ∈ Y ⊙ Z ∧ z ≡ a0 · b0 exists a, (b · c).
P: cphase_space
X, Y, Z: propset P
z, w, c, a, b: P
Ha: a ∈ X
Hb: b ∈ Y
Hw: w ≡ a · b
Hc: c ∈ Z
Hz: z ≡ w · c
a ∈ X ∧ b · c ∈ Y ⊙ Z ∧ z ≡ a · (b · c) rewrite elem_of_prod.
P: cphase_space
X, Y, Z: propset P
z, w, c, a, b: P
Ha: a ∈ X
Hb: b ∈ Y
Hw: w ≡ a · b
Hc: c ∈ Z
Hz: z ≡ w · c
a ∈ X ∧ (∃ a0 b0 : P, a0 ∈ Y ∧ b0 ∈ Z ∧ b · c ≡ a0 · b0) ∧ z ≡ a · (b · c) split_and!; auto.
P: cphase_space
X, Y, Z: propset P
z, w, c, a, b: P
Ha: a ∈ X
Hb: b ∈ Y
Hw: w ≡ a · b
Hc: c ∈ Z
Hz: z ≡ w · c
∃ a0 b0 : P, a0 ∈ Y ∧ b0 ∈ Z ∧ b · c ≡ a0 · b0
P: cphase_space
X, Y, Z: propset P
z, w, c, a, b: P
Ha: a ∈ X
Hb: b ∈ Y
Hw: w ≡ a · b
Hc: c ∈ Z
Hz: z ≡ w · c
z ≡ a · (b · c)
    -
P: cphase_space
X, Y, Z: propset P
z, w, c, a, b: P
Ha: a ∈ X
Hb: b ∈ Y
Hw: w ≡ a · b
Hc: c ∈ Z
Hz: z ≡ w · c
∃ a0 b0 : P, a0 ∈ Y ∧ b0 ∈ Z ∧ b · c ≡ a0 · b0 by exists b, c.
    -
P: cphase_space
X, Y, Z: propset P
z, w, c, a, b: P
Ha: a ∈ X
Hb: b ∈ Y
Hw: w ≡ a · b
Hc: c ∈ Z
Hz: z ≡ w · c
z ≡ a · (b · c) rewrite Hz, Hw.
P: cphase_space
X, Y, Z: propset P
z, w, c, a, b: P
Ha: a ∈ X
Hb: b ∈ Y
Hw: w ≡ a · b
Hc: c ∈ Z
Hz: z ≡ w · c
a · b · c ≡ a · (b · c) symmetry.
P: cphase_space
X, Y, Z: propset P
z, w, c, a, b: P
Ha: a ∈ X
Hb: b ∈ Y
Hw: w ≡ a · b
Hc: c ∈ Z
Hz: z ≡ w · c
a · (b · c) ≡ a · b · c apply cph_assoc.
  Qed.

  Lemma prod_comm X Y : X ⊙ Y ⊆ Y ⊙ X.
P: cphase_space
X, Y: propset P
X ⊙ Y ⊆ Y ⊙ X
  Proof.
P: cphase_space
X, Y: propset P
X ⊙ Y ⊆ Y ⊙ X
    intros z (a & b & Ha & Hb & Hz)%elem_of_prod.
P: cphase_space
X, Y: propset P
z, a, b: P
Ha: a ∈ X
Hb: b ∈ Y
Hz: z ≡ a · b
z ∈ Y ⊙ X apply elem_of_prod.
P: cphase_space
X, Y: propset P
z, a, b: P
Ha: a ∈ X
Hb: b ∈ Y
Hz: z ≡ a · b
∃ a0 b0 : P, a0 ∈ Y ∧ b0 ∈ X ∧ z ≡ a0 · b0
    exists b, a.
P: cphase_space
X, Y: propset P
z, a, b: P
Ha: a ∈ X
Hb: b ∈ Y
Hz: z ≡ a · b
b ∈ Y ∧ a ∈ X ∧ z ≡ b · a split_and!; auto.
P: cphase_space
X, Y: propset P
z, a, b: P
Ha: a ∈ X
Hb: b ∈ Y
Hz: z ≡ a · b
z ≡ b · a by rewrite Hz, cph_comm.
  Qed.

  Lemma prod_one_r F : fact F -> F ⊙ one_set ⊆ F.
P: cphase_space
F: propset P
fact F → F ⊙ one_set ⊆ F
  Proof.
P: cphase_space
F: propset P
fact F → F ⊙ one_set ⊆ F
    intros HF z (a & b & Ha & Hb%elem_of_one & Hz)%elem_of_prod.
P: cphase_space
F: propset P
HF: fact F
z, a, b: P
Ha: a ∈ F
Hb: b ≡ cph_e
Hz: z ≡ a · b
z ∈ F
    apply (fact_proper _ a); [done | | done].
P: cphase_space
F: propset P
HF: fact F
z, a, b: P
Ha: a ∈ F
Hb: b ≡ cph_e
Hz: z ≡ a · b
a ≡ z by rewrite Hz, Hb, cph_unit_r.
  Qed.

  Lemma prod_one_l X : X ⊆ one_set ⊙ X.
P: cphase_space
X: propset P
X ⊆ one_set ⊙ X
  Proof.
P: cphase_space
X: propset P
X ⊆ one_set ⊙ X
    intros x Hx.
P: cphase_space
X: propset P
x: P
Hx: x ∈ X
x ∈ one_set ⊙ X apply elem_of_prod.
P: cphase_space
X: propset P
x: P
Hx: x ∈ X
∃ a b : P, a ∈ one_set ∧ b ∈ X ∧ x ≡ a · b exists cph_e, x.
P: cphase_space
X: propset P
x: P
Hx: x ∈ X
cph_e ∈ one_set ∧ x ∈ X ∧ x ≡ cph_e · x
    rewrite elem_of_one, cph_unit_l.
P: cphase_space
X: propset P
x: P
Hx: x ∈ X
cph_e ≡ cph_e ∧ x ∈ X ∧ x ≡ x done.
  Qed.

  Lemma stability X Y : X^⊥^⊥ ⊙ Y^⊥^⊥ ⊆ (X ⊙ Y)^⊥^⊥.
P: cphase_space
X, Y: propset P
(X^⊥)^⊥ ⊙ (Y^⊥)^⊥ ⊆ ((X ⊙ Y)^⊥)^⊥
  Proof.
P: cphase_space
X, Y: propset P
(X^⊥)^⊥ ⊙ (Y^⊥)^⊥ ⊆ ((X ⊙ Y)^⊥)^⊥
    intros z (a & b & Ha & Hb & Hz)%elem_of_prod.
P: cphase_space
X, Y: propset P
z, a, b: P
Ha: a ∈ (X^⊥)^⊥
Hb: b ∈ (Y^⊥)^⊥
Hz: z ≡ a · b
z ∈ ((X ⊙ Y)^⊥)^⊥ apply elem_of_orth.
P: cphase_space
X, Y: propset P
z, a, b: P
Ha: a ∈ (X^⊥)^⊥
Hb: b ∈ (Y^⊥)^⊥
Hz: z ≡ a · b
∀ x, x ∈ (X ⊙ Y)^⊥ → x · z ∈ ⫫
    intros w Hw.
P: cphase_space
X, Y: propset P
z, a, b: P
Ha: a ∈ (X^⊥)^⊥
Hb: b ∈ (Y^⊥)^⊥
Hz: z ≡ a · b
w: P
Hw: w ∈ (X ⊙ Y)^⊥
w · z ∈ ⫫ rewrite elem_of_orth in Hw.
P: cphase_space
X, Y: propset P
z, a, b: P
Ha: a ∈ (X^⊥)^⊥
Hb: b ∈ (Y^⊥)^⊥
Hz: z ≡ a · b
w: P
Hw: ∀ x, x ∈ X ⊙ Y → x · w ∈ ⫫
w · z ∈ ⫫
    (* first: for y ∈ Y, y · w is a counter-bag of X *)
    assert (H1 : ∀ y, y ∈ Y -> y · w ∈ X^⊥).
P: cphase_space
X, Y: propset P
z, a, b: P
Ha: a ∈ (X^⊥)^⊥
Hb: b ∈ (Y^⊥)^⊥
Hz: z ≡ a · b
w: P
Hw: ∀ x, x ∈ X ⊙ Y → x · w ∈ ⫫
∀ y, y ∈ Y → y · w ∈ X^⊥
P: cphase_space
X, Y: propset P
z, a, b: P
Ha: a ∈ (X^⊥)^⊥
Hb: b ∈ (Y^⊥)^⊥
Hz: z ≡ a · b
w: P
Hw: ∀ x, x ∈ X ⊙ Y → x · w ∈ ⫫
H1: ∀ y, y ∈ Y → y · w ∈ X^⊥
w · z ∈ ⫫
    {
P: cphase_space
X, Y: propset P
z, a, b: P
Ha: a ∈ (X^⊥)^⊥
Hb: b ∈ (Y^⊥)^⊥
Hz: z ≡ a · b
w: P
Hw: ∀ x, x ∈ X ⊙ Y → x · w ∈ ⫫
∀ y, y ∈ Y → y · w ∈ X^⊥ intros y Hy.
P: cphase_space
X, Y: propset P
z, a, b: P
Ha: a ∈ (X^⊥)^⊥
Hb: b ∈ (Y^⊥)^⊥
Hz: z ≡ a · b
w: P
Hw: ∀ x, x ∈ X ⊙ Y → x · w ∈ ⫫
y: P
Hy: y ∈ Y
y · w ∈ X^⊥ apply elem_of_orth.
P: cphase_space
X, Y: propset P
z, a, b: P
Ha: a ∈ (X^⊥)^⊥
Hb: b ∈ (Y^⊥)^⊥
Hz: z ≡ a · b
w: P
Hw: ∀ x, x ∈ X ⊙ Y → x · w ∈ ⫫
y: P
Hy: y ∈ Y
∀ x, x ∈ X → x · (y · w) ∈ ⫫ intros x Hx.
P: cphase_space
X, Y: propset P
z, a, b: P
Ha: a ∈ (X^⊥)^⊥
Hb: b ∈ (Y^⊥)^⊥
Hz: z ≡ a · b
w: P
Hw: ∀ x, x ∈ X ⊙ Y → x · w ∈ ⫫
y: P
Hy: y ∈ Y
x: P
Hx: x ∈ X
x · (y · w) ∈ ⫫
      apply (cph_pole_proper ((x · y) · w)); [symmetry; apply cph_assoc |].
P: cphase_space
X, Y: propset P
z, a, b: P
Ha: a ∈ (X^⊥)^⊥
Hb: b ∈ (Y^⊥)^⊥
Hz: z ≡ a · b
w: P
Hw: ∀ x, x ∈ X ⊙ Y → x · w ∈ ⫫
y: P
Hy: y ∈ Y
x: P
Hx: x ∈ X
x · y · w ∈ ⫫
      apply Hw, elem_of_prod.
P: cphase_space
X, Y: propset P
z, a, b: P
Ha: a ∈ (X^⊥)^⊥
Hb: b ∈ (Y^⊥)^⊥
Hz: z ≡ a · b
w: P
Hw: ∀ x, x ∈ X ⊙ Y → x · w ∈ ⫫
y: P
Hy: y ∈ Y
x: P
Hx: x ∈ X
∃ a0 b0 : P, a0 ∈ X ∧ b0 ∈ Y ∧ x · y ≡ a0 · b0 by exists x, y. }
P: cphase_space
X, Y: propset P
z, a, b: P
Ha: a ∈ (X^⊥)^⊥
Hb: b ∈ (Y^⊥)^⊥
Hz: z ≡ a · b
w: P
Hw: ∀ x, x ∈ X ⊙ Y → x · w ∈ ⫫
H1: ∀ y, y ∈ Y → y · w ∈ X^⊥
w · z ∈ ⫫
    (* then: w · a is a counter-bag of Y *)
    assert (H2 : w · a ∈ Y^⊥).
P: cphase_space
X, Y: propset P
z, a, b: P
Ha: a ∈ (X^⊥)^⊥
Hb: b ∈ (Y^⊥)^⊥
Hz: z ≡ a · b
w: P
Hw: ∀ x, x ∈ X ⊙ Y → x · w ∈ ⫫
H1: ∀ y, y ∈ Y → y · w ∈ X^⊥
w · a ∈ Y^⊥
P: cphase_space
X, Y: propset P
z, a, b: P
Ha: a ∈ (X^⊥)^⊥
Hb: b ∈ (Y^⊥)^⊥
Hz: z ≡ a · b
w: P
Hw: ∀ x, x ∈ X ⊙ Y → x · w ∈ ⫫
H1: ∀ y, y ∈ Y → y · w ∈ X^⊥
H2: w · a ∈ Y^⊥
w · z ∈ ⫫
    {
P: cphase_space
X, Y: propset P
z, a, b: P
Ha: a ∈ (X^⊥)^⊥
Hb: b ∈ (Y^⊥)^⊥
Hz: z ≡ a · b
w: P
Hw: ∀ x, x ∈ X ⊙ Y → x · w ∈ ⫫
H1: ∀ y, y ∈ Y → y · w ∈ X^⊥
w · a ∈ Y^⊥ apply elem_of_orth.
P: cphase_space
X, Y: propset P
z, a, b: P
Ha: a ∈ (X^⊥)^⊥
Hb: b ∈ (Y^⊥)^⊥
Hz: z ≡ a · b
w: P
Hw: ∀ x, x ∈ X ⊙ Y → x · w ∈ ⫫
H1: ∀ y, y ∈ Y → y · w ∈ X^⊥
∀ x, x ∈ Y → x · (w · a) ∈ ⫫ intros y Hy.
P: cphase_space
X, Y: propset P
z, a, b: P
Ha: a ∈ (X^⊥)^⊥
Hb: b ∈ (Y^⊥)^⊥
Hz: z ≡ a · b
w: P
Hw: ∀ x, x ∈ X ⊙ Y → x · w ∈ ⫫
H1: ∀ y, y ∈ Y → y · w ∈ X^⊥
y: P
Hy: y ∈ Y
y · (w · a) ∈ ⫫
      rewrite elem_of_orth in Ha.
P: cphase_space
X, Y: propset P
z, a, b: P
Ha: ∀ x, x ∈ X^⊥ → x · a ∈ ⫫
Hb: b ∈ (Y^⊥)^⊥
Hz: z ≡ a · b
w: P
Hw: ∀ x, x ∈ X ⊙ Y → x · w ∈ ⫫
H1: ∀ y, y ∈ Y → y · w ∈ X^⊥
y: P
Hy: y ∈ Y
y · (w · a) ∈ ⫫ specialize (Ha _ (H1 y Hy)).
P: cphase_space
X, Y: propset P
z, a, b, w, y: P
Ha: y · w · a ∈ ⫫
Hb: b ∈ (Y^⊥)^⊥
Hz: z ≡ a · b
Hw: ∀ x, x ∈ X ⊙ Y → x · w ∈ ⫫
H1: ∀ y, y ∈ Y → y · w ∈ X^⊥
Hy: y ∈ Y
y · (w · a) ∈ ⫫
      apply (cph_pole_proper ((y · w) · a)); [symmetry; apply cph_assoc | done]. }
P: cphase_space
X, Y: propset P
z, a, b: P
Ha: a ∈ (X^⊥)^⊥
Hb: b ∈ (Y^⊥)^⊥
Hz: z ≡ a · b
w: P
Hw: ∀ x, x ∈ X ⊙ Y → x · w ∈ ⫫
H1: ∀ y, y ∈ Y → y · w ∈ X^⊥
H2: w · a ∈ Y^⊥
w · z ∈ ⫫
    rewrite elem_of_orth in Hb.
P: cphase_space
X, Y: propset P
z, a, b: P
Ha: a ∈ (X^⊥)^⊥
Hb: ∀ x, x ∈ Y^⊥ → x · b ∈ ⫫
Hz: z ≡ a · b
w: P
Hw: ∀ x, x ∈ X ⊙ Y → x · w ∈ ⫫
H1: ∀ y, y ∈ Y → y · w ∈ X^⊥
H2: w · a ∈ Y^⊥
w · z ∈ ⫫ specialize (Hb _ H2).
P: cphase_space
X, Y: propset P
z, a, b: P
Ha: a ∈ (X^⊥)^⊥
w: P
Hb: w · a · b ∈ ⫫
Hz: z ≡ a · b
Hw: ∀ x, x ∈ X ⊙ Y → x · w ∈ ⫫
H1: ∀ y, y ∈ Y → y · w ∈ X^⊥
H2: w · a ∈ Y^⊥
w · z ∈ ⫫
    apply (cph_pole_proper ((w · a) · b)); [| done].
P: cphase_space
X, Y: propset P
z, a, b: P
Ha: a ∈ (X^⊥)^⊥
w: P
Hb: w · a · b ∈ ⫫
Hz: z ≡ a · b
Hw: ∀ x, x ∈ X ⊙ Y → x · w ∈ ⫫
H1: ∀ y, y ∈ Y → y · w ∈ X^⊥
H2: w · a ∈ Y^⊥
w · a · b ≡ w · z
    rewrite Hz.
P: cphase_space
X, Y: propset P
z, a, b: P
Ha: a ∈ (X^⊥)^⊥
w: P
Hb: w · a · b ∈ ⫫
Hz: z ≡ a · b
Hw: ∀ x, x ∈ X ⊙ Y → x · w ∈ ⫫
H1: ∀ y, y ∈ Y → y · w ∈ X^⊥
H2: w · a ∈ Y^⊥
w · a · b ≡ w · (a · b) symmetry.
P: cphase_space
X, Y: propset P
z, a, b: P
Ha: a ∈ (X^⊥)^⊥
w: P
Hb: w · a · b ∈ ⫫
Hz: z ≡ a · b
Hw: ∀ x, x ∈ X ⊙ Y → x · w ∈ ⫫
H1: ∀ y, y ∈ Y → y · w ∈ X^⊥
H2: w · a ∈ Y^⊥
w · (a · b) ≡ w · a · b apply cph_assoc.
  Qed.

  Lemma orth_union X Y : X^⊥ ∩ Y^⊥ ⊆ (X ∪ Y)^⊥.
P: cphase_space
X, Y: propset P
X^⊥ ∩ Y^⊥ ⊆ (X ∪ Y)^⊥
  Proof.
P: cphase_space
X, Y: propset P
X^⊥ ∩ Y^⊥ ⊆ (X ∪ Y)^⊥
    intros z [HX HY]%elem_of_intersection.
P: cphase_space
X, Y: propset P
z: P
HX: z ∈ X^⊥
HY: z ∈ Y^⊥
z ∈ (X ∪ Y)^⊥ rewrite elem_of_orth in HX, HY.
P: cphase_space
X, Y: propset P
z: P
HX: ∀ x, x ∈ X → x · z ∈ ⫫
HY: ∀ x, x ∈ Y → x · z ∈ ⫫
z ∈ (X ∪ Y)^⊥
    apply elem_of_orth.
P: cphase_space
X, Y: propset P
z: P
HX: ∀ x, x ∈ X → x · z ∈ ⫫
HY: ∀ x, x ∈ Y → x · z ∈ ⫫
∀ x, x ∈ X ∪ Y → x · z ∈ ⫫ intros x [Hx | Hx]%elem_of_union; auto.
  Qed.

  Lemma pole_orth_one R : R ⊆ ⫫ -> R ⊆ one_set^⊥.
P: cphase_space
R: propset P
R ⊆ ⫫ → R ⊆ one_set^⊥
  Proof.
P: cphase_space
R: propset P
R ⊆ ⫫ → R ⊆ one_set^⊥
    intros H r Hr.
P: cphase_space
R: propset P
H: R ⊆ ⫫
r: P
Hr: r ∈ R
r ∈ one_set^⊥ apply elem_of_orth.
P: cphase_space
R: propset P
H: R ⊆ ⫫
r: P
Hr: r ∈ R
∀ x, x ∈ one_set → x · r ∈ ⫫ intros x Hx%elem_of_one.
P: cphase_space
R: propset P
H: R ⊆ ⫫
r: P
Hr: r ∈ R
x: P
Hx: x ≡ cph_e
x · r ∈ ⫫
    apply (cph_pole_proper r); [by rewrite Hx, cph_unit_l | auto].
  Qed.

  Lemma cut_pole R1 R2 X : R1 ⊆ X -> R2 ⊆ X^⊥ -> R1 ⊙ R2 ⊆ ⫫.
P: cphase_space
R1, R2, X: propset P
R1 ⊆ X → R2 ⊆ X^⊥ → R1 ⊙ R2 ⊆ ⫫
  Proof.
P: cphase_space
R1, R2, X: propset P
R1 ⊆ X → R2 ⊆ X^⊥ → R1 ⊙ R2 ⊆ ⫫
    intros H1 H2.
P: cphase_space
R1, R2, X: propset P
H1: R1 ⊆ X
H2: R2 ⊆ X^⊥
R1 ⊙ R2 ⊆ ⫫ etransitivity; [by apply prod_mono |].
P: cphase_space
R1, R2, X: propset P
H1: R1 ⊆ X
H2: R2 ⊆ X^⊥
X ⊙ X^⊥ ⊆ ⫫ by apply prod_pole.
  Qed.

  Lemma weak_orth R X : R ⊆ ⫫ -> R ⊆ (X ∩ cph_J)^⊥.
P: cphase_space
R, X: propset P
R ⊆ ⫫ → R ⊆ (X ∩ cph_J)^⊥
  Proof.
P: cphase_space
R, X: propset P
R ⊆ ⫫ → R ⊆ (X ∩ cph_J)^⊥
    intros H r Hr.
P: cphase_space
R, X: propset P
H: R ⊆ ⫫
r: P
Hr: r ∈ R
r ∈ (X ∩ cph_J)^⊥ apply elem_of_orth.
P: cphase_space
R, X: propset P
H: R ⊆ ⫫
r: P
Hr: r ∈ R
∀ x, x ∈ X ∩ cph_J → x · r ∈ ⫫ intros j [_ Hj]%elem_of_intersection.
P: cphase_space
R, X: propset P
H: R ⊆ ⫫
r: P
Hr: r ∈ R
j: P
Hj: j ∈ cph_J
j · r ∈ ⫫
    by apply cph_J_weak, H.
  Qed.

  Lemma contr_orth R X :
    R ⊆ ((X ∩ cph_J)^⊥^⊥ ⊙ (X ∩ cph_J)^⊥^⊥)^⊥ -> R ⊆ (X ∩ cph_J)^⊥.
P: cphase_space
R, X: propset P
R ⊆ (((X ∩ cph_J)^⊥)^⊥ ⊙ ((X ∩ cph_J)^⊥)^⊥)^⊥ → R ⊆ (X ∩ cph_J)^⊥
  Proof.
P: cphase_space
R, X: propset P
R ⊆ (((X ∩ cph_J)^⊥)^⊥ ⊙ ((X ∩ cph_J)^⊥)^⊥)^⊥ → R ⊆ (X ∩ cph_J)^⊥
    intros H r Hr.
P: cphase_space
R, X: propset P
H: R ⊆ (((X ∩ cph_J)^⊥)^⊥ ⊙ ((X ∩ cph_J)^⊥)^⊥)^⊥
r: P
Hr: r ∈ R
r ∈ (X ∩ cph_J)^⊥ apply elem_of_orth.
P: cphase_space
R, X: propset P
H: R ⊆ (((X ∩ cph_J)^⊥)^⊥ ⊙ ((X ∩ cph_J)^⊥)^⊥)^⊥
r: P
Hr: r ∈ R
∀ x, x ∈ X ∩ cph_J → x · r ∈ ⫫ intros j Hj.
P: cphase_space
R, X: propset P
H: R ⊆ (((X ∩ cph_J)^⊥)^⊥ ⊙ ((X ∩ cph_J)^⊥)^⊥)^⊥
r: P
Hr: r ∈ R
j: P
Hj: j ∈ X ∩ cph_J
j · r ∈ ⫫
    pose proof Hj as [_ HJ]%elem_of_intersection.
P: cphase_space
R, X: propset P
H: R ⊆ (((X ∩ cph_J)^⊥)^⊥ ⊙ ((X ∩ cph_J)^⊥)^⊥)^⊥
r: P
Hr: r ∈ R
j: P
Hj: j ∈ X ∩ cph_J
HJ: j ∈ cph_J
j · r ∈ ⫫
    apply cph_J_contr; [done |].
P: cphase_space
R, X: propset P
H: R ⊆ (((X ∩ cph_J)^⊥)^⊥ ⊙ ((X ∩ cph_J)^⊥)^⊥)^⊥
r: P
Hr: r ∈ R
j: P
Hj: j ∈ X ∩ cph_J
HJ: j ∈ cph_J
j · j · r ∈ ⫫
    specialize (H r Hr).
P: cphase_space
R, X: propset P
r: P
H: r ∈ (((X ∩ cph_J)^⊥)^⊥ ⊙ ((X ∩ cph_J)^⊥)^⊥)^⊥
Hr: r ∈ R
j: P
Hj: j ∈ X ∩ cph_J
HJ: j ∈ cph_J
j · j · r ∈ ⫫ rewrite elem_of_orth in H.
P: cphase_space
R, X: propset P
r: P
H: ∀ x, x ∈ ((X ∩ cph_J)^⊥)^⊥ ⊙ ((X ∩ cph_J)^⊥)^⊥ → x · r ∈ ⫫
Hr: r ∈ R
j: P
Hj: j ∈ X ∩ cph_J
HJ: j ∈ cph_J
j · j · r ∈ ⫫ apply H, elem_of_prod.
P: cphase_space
R, X: propset P
r: P
H: ∀ x, x ∈ ((X ∩ cph_J)^⊥)^⊥ ⊙ ((X ∩ cph_J)^⊥)^⊥ → x · r ∈ ⫫
Hr: r ∈ R
j: P
Hj: j ∈ X ∩ cph_J
HJ: j ∈ cph_J
∃ a b : P, a ∈ ((X ∩ cph_J)^⊥)^⊥ ∧ b ∈ ((X ∩ cph_J)^⊥)^⊥ ∧ j · j ≡ a · b
    exists j, j.
P: cphase_space
R, X: propset P
r: P
H: ∀ x, x ∈ ((X ∩ cph_J)^⊥)^⊥ ⊙ ((X ∩ cph_J)^⊥)^⊥ → x · r ∈ ⫫
Hr: r ∈ R
j: P
Hj: j ∈ X ∩ cph_J
HJ: j ∈ cph_J
j ∈ ((X ∩ cph_J)^⊥)^⊥ ∧ j ∈ ((X ∩ cph_J)^⊥)^⊥ ∧ j · j ≡ j · j split_and!; [by apply biorth | by apply biorth | done].
  Qed.