Intuitionistic.CutElim: completeness and cut elimination for ILL

Phase.v proved soundness: whatever is provable, with or without cuts, is valid in every phase space. This file proves the converse: whatever is valid has a cut-free proof. Chaining the two gives cut elimination:

         Γ ⊢ A   ──soundness──▶   Γ ⊨ A   ──completeness──▶   Γ ⊢cf A

This is Okada's semantic proof of cut elimination (1996, 1999). Gentzen's syntactic proof rewrites a derivation step by step, pushing each cut upwards. It needs a delicate termination argument, and the ! rules make that worse (they call for a "multicut"). The semantic proof sidesteps all of it. We build one phase space out of cut-free provability, and soundness does the rest.

The syntactic phase space

a phase is a context Γ : list iformula, taken up to permutation;
· is ++ and ε is [];
the closure of a set X of contexts is

          cl X = { Γ | for every "test" (Δ, C):
                         if  x ++ Δ ⊢cf C  for all x ∈ X,
                         then Γ ++ Δ ⊢cf C }

Γ lies in cl X when it passes every test that all members of X pass;

the reusable phases are the banged contexts ‼Σ;
⊥ denotes the contexts that prove ⊥ without cut.

Okada's lemma

In this model, every formula A satisfies

        [A] ∈ ⟦A⟧ ⊆ { Γ | Γ ⊢cf A }

Given that, take a provable Γ ⊢ C. Soundness gives ⦅Γ⦆ ⊆ ⟦C⟧, and Γ ∈ ⦅Γ⦆ holds by the left half of the lemma. So Γ ∈ ⟦C⟧, and the right half gives Γ ⊢cf C.

From LinearLogic.Intuitionistic Require Export Phase.[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]

The closure operator on contexts

Definition syn_cl (X : propset (list iformula)) : propset (list iformula) :=
  {[ Γ | ∀ Δ C, (∀ x, x ∈ X -> x ++ Δ ⊢cf C) -> Γ ++ Δ ⊢cf C ]}.

Lemma elem_of_syn_cl X Γ :
  Γ ∈ syn_cl X ↔ ∀ Δ C, (∀ x, x ∈ X -> x ++ Δ ⊢cf C) -> Γ ++ Δ ⊢cf C.X: propset (list iformula)
Γ: list iformula
Γ ∈ syn_cl X
↔ ∀ (Δ : list iformula) (C : iformula),
    (∀ x : list iformula, x ∈ X → x ++ Δ ⊢cf C) → Γ ++ Δ ⊢cf C
Proof.X: propset (list iformula)
Γ: list iformula
Γ ∈ syn_cl X
↔ ∀ (Δ : list iformula) (C : iformula),
    (∀ x : list iformula, x ∈ X → x ++ Δ ⊢cf C) → Γ ++ Δ ⊢cf C unfold syn_cl.X: propset (list iformula)
Γ: list iformula
Γ
∈ {[ Γ0 | ∀ (Δ : list iformula) (C : iformula),
            (∀ x : list iformula, x ∈ X → x ++ Δ ⊢cf C) → Γ0 ++ Δ ⊢cf C ]}
↔ ∀ (Δ : list iformula) (C : iformula),
    (∀ x : list iformula, x ∈ X → x ++ Δ ⊢cf C) → Γ ++ Δ ⊢cf C by rewrite elem_of_PropSet. Qed.

stdpp's set_unfold can see through syn_cl and, below, down.

#[global] Instance set_unfold_syn_cl X Γ :
  SetUnfoldElemOf Γ (syn_cl X)
    (∀ Δ C, (∀ x, x ∈ X -> x ++ Δ ⊢cf C) -> Γ ++ Δ ⊢cf C).X: propset (list iformula)
Γ: list iformula
SetUnfoldElemOf Γ (syn_cl X)
  (∀ (Δ : list iformula) (C : iformula),
     (∀ x : list iformula, x ∈ X → x ++ Δ ⊢cf C) → Γ ++ Δ ⊢cf C)
Proof.X: propset (list iformula)
Γ: list iformula
SetUnfoldElemOf Γ (syn_cl X)
  (∀ (Δ : list iformula) (C : iformula),
     (∀ x : list iformula, x ∈ X → x ++ Δ ⊢cf C) → Γ ++ Δ ⊢cf C) constructor.X: propset (list iformula)
Γ: list iformula
Γ ∈ syn_cl X
↔ ∀ (Δ : list iformula) (C : iformula),
    (∀ x : list iformula, x ∈ X → x ++ Δ ⊢cf C) → Γ ++ Δ ⊢cf C apply elem_of_syn_cl. Qed.

The syntactic phase space

After set_unfold, every axiom is a statement about tests, and most are one-liners. The two interesting ones are stability (a test of a product is split into a test of each factor) and the axioms for J, which are exactly the derived rules weaken_bangs and contract_bangs of Sequent.v.

Definition syntactic : phase_space.phase_space
Proof.phase_space
  refine (Build_phase_space (list iformula) (@Permutation iformula) app []
            syn_cl {[ Γ | ∃ Σ, Γ = ‼Σ ]} {[ Γ | Γ ⊢cf ⊥ ]}
            _ _ _ _ _ _ _ _ _ _ _ _ _ _);
    try apply _; unfold prod_with; set_unfold.∀ x x0 x1 : list iformula, x ++ x0 ++ x1 ≡ (x ++ x0) ++ x1
∀ x x0 : list iformula, x ++ x0 ≡ x0 ++ x
∀ x : list iformula, x ≡ x
∀ (x : propset (list iformula)) (x0 : list iformula),
  x0 ∈ x
  → ∀ (Δ : list iformula) (C : iformula),
      (∀ x1 : list iformula, x1 ∈ x → x1 ++ Δ ⊢cf C) → x0 ++ Δ ⊢cf C
∀ x x0 : propset (list iformula),
  (∀ x1 : list iformula,
     x1 ∈ x
     → ∀ (Δ : list iformula) (C : iformula),
         (∀ x2 : list iformula, x2 ∈ x0 → x2 ++ Δ ⊢cf C) → x1 ++ Δ ⊢cf C)
  → ∀ x1 : list iformula,
      (∀ (Δ : list iformula) (C : iformula),
         (∀ x2 : list iformula, x2 ∈ x → x2 ++ Δ ⊢cf C) → x1 ++ Δ ⊢cf C)
      → ∀ (Δ : list iformula) (C : iformula),
          (∀ x2 : list iformula, x2 ∈ x0 → x2 ++ Δ ⊢cf C) → x1 ++ Δ ⊢cf C
∀ (x : propset (list iformula)) (x0 x1 : list iformula),
  x0 ≡ x1
  → (∀ (Δ : list iformula) (C : iformula),
       (∀ x2 : list iformula, x2 ∈ x → x2 ++ Δ ⊢cf C) → x0 ++ Δ ⊢cf C)
    → ∀ (Δ : list iformula) (C : iformula),
        (∀ x2 : list iformula, x2 ∈ x → x2 ++ Δ ⊢cf C) → x1 ++ Δ ⊢cf C
∀ (x x0 : propset (list iformula)) (x1 x2 : list iformula),
  (∀ (Δ : list iformula) (C : iformula),
     (∀ x3 : list iformula, x3 ∈ x → x3 ++ Δ ⊢cf C) → x1 ++ Δ ⊢cf C)
  → (∀ (Δ : list iformula) (C : iformula),
       (∀ x3 : list iformula, x3 ∈ x0 → x3 ++ Δ ⊢cf C) → x2 ++ Δ ⊢cf C)
    → ∀ (Δ : list iformula) (C : iformula),
        (∀ x3 : list iformula,
           x3 ∈ {[ z | ∃ a b : list iformula, a ∈ x ∧ b ∈ x0 ∧ z ≡ a ++ b ]}
           → x3 ++ Δ ⊢cf C)
        → (x1 ++ x2) ++ Δ ⊢cf C
∀ x x0 : list iformula,
  x ≡ x0 → (∃ x1 : list iformula, x = ‼x1) → ∃ x1 : list iformula, x0 = ‼x1
∃ x : list iformula, [] = ‼x
∀ x x0 : list iformula,
  (∃ x1 : list iformula, x = ‼x1)
  → (∃ x1 : list iformula, x0 = ‼x1) → ∃ x1 : list iformula, x ++ x0 = ‼x1
∀ x : list iformula,
  (∃ x0 : list iformula, x = ‼x0)
  → ∀ (Δ : list iformula) (C : iformula),
      (∀ x0 : list iformula, x0 ∈ {[ z | z ≡ [] ]} → x0 ++ Δ ⊢cf C)
      → x ++ Δ ⊢cf C
∀ x : list iformula,
  (∃ x0 : list iformula, x = ‼x0)
  → ∀ (Δ : list iformula) (C : iformula),
      (∀ x0 : list iformula, x0 ∈ {[ z | z ≡ x ++ x ]} → x0 ++ Δ ⊢cf C)
      → x ++ Δ ⊢cf C
  - (* assoc *)∀ x x0 x1 : list iformula, x ++ x0 ++ x1 ≡ (x ++ x0) ++ x1 intros.x, x0, x1: list iformula
x ++ x0 ++ x1 ≡ (x ++ x0) ++ x1 by rewrite (assoc_L (++)).
  - (* comm *)∀ x x0 : list iformula, x ++ x0 ≡ x0 ++ x intros.x, x0: list iformula
x ++ x0 ≡ x0 ++ x apply Permutation_app_comm.
  - (* unit *)∀ x : list iformula, x ≡ x done.
  - (* cl_ext: members of X pass every test that X passes *)∀ (x : propset (list iformula)) (x0 : list iformula),
  x0 ∈ x
  → ∀ (Δ : list iformula) (C : iformula),
      (∀ x1 : list iformula, x1 ∈ x → x1 ++ Δ ⊢cf C) → x0 ++ Δ ⊢cf C
    intros X Γ HΓ Δ C H.X: propset (list iformula)
Γ: list iformula
HΓ: Γ ∈ X
Δ: list iformula
C: iformula
H: ∀ x : list iformula, x ∈ X → x ++ Δ ⊢cf C
Γ ++ Δ ⊢cf C by apply H.
  - (* cl_least: a test passed by Y is passed by X ⊆ cl Y, hence by cl X *)∀ x x0 : propset (list iformula),
  (∀ x1 : list iformula,
     x1 ∈ x
     → ∀ (Δ : list iformula) (C : iformula),
         (∀ x2 : list iformula, x2 ∈ x0 → x2 ++ Δ ⊢cf C) → x1 ++ Δ ⊢cf C)
  → ∀ x1 : list iformula,
      (∀ (Δ : list iformula) (C : iformula),
         (∀ x2 : list iformula, x2 ∈ x → x2 ++ Δ ⊢cf C) → x1 ++ Δ ⊢cf C)
      → ∀ (Δ : list iformula) (C : iformula),
          (∀ x2 : list iformula, x2 ∈ x0 → x2 ++ Δ ⊢cf C) → x1 ++ Δ ⊢cf C
    intros X Y HXY Γ HΓ Δ C H.X, Y: propset (list iformula)
HXY: ∀ x : list iformula,
  x ∈ X
  → ∀ (Δ : list iformula) (C : iformula),
      (∀ x0 : list iformula, x0 ∈ Y → x0 ++ Δ ⊢cf C) → x ++ Δ ⊢cf C
Γ: list iformula
HΓ: ∀ (Δ : list iformula) (C : iformula),
  (∀ x : list iformula, x ∈ X → x ++ Δ ⊢cf C) → Γ ++ Δ ⊢cf C
Δ: list iformula
C: iformula
H: ∀ x : list iformula, x ∈ Y → x ++ Δ ⊢cf C
Γ ++ Δ ⊢cf C apply HΓ.X, Y: propset (list iformula)
HXY: ∀ x : list iformula,
  x ∈ X
  → ∀ (Δ : list iformula) (C : iformula),
      (∀ x0 : list iformula, x0 ∈ Y → x0 ++ Δ ⊢cf C) → x ++ Δ ⊢cf C
Γ: list iformula
HΓ: ∀ (Δ : list iformula) (C : iformula),
  (∀ x : list iformula, x ∈ X → x ++ Δ ⊢cf C) → Γ ++ Δ ⊢cf C
Δ: list iformula
C: iformula
H: ∀ x : list iformula, x ∈ Y → x ++ Δ ⊢cf C
∀ x : list iformula, x ∈ X → x ++ Δ ⊢cf C intros x Hx.X, Y: propset (list iformula)
HXY: ∀ x : list iformula,
  x ∈ X
  → ∀ (Δ : list iformula) (C : iformula),
      (∀ x0 : list iformula, x0 ∈ Y → x0 ++ Δ ⊢cf C) → x ++ Δ ⊢cf C
Γ: list iformula
HΓ: ∀ (Δ : list iformula) (C : iformula),
  (∀ x : list iformula, x ∈ X → x ++ Δ ⊢cf C) → Γ ++ Δ ⊢cf C
Δ: list iformula
C: iformula
H: ∀ x : list iformula, x ∈ Y → x ++ Δ ⊢cf C
x: list iformula
Hx: x ∈ X
x ++ Δ ⊢cf C by apply HXY.
  - (* cl respects ≡ₚ: by exchange *)∀ (x : propset (list iformula)) (x0 x1 : list iformula),
  x0 ≡ x1
  → (∀ (Δ : list iformula) (C : iformula),
       (∀ x2 : list iformula, x2 ∈ x → x2 ++ Δ ⊢cf C) → x0 ++ Δ ⊢cf C)
    → ∀ (Δ : list iformula) (C : iformula),
        (∀ x2 : list iformula, x2 ∈ x → x2 ++ Δ ⊢cf C) → x1 ++ Δ ⊢cf C
    intros X Γ Γ' HΓ H Δ C HX.X: propset (list iformula)
Γ, Γ': list iformula
HΓ: Γ ≡ Γ'
H: ∀ (Δ : list iformula) (C : iformula),
  (∀ x : list iformula, x ∈ X → x ++ Δ ⊢cf C) → Γ ++ Δ ⊢cf C
Δ: list iformula
C: iformula
HX: ∀ x : list iformula, x ∈ X → x ++ Δ ⊢cf C
Γ' ++ Δ ⊢cf C apply (ex' (H Δ C HX)).X: propset (list iformula)
Γ, Γ': list iformula
HΓ: Γ ≡ Γ'
H: ∀ (Δ : list iformula) (C : iformula),
  (∀ x : list iformula, x ∈ X → x ++ Δ ⊢cf C) → Γ ++ Δ ⊢cf C
Δ: list iformula
C: iformula
HX: ∀ x : list iformula, x ∈ X → x ++ Δ ⊢cf C
Γ ++ Δ ≡ₚ Γ' ++ Δ by rewrite HΓ.
  - (* stability: test Γ with Γ' ++ Δ, then test Γ' with x ++ Δ *)∀ (x x0 : propset (list iformula)) (x1 x2 : list iformula),
  (∀ (Δ : list iformula) (C : iformula),
     (∀ x3 : list iformula, x3 ∈ x → x3 ++ Δ ⊢cf C) → x1 ++ Δ ⊢cf C)
  → (∀ (Δ : list iformula) (C : iformula),
       (∀ x3 : list iformula, x3 ∈ x0 → x3 ++ Δ ⊢cf C) → x2 ++ Δ ⊢cf C)
    → ∀ (Δ : list iformula) (C : iformula),
        (∀ x3 : list iformula,
           x3 ∈ {[ z | ∃ a b : list iformula, a ∈ x ∧ b ∈ x0 ∧ z ≡ a ++ b ]}
           → x3 ++ Δ ⊢cf C)
        → (x1 ++ x2) ++ Δ ⊢cf C
    intros X Y Γ Γ' HΓ HΓ' Δ C H.X, Y: propset (list iformula)
Γ, Γ': list iformula
HΓ: ∀ (Δ : list iformula) (C : iformula),
  (∀ x : list iformula, x ∈ X → x ++ Δ ⊢cf C) → Γ ++ Δ ⊢cf C
HΓ': ∀ (Δ : list iformula) (C : iformula),
  (∀ x : list iformula, x ∈ Y → x ++ Δ ⊢cf C) → Γ' ++ Δ ⊢cf C
Δ: list iformula
C: iformula
H: ∀ x : list iformula,
  x ∈ {[ z | ∃ a b : list iformula, a ∈ X ∧ b ∈ Y ∧ z ≡ a ++ b ]}
  → x ++ Δ ⊢cf C
(Γ ++ Γ') ++ Δ ⊢cf C rewrite <- (assoc_L (++)).X, Y: propset (list iformula)
Γ, Γ': list iformula
HΓ: ∀ (Δ : list iformula) (C : iformula),
  (∀ x : list iformula, x ∈ X → x ++ Δ ⊢cf C) → Γ ++ Δ ⊢cf C
HΓ': ∀ (Δ : list iformula) (C : iformula),
  (∀ x : list iformula, x ∈ Y → x ++ Δ ⊢cf C) → Γ' ++ Δ ⊢cf C
Δ: list iformula
C: iformula
H: ∀ x : list iformula,
  x ∈ {[ z | ∃ a b : list iformula, a ∈ X ∧ b ∈ Y ∧ z ≡ a ++ b ]}
  → x ++ Δ ⊢cf C
Γ ++ Γ' ++ Δ ⊢cf C
    apply HΓ.X, Y: propset (list iformula)
Γ, Γ': list iformula
HΓ: ∀ (Δ : list iformula) (C : iformula),
  (∀ x : list iformula, x ∈ X → x ++ Δ ⊢cf C) → Γ ++ Δ ⊢cf C
HΓ': ∀ (Δ : list iformula) (C : iformula),
  (∀ x : list iformula, x ∈ Y → x ++ Δ ⊢cf C) → Γ' ++ Δ ⊢cf C
Δ: list iformula
C: iformula
H: ∀ x : list iformula,
  x ∈ {[ z | ∃ a b : list iformula, a ∈ X ∧ b ∈ Y ∧ z ≡ a ++ b ]}
  → x ++ Δ ⊢cf C
∀ x : list iformula, x ∈ X → x ++ Γ' ++ Δ ⊢cf C intros x Hx.X, Y: propset (list iformula)
Γ, Γ': list iformula
HΓ: ∀ (Δ : list iformula) (C : iformula),
  (∀ x : list iformula, x ∈ X → x ++ Δ ⊢cf C) → Γ ++ Δ ⊢cf C
HΓ': ∀ (Δ : list iformula) (C : iformula),
  (∀ x : list iformula, x ∈ Y → x ++ Δ ⊢cf C) → Γ' ++ Δ ⊢cf C
Δ: list iformula
C: iformula
H: ∀ x : list iformula,
  x ∈ {[ z | ∃ a b : list iformula, a ∈ X ∧ b ∈ Y ∧ z ≡ a ++ b ]}
  → x ++ Δ ⊢cf C
x: list iformula
Hx: x ∈ X
x ++ Γ' ++ Δ ⊢cf C ex_to (Γ' ++ x ++ Δ).X, Y: propset (list iformula)
Γ, Γ': list iformula
HΓ: ∀ (Δ : list iformula) (C : iformula),
  (∀ x : list iformula, x ∈ X → x ++ Δ ⊢cf C) → Γ ++ Δ ⊢cf C
HΓ': ∀ (Δ : list iformula) (C : iformula),
  (∀ x : list iformula, x ∈ Y → x ++ Δ ⊢cf C) → Γ' ++ Δ ⊢cf C
Δ: list iformula
C: iformula
H: ∀ x : list iformula,
  x ∈ {[ z | ∃ a b : list iformula, a ∈ X ∧ b ∈ Y ∧ z ≡ a ++ b ]}
  → x ++ Δ ⊢cf C
x: list iformula
Hx: x ∈ X
Γ' ++ x ++ Δ ⊢cf C
    apply HΓ'.X, Y: propset (list iformula)
Γ, Γ': list iformula
HΓ: ∀ (Δ : list iformula) (C : iformula),
  (∀ x : list iformula, x ∈ X → x ++ Δ ⊢cf C) → Γ ++ Δ ⊢cf C
HΓ': ∀ (Δ : list iformula) (C : iformula),
  (∀ x : list iformula, x ∈ Y → x ++ Δ ⊢cf C) → Γ' ++ Δ ⊢cf C
Δ: list iformula
C: iformula
H: ∀ x : list iformula,
  x ∈ {[ z | ∃ a b : list iformula, a ∈ X ∧ b ∈ Y ∧ z ≡ a ++ b ]}
  → x ++ Δ ⊢cf C
x: list iformula
Hx: x ∈ X
∀ x0 : list iformula, x0 ∈ Y → x0 ++ x ++ Δ ⊢cf C intros y Hy.X, Y: propset (list iformula)
Γ, Γ': list iformula
HΓ: ∀ (Δ : list iformula) (C : iformula),
  (∀ x : list iformula, x ∈ X → x ++ Δ ⊢cf C) → Γ ++ Δ ⊢cf C
HΓ': ∀ (Δ : list iformula) (C : iformula),
  (∀ x : list iformula, x ∈ Y → x ++ Δ ⊢cf C) → Γ' ++ Δ ⊢cf C
Δ: list iformula
C: iformula
H: ∀ x : list iformula,
  x ∈ {[ z | ∃ a b : list iformula, a ∈ X ∧ b ∈ Y ∧ z ≡ a ++ b ]}
  → x ++ Δ ⊢cf C
x: list iformula
Hx: x ∈ X
y: list iformula
Hy: y ∈ Y
y ++ x ++ Δ ⊢cf C ex_to ((x ++ y) ++ Δ).X, Y: propset (list iformula)
Γ, Γ': list iformula
HΓ: ∀ (Δ : list iformula) (C : iformula),
  (∀ x : list iformula, x ∈ X → x ++ Δ ⊢cf C) → Γ ++ Δ ⊢cf C
HΓ': ∀ (Δ : list iformula) (C : iformula),
  (∀ x : list iformula, x ∈ Y → x ++ Δ ⊢cf C) → Γ' ++ Δ ⊢cf C
Δ: list iformula
C: iformula
H: ∀ x : list iformula,
  x ∈ {[ z | ∃ a b : list iformula, a ∈ X ∧ b ∈ Y ∧ z ≡ a ++ b ]}
  → x ++ Δ ⊢cf C
x: list iformula
Hx: x ∈ X
y: list iformula
Hy: y ∈ Y
(x ++ y) ++ Δ ⊢cf C
    apply H.X, Y: propset (list iformula)
Γ, Γ': list iformula
HΓ: ∀ (Δ : list iformula) (C : iformula),
  (∀ x : list iformula, x ∈ X → x ++ Δ ⊢cf C) → Γ ++ Δ ⊢cf C
HΓ': ∀ (Δ : list iformula) (C : iformula),
  (∀ x : list iformula, x ∈ Y → x ++ Δ ⊢cf C) → Γ' ++ Δ ⊢cf C
Δ: list iformula
C: iformula
H: ∀ x : list iformula,
  x ∈ {[ z | ∃ a b : list iformula, a ∈ X ∧ b ∈ Y ∧ z ≡ a ++ b ]}
  → x ++ Δ ⊢cf C
x: list iformula
Hx: x ∈ X
y: list iformula
Hy: y ∈ Y
x ++ y ∈ {[ z | ∃ a b : list iformula, a ∈ X ∧ b ∈ Y ∧ z ≡ a ++ b ]} by exists x, y.
  - (* J respects ≡ₚ: a permutation of ‼Σ is ‼Σ' for some Σ' *)∀ x x0 : list iformula,
  x ≡ x0 → (∃ x1 : list iformula, x = ‼x1) → ∃ x1 : list iformula, x0 = ‼x1
    intros Γ Γ' HΓ [Σ ->].Γ', Σ: list iformula
HΓ: ‼Σ ≡ Γ'
∃ x : list iformula, Γ' = ‼x
    destruct (Permutation_map_inv _ _ (symmetry HΓ)) as (Σ' & -> & _).Σ, Σ': list iformula
HΓ: ‼Σ ≡ ‼Σ'
∃ x : list iformula, ‼Σ' = ‼x
    by exists Σ'.
  - (* ε ∈ J *)∃ x : list iformula, [] = ‼x by exists [].
  - (* J is closed under · *)∀ x x0 : list iformula,
  (∃ x1 : list iformula, x = ‼x1)
  → (∃ x1 : list iformula, x0 = ‼x1) → ∃ x1 : list iformula, x ++ x0 = ‼x1
    intros Γ Γ' [Σ ->] [Σ' ->].Σ, Σ': list iformula
∃ x : list iformula, ‼Σ ++ ‼Σ' = ‼x exists (Σ ++ Σ').Σ, Σ': list iformula
‼Σ ++ ‼Σ' = ‼(Σ ++ Σ') by rewrite map_app.
  - (* reusable contexts can be discarded: weakening *)∀ x : list iformula,
  (∃ x0 : list iformula, x = ‼x0)
  → ∀ (Δ : list iformula) (C : iformula),
      (∀ x0 : list iformula, x0 ∈ {[ z | z ≡ [] ]} → x0 ++ Δ ⊢cf C)
      → x ++ Δ ⊢cf C
    intros Γ [Σ ->] Δ C H.Σ, Δ: list iformula
C: iformula
H: ∀ x : list iformula, x ∈ {[ z | z ≡ [] ]} → x ++ Δ ⊢cf C
‼Σ ++ Δ ⊢cf C
    apply weaken_bangs, (H []).Σ, Δ: list iformula
C: iformula
H: ∀ x : list iformula, x ∈ {[ z | z ≡ [] ]} → x ++ Δ ⊢cf C
[] ∈ {[ z | z ≡ [] ]} by apply elem_of_PropSet.
  - (* reusable contexts can be duplicated: contraction *)∀ x : list iformula,
  (∃ x0 : list iformula, x = ‼x0)
  → ∀ (Δ : list iformula) (C : iformula),
      (∀ x0 : list iformula, x0 ∈ {[ z | z ≡ x ++ x ]} → x0 ++ Δ ⊢cf C)
      → x ++ Δ ⊢cf C
    intros Γ [Σ ->] Δ C H.Σ, Δ: list iformula
C: iformula
H: ∀ x : list iformula, x ∈ {[ z | z ≡ ‼Σ ++ ‼Σ ]} → x ++ Δ ⊢cf C
‼Σ ++ Δ ⊢cf C
    apply contract_bangs.Σ, Δ: list iformula
C: iformula
H: ∀ x : list iformula, x ∈ {[ z | z ≡ ‼Σ ++ ‼Σ ]} → x ++ Δ ⊢cf C
‼Σ ++ ‼Σ ++ Δ ⊢cf C rewrite (assoc_L (++)).Σ, Δ: list iformula
C: iformula
H: ∀ x : list iformula, x ∈ {[ z | z ≡ ‼Σ ++ ‼Σ ]} → x ++ Δ ⊢cf C
(‼Σ ++ ‼Σ) ++ Δ ⊢cf C apply H.Σ, Δ: list iformula
C: iformula
H: ∀ x : list iformula, x ∈ {[ z | z ≡ ‼Σ ++ ‼Σ ]} → x ++ Δ ⊢cf C
‼Σ ++ ‼Σ ∈ {[ z | z ≡ ‼Σ ++ ‼Σ ]}
    by apply elem_of_PropSet.
Defined.

Reduce the projections of syntactic, leaving ∈ alone.

Ltac syn_simpl :=
  cbn [ph_cl ph_J ph_bot ph_equiv ph_op ph_e syntactic carrier] in *.

Each variable $p denotes the contexts that prove $p without cut.

Definition down (A : iformula) : propset syntactic := {[ Γ | Γ ⊢cf A ]}.
Definition syn_val : nat -> propset syntactic := λ p, down ($p).

Lemma elem_of_down A Γ : Γ ∈ down A ↔ Γ ⊢cf A.A: iformula
Γ: list iformula
Γ ∈ down A ↔ Γ ⊢cf A
Proof.A: iformula
Γ: list iformula
Γ ∈ down A ↔ Γ ⊢cf A unfold down.A: iformula
Γ: list iformula
Γ ∈ {[ Γ0 | Γ0 ⊢cf A ]} ↔ Γ ⊢cf A by rewrite elem_of_PropSet. Qed.

#[global] Instance set_unfold_down A Γ : SetUnfoldElemOf Γ (down A) (Γ ⊢cf A).A: iformula
Γ: list iformula
SetUnfoldElemOf Γ (down A) (Γ ⊢cf A)
Proof.A: iformula
Γ: list iformula
SetUnfoldElemOf Γ (down A) (Γ ⊢cf A) constructor.A: iformula
Γ: list iformula
Γ ∈ down A ↔ Γ ⊢cf A apply elem_of_down. Qed.

elem_of_syn_cl, stated over the carrier of syntactic. Then the lemmas of Phase.v can infer the phase space.

Lemma elem_of_cl_syn (X : propset syntactic) (Γ : syntactic) :
  Γ ∈ cl X ↔ ∀ Δ C, (∀ x : syntactic, x ∈ X -> x ++ Δ ⊢cf C) -> Γ ++ Δ ⊢cf C.X: propset syntactic
Γ: syntactic
Γ ∈ cl X
↔ ∀ (Δ : list iformula) (C : iformula),
    (∀ x : syntactic, x ∈ X → x ++ Δ ⊢cf C) → Γ ++ Δ ⊢cf C
Proof.X: propset syntactic
Γ: syntactic
Γ ∈ cl X
↔ ∀ (Δ : list iformula) (C : iformula),
    (∀ x : syntactic, x ∈ X → x ++ Δ ⊢cf C) → Γ ++ Δ ⊢cf C apply elem_of_syn_cl. Qed.

Facts of the syntactic model

Okada's lemma has two halves, and each half has one tool.

Left rules put a formula into a fact._ To show Γ ∈ cl X, pick one member Γ' of X and check that every test passed by Γ' is also passed by Γ. That check is usually a single left rule. For example, [A ⊗ B] passes every test that [A; B] passes, by tensorL:

Γ' ++ Δ ⊢cf C ─────────────── (a left rule) Γ' ∈ X Γ ++ Δ ⊢cf C ─────────────────────────────────────────────── cl_left Γ ∈ cl X

Lemma cl_left (X : propset syntactic) (Γ Γ' : syntactic) :
  Γ' ∈ X -> (∀ Δ C, Γ' ++ Δ ⊢cf C -> Γ ++ Δ ⊢cf C) -> Γ ∈ cl X.X: propset syntactic
Γ, Γ': syntactic
Γ' ∈ X
→ (∀ (Δ : list iformula) (C : iformula), Γ' ++ Δ ⊢cf C → Γ ++ Δ ⊢cf C)
  → Γ ∈ cl X
Proof.X: propset syntactic
Γ, Γ': syntactic
Γ' ∈ X
→ (∀ (Δ : list iformula) (C : iformula), Γ' ++ Δ ⊢cf C → Γ ++ Δ ⊢cf C)
  → Γ ∈ cl X
  intros HΓ' Hrule.X: propset syntactic
Γ, Γ': syntactic
HΓ': Γ' ∈ X
Hrule: ∀ (Δ : list iformula) (C : iformula), Γ' ++ Δ ⊢cf C → Γ ++ Δ ⊢cf C
Γ ∈ cl X apply elem_of_cl_syn.X: propset syntactic
Γ, Γ': syntactic
HΓ': Γ' ∈ X
Hrule: ∀ (Δ : list iformula) (C : iformula), Γ' ++ Δ ⊢cf C → Γ ++ Δ ⊢cf C
∀ (Δ : list iformula) (C : iformula),
  (∀ x : syntactic, x ∈ X → x ++ Δ ⊢cf C) → Γ ++ Δ ⊢cf C intros Δ C H.X: propset syntactic
Γ, Γ': syntactic
HΓ': Γ' ∈ X
Hrule: ∀ (Δ : list iformula) (C : iformula), Γ' ++ Δ ⊢cf C → Γ ++ Δ ⊢cf C
Δ: list iformula
C: iformula
H: ∀ x : syntactic, x ∈ X → x ++ Δ ⊢cf C
Γ ++ Δ ⊢cf C by apply Hrule, H.
Qed.

The same for a fact F, which is its own closure.

Lemma fact_left (F : propset syntactic) (Γ Γ' : syntactic) :
  fact F -> Γ' ∈ F -> (∀ Δ C, Γ' ++ Δ ⊢cf C -> Γ ++ Δ ⊢cf C) -> Γ ∈ F.F: propset syntactic
Γ, Γ': syntactic
fact F
→ Γ' ∈ F
  → (∀ (Δ : list iformula) (C : iformula), Γ' ++ Δ ⊢cf C → Γ ++ Δ ⊢cf C)
    → Γ ∈ F
Proof.F: propset syntactic
Γ, Γ': syntactic
fact F
→ Γ' ∈ F
  → (∀ (Δ : list iformula) (C : iformula), Γ' ++ Δ ⊢cf C → Γ ++ Δ ⊢cf C)
    → Γ ∈ F intros HF HΓ' Hrule.F: propset syntactic
Γ, Γ': syntactic
HF: fact F
HΓ': Γ' ∈ F
Hrule: ∀ (Δ : list iformula) (C : iformula), Γ' ++ Δ ⊢cf C → Γ ++ Δ ⊢cf C
Γ ∈ F by apply HF, (cl_left _ _ Γ'). Qed.

Right rules bound a fact from above._ The closure of a set of proofs of C contains only proofs of C: use the trivial test ([], C).

Lemma cl_down (X : propset syntactic) C : X ⊆ down C -> cl X ⊆ down C.X: propset syntactic
C: iformula
X ⊆ down C → cl X ⊆ down C
Proof.X: propset syntactic
C: iformula
X ⊆ down C → cl X ⊆ down C
  intros HX Γ HΓ.X: propset syntactic
C: iformula
HX: X ⊆ down C
Γ: syntactic
HΓ: Γ ∈ cl X
Γ ∈ down C rewrite elem_of_cl_syn in HΓ.X: propset syntactic
C: iformula
HX: X ⊆ down C
Γ: syntactic
HΓ: ∀ (Δ : list iformula) (C : iformula),
  (∀ x : syntactic, x ∈ X → x ++ Δ ⊢cf C) → Γ ++ Δ ⊢cf C
Γ ∈ down C
  rewrite elem_of_down, <- (right_id_L [] (++) Γ).X: propset syntactic
C: iformula
HX: X ⊆ down C
Γ: syntactic
HΓ: ∀ (Δ : list iformula) (C : iformula),
  (∀ x : syntactic, x ∈ X → x ++ Δ ⊢cf C) → Γ ++ Δ ⊢cf C
Γ ++ [] ⊢cf C apply HΓ.X: propset syntactic
C: iformula
HX: X ⊆ down C
Γ: syntactic
HΓ: ∀ (Δ : list iformula) (C : iformula),
  (∀ x : syntactic, x ∈ X → x ++ Δ ⊢cf C) → Γ ++ Δ ⊢cf C
∀ x : syntactic, x ∈ X → x ++ [] ⊢cf C
  intros x Hx.X: propset syntactic
C: iformula
HX: X ⊆ down C
Γ: syntactic
HΓ: ∀ (Δ : list iformula) (C : iformula),
  (∀ x : syntactic, x ∈ X → x ++ Δ ⊢cf C) → Γ ++ Δ ⊢cf C
x: syntactic
Hx: x ∈ X
x ++ [] ⊢cf C rewrite (right_id_L [] (++)).X: propset syntactic
C: iformula
HX: X ⊆ down C
Γ: syntactic
HΓ: ∀ (Δ : list iformula) (C : iformula),
  (∀ x : syntactic, x ∈ X → x ++ Δ ⊢cf C) → Γ ++ Δ ⊢cf C
x: syntactic
Hx: x ∈ X
x ⊢cf C by apply elem_of_down, HX.
Qed.

Okada's lemma

By induction on A. In each case the first half uses the left rule of the connective (through cl_left / fact_left), and the second half uses its right rule (through cl_down).

Lemma okada A : [A] ∈ ⟦A⟧syn_val ∧ ⟦A⟧syn_val ⊆ down A.A: iformula
[A] ∈ ⟦A⟧syn_val ∧ ⟦A⟧syn_val ⊆ down A
Proof.A: iformula
[A] ∈ ⟦A⟧syn_val ∧ ⟦A⟧syn_val ⊆ down A
  induction A as [p | | | | | A [HA1 HA2] B [HB1 HB2] | A [HA1 HA2] B [HB1 HB2]
                 | A [HA1 HA2] B [HB1 HB2] | A [HA1 HA2] B [HB1 HB2]
                 | A [HA1 HA2]]; cbn [interp].p: nat
[$p] ∈ cl (syn_val p) ∧ cl (syn_val p) ⊆ down $p
[𝟙] ∈ ph_one ∧ ph_one ⊆ down 𝟙
[⊥] ∈ cl ph_bot ∧ cl ph_bot ⊆ down ⊥
[⊤] ∈ ph_top ∧ ph_top ⊆ down ⊤
[𝟘] ∈ ph_zero ∧ ph_zero ⊆ down 𝟘
A: iformula
HA1: [A] ∈ ⟦A⟧syn_val
B: iformula
HA2: ⟦A⟧syn_val ⊆ down A
HB1: [B] ∈ ⟦B⟧syn_val
HB2: ⟦B⟧syn_val ⊆ down B
[A ⊗ B] ∈ ph_tensor ⟦A⟧syn_val ⟦B⟧syn_val
∧ ph_tensor ⟦A⟧syn_val ⟦B⟧syn_val ⊆ down (A ⊗ B)
A: iformula
HA1: [A] ∈ ⟦A⟧syn_val
B: iformula
HA2: ⟦A⟧syn_val ⊆ down A
HB1: [B] ∈ ⟦B⟧syn_val
HB2: ⟦B⟧syn_val ⊆ down B
[A ⊸ B] ∈ ph_lolli ⟦A⟧syn_val ⟦B⟧syn_val
∧ ph_lolli ⟦A⟧syn_val ⟦B⟧syn_val ⊆ down (A ⊸ B)
A: iformula
HA1: [A] ∈ ⟦A⟧syn_val
B: iformula
HA2: ⟦A⟧syn_val ⊆ down A
HB1: [B] ∈ ⟦B⟧syn_val
HB2: ⟦B⟧syn_val ⊆ down B
[A & B] ∈ ⟦A⟧syn_val ∩ ⟦B⟧syn_val ∧ ⟦A⟧syn_val ∩ ⟦B⟧syn_val ⊆ down (A & B)
A: iformula
HA1: [A] ∈ ⟦A⟧syn_val
B: iformula
HA2: ⟦A⟧syn_val ⊆ down A
HB1: [B] ∈ ⟦B⟧syn_val
HB2: ⟦B⟧syn_val ⊆ down B
[A ⊕ B] ∈ ph_plus ⟦A⟧syn_val ⟦B⟧syn_val
∧ ph_plus ⟦A⟧syn_val ⟦B⟧syn_val ⊆ down (A ⊕ B)
A: iformula
HA1: [A] ∈ ⟦A⟧syn_val
HA2: ⟦A⟧syn_val ⊆ down A
[!A] ∈ ph_bang ⟦A⟧syn_val ∧ ph_bang ⟦A⟧syn_val ⊆ down (!A)
  - (* $p *)p: nat
[$p] ∈ cl (syn_val p) ∧ cl (syn_val p) ⊆ down $p
    split; [| by apply cl_down].p: nat
[$p] ∈ cl (syn_val p)
    apply ph_cl_ext, elem_of_down, ax.
  - (* 𝟙 *)[𝟙] ∈ ph_one ∧ ph_one ⊆ down 𝟙
    split.[𝟙] ∈ ph_one
ph_one ⊆ down 𝟙
    +[𝟙] ∈ ph_one apply (cl_left _ _ []); [by apply elem_of_one | intros; by apply oneL].
    +ph_one ⊆ down 𝟙 apply cl_down.one_set ⊆ down 𝟙 intros x Hx%elem_of_one.x: syntactic
Hx: x ≡ ε
x ∈ down 𝟙 apply elem_of_down.x: syntactic
Hx: x ≡ ε
x ⊢cf 𝟙
      syn_simpl.x: list iformula
Hx: x ≡ []
x ⊢cf 𝟙 apply Permutation_nil_r in Hx as ->.[] ⊢cf 𝟙 apply oneR.
  - (* ⊥ *)[⊥] ∈ cl ph_bot ∧ cl ph_bot ⊆ down ⊥
    split; [| by apply cl_down].[⊥] ∈ cl ph_bot
    apply ph_cl_ext.[⊥] ∈ ph_bot set_unfold.[⊥] ⊢cf ⊥ apply ax.
  - (* ⊤ *)[⊤] ∈ ph_top ∧ ph_top ⊆ down ⊤
    split; [apply elem_of_top |].ph_top ⊆ down ⊤ intros x _.x: syntactic
x ∈ down ⊤ apply elem_of_down, topR.
  - (* 𝟘: the empty set passes every test *)[𝟘] ∈ ph_zero ∧ ph_zero ⊆ down 𝟘
    split; [| apply cl_down; set_solver].[𝟘] ∈ ph_zero
    apply elem_of_cl_syn.∀ (Δ : list iformula) (C : iformula),
  (∀ x : syntactic, x ∈ ∅ → x ++ Δ ⊢cf C) → [𝟘] ++ Δ ⊢cf C intros Δ C _.Δ: list iformula
C: iformula
[𝟘] ++ Δ ⊢cf C apply zeroL.
  - (* A ⊗ B *)A: iformula
HA1: [A] ∈ ⟦A⟧syn_val
B: iformula
HA2: ⟦A⟧syn_val ⊆ down A
HB1: [B] ∈ ⟦B⟧syn_val
HB2: ⟦B⟧syn_val ⊆ down B
[A ⊗ B] ∈ ph_tensor ⟦A⟧syn_val ⟦B⟧syn_val
∧ ph_tensor ⟦A⟧syn_val ⟦B⟧syn_val ⊆ down (A ⊗ B)
    split.A: iformula
HA1: [A] ∈ ⟦A⟧syn_val
B: iformula
HA2: ⟦A⟧syn_val ⊆ down A
HB1: [B] ∈ ⟦B⟧syn_val
HB2: ⟦B⟧syn_val ⊆ down B
[A ⊗ B] ∈ ph_tensor ⟦A⟧syn_val ⟦B⟧syn_val
A: iformula
HA1: [A] ∈ ⟦A⟧syn_val
B: iformula
HA2: ⟦A⟧syn_val ⊆ down A
HB1: [B] ∈ ⟦B⟧syn_val
HB2: ⟦B⟧syn_val ⊆ down B
ph_tensor ⟦A⟧syn_val ⟦B⟧syn_val ⊆ down (A ⊗ B)
    +A: iformula
HA1: [A] ∈ ⟦A⟧syn_val
B: iformula
HA2: ⟦A⟧syn_val ⊆ down A
HB1: [B] ∈ ⟦B⟧syn_val
HB2: ⟦B⟧syn_val ⊆ down B
[A ⊗ B] ∈ ph_tensor ⟦A⟧syn_val ⟦B⟧syn_val apply (cl_left _ _ [A; B]); [| intros; by apply tensorL].A: iformula
HA1: [A] ∈ ⟦A⟧syn_val
B: iformula
HA2: ⟦A⟧syn_val ⊆ down A
HB1: [B] ∈ ⟦B⟧syn_val
HB2: ⟦B⟧syn_val ⊆ down B
[A; B] ∈ ⟦A⟧syn_val ⊙ ⟦B⟧syn_val
      apply elem_of_prod.A: iformula
HA1: [A] ∈ ⟦A⟧syn_val
B: iformula
HA2: ⟦A⟧syn_val ⊆ down A
HB1: [B] ∈ ⟦B⟧syn_val
HB2: ⟦B⟧syn_val ⊆ down B
∃ a b : syntactic, a ∈ ⟦A⟧syn_val ∧ b ∈ ⟦B⟧syn_val ∧ [A; B] ≡ a · b by exists [A], [B].
    +A: iformula
HA1: [A] ∈ ⟦A⟧syn_val
B: iformula
HA2: ⟦A⟧syn_val ⊆ down A
HB1: [B] ∈ ⟦B⟧syn_val
HB2: ⟦B⟧syn_val ⊆ down B
ph_tensor ⟦A⟧syn_val ⟦B⟧syn_val ⊆ down (A ⊗ B) apply cl_down.A: iformula
HA1: [A] ∈ ⟦A⟧syn_val
B: iformula
HA2: ⟦A⟧syn_val ⊆ down A
HB1: [B] ∈ ⟦B⟧syn_val
HB2: ⟦B⟧syn_val ⊆ down B
⟦A⟧syn_val ⊙ ⟦B⟧syn_val ⊆ down (A ⊗ B) intros x (a & b & Ha%HA2 & Hb%HB2 & Hx)%elem_of_prod.A: iformula
HA1: [A] ∈ ⟦A⟧syn_val
B: iformula
HA2: ⟦A⟧syn_val ⊆ down A
HB1: [B] ∈ ⟦B⟧syn_val
HB2: ⟦B⟧syn_val ⊆ down B
x, a, b: syntactic
Ha: a ∈ down A
Hb: b ∈ down B
Hx: x ≡ a · b
x ∈ down (A ⊗ B)
      apply elem_of_down.A: iformula
HA1: [A] ∈ ⟦A⟧syn_val
B: iformula
HA2: ⟦A⟧syn_val ⊆ down A
HB1: [B] ∈ ⟦B⟧syn_val
HB2: ⟦B⟧syn_val ⊆ down B
x, a, b: syntactic
Ha: a ∈ down A
Hb: b ∈ down B
Hx: x ≡ a · b
x ⊢cf A ⊗ B apply (ex' (Γ := a ++ b)); [| by symmetry].A: iformula
HA1: [A] ∈ ⟦A⟧syn_val
B: iformula
HA2: ⟦A⟧syn_val ⊆ down A
HB1: [B] ∈ ⟦B⟧syn_val
HB2: ⟦B⟧syn_val ⊆ down B
x, a, b: syntactic
Ha: a ∈ down A
Hb: b ∈ down B
Hx: x ≡ a · b
a ++ b ⊢cf A ⊗ B
      apply tensorR; by apply elem_of_down.
  - (* A ⊸ B *)A: iformula
HA1: [A] ∈ ⟦A⟧syn_val
B: iformula
HA2: ⟦A⟧syn_val ⊆ down A
HB1: [B] ∈ ⟦B⟧syn_val
HB2: ⟦B⟧syn_val ⊆ down B
[A ⊸ B] ∈ ph_lolli ⟦A⟧syn_val ⟦B⟧syn_val
∧ ph_lolli ⟦A⟧syn_val ⟦B⟧syn_val ⊆ down (A ⊸ B)
    split.A: iformula
HA1: [A] ∈ ⟦A⟧syn_val
B: iformula
HA2: ⟦A⟧syn_val ⊆ down A
HB1: [B] ∈ ⟦B⟧syn_val
HB2: ⟦B⟧syn_val ⊆ down B
[A ⊸ B] ∈ ph_lolli ⟦A⟧syn_val ⟦B⟧syn_val
A: iformula
HA1: [A] ∈ ⟦A⟧syn_val
B: iformula
HA2: ⟦A⟧syn_val ⊆ down A
HB1: [B] ∈ ⟦B⟧syn_val
HB2: ⟦B⟧syn_val ⊆ down B
ph_lolli ⟦A⟧syn_val ⟦B⟧syn_val ⊆ down (A ⊸ B)
    +A: iformula
HA1: [A] ∈ ⟦A⟧syn_val
B: iformula
HA2: ⟦A⟧syn_val ⊆ down A
HB1: [B] ∈ ⟦B⟧syn_val
HB2: ⟦B⟧syn_val ⊆ down B
[A ⊸ B] ∈ ph_lolli ⟦A⟧syn_val ⟦B⟧syn_val apply elem_of_lolli.A: iformula
HA1: [A] ∈ ⟦A⟧syn_val
B: iformula
HA2: ⟦A⟧syn_val ⊆ down A
HB1: [B] ∈ ⟦B⟧syn_val
HB2: ⟦B⟧syn_val ⊆ down B
∀ a : syntactic, a ∈ ⟦A⟧syn_val → [A ⊸ B] · a ∈ ⟦B⟧syn_val intros a Ha%HA2%elem_of_down.A: iformula
HA1: [A] ∈ ⟦A⟧syn_val
B: iformula
HA2: ⟦A⟧syn_val ⊆ down A
HB1: [B] ∈ ⟦B⟧syn_val
HB2: ⟦B⟧syn_val ⊆ down B
a: syntactic
Ha: a ⊢cf A
[A ⊸ B] · a ∈ ⟦B⟧syn_val
      apply (fact_left _ _ [B]); [apply interp_fact | done |].A: iformula
HA1: [A] ∈ ⟦A⟧syn_val
B: iformula
HA2: ⟦A⟧syn_val ⊆ down A
HB1: [B] ∈ ⟦B⟧syn_val
HB2: ⟦B⟧syn_val ⊆ down B
a: syntactic
Ha: a ⊢cf A
∀ (Δ : list iformula) (C : iformula), [B] ++ Δ ⊢cf C → [A ⊸ B] · a ++ Δ ⊢cf C
      intros Δ C H.A: iformula
HA1: [A] ∈ ⟦A⟧syn_val
B: iformula
HA2: ⟦A⟧syn_val ⊆ down A
HB1: [B] ∈ ⟦B⟧syn_val
HB2: ⟦B⟧syn_val ⊆ down B
a: syntactic
Ha: a ⊢cf A
Δ: list iformula
C: iformula
H: [B] ++ Δ ⊢cf C
[A ⊸ B] · a ++ Δ ⊢cf C by apply lolliL.
    +A: iformula
HA1: [A] ∈ ⟦A⟧syn_val
B: iformula
HA2: ⟦A⟧syn_val ⊆ down A
HB1: [B] ∈ ⟦B⟧syn_val
HB2: ⟦B⟧syn_val ⊆ down B
ph_lolli ⟦A⟧syn_val ⟦B⟧syn_val ⊆ down (A ⊸ B) intros f Hf.A: iformula
HA1: [A] ∈ ⟦A⟧syn_val
B: iformula
HA2: ⟦A⟧syn_val ⊆ down A
HB1: [B] ∈ ⟦B⟧syn_val
HB2: ⟦B⟧syn_val ⊆ down B
f: syntactic
Hf: f ∈ ph_lolli ⟦A⟧syn_val ⟦B⟧syn_val
f ∈ down (A ⊸ B) rewrite elem_of_lolli in Hf.A: iformula
HA1: [A] ∈ ⟦A⟧syn_val
B: iformula
HA2: ⟦A⟧syn_val ⊆ down A
HB1: [B] ∈ ⟦B⟧syn_val
HB2: ⟦B⟧syn_val ⊆ down B
f: syntactic
Hf: ∀ a : syntactic, a ∈ ⟦A⟧syn_val → f · a ∈ ⟦B⟧syn_val
f ∈ down (A ⊸ B) apply elem_of_down.A: iformula
HA1: [A] ∈ ⟦A⟧syn_val
B: iformula
HA2: ⟦A⟧syn_val ⊆ down A
HB1: [B] ∈ ⟦B⟧syn_val
HB2: ⟦B⟧syn_val ⊆ down B
f: syntactic
Hf: ∀ a : syntactic, a ∈ ⟦A⟧syn_val → f · a ∈ ⟦B⟧syn_val
f ⊢cf A ⊸ B
      apply lolliR.A: iformula
HA1: [A] ∈ ⟦A⟧syn_val
B: iformula
HA2: ⟦A⟧syn_val ⊆ down A
HB1: [B] ∈ ⟦B⟧syn_val
HB2: ⟦B⟧syn_val ⊆ down B
f: syntactic
Hf: ∀ a : syntactic, a ∈ ⟦A⟧syn_val → f · a ∈ ⟦B⟧syn_val
A :: f ⊢cf B ex_to (f ++ [A]).A: iformula
HA1: [A] ∈ ⟦A⟧syn_val
B: iformula
HA2: ⟦A⟧syn_val ⊆ down A
HB1: [B] ∈ ⟦B⟧syn_val
HB2: ⟦B⟧syn_val ⊆ down B
f: syntactic
Hf: ∀ a : syntactic, a ∈ ⟦A⟧syn_val → f · a ∈ ⟦B⟧syn_val
f ++ [A] ⊢cf B by apply elem_of_down, HB2, Hf.
  - (* A & B *)A: iformula
HA1: [A] ∈ ⟦A⟧syn_val
B: iformula
HA2: ⟦A⟧syn_val ⊆ down A
HB1: [B] ∈ ⟦B⟧syn_val
HB2: ⟦B⟧syn_val ⊆ down B
[A & B] ∈ ⟦A⟧syn_val ∩ ⟦B⟧syn_val ∧ ⟦A⟧syn_val ∩ ⟦B⟧syn_val ⊆ down (A & B)
    split.A: iformula
HA1: [A] ∈ ⟦A⟧syn_val
B: iformula
HA2: ⟦A⟧syn_val ⊆ down A
HB1: [B] ∈ ⟦B⟧syn_val
HB2: ⟦B⟧syn_val ⊆ down B
[A & B] ∈ ⟦A⟧syn_val ∩ ⟦B⟧syn_val
A: iformula
HA1: [A] ∈ ⟦A⟧syn_val
B: iformula
HA2: ⟦A⟧syn_val ⊆ down A
HB1: [B] ∈ ⟦B⟧syn_val
HB2: ⟦B⟧syn_val ⊆ down B
⟦A⟧syn_val ∩ ⟦B⟧syn_val ⊆ down (A & B)
    +A: iformula
HA1: [A] ∈ ⟦A⟧syn_val
B: iformula
HA2: ⟦A⟧syn_val ⊆ down A
HB1: [B] ∈ ⟦B⟧syn_val
HB2: ⟦B⟧syn_val ⊆ down B
[A & B] ∈ ⟦A⟧syn_val ∩ ⟦B⟧syn_val apply elem_of_intersection.A: iformula
HA1: [A] ∈ ⟦A⟧syn_val
B: iformula
HA2: ⟦A⟧syn_val ⊆ down A
HB1: [B] ∈ ⟦B⟧syn_val
HB2: ⟦B⟧syn_val ⊆ down B
[A & B] ∈ ⟦A⟧syn_val ∧ [A & B] ∈ ⟦B⟧syn_val split.A: iformula
HA1: [A] ∈ ⟦A⟧syn_val
B: iformula
HA2: ⟦A⟧syn_val ⊆ down A
HB1: [B] ∈ ⟦B⟧syn_val
HB2: ⟦B⟧syn_val ⊆ down B
[A & B] ∈ ⟦A⟧syn_val
A: iformula
HA1: [A] ∈ ⟦A⟧syn_val
B: iformula
HA2: ⟦A⟧syn_val ⊆ down A
HB1: [B] ∈ ⟦B⟧syn_val
HB2: ⟦B⟧syn_val ⊆ down B
[A & B] ∈ ⟦B⟧syn_val
      *A: iformula
HA1: [A] ∈ ⟦A⟧syn_val
B: iformula
HA2: ⟦A⟧syn_val ⊆ down A
HB1: [B] ∈ ⟦B⟧syn_val
HB2: ⟦B⟧syn_val ⊆ down B
[A & B] ∈ ⟦A⟧syn_val apply (fact_left _ _ [A]); [apply interp_fact | done |].A: iformula
HA1: [A] ∈ ⟦A⟧syn_val
B: iformula
HA2: ⟦A⟧syn_val ⊆ down A
HB1: [B] ∈ ⟦B⟧syn_val
HB2: ⟦B⟧syn_val ⊆ down B
∀ (Δ : list iformula) (C : iformula), [A] ++ Δ ⊢cf C → [A & B] ++ Δ ⊢cf C
        intros; by apply withL1.
      *A: iformula
HA1: [A] ∈ ⟦A⟧syn_val
B: iformula
HA2: ⟦A⟧syn_val ⊆ down A
HB1: [B] ∈ ⟦B⟧syn_val
HB2: ⟦B⟧syn_val ⊆ down B
[A & B] ∈ ⟦B⟧syn_val apply (fact_left _ _ [B]); [apply interp_fact | done |].A: iformula
HA1: [A] ∈ ⟦A⟧syn_val
B: iformula
HA2: ⟦A⟧syn_val ⊆ down A
HB1: [B] ∈ ⟦B⟧syn_val
HB2: ⟦B⟧syn_val ⊆ down B
∀ (Δ : list iformula) (C : iformula), [B] ++ Δ ⊢cf C → [A & B] ++ Δ ⊢cf C
        intros; by apply withL2.
    +A: iformula
HA1: [A] ∈ ⟦A⟧syn_val
B: iformula
HA2: ⟦A⟧syn_val ⊆ down A
HB1: [B] ∈ ⟦B⟧syn_val
HB2: ⟦B⟧syn_val ⊆ down B
⟦A⟧syn_val ∩ ⟦B⟧syn_val ⊆ down (A & B) intros x [Ha%HA2 Hb%HB2]%elem_of_intersection.A: iformula
HA1: [A] ∈ ⟦A⟧syn_val
B: iformula
HA2: ⟦A⟧syn_val ⊆ down A
HB1: [B] ∈ ⟦B⟧syn_val
HB2: ⟦B⟧syn_val ⊆ down B
x: syntactic
Ha: x ∈ down A
Hb: x ∈ down B
x ∈ down (A & B)
      apply elem_of_down, withR; by apply elem_of_down.
  - (* A ⊕ B: two witnesses, one per premise of plusL *)A: iformula
HA1: [A] ∈ ⟦A⟧syn_val
B: iformula
HA2: ⟦A⟧syn_val ⊆ down A
HB1: [B] ∈ ⟦B⟧syn_val
HB2: ⟦B⟧syn_val ⊆ down B
[A ⊕ B] ∈ ph_plus ⟦A⟧syn_val ⟦B⟧syn_val
∧ ph_plus ⟦A⟧syn_val ⟦B⟧syn_val ⊆ down (A ⊕ B)
    split.A: iformula
HA1: [A] ∈ ⟦A⟧syn_val
B: iformula
HA2: ⟦A⟧syn_val ⊆ down A
HB1: [B] ∈ ⟦B⟧syn_val
HB2: ⟦B⟧syn_val ⊆ down B
[A ⊕ B] ∈ ph_plus ⟦A⟧syn_val ⟦B⟧syn_val
A: iformula
HA1: [A] ∈ ⟦A⟧syn_val
B: iformula
HA2: ⟦A⟧syn_val ⊆ down A
HB1: [B] ∈ ⟦B⟧syn_val
HB2: ⟦B⟧syn_val ⊆ down B
ph_plus ⟦A⟧syn_val ⟦B⟧syn_val ⊆ down (A ⊕ B)
    +A: iformula
HA1: [A] ∈ ⟦A⟧syn_val
B: iformula
HA2: ⟦A⟧syn_val ⊆ down A
HB1: [B] ∈ ⟦B⟧syn_val
HB2: ⟦B⟧syn_val ⊆ down B
[A ⊕ B] ∈ ph_plus ⟦A⟧syn_val ⟦B⟧syn_val apply elem_of_cl_syn.A: iformula
HA1: [A] ∈ ⟦A⟧syn_val
B: iformula
HA2: ⟦A⟧syn_val ⊆ down A
HB1: [B] ∈ ⟦B⟧syn_val
HB2: ⟦B⟧syn_val ⊆ down B
∀ (Δ : list iformula) (C : iformula),
  (∀ x : syntactic, x ∈ ⟦A⟧syn_val ∪ ⟦B⟧syn_val → x ++ Δ ⊢cf C)
  → [A ⊕ B] ++ Δ ⊢cf C intros Δ C H.A: iformula
HA1: [A] ∈ ⟦A⟧syn_val
B: iformula
HA2: ⟦A⟧syn_val ⊆ down A
HB1: [B] ∈ ⟦B⟧syn_val
HB2: ⟦B⟧syn_val ⊆ down B
Δ: list iformula
C: iformula
H: ∀ x : syntactic, x ∈ ⟦A⟧syn_val ∪ ⟦B⟧syn_val → x ++ Δ ⊢cf C
[A ⊕ B] ++ Δ ⊢cf C
      apply plusL; [apply (H [A]) | apply (H [B])]; set_solver.
    +A: iformula
HA1: [A] ∈ ⟦A⟧syn_val
B: iformula
HA2: ⟦A⟧syn_val ⊆ down A
HB1: [B] ∈ ⟦B⟧syn_val
HB2: ⟦B⟧syn_val ⊆ down B
ph_plus ⟦A⟧syn_val ⟦B⟧syn_val ⊆ down (A ⊕ B) apply cl_down.A: iformula
HA1: [A] ∈ ⟦A⟧syn_val
B: iformula
HA2: ⟦A⟧syn_val ⊆ down A
HB1: [B] ∈ ⟦B⟧syn_val
HB2: ⟦B⟧syn_val ⊆ down B
⟦A⟧syn_val ∪ ⟦B⟧syn_val ⊆ down (A ⊕ B) intros x [Hx%HA2 | Hx%HB2]%elem_of_union;
        apply elem_of_down; [apply plusR1 | apply plusR2]; by apply elem_of_down.
  - (* !A *)A: iformula
HA1: [A] ∈ ⟦A⟧syn_val
HA2: ⟦A⟧syn_val ⊆ down A
[!A] ∈ ph_bang ⟦A⟧syn_val ∧ ph_bang ⟦A⟧syn_val ⊆ down (!A)
    split.A: iformula
HA1: [A] ∈ ⟦A⟧syn_val
HA2: ⟦A⟧syn_val ⊆ down A
[!A] ∈ ph_bang ⟦A⟧syn_val
A: iformula
HA1: [A] ∈ ⟦A⟧syn_val
HA2: ⟦A⟧syn_val ⊆ down A
ph_bang ⟦A⟧syn_val ⊆ down (!A)
    +A: iformula
HA1: [A] ∈ ⟦A⟧syn_val
HA2: ⟦A⟧syn_val ⊆ down A
[!A] ∈ ph_bang ⟦A⟧syn_val apply ph_cl_ext, elem_of_intersection.A: iformula
HA1: [A] ∈ ⟦A⟧syn_val
HA2: ⟦A⟧syn_val ⊆ down A
[!A] ∈ ⟦A⟧syn_val ∧ [!A] ∈ J split.A: iformula
HA1: [A] ∈ ⟦A⟧syn_val
HA2: ⟦A⟧syn_val ⊆ down A
[!A] ∈ ⟦A⟧syn_val
A: iformula
HA1: [A] ∈ ⟦A⟧syn_val
HA2: ⟦A⟧syn_val ⊆ down A
[!A] ∈ J
      *A: iformula
HA1: [A] ∈ ⟦A⟧syn_val
HA2: ⟦A⟧syn_val ⊆ down A
[!A] ∈ ⟦A⟧syn_val apply (fact_left _ _ [A]); [apply interp_fact | done |].A: iformula
HA1: [A] ∈ ⟦A⟧syn_val
HA2: ⟦A⟧syn_val ⊆ down A
∀ (Δ : list iformula) (C : iformula), [A] ++ Δ ⊢cf C → [!A] ++ Δ ⊢cf C
        intros; by apply bangD.
      *A: iformula
HA1: [A] ∈ ⟦A⟧syn_val
HA2: ⟦A⟧syn_val ⊆ down A
[!A] ∈ J syn_simpl.A: iformula
HA1: [A] ∈ ⟦A⟧syn_val
HA2: ⟦A⟧syn_val ⊆ down A
[!A] ∈ {[ Γ | ∃ Σ : list iformula, Γ = ‼Σ ]} set_unfold.A: iformula
HA1: [A] ∈ ⟦A⟧syn_val
HA2: ∀ x : list iformula, x ∈ ⟦A⟧syn_val → x ⊢cf A
∃ x : list iformula, [!A] = ‼x by exists [A].
    +A: iformula
HA1: [A] ∈ ⟦A⟧syn_val
HA2: ⟦A⟧syn_val ⊆ down A
ph_bang ⟦A⟧syn_val ⊆ down (!A) apply cl_down.A: iformula
HA1: [A] ∈ ⟦A⟧syn_val
HA2: ⟦A⟧syn_val ⊆ down A
⟦A⟧syn_val ∩ J ⊆ down (!A) intros x [Hx%HA2 HJ]%elem_of_intersection.A: iformula
HA1: [A] ∈ ⟦A⟧syn_val
HA2: ⟦A⟧syn_val ⊆ down A
x: syntactic
Hx: x ∈ down A
HJ: x ∈ J
x ∈ down (!A)
      syn_simpl.A: iformula
HA1: [A] ∈ ⟦A⟧syn_val
HA2: ⟦A⟧syn_val ⊆ down A
x: list iformula
Hx: x ∈ down A
HJ: x ∈ {[ Γ | ∃ Σ : list iformula, Γ = ‼Σ ]}
x ∈ down (!A) set_unfold in HJ.A: iformula
HA1: [A] ∈ ⟦A⟧syn_val
HA2: ⟦A⟧syn_val ⊆ down A
x: list iformula
Hx: x ∈ down A
HJ: ∃ x0 : list iformula, (λ x1 : list iformula, x = ‼x1) x0
x ∈ down (!A) destruct HJ as [Σ ->].A: iformula
HA1: [A] ∈ ⟦A⟧syn_val
HA2: ⟦A⟧syn_val ⊆ down A
Σ: list iformula
Hx: ‼Σ ∈ down A
‼Σ ∈ down (!A)
      apply elem_of_down, bangR, elem_of_down, Hx.
Qed.

In the syntactic model, every context Γ is a bag for itself.

Lemma ctx_self Γ : Γ ∈ ⦅Γ⦆syn_val.Γ: list iformula
Γ ∈ ⦅Γ⦆syn_val
Proof.Γ: list iformula
Γ ∈ ⦅Γ⦆syn_val
  induction Γ as [| A Γ IH]; cbn [interp_ctx].[] ∈ one_set
A: iformula
Γ: list iformula
IH: Γ ∈ ⦅Γ⦆syn_val
A :: Γ ∈ ⟦A⟧syn_val ⊙ ⦅Γ⦆syn_val
  -[] ∈ one_set by apply elem_of_one.
  -A: iformula
Γ: list iformula
IH: Γ ∈ ⦅Γ⦆syn_val
A :: Γ ∈ ⟦A⟧syn_val ⊙ ⦅Γ⦆syn_val apply elem_of_prod.A: iformula
Γ: list iformula
IH: Γ ∈ ⦅Γ⦆syn_val
∃ a b : syntactic, a ∈ ⟦A⟧syn_val ∧ b ∈ ⦅Γ⦆syn_val ∧ A :: Γ ≡ a · b exists [A], Γ.A: iformula
Γ: list iformula
IH: Γ ∈ ⦅Γ⦆syn_val
[A] ∈ ⟦A⟧syn_val ∧ Γ ∈ ⦅Γ⦆syn_val ∧ A :: Γ ≡ [A] · Γ split_and!; [apply okada | done | done].
Qed.

The main theorems

Completeness: a valid sequent has a cut-free proof.

Theorem completeness Γ A : Γ ⊨ A -> Γ ⊢cf A.Γ: list iformula
A: iformula
Γ ⊨ A → Γ ⊢cf A
Proof.Γ: list iformula
A: iformula
Γ ⊨ A → Γ ⊢cf A
  intros H.Γ: list iformula
A: iformula
H: Γ ⊨ A
Γ ⊢cf A apply elem_of_down, (proj2 (okada A)), (H syntactic syn_val), ctx_self.
Qed.

Cut elimination: every proof can be replaced by a cut-free one.

Theorem cut_elimination Γ A : Γ ⊢ A -> Γ ⊢cf A.Γ: list iformula
A: iformula
Γ ⊢ A → Γ ⊢cf A
Proof.Γ: list iformula
A: iformula
Γ ⊢ A → Γ ⊢cf A intros H.Γ: list iformula
A: iformula
H: Γ ⊢ A
Γ ⊢cf A by apply completeness, (soundness true). Qed.

As a consequence, cut is admissible in the cut-free calculus: adding it as a rule proves nothing new.

Corollary cut_admissible Γ Δ A C : Γ ⊢cf A -> A :: Δ ⊢cf C -> Γ ++ Δ ⊢cf C.Γ, Δ: list iformula
A, C: iformula
Γ ⊢cf A → A :: Δ ⊢cf C → Γ ++ Δ ⊢cf C
Proof.Γ, Δ: list iformula
A, C: iformula
Γ ⊢cf A → A :: Δ ⊢cf C → Γ ++ Δ ⊢cf C
  intros H1 H2.Γ, Δ: list iformula
A, C: iformula
H1: Γ ⊢cf A
H2: A :: Δ ⊢cf C
Γ ++ Δ ⊢cf C apply cut_elimination, (cut _ _ _ A); [done | |];
    by apply cf_to_full.
Qed.

All three notions coincide.

Theorem provable_valid_cutfree Γ A :
  (Γ ⊢ A ↔ Γ ⊨ A) ∧ (Γ ⊨ A ↔ Γ ⊢cf A).Γ: list iformula
A: iformula
(Γ ⊢ A ↔ Γ ⊨ A) ∧ (Γ ⊨ A ↔ Γ ⊢cf A)
Proof.Γ: list iformula
A: iformula
(Γ ⊢ A ↔ Γ ⊨ A) ∧ (Γ ⊨ A ↔ Γ ⊢cf A)
  split; split.Γ: list iformula
A: iformula
Γ ⊢ A → Γ ⊨ A
Γ: list iformula
A: iformula
Γ ⊨ A → Γ ⊢ A
Γ: list iformula
A: iformula
Γ ⊨ A → Γ ⊢cf A
Γ: list iformula
A: iformula
Γ ⊢cf A → Γ ⊨ A
  -Γ: list iformula
A: iformula
Γ ⊢ A → Γ ⊨ A apply soundness.
  -Γ: list iformula
A: iformula
Γ ⊨ A → Γ ⊢ A intros H.Γ: list iformula
A: iformula
H: Γ ⊨ A
Γ ⊢ A by apply cf_to_full, completeness.
  -Γ: list iformula
A: iformula
Γ ⊨ A → Γ ⊢cf A apply completeness.
  -Γ: list iformula
A: iformula
Γ ⊢cf A → Γ ⊨ A apply soundness.
Qed.