Intuitionistic.Phase: phase semantics and soundness for ILL

Truth tables explain classical logic and Kripke models explain intuitionistic logic. Phase semantics (Girard 1987) plays the same role for linear logic, and its intuition is short:

a phase is an element of a commutative monoid (M, ·, ε). Think of it as a bag of resources, with · putting two bags together;
a formula denotes a set of phases: the bags of resources that are enough to produce it;
a sequent A₁, …, Aₙ ⊢ C is valid when combining one bag from each Aᵢ always gives a bag in C.

· need not be idempotent, so m · m can differ from m. That is how the semantics refuses to duplicate resources.

The connectives ⊗, ⊕, 𝟙, 𝟘, ! require sets to be closed under a closure operator cl. Closed sets are called facts. In the intuitionistic semantics, cl is any closure operator that is stable under ·, and ⊥ is just some fact. The classical semantics (Classical/Phase.v) is the special case cl X = X^⊥⊥, in which ⊥ determines everything else.

This file contains:

phase spaces, with sets taken from stdpp's propset;
the interpretation of formulas and sequents;
soundness: Γ ⊢[c] C → Γ ⊨ C;
countermodels: ILL has neither contraction nor weakening.

Intuitionistic/CutElim.v proves the converse and uses it to eliminate cuts.

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.Intuitionistic Require Export Sequent.

Phase spaces

Before the record we define the pointwise product of two sets, for any monoid operation op and equivalence eq: X ⊙ Y = { z | z ≡ x · y for some x ∈ X, y ∈ Y }. The stability axiom of the record uses it.

Definition prod_with {M} (eq : relation M) (op : M -> M -> M) (X Y : propset M)
  : propset M := {[ z | ∃ a b, a ∈ X ∧ b ∈ Y ∧ eq z (op a b) ]}.

An intuitionistic phase space has four components:

a commutative monoid (M, ·, ε), commutative only up to an equivalence ≡. The syntactic model of CutElim.v uses lists up to permutation, so equality would be too strict. We use stdpp's Equiv class and Proper instances, so rewrite works under ≡;
a closure operator cl on propset M that is stable: cl X ⊙ cl Y ⊆ cl (X ⊙ Y);
a set J of reusable phases. J contains ε and is closed under ·, and each j ∈ J can be discarded (j ∈ cl {ε}) and duplicated (j ∈ cl {j · j}). J is the semantic shadow of !;
a set ph_bot. Its closure interprets the constant ⊥.

Record phase_space : Type := {
  carrier :> Type;
  ph_equiv : Equiv carrier;
  ph_op : carrier -> carrier -> carrier;
  ph_e  : carrier;
  ph_cl : propset carrier -> propset carrier;
  ph_J  : propset carrier;
  ph_bot : propset carrier;

  (* (M, ·, ε) is a commutative monoid up to ≡ *)
  ph_equivalence : Equivalence (@equiv _ ph_equiv);
  ph_op_proper : Proper (@equiv _ ph_equiv ==> @equiv _ ph_equiv ==> @equiv _ ph_equiv) ph_op;
  ph_assoc  : ∀ x y z, @equiv _ ph_equiv (ph_op x (ph_op y z)) (ph_op (ph_op x y) z);
  ph_comm   : ∀ x y, @equiv _ ph_equiv (ph_op x y) (ph_op y x);
  ph_unit_l : ∀ x, @equiv _ ph_equiv (ph_op ph_e x) x;

  (* cl is a closure operator: extensive, and monotone + idempotent
     (packed into ph_cl_least); it respects ≡ and is stable under · *)
  ph_cl_ext    : ∀ X, X ⊆ ph_cl X;
  ph_cl_least  : ∀ X Y, X ⊆ ph_cl Y -> ph_cl X ⊆ ph_cl Y;
  ph_cl_proper : ∀ X x y, @equiv _ ph_equiv x y -> x ∈ ph_cl X -> y ∈ ph_cl X;
  ph_cl_stable : ∀ X Y x y, x ∈ ph_cl X -> y ∈ ph_cl Y ->
      ph_op x y ∈ ph_cl (prod_with (@equiv _ ph_equiv) ph_op X Y);

  (* J: the reusable phases *)
  ph_J_proper : ∀ x y, @equiv _ ph_equiv x y -> x ∈ ph_J -> y ∈ ph_J;
  ph_J_unit   : ph_e ∈ ph_J;
  ph_J_op     : ∀ x y, x ∈ ph_J -> y ∈ ph_J -> ph_op x y ∈ ph_J;
  ph_J_weak   : ∀ x, x ∈ ph_J -> x ∈ ph_cl {[ z | @equiv _ ph_equiv z ph_e ]};
  ph_J_contr  : ∀ x, x ∈ ph_J -> x ∈ ph_cl {[ z | @equiv _ ph_equiv z (ph_op x x) ]};
}.

Arguments ph_op {_}. Arguments ph_e {_}. Arguments ph_cl {_}.
Arguments ph_J {_}. Arguments ph_bot {_}.
Arguments ph_assoc {_}. Arguments ph_comm {_}. Arguments ph_unit_l {_}.
Arguments ph_cl_ext {_}. Arguments ph_cl_least {_}. Arguments ph_cl_proper {_}.
Arguments ph_cl_stable {_}. Arguments ph_J_proper {_}. Arguments ph_J_unit {_}.
Arguments ph_J_op {_}. Arguments ph_J_weak {_}. Arguments ph_J_contr {_}.

#[export] Existing Instance ph_equiv.
#[export] Instance ph_equivalence' (P : phase_space) : Equivalence (≡@{P})
  := ph_equivalence P.
#[export] Instance ph_op_proper' (P : phase_space)
  : Proper ((≡) ==> (≡) ==> (≡)) (@ph_op P) := ph_op_proper P.

Notations

Declare Scope ill_phase_scope.
Open Scope ill_phase_scope.

Notation "x · y" := (ph_op x y) (at level 40, left associativity)
  : ill_phase_scope.
Notation ε := ph_e.
Notation cl := ph_cl.
Notation J := ph_J.

{ε} up to ≡, and the pointwise product X ⊙ Y = { z | z ≡ x · y, x ∈ X, y ∈ Y }.

Definition one_set {P : phase_space} : propset P := {[ z | z ≡ ε ]}.
Definition prod_set {P : phase_space} (X Y : propset P) : propset P :=
  prod_with (≡) ph_op X Y.
Infix "⊙" := prod_set (at level 40, left associativity) : ill_phase_scope.

stdpp keeps propset membership opaque. Each set former therefore comes with an elem_of_… lemma, and with a SetUnfoldElemOf instance so that stdpp's set_unfold and set_solver can see through it.

Section elem_of.
  Context {P : phase_space}.
  Implicit Types (X Y : propset P) (z : P).

  Lemma elem_of_one z : z ∈ one_set ↔ z ≡ ε.P: phase_space
z: P
z ∈ one_set ↔ z ≡ ε
  Proof.P: phase_space
z: P
z ∈ one_set ↔ z ≡ ε unfold one_set.P: phase_space
z: P
z ∈ {[ z0 | z0 ≡ ε ]} ↔ z ≡ ε by rewrite elem_of_PropSet. Qed.
  Lemma elem_of_prod X Y z : z ∈ X ⊙ Y ↔ ∃ a b, a ∈ X ∧ b ∈ Y ∧ z ≡ a · b.P: phase_space
X, Y: propset P
z: P
z ∈ X ⊙ Y ↔ ∃ a b : P, a ∈ X ∧ b ∈ Y ∧ z ≡ a · b
  Proof.P: phase_space
X, Y: propset P
z: P
z ∈ X ⊙ Y ↔ ∃ a b : P, a ∈ X ∧ b ∈ Y ∧ z ≡ a · b unfold prod_set, prod_with.P: phase_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.

  #[global] Instance set_unfold_one z : SetUnfoldElemOf z one_set (z ≡ ε).P: phase_space
z: P
SetUnfoldElemOf z one_set (z ≡ ε)
  Proof.P: phase_space
z: P
SetUnfoldElemOf z one_set (z ≡ ε) constructor.P: phase_space
z: P
z ∈ one_set ↔ z ≡ ε apply elem_of_one. Qed.
  #[global] Instance set_unfold_prod X Y z (Q R : P -> Prop) :
    (∀ a, SetUnfoldElemOf a X (Q a)) -> (∀ b, SetUnfoldElemOf b Y (R b)) ->
    SetUnfoldElemOf z (X ⊙ Y) (∃ a b, Q a ∧ R b ∧ z ≡ a · b).P: phase_space
X, Y: propset P
z: P
Q, R: P → Prop
(∀ a : P, SetUnfoldElemOf a X (Q a))
→ (∀ b : P, SetUnfoldElemOf b Y (R b))
  → SetUnfoldElemOf z (X ⊙ Y) (∃ a b : P, Q a ∧ R b ∧ z ≡ a · b)
  Proof.P: phase_space
X, Y: propset P
z: P
Q, R: P → Prop
(∀ a : P, SetUnfoldElemOf a X (Q a))
→ (∀ b : P, SetUnfoldElemOf b Y (R b))
  → SetUnfoldElemOf z (X ⊙ Y) (∃ a b : P, Q a ∧ R b ∧ z ≡ a · b)
    intros HX HY.P: phase_space
X, Y: propset P
z: P
Q, R: P → Prop
HX: ∀ a : P, SetUnfoldElemOf a X (Q a)
HY: ∀ b : P, SetUnfoldElemOf b Y (R b)
SetUnfoldElemOf z (X ⊙ Y) (∃ a b : P, Q a ∧ R b ∧ z ≡ a · b) constructor.P: phase_space
X, Y: propset P
z: P
Q, R: P → Prop
HX: ∀ a : P, SetUnfoldElemOf a X (Q a)
HY: ∀ b : P, SetUnfoldElemOf b Y (R b)
z ∈ X ⊙ Y ↔ ∃ a b : P, Q a ∧ R b ∧ z ≡ a · b rewrite elem_of_prod.P: phase_space
X, Y: propset P
z: P
Q, R: P → Prop
HX: ∀ a : P, SetUnfoldElemOf a X (Q a)
HY: ∀ b : P, SetUnfoldElemOf b Y (R b)
(∃ a b : P, a ∈ X ∧ b ∈ Y ∧ z ≡ a · b) ↔ ∃ a b : P, Q a ∧ R b ∧ z ≡ a · b
    setoid_rewrite (λ a, @set_unfold_elem_of _ _ _ a X (Q a) (HX a)).P: phase_space
X, Y: propset P
z: P
Q, R: P → Prop
HX: ∀ a : P, SetUnfoldElemOf a X (Q a)
HY: ∀ b : P, SetUnfoldElemOf b Y (R b)
(∃ a b : P, Q a ∧ b ∈ Y ∧ z ≡ a · b) ↔ ∃ a b : P, Q a ∧ R b ∧ z ≡ a · b
    by setoid_rewrite (λ b, @set_unfold_elem_of _ _ _ b Y (R b) (HY b)).
  Qed.
End elem_of.

Facts and the algebra of sets of phases

Most of the soundness proof is reasoning about inclusions X ⊆ Y between sets of phases, not about individual phases. This section collects the inclusions we need. cl and ⊙ are monotone, and we register this with stdpp's Proper machinery so that ⊆ works with rewrite: in a goal L ⊆ R, rewrite H with H : X ⊆ X' replaces X by X' inside L. A proof of L ⊆ R then reads as a short calculation L ⊆ L' ⊆ … ⊆ R.

Section Facts.
  Context {P : phase_space}.
  Implicit Types (X Y Z G F : propset P) (x y z m g : P).

  Lemma cl_mono X Y : X ⊆ Y -> cl X ⊆ cl Y.P: phase_space
X, Y: propset P
X ⊆ Y → cl X ⊆ cl Y
  Proof.P: phase_space
X, Y: propset P
X ⊆ Y → cl X ⊆ cl Y intros H.P: phase_space
X, Y: propset P
H: X ⊆ Y
cl X ⊆ cl Y apply ph_cl_least.P: phase_space
X, Y: propset P
H: X ⊆ Y
X ⊆ cl Y intros x Hx.P: phase_space
X, Y: propset P
H: X ⊆ Y
x: P
Hx: x ∈ X
x ∈ cl Y apply ph_cl_ext, H, Hx. Qed.

  #[global] Instance cl_subseteq_proper : Proper ((⊆) ==> (⊆)) (@ph_cl P).P: phase_space
Proper (subseteq ==> subseteq) cl
  Proof.P: phase_space
Proper (subseteq ==> subseteq) cl intros X Y.P: phase_space
X, Y: propset P
X ⊆ Y → cl X ⊆ cl Y apply cl_mono. Qed.

A fact is a closed set: cl F ⊆ F, so cl F = F.

  Definition fact F : Prop := cl F ⊆ F.

  Lemma fact_cl X : fact (cl X).P: phase_space
X: propset P
fact (cl X)
  Proof.P: phase_space
X: propset P
fact (cl X) apply ph_cl_least.P: phase_space
X: propset P
cl X ⊆ cl X done. Qed.

Facts are closed under ≡.

  Lemma fact_proper F x y : fact F -> x ≡ y -> x ∈ F -> y ∈ F.P: phase_space
F: propset P
x, y: P
fact F → x ≡ y → x ∈ F → y ∈ F
  Proof.P: phase_space
F: propset P
x, y: P
fact F → x ≡ y → x ∈ F → y ∈ F
    intros HF Hxy Hx.P: phase_space
F: propset P
x, y: P
HF: fact F
Hxy: x ≡ y
Hx: x ∈ F
y ∈ F apply HF, (ph_cl_proper _ x); [done |].P: phase_space
F: propset P
x, y: P
HF: fact F
Hxy: x ≡ y
Hx: x ∈ F
x ∈ cl F by apply ph_cl_ext.
  Qed.

cl X is the least fact containing X.

  Lemma cl_least_fact X F : fact F -> X ⊆ F -> cl X ⊆ F.P: phase_space
X, F: propset P
fact F → X ⊆ F → cl X ⊆ F
  Proof.P: phase_space
X, F: propset P
fact F → X ⊆ F → cl X ⊆ F intros HF H.P: phase_space
X, F: propset P
HF: fact F
H: X ⊆ F
cl X ⊆ F by rewrite H. Qed.

Products

⊙ is monotone, commutative, associative, and has {ε} as its unit, all up to ⊆. prod_assoc_l and prod_assoc_r move the brackets to the left and to the right. The proofs unfold ⊙ and use the monoid laws of ·.

  Lemma prod_mono X X' Y Y' : X ⊆ X' -> Y ⊆ Y' -> X ⊙ Y ⊆ X' ⊙ Y'.P: phase_space
X, X', Y, Y': propset P
X ⊆ X' → Y ⊆ Y' → X ⊙ Y ⊆ X' ⊙ Y'
  Proof.P: phase_space
X, X', Y, Y': propset P
X ⊆ X' → Y ⊆ Y' → X ⊙ Y ⊆ X' ⊙ Y' set_solver. Qed.

  #[global] Instance prod_subseteq_proper :
    Proper ((⊆) ==> (⊆) ==> (⊆)) (@prod_set P).P: phase_space
Proper (subseteq ==> subseteq ==> subseteq) prod_set
  Proof.P: phase_space
Proper (subseteq ==> subseteq ==> subseteq) prod_set intros X X' HX Y Y' HY.P: phase_space
X, X': propset P
HX: X ⊆ X'
Y, Y': propset P
HY: Y ⊆ Y'
X ⊙ Y ⊆ X' ⊙ Y' by apply prod_mono. Qed.

  Lemma prod_comm X Y : X ⊙ Y ⊆ Y ⊙ X.P: phase_space
X, Y: propset P
X ⊙ Y ⊆ Y ⊙ X
  Proof.P: phase_space
X, Y: propset P
X ⊙ Y ⊆ Y ⊙ X
    intros m (a & b & Ha & Hb & Hm)%elem_of_prod.P: phase_space
X, Y: propset P
m, a, b: P
Ha: a ∈ X
Hb: b ∈ Y
Hm: m ≡ a · b
m ∈ Y ⊙ X
    apply elem_of_prod.P: phase_space
X, Y: propset P
m, a, b: P
Ha: a ∈ X
Hb: b ∈ Y
Hm: m ≡ a · b
∃ a0 b0 : P, a0 ∈ Y ∧ b0 ∈ X ∧ m ≡ a0 · b0 exists b, a.P: phase_space
X, Y: propset P
m, a, b: P
Ha: a ∈ X
Hb: b ∈ Y
Hm: m ≡ a · b
b ∈ Y ∧ a ∈ X ∧ m ≡ b · a by rewrite Hm, ph_comm.
  Qed.

  Lemma prod_assoc_l X Y Z : X ⊙ (Y ⊙ Z) ⊆ (X ⊙ Y) ⊙ Z.P: phase_space
X, Y, Z: propset P
X ⊙ (Y ⊙ Z) ⊆ X ⊙ Y ⊙ Z
  Proof.P: phase_space
X, Y, Z: propset P
X ⊙ (Y ⊙ Z) ⊆ X ⊙ Y ⊙ Z
    intros m (a & n & Ha & (b & c & Hb & Hc & Hn)%elem_of_prod & Hm)%elem_of_prod.P: phase_space
X, Y, Z: propset P
m, a, n: P
Ha: a ∈ X
b, c: P
Hb: b ∈ Y
Hc: c ∈ Z
Hn: n ≡ b · c
Hm: m ≡ a · n
m ∈ X ⊙ Y ⊙ Z
    apply elem_of_prod.P: phase_space
X, Y, Z: propset P
m, a, n: P
Ha: a ∈ X
b, c: P
Hb: b ∈ Y
Hc: c ∈ Z
Hn: n ≡ b · c
Hm: m ≡ a · n
∃ a0 b0 : P, a0 ∈ X ⊙ Y ∧ b0 ∈ Z ∧ m ≡ a0 · b0 exists (a · b), c.P: phase_space
X, Y, Z: propset P
m, a, n: P
Ha: a ∈ X
b, c: P
Hb: b ∈ Y
Hc: c ∈ Z
Hn: n ≡ b · c
Hm: m ≡ a · n
a · b ∈ X ⊙ Y ∧ c ∈ Z ∧ m ≡ a · b · c split_and!; [| done |].P: phase_space
X, Y, Z: propset P
m, a, n: P
Ha: a ∈ X
b, c: P
Hb: b ∈ Y
Hc: c ∈ Z
Hn: n ≡ b · c
Hm: m ≡ a · n
a · b ∈ X ⊙ Y
P: phase_space
X, Y, Z: propset P
m, a, n: P
Ha: a ∈ X
b, c: P
Hb: b ∈ Y
Hc: c ∈ Z
Hn: n ≡ b · c
Hm: m ≡ a · n
m ≡ a · b · c
    -P: phase_space
X, Y, Z: propset P
m, a, n: P
Ha: a ∈ X
b, c: P
Hb: b ∈ Y
Hc: c ∈ Z
Hn: n ≡ b · c
Hm: m ≡ a · n
a · b ∈ X ⊙ Y apply elem_of_prod.P: phase_space
X, Y, Z: propset P
m, a, n: P
Ha: a ∈ X
b, c: P
Hb: b ∈ Y
Hc: c ∈ Z
Hn: n ≡ b · c
Hm: m ≡ a · n
∃ a0 b0 : P, a0 ∈ X ∧ b0 ∈ Y ∧ a · b ≡ a0 · b0 by exists a, b.
    -P: phase_space
X, Y, Z: propset P
m, a, n: P
Ha: a ∈ X
b, c: P
Hb: b ∈ Y
Hc: c ∈ Z
Hn: n ≡ b · c
Hm: m ≡ a · n
m ≡ a · b · c by rewrite Hm, Hn, ph_assoc.
  Qed.

  Lemma prod_assoc_r X Y Z : (X ⊙ Y) ⊙ Z ⊆ X ⊙ (Y ⊙ Z).P: phase_space
X, Y, Z: propset P
X ⊙ Y ⊙ Z ⊆ X ⊙ (Y ⊙ Z)
  Proof.P: phase_space
X, Y, Z: propset P
X ⊙ Y ⊙ Z ⊆ X ⊙ (Y ⊙ Z)
    intros m (n & c & (a & b & Ha & Hb & Hn)%elem_of_prod & Hc & Hm)%elem_of_prod.P: phase_space
X, Y, Z: propset P
m, n, c, a, b: P
Ha: a ∈ X
Hb: b ∈ Y
Hn: n ≡ a · b
Hc: c ∈ Z
Hm: m ≡ n · c
m ∈ X ⊙ (Y ⊙ Z)
    apply elem_of_prod.P: phase_space
X, Y, Z: propset P
m, n, c, a, b: P
Ha: a ∈ X
Hb: b ∈ Y
Hn: n ≡ a · b
Hc: c ∈ Z
Hm: m ≡ n · c
∃ a0 b0 : P, a0 ∈ X ∧ b0 ∈ Y ⊙ Z ∧ m ≡ a0 · b0 exists a, (b · c).P: phase_space
X, Y, Z: propset P
m, n, c, a, b: P
Ha: a ∈ X
Hb: b ∈ Y
Hn: n ≡ a · b
Hc: c ∈ Z
Hm: m ≡ n · c
a ∈ X ∧ b · c ∈ Y ⊙ Z ∧ m ≡ a · (b · c) split_and!; [done | |].P: phase_space
X, Y, Z: propset P
m, n, c, a, b: P
Ha: a ∈ X
Hb: b ∈ Y
Hn: n ≡ a · b
Hc: c ∈ Z
Hm: m ≡ n · c
b · c ∈ Y ⊙ Z
P: phase_space
X, Y, Z: propset P
m, n, c, a, b: P
Ha: a ∈ X
Hb: b ∈ Y
Hn: n ≡ a · b
Hc: c ∈ Z
Hm: m ≡ n · c
m ≡ a · (b · c)
    -P: phase_space
X, Y, Z: propset P
m, n, c, a, b: P
Ha: a ∈ X
Hb: b ∈ Y
Hn: n ≡ a · b
Hc: c ∈ Z
Hm: m ≡ n · c
b · c ∈ Y ⊙ Z apply elem_of_prod.P: phase_space
X, Y, Z: propset P
m, n, c, a, b: P
Ha: a ∈ X
Hb: b ∈ Y
Hn: n ≡ a · b
Hc: c ∈ Z
Hm: m ≡ n · c
∃ a0 b0 : P, a0 ∈ Y ∧ b0 ∈ Z ∧ b · c ≡ a0 · b0 by exists b, c.
    -P: phase_space
X, Y, Z: propset P
m, n, c, a, b: P
Ha: a ∈ X
Hb: b ∈ Y
Hn: n ≡ a · b
Hc: c ∈ Z
Hm: m ≡ n · c
m ≡ a · (b · c) by rewrite Hm, Hn, ph_assoc.
  Qed.

  Lemma prod_unit_l X : X ⊆ one_set ⊙ X.P: phase_space
X: propset P
X ⊆ one_set ⊙ X
  Proof.P: phase_space
X: propset P
X ⊆ one_set ⊙ X
    intros x Hx.P: phase_space
X: propset P
x: P
Hx: x ∈ X
x ∈ one_set ⊙ X apply elem_of_prod.P: phase_space
X: propset P
x: P
Hx: x ∈ X
∃ a b : P, a ∈ one_set ∧ b ∈ X ∧ x ≡ a · b exists ε, x.P: phase_space
X: propset P
x: P
Hx: x ∈ X
ε ∈ one_set ∧ x ∈ X ∧ x ≡ ε · x by rewrite elem_of_one, ph_unit_l.
  Qed.

The converse of prod_unit_l needs ≡-closure, so we state it for a fact F that contains X.

  Lemma prod_one_l X F : fact F -> X ⊆ F -> one_set ⊙ X ⊆ F.P: phase_space
X, F: propset P
fact F → X ⊆ F → one_set ⊙ X ⊆ F
  Proof.P: phase_space
X, F: propset P
fact F → X ⊆ F → one_set ⊙ X ⊆ F
    intros HF HX m (e & x & He%elem_of_one & Hx & Hm)%elem_of_prod.P: phase_space
X, F: propset P
HF: fact F
HX: X ⊆ F
m, e, x: P
He: e ≡ ε
Hx: x ∈ X
Hm: m ≡ e · x
m ∈ F
    apply (fact_proper _ x); [done | | by apply HX].P: phase_space
X, F: propset P
HF: fact F
HX: X ⊆ F
m, e, x: P
He: e ≡ ε
Hx: x ∈ X
Hm: m ≡ e · x
x ≡ m
    by rewrite Hm, He, ph_unit_l.
  Qed.

The stability axiom of the record, stated for sets.

  Lemma cl_prod X Y : cl X ⊙ cl Y ⊆ cl (X ⊙ Y).P: phase_space
X, Y: propset P
cl X ⊙ cl Y ⊆ cl (X ⊙ Y)
  Proof.P: phase_space
X, Y: propset P
cl X ⊙ cl Y ⊆ cl (X ⊙ Y)
    intros m (x & y & Hx & Hy & Hm)%elem_of_prod.P: phase_space
X, Y: propset P
m, x, y: P
Hx: x ∈ cl X
Hy: y ∈ cl Y
Hm: m ≡ x · y
m ∈ cl (X ⊙ Y)
    apply (ph_cl_proper _ (x · y)); [by symmetry |].P: phase_space
X, Y: propset P
m, x, y: P
Hx: x ∈ cl X
Hy: y ∈ cl Y
Hm: m ≡ x · y
x · y ∈ cl (X ⊙ Y) by apply ph_cl_stable.
  Qed.

The workhorse of the soundness proof. To show that cl X ⊙ G lies in a fact F, it is enough to check the generators X of the closure. This is where stability is used.

  Lemma prod_cl_l X G F : fact F -> X ⊙ G ⊆ F -> cl X ⊙ G ⊆ F.P: phase_space
X, G, F: propset P
fact F → X ⊙ G ⊆ F → cl X ⊙ G ⊆ F
  Proof.P: phase_space
X, G, F: propset P
fact F → X ⊙ G ⊆ F → cl X ⊙ G ⊆ F intros HF H.P: phase_space
X, G, F: propset P
HF: fact F
H: X ⊙ G ⊆ F
cl X ⊙ G ⊆ F rewrite (ph_cl_ext G), cl_prod.P: phase_space
X, G, F: propset P
HF: fact F
H: X ⊙ G ⊆ F
cl (X ⊙ G) ⊆ F by apply cl_least_fact. Qed.

The phase connectives

The phase-space counterpart of each connective:

      𝟙      ↦  cl {ε}
      X ⊗ Y  ↦  cl (X ⊙ Y)
      X ⊸ Y  ↦  { m | ∀ a ∈ X, m · a ∈ Y }
      X & Y  ↦  X ∩ Y
      ⊤      ↦  M
      X ⊕ Y  ↦  cl (X ∪ Y)
      𝟘      ↦  cl ∅
      !X     ↦  cl (X ∩ J)
      ⊥      ↦  cl ph_bot            (part of the model)

⊸ and & need no closure: when X and Y are facts, so are X ⊸ Y and X ∩ Y.

  Definition ph_one : propset P := cl one_set.
  Definition ph_tensor X Y : propset P := cl (X ⊙ Y).
  Definition ph_lolli X Y : propset P := {[ m | ∀ a, a ∈ X -> m · a ∈ Y ]}.
  Definition ph_top : propset P := {[ _ | True ]}.
  Definition ph_plus X Y : propset P := cl (X ∪ Y).
  Definition ph_zero : propset P := cl ∅.
  Definition ph_bang X : propset P := cl (X ∩ J).

  Lemma elem_of_lolli X Y m : m ∈ ph_lolli X Y ↔ ∀ a, a ∈ X -> m · a ∈ Y.P: phase_space
X, Y: propset P
m: P
m ∈ ph_lolli X Y ↔ ∀ a : P, a ∈ X → m · a ∈ Y
  Proof.P: phase_space
X, Y: propset P
m: P
m ∈ ph_lolli X Y ↔ ∀ a : P, a ∈ X → m · a ∈ Y unfold ph_lolli.P: phase_space
X, Y: propset P
m: P
m ∈ {[ m0 | ∀ a : P, a ∈ X → m0 · a ∈ Y ]} ↔ ∀ a : P, a ∈ X → m · a ∈ Y by rewrite elem_of_PropSet. Qed.
  Lemma elem_of_top m : m ∈ ph_top.P: phase_space
m: P
m ∈ ph_top
  Proof.P: phase_space
m: P
m ∈ ph_top unfold ph_top.P: phase_space
m: P
m ∈ {[ _ | True ]} by rewrite elem_of_PropSet. Qed.

  #[global] Instance set_unfold_lolli X Y m :
    SetUnfoldElemOf m (ph_lolli X Y) (∀ a, a ∈ X -> m · a ∈ Y).P: phase_space
X, Y: propset P
m: P
SetUnfoldElemOf m (ph_lolli X Y) (∀ a : P, a ∈ X → m · a ∈ Y)
  Proof.P: phase_space
X, Y: propset P
m: P
SetUnfoldElemOf m (ph_lolli X Y) (∀ a : P, a ∈ X → m · a ∈ Y) constructor.P: phase_space
X, Y: propset P
m: P
m ∈ ph_lolli X Y ↔ ∀ a : P, a ∈ X → m · a ∈ Y apply elem_of_lolli. Qed.
  #[global] Instance set_unfold_top m : SetUnfoldElemOf m ph_top True.P: phase_space
m: P
SetUnfoldElemOf m ph_top True
  Proof.P: phase_space
m: P
SetUnfoldElemOf m ph_top True constructor.P: phase_space
m: P
m ∈ ph_top ↔ True split; [done | intros; apply elem_of_top]. Qed.

X ⊸ Y is the largest G with G ⊙ X ⊆ Y. The two directions are the semantic ⊸R and ⊸L.

  Lemma lolli_intro X Y G : G ⊙ X ⊆ Y -> G ⊆ ph_lolli X Y.P: phase_space
X, Y, G: propset P
G ⊙ X ⊆ Y → G ⊆ ph_lolli X Y
  Proof.P: phase_space
X, Y, G: propset P
G ⊙ X ⊆ Y → G ⊆ ph_lolli X Y
    intros H m Hm.P: phase_space
X, Y, G: propset P
H: G ⊙ X ⊆ Y
m: P
Hm: m ∈ G
m ∈ ph_lolli X Y apply elem_of_lolli.P: phase_space
X, Y, G: propset P
H: G ⊙ X ⊆ Y
m: P
Hm: m ∈ G
∀ a : P, a ∈ X → m · a ∈ Y intros a Ha.P: phase_space
X, Y, G: propset P
H: G ⊙ X ⊆ Y
m: P
Hm: m ∈ G
a: P
Ha: a ∈ X
m · a ∈ Y
    apply H, elem_of_prod.P: phase_space
X, Y, G: propset P
H: G ⊙ X ⊆ Y
m: P
Hm: m ∈ G
a: P
Ha: a ∈ X
∃ a0 b : P, a0 ∈ G ∧ b ∈ X ∧ m · a ≡ a0 · b by exists m, a.
  Qed.

  Lemma lolli_elim X Y : fact Y -> ph_lolli X Y ⊙ X ⊆ Y.P: phase_space
X, Y: propset P
fact Y → ph_lolli X Y ⊙ X ⊆ Y
  Proof.P: phase_space
X, Y: propset P
fact Y → ph_lolli X Y ⊙ X ⊆ Y
    intros HY m (f & a & Hf & Ha & Hm)%elem_of_prod.P: phase_space
X, Y: propset P
HY: fact Y
m, f, a: P
Hf: f ∈ ph_lolli X Y
Ha: a ∈ X
Hm: m ≡ f · a
m ∈ Y
    apply (fact_proper _ (f · a)); [done | by symmetry |].P: phase_space
X, Y: propset P
HY: fact Y
m, f, a: P
Hf: f ∈ ph_lolli X Y
Ha: a ∈ X
Hm: m ≡ f · a
f · a ∈ Y
    rewrite elem_of_lolli in Hf.P: phase_space
X, Y: propset P
HY: fact Y
m, f, a: P
Hf: ∀ a : P, a ∈ X → f · a ∈ Y
Ha: a ∈ X
Hm: m ≡ f · a
f · a ∈ Y by apply Hf.
  Qed.

  Lemma fact_lolli X Y : fact Y -> fact (ph_lolli X Y).P: phase_space
X, Y: propset P
fact Y → fact (ph_lolli X Y)
  Proof.P: phase_space
X, Y: propset P
fact Y → fact (ph_lolli X Y) intros HY.P: phase_space
X, Y: propset P
HY: fact Y
fact (ph_lolli X Y) apply lolli_intro, prod_cl_l, lolli_elim; done. Qed.

  Lemma fact_inter X Y : fact X -> fact Y -> fact (X ∩ Y).P: phase_space
X, Y: propset P
fact X → fact Y → fact (X ∩ Y)
  Proof.P: phase_space
X, Y: propset P
fact X → fact Y → fact (X ∩ Y)
    intros HX HY m Hm.P: phase_space
X, Y: propset P
HX: fact X
HY: fact Y
m: P
Hm: m ∈ cl (X ∩ Y)
m ∈ X ∩ Y apply elem_of_intersection.P: phase_space
X, Y: propset P
HX: fact X
HY: fact Y
m: P
Hm: m ∈ cl (X ∩ Y)
m ∈ X ∧ m ∈ Y
    split; [apply HX | apply HY]; revert m Hm; apply cl_mono; set_solver.
  Qed.

  Lemma fact_top : fact ph_top.P: phase_space
fact ph_top
  Proof.P: phase_space
fact ph_top intros m _.P: phase_space
m: P
m ∈ ph_top apply elem_of_top. Qed.

Using a tensor X ⊗ Y next to G is the same as using X, Y and G side by side: the semantic ⊗L.

  Lemma tensor_l X Y G F : fact F -> X ⊙ (Y ⊙ G) ⊆ F -> ph_tensor X Y ⊙ G ⊆ F.P: phase_space
X, Y, G, F: propset P
fact F → X ⊙ (Y ⊙ G) ⊆ F → ph_tensor X Y ⊙ G ⊆ F
  Proof.P: phase_space
X, Y, G, F: propset P
fact F → X ⊙ (Y ⊙ G) ⊆ F → ph_tensor X Y ⊙ G ⊆ F intros HF H.P: phase_space
X, Y, G, F: propset P
HF: fact F
H: X ⊙ (Y ⊙ G) ⊆ F
ph_tensor X Y ⊙ G ⊆ F apply prod_cl_l; [done |].P: phase_space
X, Y, G, F: propset P
HF: fact F
H: X ⊙ (Y ⊙ G) ⊆ F
X ⊙ Y ⊙ G ⊆ F by rewrite prod_assoc_r. Qed.

The axioms on J say that a phase of !X can be discarded (it lies in 𝟙) and duplicated (it lies in !X ⊗ !X). These are the semantic !W and !C.

  Lemma bang_weak X : ph_bang X ⊆ ph_one.P: phase_space
X: propset P
ph_bang X ⊆ ph_one
  Proof.P: phase_space
X: propset P
ph_bang X ⊆ ph_one
    apply ph_cl_least.P: phase_space
X: propset P
X ∩ J ⊆ cl one_set intros j [_ HJ]%elem_of_intersection.P: phase_space
X: propset P
j: P
HJ: j ∈ J
j ∈ cl one_set by apply ph_J_weak.
  Qed.

  Lemma bang_contr X : ph_bang X ⊆ ph_tensor (ph_bang X) (ph_bang X).P: phase_space
X: propset P
ph_bang X ⊆ ph_tensor (ph_bang X) (ph_bang X)
  Proof.P: phase_space
X: propset P
ph_bang X ⊆ ph_tensor (ph_bang X) (ph_bang X)
    apply ph_cl_least.P: phase_space
X: propset P
X ∩ J ⊆ cl (ph_bang X ⊙ ph_bang X) intros j Hj.P: phase_space
X: propset P
j: P
Hj: j ∈ X ∩ J
j ∈ cl (ph_bang X ⊙ ph_bang X)
    apply (cl_mono ((X ∩ J) ⊙ (X ∩ J))); [apply prod_mono; apply ph_cl_ext |].P: phase_space
X: propset P
j: P
Hj: j ∈ X ∩ J
j ∈ cl (X ∩ J ⊙ (X ∩ J))
    apply (cl_mono {[ z | z ≡ j · j ]}); [set_solver |].P: phase_space
X: propset P
j: P
Hj: j ∈ X ∩ J
j ∈ cl {[ z | z ≡ j · j ]}
    apply ph_J_contr.P: phase_space
X: propset P
j: P
Hj: j ∈ X ∩ J
j ∈ J set_solver.
  Qed.
End Facts.

Interpreting formulas and sequents

A valuation v gives each propositional variable a set of phases. The variable $p denotes cl (v p), which makes it a fact.

Fixpoint interp {P : phase_space} (v : nat -> propset P) (A : iformula)
  : propset P :=
  match A with
  | IAtom p     => cl (v p)
  | IOne        => ph_one
  | IBot        => cl ph_bot
  | ITop        => ph_top
  | IZero       => ph_zero
  | ITensor A B => ph_tensor (interp v A) (interp v B)
  | ILolli A B  => ph_lolli (interp v A) (interp v B)
  | IWith A B   => interp v A ∩ interp v B
  | IPlus A B   => ph_plus (interp v A) (interp v B)
  | IBang A     => ph_bang (interp v A)
  end.

Notation "⟦ A ⟧ v" := (interp v A)
  (at level 1, A at level 200, v at level 1, format "⟦ A ⟧ v")
  : ill_phase_scope.

A context [A₁; …; Aₙ] denotes ⟦A₁⟧ ⊙ … ⊙ ⟦Aₙ⟧ ⊙ {ε}: the bags obtained by taking one bag for each hypothesis and combining them.

Fixpoint interp_ctx {P : phase_space} (v : nat -> propset P)
    (Γ : list iformula) : propset P :=
  match Γ with
  | []     => one_set
  | A :: Γ => ⟦A⟧v ⊙ interp_ctx v Γ
  end.

Notation "⦅ Γ ⦆ v" := (interp_ctx v Γ)
  (at level 1, Γ at level 200, v at level 1, format "⦅ Γ ⦆ v")
  : ill_phase_scope.

A sequent is valid in a model when the bags for the hypotheses always give a bag for the conclusion. It is valid outright when that holds in every phase space under every valuation.

Definition valid_in {P : phase_space} (v : nat -> propset P) Γ A : Prop :=
  ⦅Γ⦆v ⊆ ⟦A⟧v.

Definition valid (Γ : list iformula) (A : iformula) : Prop :=
  ∀ (P : phase_space) (v : nat -> propset P), valid_in v Γ A.

Notation "Γ ⊨ A" := (valid Γ A) (at level 80, no associativity)
  : ill_phase_scope.

Section Interp.
  Context {P : phase_space} (v : nat -> propset P).

Every formula denotes a fact.

  Lemma interp_fact A : fact (⟦A⟧v).P: phase_space
v: nat → propset P
A: iformula
fact ⟦A⟧v
  Proof.P: phase_space
v: nat → propset P
A: iformula
fact ⟦A⟧v
    induction A; cbn [interp];
      unfold ph_one, ph_zero, ph_tensor, ph_plus, ph_bang;
      auto using fact_cl, fact_lolli, fact_inter, fact_top.
  Qed.

Split a bag for Γ ++ Δ into a bag for Γ and a bag for Δ.

  Lemma ctx_app Γ Δ : ⦅Γ ++ Δ⦆v ⊆ ⦅Γ⦆v ⊙ ⦅Δ⦆v.P: phase_space
v: nat → propset P
Γ, Δ: list iformula
⦅Γ ++ Δ⦆v ⊆ ⦅Γ⦆v ⊙ ⦅Δ⦆v
  Proof.P: phase_space
v: nat → propset P
Γ, Δ: list iformula
⦅Γ ++ Δ⦆v ⊆ ⦅Γ⦆v ⊙ ⦅Δ⦆v
    induction Γ as [| A Γ IH]; cbn [interp_ctx app].P: phase_space
v: nat → propset P
Δ: list iformula
⦅Δ⦆v ⊆ one_set ⊙ ⦅Δ⦆v
P: phase_space
v: nat → propset P
A: iformula
Γ, Δ: list iformula
IH: ⦅Γ ++ Δ⦆v ⊆ ⦅Γ⦆v ⊙ ⦅Δ⦆v
⟦A⟧v ⊙ ⦅Γ ++ Δ⦆v ⊆ ⟦A⟧v ⊙ ⦅Γ⦆v ⊙ ⦅Δ⦆v
    -P: phase_space
v: nat → propset P
Δ: list iformula
⦅Δ⦆v ⊆ one_set ⊙ ⦅Δ⦆v apply prod_unit_l.
    -P: phase_space
v: nat → propset P
A: iformula
Γ, Δ: list iformula
IH: ⦅Γ ++ Δ⦆v ⊆ ⦅Γ⦆v ⊙ ⦅Δ⦆v
⟦A⟧v ⊙ ⦅Γ ++ Δ⦆v ⊆ ⟦A⟧v ⊙ ⦅Γ⦆v ⊙ ⦅Δ⦆v by rewrite IH, prod_assoc_l.
  Qed.

· is commutative, so the order of hypotheses is irrelevant. This is the semantic content of the exchange rule.

  Lemma ctx_perm Γ Γ' : Γ ≡ₚ Γ' -> ⦅Γ⦆v ⊆ ⦅Γ'⦆v.P: phase_space
v: nat → propset P
Γ, Γ': list iformula
Γ ≡ₚ Γ' → ⦅Γ⦆v ⊆ ⦅Γ'⦆v
  Proof.P: phase_space
v: nat → propset P
Γ, Γ': list iformula
Γ ≡ₚ Γ' → ⦅Γ⦆v ⊆ ⦅Γ'⦆v
    induction 1 as [| A Γ Γ' _ IH | A B Γ | Γ Γ' Γ'' _ IH1 _ IH2];
      cbn [interp_ctx].P: phase_space
v: nat → propset P
one_set ⊆ one_set
P: phase_space
v: nat → propset P
A: iformula
Γ, Γ': list iformula
IH: ⦅Γ⦆v ⊆ ⦅Γ'⦆v
⟦A⟧v ⊙ ⦅Γ⦆v ⊆ ⟦A⟧v ⊙ ⦅Γ'⦆v
P: phase_space
v: nat → propset P
A, B: iformula
Γ: list iformula
⟦B⟧v ⊙ (⟦A⟧v ⊙ ⦅Γ⦆v) ⊆ ⟦A⟧v ⊙ (⟦B⟧v ⊙ ⦅Γ⦆v)
P: phase_space
v: nat → propset P
Γ, Γ', Γ'': list iformula
IH1: ⦅Γ⦆v ⊆ ⦅Γ'⦆v
IH2: ⦅Γ'⦆v ⊆ ⦅Γ''⦆v
⦅Γ⦆v ⊆ ⦅Γ''⦆v
    -P: phase_space
v: nat → propset P
one_set ⊆ one_set done.
    -P: phase_space
v: nat → propset P
A: iformula
Γ, Γ': list iformula
IH: ⦅Γ⦆v ⊆ ⦅Γ'⦆v
⟦A⟧v ⊙ ⦅Γ⦆v ⊆ ⟦A⟧v ⊙ ⦅Γ'⦆v by rewrite IH.
    -P: phase_space
v: nat → propset P
A, B: iformula
Γ: list iformula
⟦B⟧v ⊙ (⟦A⟧v ⊙ ⦅Γ⦆v) ⊆ ⟦A⟧v ⊙ (⟦B⟧v ⊙ ⦅Γ⦆v) by rewrite prod_assoc_l, (prod_comm (⟦B⟧v)), prod_assoc_r.
    -P: phase_space
v: nat → propset P
Γ, Γ', Γ'': list iformula
IH1: ⦅Γ⦆v ⊆ ⦅Γ'⦆v
IH2: ⦅Γ'⦆v ⊆ ⦅Γ''⦆v
⦅Γ⦆v ⊆ ⦅Γ''⦆v by rewrite IH1, IH2.
  Qed.

A bag for a banged context ‼Σ lies in the closure of the bags that are both in ⦅‼Σ⦆ and reusable. Promotion uses this.

  Lemma ctx_bangs Σ : ⦅‼Σ⦆v ⊆ cl (⦅‼Σ⦆v ∩ J).P: phase_space
v: nat → propset P
Σ: list iformula
⦅‼Σ⦆v ⊆ cl (⦅‼Σ⦆v ∩ J)
  Proof.P: phase_space
v: nat → propset P
Σ: list iformula
⦅‼Σ⦆v ⊆ cl (⦅‼Σ⦆v ∩ J)
    induction Σ as [| A Σ IH]; cbn [interp_ctx map interp].P: phase_space
v: nat → propset P
one_set ⊆ cl (one_set ∩ J)
P: phase_space
v: nat → propset P
A: iformula
Σ: list iformula
IH: ⦅‼Σ⦆v ⊆ cl (⦅‼Σ⦆v ∩ J)
ph_bang ⟦A⟧v ⊙ ⦅‼Σ⦆v ⊆ cl ((ph_bang ⟦A⟧v ⊙ ⦅‼Σ⦆v) ∩ J)
    -P: phase_space
v: nat → propset P
one_set ⊆ cl (one_set ∩ J) intros m Hm.P: phase_space
v: nat → propset P
m: P
Hm: m ∈ one_set
m ∈ cl (one_set ∩ J) apply ph_cl_ext, elem_of_intersection.P: phase_space
v: nat → propset P
m: P
Hm: m ∈ one_set
m ∈ one_set ∧ m ∈ J split; [done |].P: phase_space
v: nat → propset P
m: P
Hm: m ∈ one_set
m ∈ J
      apply elem_of_one in Hm.P: phase_space
v: nat → propset P
m: P
Hm: m ≡ ε
m ∈ J
      apply (ph_J_proper ε); [by symmetry | apply ph_J_unit].
    - (* cl (⟦A⟧ ∩ J) ⊙ cl (⦅‼Σ⦆ ∩ J) ⊆ cl ((⟦A⟧ ∩ J) ⊙ (⦅‼Σ⦆ ∩ J)) *)P: phase_space
v: nat → propset P
A: iformula
Σ: list iformula
IH: ⦅‼Σ⦆v ⊆ cl (⦅‼Σ⦆v ∩ J)
ph_bang ⟦A⟧v ⊙ ⦅‼Σ⦆v ⊆ cl ((ph_bang ⟦A⟧v ⊙ ⦅‼Σ⦆v) ∩ J)
      rewrite IH at 1.P: phase_space
v: nat → propset P
A: iformula
Σ: list iformula
IH: ⦅‼Σ⦆v ⊆ cl (⦅‼Σ⦆v ∩ J)
ph_bang ⟦A⟧v ⊙ cl (⦅‼Σ⦆v ∩ J) ⊆ cl ((ph_bang ⟦A⟧v ⊙ ⦅‼Σ⦆v) ∩ J) unfold ph_bang.P: phase_space
v: nat → propset P
A: iformula
Σ: list iformula
IH: ⦅‼Σ⦆v ⊆ cl (⦅‼Σ⦆v ∩ J)
cl (⟦A⟧v ∩ J) ⊙ cl (⦅‼Σ⦆v ∩ J) ⊆ cl ((cl (⟦A⟧v ∩ J) ⊙ ⦅‼Σ⦆v) ∩ J) rewrite cl_prod.P: phase_space
v: nat → propset P
A: iformula
Σ: list iformula
IH: ⦅‼Σ⦆v ⊆ cl (⦅‼Σ⦆v ∩ J)
cl (⟦A⟧v ∩ J ⊙ (⦅‼Σ⦆v ∩ J)) ⊆ cl ((cl (⟦A⟧v ∩ J) ⊙ ⦅‼Σ⦆v) ∩ J) apply cl_mono.P: phase_space
v: nat → propset P
A: iformula
Σ: list iformula
IH: ⦅‼Σ⦆v ⊆ cl (⦅‼Σ⦆v ∩ J)
⟦A⟧v ∩ J ⊙ (⦅‼Σ⦆v ∩ J) ⊆ (cl (⟦A⟧v ∩ J) ⊙ ⦅‼Σ⦆v) ∩ J
      intros m (a & g & [Ha HJa]%elem_of_intersection
                      & [Hg HJg]%elem_of_intersection & Hm)%elem_of_prod.P: phase_space
v: nat → propset P
A: iformula
Σ: list iformula
IH: ⦅‼Σ⦆v ⊆ cl (⦅‼Σ⦆v ∩ J)
m, a, g: P
Ha: a ∈ ⟦A⟧v
HJa: a ∈ J
Hg: g ∈ ⦅‼Σ⦆v
HJg: g ∈ J
Hm: m ≡ a · g
m ∈ (cl (⟦A⟧v ∩ J) ⊙ ⦅‼Σ⦆v) ∩ J
      apply elem_of_intersection.P: phase_space
v: nat → propset P
A: iformula
Σ: list iformula
IH: ⦅‼Σ⦆v ⊆ cl (⦅‼Σ⦆v ∩ J)
m, a, g: P
Ha: a ∈ ⟦A⟧v
HJa: a ∈ J
Hg: g ∈ ⦅‼Σ⦆v
HJg: g ∈ J
Hm: m ≡ a · g
m ∈ cl (⟦A⟧v ∩ J) ⊙ ⦅‼Σ⦆v ∧ m ∈ J split.P: phase_space
v: nat → propset P
A: iformula
Σ: list iformula
IH: ⦅‼Σ⦆v ⊆ cl (⦅‼Σ⦆v ∩ J)
m, a, g: P
Ha: a ∈ ⟦A⟧v
HJa: a ∈ J
Hg: g ∈ ⦅‼Σ⦆v
HJg: g ∈ J
Hm: m ≡ a · g
m ∈ cl (⟦A⟧v ∩ J) ⊙ ⦅‼Σ⦆v
P: phase_space
v: nat → propset P
A: iformula
Σ: list iformula
IH: ⦅‼Σ⦆v ⊆ cl (⦅‼Σ⦆v ∩ J)
m, a, g: P
Ha: a ∈ ⟦A⟧v
HJa: a ∈ J
Hg: g ∈ ⦅‼Σ⦆v
HJg: g ∈ J
Hm: m ≡ a · g
m ∈ J
      +P: phase_space
v: nat → propset P
A: iformula
Σ: list iformula
IH: ⦅‼Σ⦆v ⊆ cl (⦅‼Σ⦆v ∩ J)
m, a, g: P
Ha: a ∈ ⟦A⟧v
HJa: a ∈ J
Hg: g ∈ ⦅‼Σ⦆v
HJg: g ∈ J
Hm: m ≡ a · g
m ∈ cl (⟦A⟧v ∩ J) ⊙ ⦅‼Σ⦆v apply elem_of_prod.P: phase_space
v: nat → propset P
A: iformula
Σ: list iformula
IH: ⦅‼Σ⦆v ⊆ cl (⦅‼Σ⦆v ∩ J)
m, a, g: P
Ha: a ∈ ⟦A⟧v
HJa: a ∈ J
Hg: g ∈ ⦅‼Σ⦆v
HJg: g ∈ J
Hm: m ≡ a · g
∃ a0 b : P, a0 ∈ cl (⟦A⟧v ∩ J) ∧ b ∈ ⦅‼Σ⦆v ∧ m ≡ a0 · b exists a, g.P: phase_space
v: nat → propset P
A: iformula
Σ: list iformula
IH: ⦅‼Σ⦆v ⊆ cl (⦅‼Σ⦆v ∩ J)
m, a, g: P
Ha: a ∈ ⟦A⟧v
HJa: a ∈ J
Hg: g ∈ ⦅‼Σ⦆v
HJg: g ∈ J
Hm: m ≡ a · g
a ∈ cl (⟦A⟧v ∩ J) ∧ g ∈ ⦅‼Σ⦆v ∧ m ≡ a · g split_and!; [by apply ph_cl_ext | done..].
      +P: phase_space
v: nat → propset P
A: iformula
Σ: list iformula
IH: ⦅‼Σ⦆v ⊆ cl (⦅‼Σ⦆v ∩ J)
m, a, g: P
Ha: a ∈ ⟦A⟧v
HJa: a ∈ J
Hg: g ∈ ⦅‼Σ⦆v
HJg: g ∈ J
Hm: m ≡ a · g
m ∈ J apply (ph_J_proper (a · g)); [by symmetry | by apply ph_J_op].
  Qed.
End Interp.

Soundness

Every derivable sequent is valid. The proof is by induction on the derivation. Each case is a short calculation with the inclusions above: a right rule builds the conclusion from the premises, and a left rule A :: Γ ⊢ C reduces ⟦A⟧ ⊙ ⦅Γ⦆ to the generators of ⟦A⟧ with prod_cl_l. c is arbitrary, so this covers the calculus with cut and the cut-free calculus alike.

Theorem soundness c Γ A : Γ ⊢[c] A -> Γ ⊨ A.c: bool
Γ: list iformula
A: iformula
Γ ⊢[c] A → Γ ⊨ A
Proof.c: bool
Γ: list iformula
A: iformula
Γ ⊢[c] A → Γ ⊨ A
  intros H P v.c: bool
Γ: list iformula
A: iformula
H: Γ ⊢[c] A
P: phase_space
v: nat → propset P
valid_in v Γ A
  induction H; unfold valid_in in *; cbn [interp interp_ctx map] in *.c: bool
A: iformula
P: phase_space
v: nat → propset P
⟦A⟧v ⊙ one_set ⊆ ⟦A⟧v
c: bool
Γ, Δ: list iformula
A, C: iformula
H: c = true
H0: Γ ⊢[c] A
H1: A :: Δ ⊢[c] C
P: phase_space
v: nat → propset P
IHill1: ⦅Γ⦆v ⊆ ⟦A⟧v
IHill2: ⟦A⟧v ⊙ ⦅Δ⦆v ⊆ ⟦C⟧v
⦅Γ ++ Δ⦆v ⊆ ⟦C⟧v
c: bool
Γ, Γ': list iformula
C: iformula
H: Γ ≡ₚ Γ'
H0: Γ ⊢[c] C
P: phase_space
v: nat → propset P
IHill: ⦅Γ⦆v ⊆ ⟦C⟧v
⦅Γ'⦆v ⊆ ⟦C⟧v
c: bool
P: phase_space
v: nat → propset P
one_set ⊆ ph_one
c: bool
Γ: list iformula
C: iformula
H: Γ ⊢[c] C
P: phase_space
v: nat → propset P
IHill: ⦅Γ⦆v ⊆ ⟦C⟧v
ph_one ⊙ ⦅Γ⦆v ⊆ ⟦C⟧v
c: bool
Γ, Δ: list iformula
A, B: iformula
H: Γ ⊢[c] A
H0: Δ ⊢[c] B
P: phase_space
v: nat → propset P
IHill1: ⦅Γ⦆v ⊆ ⟦A⟧v
IHill2: ⦅Δ⦆v ⊆ ⟦B⟧v
⦅Γ ++ Δ⦆v ⊆ ph_tensor ⟦A⟧v ⟦B⟧v
c: bool
Γ: list iformula
A, B, C: iformula
H: A :: B :: Γ ⊢[c] C
P: phase_space
v: nat → propset P
IHill: ⟦A⟧v ⊙ (⟦B⟧v ⊙ ⦅Γ⦆v) ⊆ ⟦C⟧v
ph_tensor ⟦A⟧v ⟦B⟧v ⊙ ⦅Γ⦆v ⊆ ⟦C⟧v
c: bool
Γ: list iformula
A, B: iformula
H: A :: Γ ⊢[c] B
P: phase_space
v: nat → propset P
IHill: ⟦A⟧v ⊙ ⦅Γ⦆v ⊆ ⟦B⟧v
⦅Γ⦆v ⊆ ph_lolli ⟦A⟧v ⟦B⟧v
c: bool
Γ, Δ: list iformula
A, B, C: iformula
H: Γ ⊢[c] A
H0: B :: Δ ⊢[c] C
P: phase_space
v: nat → propset P
IHill1: ⦅Γ⦆v ⊆ ⟦A⟧v
IHill2: ⟦B⟧v ⊙ ⦅Δ⦆v ⊆ ⟦C⟧v
ph_lolli ⟦A⟧v ⟦B⟧v ⊙ ⦅Γ ++ Δ⦆v ⊆ ⟦C⟧v
c: bool
Γ: list iformula
A, B: iformula
H: Γ ⊢[c] A
H0: Γ ⊢[c] B
P: phase_space
v: nat → propset P
IHill1: ⦅Γ⦆v ⊆ ⟦A⟧v
IHill2: ⦅Γ⦆v ⊆ ⟦B⟧v
⦅Γ⦆v ⊆ ⟦A⟧v ∩ ⟦B⟧v
c: bool
Γ: list iformula
A, B, C: iformula
H: A :: Γ ⊢[c] C
P: phase_space
v: nat → propset P
IHill: ⟦A⟧v ⊙ ⦅Γ⦆v ⊆ ⟦C⟧v
⟦A⟧v ∩ ⟦B⟧v ⊙ ⦅Γ⦆v ⊆ ⟦C⟧v
c: bool
Γ: list iformula
A, B, C: iformula
H: B :: Γ ⊢[c] C
P: phase_space
v: nat → propset P
IHill: ⟦B⟧v ⊙ ⦅Γ⦆v ⊆ ⟦C⟧v
⟦A⟧v ∩ ⟦B⟧v ⊙ ⦅Γ⦆v ⊆ ⟦C⟧v
c: bool
Γ: list iformula
P: phase_space
v: nat → propset P
⦅Γ⦆v ⊆ ph_top
c: bool
Γ: list iformula
A, B: iformula
H: Γ ⊢[c] A
P: phase_space
v: nat → propset P
IHill: ⦅Γ⦆v ⊆ ⟦A⟧v
⦅Γ⦆v ⊆ ph_plus ⟦A⟧v ⟦B⟧v
c: bool
Γ: list iformula
A, B: iformula
H: Γ ⊢[c] B
P: phase_space
v: nat → propset P
IHill: ⦅Γ⦆v ⊆ ⟦B⟧v
⦅Γ⦆v ⊆ ph_plus ⟦A⟧v ⟦B⟧v
c: bool
Γ: list iformula
A, B, C: iformula
H: A :: Γ ⊢[c] C
H0: B :: Γ ⊢[c] C
P: phase_space
v: nat → propset P
IHill1: ⟦A⟧v ⊙ ⦅Γ⦆v ⊆ ⟦C⟧v
IHill2: ⟦B⟧v ⊙ ⦅Γ⦆v ⊆ ⟦C⟧v
ph_plus ⟦A⟧v ⟦B⟧v ⊙ ⦅Γ⦆v ⊆ ⟦C⟧v
c: bool
Γ: list iformula
C: iformula
P: phase_space
v: nat → propset P
ph_zero ⊙ ⦅Γ⦆v ⊆ ⟦C⟧v
c: bool
Σ: list iformula
A: iformula
H: ‼Σ ⊢[c] A
P: phase_space
v: nat → propset P
IHill: ⦅‼Σ⦆v ⊆ ⟦A⟧v
⦅‼Σ⦆v ⊆ ph_bang ⟦A⟧v
c: bool
Γ: list iformula
A, C: iformula
H: A :: Γ ⊢[c] C
P: phase_space
v: nat → propset P
IHill: ⟦A⟧v ⊙ ⦅Γ⦆v ⊆ ⟦C⟧v
ph_bang ⟦A⟧v ⊙ ⦅Γ⦆v ⊆ ⟦C⟧v
c: bool
Γ: list iformula
A, C: iformula
H: Γ ⊢[c] C
P: phase_space
v: nat → propset P
IHill: ⦅Γ⦆v ⊆ ⟦C⟧v
ph_bang ⟦A⟧v ⊙ ⦅Γ⦆v ⊆ ⟦C⟧v
c: bool
Γ: list iformula
A, C: iformula
H: !A :: !A :: Γ ⊢[c] C
P: phase_space
v: nat → propset P
IHill: ph_bang ⟦A⟧v ⊙ (ph_bang ⟦A⟧v ⊙ ⦅Γ⦆v) ⊆ ⟦C⟧v
ph_bang ⟦A⟧v ⊙ ⦅Γ⦆v ⊆ ⟦C⟧v
  - (* ax: ⟦A⟧ ⊙ {ε} ⊆ ⟦A⟧ *)c: bool
A: iformula
P: phase_space
v: nat → propset P
⟦A⟧v ⊙ one_set ⊆ ⟦A⟧v
    rewrite prod_comm.c: bool
A: iformula
P: phase_space
v: nat → propset P
one_set ⊙ ⟦A⟧v ⊆ ⟦A⟧v apply prod_one_l; [apply interp_fact | done].
  - (* cut: feed the Γ-part into the A-hole of A :: Δ *)c: bool
Γ, Δ: list iformula
A, C: iformula
H: c = true
H0: Γ ⊢[c] A
H1: A :: Δ ⊢[c] C
P: phase_space
v: nat → propset P
IHill1: ⦅Γ⦆v ⊆ ⟦A⟧v
IHill2: ⟦A⟧v ⊙ ⦅Δ⦆v ⊆ ⟦C⟧v
⦅Γ ++ Δ⦆v ⊆ ⟦C⟧v
    by rewrite ctx_app, IHill1.
  - (* ex *)c: bool
Γ, Γ': list iformula
C: iformula
H: Γ ≡ₚ Γ'
H0: Γ ⊢[c] C
P: phase_space
v: nat → propset P
IHill: ⦅Γ⦆v ⊆ ⟦C⟧v
⦅Γ'⦆v ⊆ ⟦C⟧v
    rewrite <- IHill.c: bool
Γ, Γ': list iformula
C: iformula
H: Γ ≡ₚ Γ'
H0: Γ ⊢[c] C
P: phase_space
v: nat → propset P
IHill: ⦅Γ⦆v ⊆ ⟦C⟧v
⦅Γ'⦆v ⊆ ⦅Γ⦆v apply ctx_perm.c: bool
Γ, Γ': list iformula
C: iformula
H: Γ ≡ₚ Γ'
H0: Γ ⊢[c] C
P: phase_space
v: nat → propset P
IHill: ⦅Γ⦆v ⊆ ⟦C⟧v
Γ' ≡ₚ Γ by symmetry.
  - (* 𝟙R *)c: bool
P: phase_space
v: nat → propset P
one_set ⊆ ph_one
    apply ph_cl_ext.
  - (* 𝟙L *)c: bool
Γ: list iformula
C: iformula
H: Γ ⊢[c] C
P: phase_space
v: nat → propset P
IHill: ⦅Γ⦆v ⊆ ⟦C⟧v
ph_one ⊙ ⦅Γ⦆v ⊆ ⟦C⟧v
    apply prod_cl_l, prod_one_l; auto using interp_fact.
  - (* ⊗R *)c: bool
Γ, Δ: list iformula
A, B: iformula
H: Γ ⊢[c] A
H0: Δ ⊢[c] B
P: phase_space
v: nat → propset P
IHill1: ⦅Γ⦆v ⊆ ⟦A⟧v
IHill2: ⦅Δ⦆v ⊆ ⟦B⟧v
⦅Γ ++ Δ⦆v ⊆ ph_tensor ⟦A⟧v ⟦B⟧v
    rewrite ctx_app, IHill1, IHill2.c: bool
Γ, Δ: list iformula
A, B: iformula
H: Γ ⊢[c] A
H0: Δ ⊢[c] B
P: phase_space
v: nat → propset P
IHill1: ⦅Γ⦆v ⊆ ⟦A⟧v
IHill2: ⦅Δ⦆v ⊆ ⟦B⟧v
⟦A⟧v ⊙ ⟦B⟧v ⊆ ph_tensor ⟦A⟧v ⟦B⟧v apply ph_cl_ext.
  - (* ⊗L *)c: bool
Γ: list iformula
A, B, C: iformula
H: A :: B :: Γ ⊢[c] C
P: phase_space
v: nat → propset P
IHill: ⟦A⟧v ⊙ (⟦B⟧v ⊙ ⦅Γ⦆v) ⊆ ⟦C⟧v
ph_tensor ⟦A⟧v ⟦B⟧v ⊙ ⦅Γ⦆v ⊆ ⟦C⟧v
    apply tensor_l; auto using interp_fact.
  - (* ⊸R *)c: bool
Γ: list iformula
A, B: iformula
H: A :: Γ ⊢[c] B
P: phase_space
v: nat → propset P
IHill: ⟦A⟧v ⊙ ⦅Γ⦆v ⊆ ⟦B⟧v
⦅Γ⦆v ⊆ ph_lolli ⟦A⟧v ⟦B⟧v
    apply lolli_intro.c: bool
Γ: list iformula
A, B: iformula
H: A :: Γ ⊢[c] B
P: phase_space
v: nat → propset P
IHill: ⟦A⟧v ⊙ ⦅Γ⦆v ⊆ ⟦B⟧v
⦅Γ⦆v ⊙ ⟦A⟧v ⊆ ⟦B⟧v by rewrite prod_comm.
  - (* ⊸L: (A ⊸ B) ⊙ (Γ ⊙ Δ) ⊆ ((A ⊸ B) ⊙ A) ⊙ Δ ⊆ B ⊙ Δ *)c: bool
Γ, Δ: list iformula
A, B, C: iformula
H: Γ ⊢[c] A
H0: B :: Δ ⊢[c] C
P: phase_space
v: nat → propset P
IHill1: ⦅Γ⦆v ⊆ ⟦A⟧v
IHill2: ⟦B⟧v ⊙ ⦅Δ⦆v ⊆ ⟦C⟧v
ph_lolli ⟦A⟧v ⟦B⟧v ⊙ ⦅Γ ++ Δ⦆v ⊆ ⟦C⟧v
    by rewrite ctx_app, prod_assoc_l, IHill1, lolli_elim by apply interp_fact.
  - (* &R *)c: bool
Γ: list iformula
A, B: iformula
H: Γ ⊢[c] A
H0: Γ ⊢[c] B
P: phase_space
v: nat → propset P
IHill1: ⦅Γ⦆v ⊆ ⟦A⟧v
IHill2: ⦅Γ⦆v ⊆ ⟦B⟧v
⦅Γ⦆v ⊆ ⟦A⟧v ∩ ⟦B⟧v
    set_solver.
  - (* &L₁ *)c: bool
Γ: list iformula
A, B, C: iformula
H: A :: Γ ⊢[c] C
P: phase_space
v: nat → propset P
IHill: ⟦A⟧v ⊙ ⦅Γ⦆v ⊆ ⟦C⟧v
⟦A⟧v ∩ ⟦B⟧v ⊙ ⦅Γ⦆v ⊆ ⟦C⟧v
    by rewrite intersection_subseteq_l.
  - (* &L₂ *)c: bool
Γ: list iformula
A, B, C: iformula
H: B :: Γ ⊢[c] C
P: phase_space
v: nat → propset P
IHill: ⟦B⟧v ⊙ ⦅Γ⦆v ⊆ ⟦C⟧v
⟦A⟧v ∩ ⟦B⟧v ⊙ ⦅Γ⦆v ⊆ ⟦C⟧v
    by rewrite intersection_subseteq_r.
  - (* ⊤R *)c: bool
Γ: list iformula
P: phase_space
v: nat → propset P
⦅Γ⦆v ⊆ ph_top
    intros m _.c: bool
Γ: list iformula
P: phase_space
v: nat → propset P
m: P
m ∈ ph_top apply elem_of_top.
  - (* ⊕R₁ *)c: bool
Γ: list iformula
A, B: iformula
H: Γ ⊢[c] A
P: phase_space
v: nat → propset P
IHill: ⦅Γ⦆v ⊆ ⟦A⟧v
⦅Γ⦆v ⊆ ph_plus ⟦A⟧v ⟦B⟧v
    rewrite IHill.c: bool
Γ: list iformula
A, B: iformula
H: Γ ⊢[c] A
P: phase_space
v: nat → propset P
IHill: ⦅Γ⦆v ⊆ ⟦A⟧v
⟦A⟧v ⊆ ph_plus ⟦A⟧v ⟦B⟧v etrans; [| apply ph_cl_ext].c: bool
Γ: list iformula
A, B: iformula
H: Γ ⊢[c] A
P: phase_space
v: nat → propset P
IHill: ⦅Γ⦆v ⊆ ⟦A⟧v
⟦A⟧v ⊆ ⟦A⟧v ∪ ⟦B⟧v set_solver.
  - (* ⊕R₂ *)c: bool
Γ: list iformula
A, B: iformula
H: Γ ⊢[c] B
P: phase_space
v: nat → propset P
IHill: ⦅Γ⦆v ⊆ ⟦B⟧v
⦅Γ⦆v ⊆ ph_plus ⟦A⟧v ⟦B⟧v
    rewrite IHill.c: bool
Γ: list iformula
A, B: iformula
H: Γ ⊢[c] B
P: phase_space
v: nat → propset P
IHill: ⦅Γ⦆v ⊆ ⟦B⟧v
⟦B⟧v ⊆ ph_plus ⟦A⟧v ⟦B⟧v etrans; [| apply ph_cl_ext].c: bool
Γ: list iformula
A, B: iformula
H: Γ ⊢[c] B
P: phase_space
v: nat → propset P
IHill: ⦅Γ⦆v ⊆ ⟦B⟧v
⟦B⟧v ⊆ ⟦A⟧v ∪ ⟦B⟧v set_solver.
  - (* ⊕L: a generator of ⟦A ⊕ B⟧ is in ⟦A⟧ or in ⟦B⟧ *)c: bool
Γ: list iformula
A, B, C: iformula
H: A :: Γ ⊢[c] C
H0: B :: Γ ⊢[c] C
P: phase_space
v: nat → propset P
IHill1: ⟦A⟧v ⊙ ⦅Γ⦆v ⊆ ⟦C⟧v
IHill2: ⟦B⟧v ⊙ ⦅Γ⦆v ⊆ ⟦C⟧v
ph_plus ⟦A⟧v ⟦B⟧v ⊙ ⦅Γ⦆v ⊆ ⟦C⟧v
    apply prod_cl_l; [apply interp_fact | set_solver].
  - (* 𝟘L: ⟦𝟘⟧ has no generators *)c: bool
Γ: list iformula
C: iformula
P: phase_space
v: nat → propset P
ph_zero ⊙ ⦅Γ⦆v ⊆ ⟦C⟧v
    apply prod_cl_l; [apply interp_fact | set_solver].
  - (* !R (promotion): the bag for ‼Σ is reusable *)c: bool
Σ: list iformula
A: iformula
H: ‼Σ ⊢[c] A
P: phase_space
v: nat → propset P
IHill: ⦅‼Σ⦆v ⊆ ⟦A⟧v
⦅‼Σ⦆v ⊆ ph_bang ⟦A⟧v
    rewrite ctx_bangs.c: bool
Σ: list iformula
A: iformula
H: ‼Σ ⊢[c] A
P: phase_space
v: nat → propset P
IHill: ⦅‼Σ⦆v ⊆ ⟦A⟧v
cl (⦅‼Σ⦆v ∩ J) ⊆ ph_bang ⟦A⟧v apply cl_mono.c: bool
Σ: list iformula
A: iformula
H: ‼Σ ⊢[c] A
P: phase_space
v: nat → propset P
IHill: ⦅‼Σ⦆v ⊆ ⟦A⟧v
⦅‼Σ⦆v ∩ J ⊆ ⟦A⟧v ∩ J set_solver.
  - (* !D (dereliction): generators of ⟦!A⟧ are in ⟦A⟧ *)c: bool
Γ: list iformula
A, C: iformula
H: A :: Γ ⊢[c] C
P: phase_space
v: nat → propset P
IHill: ⟦A⟧v ⊙ ⦅Γ⦆v ⊆ ⟦C⟧v
ph_bang ⟦A⟧v ⊙ ⦅Γ⦆v ⊆ ⟦C⟧v
    apply prod_cl_l; [apply interp_fact |].c: bool
Γ: list iformula
A, C: iformula
H: A :: Γ ⊢[c] C
P: phase_space
v: nat → propset P
IHill: ⟦A⟧v ⊙ ⦅Γ⦆v ⊆ ⟦C⟧v
⟦A⟧v ∩ J ⊙ ⦅Γ⦆v ⊆ ⟦C⟧v by rewrite intersection_subseteq_l.
  - (* !W (weakening) *)c: bool
Γ: list iformula
A, C: iformula
H: Γ ⊢[c] C
P: phase_space
v: nat → propset P
IHill: ⦅Γ⦆v ⊆ ⟦C⟧v
ph_bang ⟦A⟧v ⊙ ⦅Γ⦆v ⊆ ⟦C⟧v
    rewrite bang_weak.c: bool
Γ: list iformula
A, C: iformula
H: Γ ⊢[c] C
P: phase_space
v: nat → propset P
IHill: ⦅Γ⦆v ⊆ ⟦C⟧v
ph_one ⊙ ⦅Γ⦆v ⊆ ⟦C⟧v apply prod_cl_l, prod_one_l; auto using interp_fact.
  - (* !C (contraction) *)c: bool
Γ: list iformula
A, C: iformula
H: !A :: !A :: Γ ⊢[c] C
P: phase_space
v: nat → propset P
IHill: ph_bang ⟦A⟧v ⊙ (ph_bang ⟦A⟧v ⊙ ⦅Γ⦆v) ⊆ ⟦C⟧v
ph_bang ⟦A⟧v ⊙ ⦅Γ⦆v ⊆ ⟦C⟧v
    rewrite bang_contr.c: bool
Γ: list iformula
A, C: iformula
H: !A :: !A :: Γ ⊢[c] C
P: phase_space
v: nat → propset P
IHill: ph_bang ⟦A⟧v ⊙ (ph_bang ⟦A⟧v ⊙ ⦅Γ⦆v) ⊆ ⟦C⟧v
ph_tensor (ph_bang ⟦A⟧v) (ph_bang ⟦A⟧v) ⊙ ⦅Γ⦆v ⊆ ⟦C⟧v apply tensor_l; auto using interp_fact.
Qed.

Using the semantics: what ILL cannot prove

Soundness gives a way to show that a sequent is not derivable: find a phase space in which it fails. One small phase space is enough for every example below:

phases are natural numbers, counting how many resources a bag holds;
· is + and ε is 0;
cl is the identity, so every set is a fact;
the reusable phases are J = {0}: only the empty bag is free to copy or drop;
⊥ denotes ∅.

Each variable $p denotes {1}, one unit of resource.

Definition counting_space : phase_space.phase_space
Proof.phase_space
  refine (Build_phase_space nat (=) Nat.add 0 (λ X, X) {[ n | n = 0 ]} ∅
            _ _ _ _ _ _ _ _ _ _ _ _ _ _).∀ x y z : nat, x + (y + z) ≡ x + y + z
∀ x y : nat, x + y ≡ y + x
∀ x : nat, 0 + x ≡ x
∀ X : propset nat, X ⊆ X
∀ X Y : propset nat, X ⊆ Y → X ⊆ Y
∀ (X : propset nat) (x y : nat), x ≡ y → x ∈ X → y ∈ X
∀ (X Y : propset nat) (x y : nat),
  x ∈ X → y ∈ Y → x + y ∈ prod_with equiv Nat.add X Y
∀ x y : nat, x ≡ y → x ∈ {[ n | n = 0 ]} → y ∈ {[ n | n = 0 ]}
0 ∈ {[ n | n = 0 ]}
∀ x y : nat,
  x ∈ {[ n | n = 0 ]} → y ∈ {[ n | n = 0 ]} → x + y ∈ {[ n | n = 0 ]}
∀ x : nat, x ∈ {[ n | n = 0 ]} → x ∈ {[ z | z ≡ 0 ]}
∀ x : nat, x ∈ {[ n | n = 0 ]} → x ∈ {[ z | z ≡ x + x ]}
  (* the monoid laws are arithmetic; the closure laws are trivial since
     cl is the identity *)
  all: try apply _; intros; unfold equiv, prod_with in *; set_unfold;
    naive_solver lia.
Defined.

Definition one_each : nat -> propset counting_space := λ _, {[ n | n = 1 ]}.

In counting_space, every set membership reduces to arithmetic. count unfolds the definitions and leaves the arithmetic behind. set_unfold can expose new redexes of interp, so it runs a few rounds.

Ltac count_unfold :=
  cbn [interp interp_ctx counting_space carrier ph_cl ph_op ph_e
       ph_J ph_bot ph_equiv] in *;
  unfold ph_one, ph_tensor, ph_plus, ph_zero, ph_bang, one_each, equiv in *.
Ltac count := do 3 (count_unfold; set_unfold).

Lemma counting_sound {Γ A} : Γ ⊢ A -> ∀ m, m ∈ ⦅Γ⦆one_each -> m ∈ ⟦A⟧one_each.Γ: list iformula
A: iformula
Γ ⊢ A → ∀ m : counting_space, m ∈ ⦅Γ⦆one_each → m ∈ ⟦A⟧one_each
Proof.Γ: list iformula
A: iformula
Γ ⊢ A → ∀ m : counting_space, m ∈ ⦅Γ⦆one_each → m ∈ ⟦A⟧one_each intros H.Γ: list iformula
A: iformula
H: Γ ⊢ A
∀ m : counting_space, m ∈ ⦅Γ⦆one_each → m ∈ ⟦A⟧one_each exact (soundness _ _ _ H counting_space one_each). Qed.

Every refutation below has the same shape: name a bag m that is in ⦅Γ⦆ but not in ⟦A⟧. After count, both conditions are statements about natural numbers.

Lemma counting_refute m Γ A :
  m ∈ ⦅Γ⦆one_each -> m ∉ ⟦A⟧one_each -> ¬ (Γ ⊢ A).m: counting_space
Γ: list iformula
A: iformula
m ∈ ⦅Γ⦆one_each → m ∉ ⟦A⟧one_each → ¬ (Γ ⊢ A)
Proof.m: counting_space
Γ: list iformula
A: iformula
m ∈ ⦅Γ⦆one_each → m ∉ ⟦A⟧one_each → ¬ (Γ ⊢ A) intros Hm HA H.m: counting_space
Γ: list iformula
A: iformula
Hm: m ∈ ⦅Γ⦆one_each
HA: m ∉ ⟦A⟧one_each
H: Γ ⊢ A
False by apply HA, (counting_sound H). Qed.

No contraction: one A does not give two. The bag 1 is not 2.

Theorem no_contraction : ¬ ([$0] ⊢ $0 ⊗ $0).¬ ([$0] ⊢ $0 ⊗ $0)
Proof.¬ ([$0] ⊢ $0 ⊗ $0) apply (counting_refute 1); count; naive_solver lia. Qed.

No weakening: a hypothesis cannot be ignored. The bag 2 is not 1.

Theorem no_weakening : ¬ ([$0; $1] ⊢ $0).¬ ([$0; $1] ⊢ $0)
Proof.¬ ([$0; $1] ⊢ $0) apply (counting_refute 2); count; naive_solver lia. Qed.

No free lunch: one euro buys a coffee or a tea, never both.

Theorem no_free_lunch : ¬ ([euro] ⊢ coffee ⊗ tea).¬ ([euro] ⊢ coffee ⊗ tea)
Proof.¬ ([euro] ⊢ coffee ⊗ tea)
  unfold euro, coffee, tea.¬ ([$0] ⊢ $1 ⊗ $2) apply (counting_refute 1); count; naive_solver lia.
Qed.

& is not ⊗: a choice of A or B does not give both.

Theorem with_is_not_tensor : ¬ ([$0 & $1] ⊢ $0 ⊗ $1).¬ ([$0 & $1] ⊢ $0 ⊗ $1)
Proof.¬ ([$0 & $1] ⊢ $0 ⊗ $1) apply (counting_refute 1); count; naive_solver lia. Qed.

A single resource cannot be promoted to an unlimited supply. The bag 1 is not reusable.

Theorem no_promotion : ¬ ([$0] ⊢ !$0).¬ ([$0] ⊢ !$0)
Proof.¬ ([$0] ⊢ !$0) apply (counting_refute 1); count; naive_solver lia. Qed.

Consistency: 𝟘 cannot be proved from nothing. ⟦𝟘⟧ = ∅.

Theorem consistency : ¬ ([] ⊢ 𝟘).¬ ([] ⊢ 𝟘)
Proof.¬ ([] ⊢ 𝟘) apply (counting_refute 0); count; naive_solver lia. Qed.

The same facts, stated as implications with no hypotheses. In Types/CurryHoward.v they become statements about which programs exist. The empty bag 0 does not turn 1 into 2, nor 2 into 1.

Theorem no_duplicator : ¬ ([] ⊢ $0 ⊸ $0 ⊗ $0).¬ ([] ⊢ $0 ⊸ $0 ⊗ $0)
Proof.¬ ([] ⊢ $0 ⊸ $0 ⊗ $0) apply (counting_refute 0); count; naive_solver lia. Qed.

Theorem no_eraser : ¬ ([] ⊢ $0 ⊗ $1 ⊸ $0).¬ ([] ⊢ $0 ⊗ $1 ⊸ $0)
Proof.¬ ([] ⊢ $0 ⊗ $1 ⊸ $0)
  apply (counting_refute 0); count; [done |].¬ ∀ x : nat, (∃ x0 x1 : nat, x0 = 1 ∧ x1 = 1 ∧ x = x0 + x1) → x = 1
  intros H.H: ∀ x : nat, (∃ x0 x1 : nat, x0 = 1 ∧ x1 = 1 ∧ x = x0 + x1) → x = 1
False enough (2 = 1) by lia.H: ∀ x : nat, (∃ x0 x1 : nat, x0 = 1 ∧ x1 = 1 ∧ x = x0 + x1) → x = 1
2 = 1 apply H.H: ∀ x : nat, (∃ x0 x1 : nat, x0 = 1 ∧ x1 = 1 ∧ x = x0 + x1) → x = 1
∃ x x0 : nat, x = 1 ∧ x0 = 1 ∧ 2 = x + x0 by exists 1, 1.
Qed.

Double-negation elimination fails in ILL. With ⊥ = ∅, the set ∼$0 = $0 ⊸ ⊥ is empty, so ∼∼$0 holds of every bag, including bags that are not {1}, such as 5. Comparison.v contrasts this with CLL, where ∼∼A ⊢ A is provable.

Theorem no_dne : ¬ ([∼∼$0] ⊢ $0).¬ ([∼∼$0] ⊢ $0)
Proof.¬ ([∼∼$0] ⊢ $0)
  apply (counting_refute 5); count; [| lia].∃ x x0 : nat,
  (nat → (∀ x1 : nat, x1 = 1 → False) → False) ∧ x0 = 0 ∧ 5 = x + x0
  exists 5, 0.(nat → (∀ x : nat, x = 1 → False) → False) ∧ 0 = 0 ∧ 5 = 5 + 0 split_and!; [| done..].nat → (∀ x : nat, x = 1 → False) → False intros _ Hf.Hf: ∀ x : nat, x = 1 → False
False by apply (Hf 1).
Qed.