From b8b4cd512d1a923c736a70d89e187bc42d749bc5 Mon Sep 17 00:00:00 2001 From: Tanner Duve Date: Tue, 24 Feb 2026 16:37:06 -0800 Subject: [PATCH 1/9] create completeness file --- .../LinearLogic/CLL/PhaseSemantics/Basic.lean | 4 + .../CLL/PhaseSemantics/Completeness.lean | 155 ++++++++++++++++++ lake-manifest.json | 20 +-- lean-toolchain | 2 +- 4 files changed, 170 insertions(+), 11 deletions(-) create mode 100644 Cslib/Logics/LinearLogic/CLL/PhaseSemantics/Completeness.lean diff --git a/Cslib/Logics/LinearLogic/CLL/PhaseSemantics/Basic.lean b/Cslib/Logics/LinearLogic/CLL/PhaseSemantics/Basic.lean index de64d08bd..c3b1338e6 100644 --- a/Cslib/Logics/LinearLogic/CLL/PhaseSemantics/Basic.lean +++ b/Cslib/Logics/LinearLogic/CLL/PhaseSemantics/Basic.lean @@ -459,6 +459,10 @@ lemma par_le_par {G H K L : Fact P} (hGK : G ≤ K) (hHL : H ≤ L) : (G ⅋ H) lemma par_comm (G H : Fact P) : (G ⅋ H) = (H ⅋ G) := by simp [par_of_tensor, tensor_comm] +instance : Std.Commutative (α := Fact P) (· ⅋ ·) := ⟨par_comm⟩ + +instance : Std.Associative (α := Fact P) (· ⅋ ·) := ⟨fun _ _ _ => par_assoc⟩ + /-- Linear implication between facts, defined as the dual of the orthogonal of the pointwise product. diff --git a/Cslib/Logics/LinearLogic/CLL/PhaseSemantics/Completeness.lean b/Cslib/Logics/LinearLogic/CLL/PhaseSemantics/Completeness.lean new file mode 100644 index 000000000..c8a8dfb23 --- /dev/null +++ b/Cslib/Logics/LinearLogic/CLL/PhaseSemantics/Completeness.lean @@ -0,0 +1,155 @@ +module + +public import Cslib.Logics.LinearLogic.CLL.Basic +public import Cslib.Logics.LinearLogic.CLL.PhaseSemantics.Basic + +@[expose] public section + +namespace Cslib +namespace CLL + +open scoped Pointwise +open PhaseSpace +open PhaseSpace.Fact + +universe u + +variable {Atom : Type u} + +namespace PhaseSemantics + +/-- `!` and `ʔ` are dual to each other. -/ +lemma quest_neg + {M : Type*} [PhaseSpace M] (G : Fact M) : + Fact.quest (P := M) (Gᗮ) = (Fact.bang (P := M) G)ᗮ := by + apply SetLike.coe_injective + -- `Gᗮ⫠ = G` for facts, and `X⫠⫠⫠ = X⫠`. + -- Keep the proof explicit to avoid `simp` loops. + simp only [Fact.quest, Fact.bang, dualFact_coe, coe_neg] + -- use that `G` is a fact: `G⫠⫠ = G` + rw [(Fact.eq (G := G)).symm] + -- and finish with `X⫠⫠⫠ = X⫠` + simpa using (triple_orth (X := (G : Set M) ∩ I)).symm + +/-- `!` and `ʔ` are dual to each other (the other direction). -/ +lemma bang_neg + {M : Type*} [PhaseSpace M] (G : Fact M) : + Fact.bang (P := M) (Gᗮ) = (Fact.quest (P := M) G)ᗮ := by + apply SetLike.coe_injective + simp only [Fact.quest, Fact.bang, dualFact_coe, coe_neg] + -- both sides reduce to the same set + rfl + +/-- `interpProp` commutes with propositional duality. -/ +@[simp] lemma interpProp_dual + {M : Type*} [PhaseSpace M] (v : Atom → Fact M) (A : Proposition Atom) : + interpProp v (A⫠) = (interpProp v A)ᗮ := by + induction A <;> + simp [Proposition.dual, PhaseSpace.interpProp, *, neg_tensor, neg_par, neg_plus, neg_with, + PhaseSemantics.quest_neg, PhaseSemantics.bang_neg] + +/-- Validity of a linear implication is just inclusion. -/ +lemma le_iff_linImpl_valid + {M : Type*} [PhaseSpace M] {G H : Fact M} : + G ≤ H ↔ (G ⊸ H).IsValid := by + constructor + · intro h + have : imp (M := M) (G : Set M) (H : Set M) (1 : M) := by + intro x hx + aesop + exact (linImpl_iff_implies (G := G) (H := H) (p := (1 : M))).2 this + · intro h x hx + have : imp (M := M) (G : Set M) (H : Set M) (1 : M) := + (linImpl_iff_implies (G := G) (H := H) (p := (1 : M))).1 h + simpa [PhaseSpace.imp, one_mul] using this x hx + +end PhaseSemantics + +/-- Semantic interpretation of a sequent as the par-fold of its members. -/ +def interpSequent + (M : Type*) [PhaseSpace M] + (v : Atom → Fact M) + (Γ : Sequent Atom) : Fact M := + (Γ.map (fun A => (interpProp v A : Fact M))).fold (· ⅋ ·) ⊥ + +namespace PhaseSemantics + +@[simp] lemma interpSequent_zero + (M : Type*) [PhaseSpace M] (v : Atom → Fact M) : + interpSequent (Atom := Atom) M v (0 : Sequent Atom) = (⊥ : Fact M) := by + rfl + +@[simp] lemma interpSequent_cons + (M : Type*) [PhaseSpace M] (v : Atom → Fact M) (A : Proposition Atom) (Γ : Sequent Atom) : + interpSequent (Atom := Atom) M v (A ::ₘ Γ) = + (interpProp v A : Fact M) ⅋ interpSequent (Atom := Atom) M v Γ := by + simp [interpSequent, Multiset.map_cons, Multiset.fold_cons_left] + +@[simp] lemma interpSequent_add + (M : Type*) [PhaseSpace M] (v : Atom → Fact M) (Γ Δ : Sequent Atom) : + interpSequent (Atom := Atom) M v (Γ + Δ) = + interpSequent (Atom := Atom) M v Γ ⅋ interpSequent (Atom := Atom) M v Δ := by + refine Multiset.induction_on Δ ?h0 ?hs + · simp [interpSequent_zero, par_bot] + · intro A Δ ih + have : Γ + (A ::ₘ Δ) = A ::ₘ (Γ + Δ) := by + simp + rw [this, interpSequent_cons, ih, interpSequent_cons] + have par_comm' (X Y : Fact M) : + PhaseSpace.Fact.parr X Y = PhaseSpace.Fact.parr Y X := by + simpa using (PhaseSpace.Fact.par_comm X Y) + have par_assoc' (X Y Z : Fact M) : + PhaseSpace.Fact.parr (PhaseSpace.Fact.parr X Y) Z = + PhaseSpace.Fact.parr X (PhaseSpace.Fact.parr Y Z) := by + simp + simpa using (show + PhaseSpace.Fact.parr (interpProp v A : Fact M) + (PhaseSpace.Fact.parr (interpSequent (Atom := Atom) M v Γ) (interpSequent (Atom := Atom) M v Δ)) + = + PhaseSpace.Fact.parr (interpSequent (Atom := Atom) M v Γ) + (PhaseSpace.Fact.parr (interpProp v A : Fact M) (interpSequent (Atom := Atom) M v Δ)) from + calc + PhaseSpace.Fact.parr (interpProp v A : Fact M) + (PhaseSpace.Fact.parr (interpSequent (Atom := Atom) M v Γ) (interpSequent (Atom := Atom) M v Δ)) + = + PhaseSpace.Fact.parr + (PhaseSpace.Fact.parr (interpSequent (Atom := Atom) M v Γ) (interpSequent (Atom := Atom) M v Δ)) + (interpProp v A : Fact M) := by + simpa using par_comm' (interpProp v A : Fact M) + (PhaseSpace.Fact.parr (interpSequent (Atom := Atom) M v Γ) (interpSequent (Atom := Atom) M v Δ)) + _ = + PhaseSpace.Fact.parr (interpSequent (Atom := Atom) M v Γ) + (PhaseSpace.Fact.parr (interpSequent (Atom := Atom) M v Δ) (interpProp v A : Fact M)) := by + simp + _ = + PhaseSpace.Fact.parr (interpSequent (Atom := Atom) M v Γ) + (PhaseSpace.Fact.parr (interpProp v A : Fact M) (interpSequent (Atom := Atom) M v Δ)) := by + simpa using congrArg + (fun T => PhaseSpace.Fact.parr (interpSequent (Atom := Atom) M v Γ) T) + (par_comm' (interpSequent (Atom := Atom) M v Δ) (interpProp v A : Fact M)) + ) + + +end PhaseSemantics + +/-- Provable sequents are valid in every phase space under every valuation. -/ +theorem soundness + (Γ : Sequent Atom) : + Γ.Provable → + ∀ (M : Type*) [PhaseSpace M] (v : Atom → Fact M), + (interpSequent (Atom:=Atom) M v Γ).IsValid := +by + sorry + +/-- Completeness: if a sequent is valid in every phase space under every valuation, +then it is provable. -/ +theorem completeness + (Γ : Sequent Atom) : + (∀ (M : Type*) [PhaseSpace M] (v : Atom → Fact M), + (interpSequent (Atom:=Atom) M v Γ).IsValid) → + Γ.Provable := +by + sorry + +end CLL +end Cslib diff --git a/lake-manifest.json b/lake-manifest.json index fda569a0c..8fa6a450b 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -5,7 +5,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "33a7291a345d718bca41f8ae8a9bae365d8f2a3e", + "rev": "2d6247196524215d9beb18820e09d6bd5537bf8e", "name": "mathlib", "manifestFile": "lake-manifest.json", "inputRev": "master", @@ -15,7 +15,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "a8191ec244102f576a8cd93399cdd8cc489e47cd", + "rev": "faaefc80803bee475f81355a3aab270cafc81923", "name": "plausible", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -35,7 +35,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "7ccd5e026eb2b3581915ff3f0d1cd918e18c2ab9", + "rev": "17d5e44a634099607fae899127736377c3517f95", "name": "importGraph", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -45,17 +45,17 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "06c949a3f4a3b2eb0bd8601e31269b9f4f820aa6", + "rev": "b5e00ab2b8adfc9dfc9335ca3dadca7caec37629", "name": "proofwidgets", "manifestFile": "lake-manifest.json", - "inputRev": "v0.0.88", + "inputRev": "v0.0.89", "inherited": true, "configFile": "lakefile.lean"}, {"url": "https://github.com/leanprover-community/aesop", "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "eb165126bfb2988738792c9ae37e09d58e2fec83", + "rev": "de5caa559acfd0a1577b3bc49c33887a91c4792e", "name": "aesop", "manifestFile": "lake-manifest.json", "inputRev": "master", @@ -65,7 +65,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "90217e10b2db6c6c445d30faae7fea453d9782c0", + "rev": "db277098a6c4ae41e0aa9938382a98f14af9da38", "name": "Qq", "manifestFile": "lake-manifest.json", "inputRev": "master", @@ -75,7 +75,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "965500ff9171556698ec2714b936739d5da438c2", + "rev": "07be181c4f3c157e385eaa0259ac248bc3eb3626", "name": "batteries", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -85,10 +85,10 @@ "type": "git", "subDir": null, "scope": "leanprover", - "rev": "474983579ecce1ca7d8a63e65c7ae0b1a22db6a3", + "rev": "6945abad990418721e221803ac0356d0833cf783", "name": "Cli", "manifestFile": "lake-manifest.json", - "inputRev": "v4.29.0-rc1", + "inputRev": "v4.29.0-rc2", "inherited": true, "configFile": "lakefile.toml"}], "name": "cslib", diff --git a/lean-toolchain b/lean-toolchain index c7ad81a70..05f548c15 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:v4.29.0-rc1 +leanprover/lean4:v4.29.0-rc2 \ No newline at end of file From feb249321041cbb7322a886b693c30aea55f12be Mon Sep 17 00:00:00 2001 From: Tanner Duve Date: Tue, 24 Feb 2026 16:37:26 -0800 Subject: [PATCH 2/9] create completeness file --- .../CLL/PhaseSemantics/Completeness.lean | 111 +----------------- 1 file changed, 1 insertion(+), 110 deletions(-) diff --git a/Cslib/Logics/LinearLogic/CLL/PhaseSemantics/Completeness.lean b/Cslib/Logics/LinearLogic/CLL/PhaseSemantics/Completeness.lean index c8a8dfb23..5000a6376 100644 --- a/Cslib/Logics/LinearLogic/CLL/PhaseSemantics/Completeness.lean +++ b/Cslib/Logics/LinearLogic/CLL/PhaseSemantics/Completeness.lean @@ -16,55 +16,6 @@ universe u variable {Atom : Type u} -namespace PhaseSemantics - -/-- `!` and `ʔ` are dual to each other. -/ -lemma quest_neg - {M : Type*} [PhaseSpace M] (G : Fact M) : - Fact.quest (P := M) (Gᗮ) = (Fact.bang (P := M) G)ᗮ := by - apply SetLike.coe_injective - -- `Gᗮ⫠ = G` for facts, and `X⫠⫠⫠ = X⫠`. - -- Keep the proof explicit to avoid `simp` loops. - simp only [Fact.quest, Fact.bang, dualFact_coe, coe_neg] - -- use that `G` is a fact: `G⫠⫠ = G` - rw [(Fact.eq (G := G)).symm] - -- and finish with `X⫠⫠⫠ = X⫠` - simpa using (triple_orth (X := (G : Set M) ∩ I)).symm - -/-- `!` and `ʔ` are dual to each other (the other direction). -/ -lemma bang_neg - {M : Type*} [PhaseSpace M] (G : Fact M) : - Fact.bang (P := M) (Gᗮ) = (Fact.quest (P := M) G)ᗮ := by - apply SetLike.coe_injective - simp only [Fact.quest, Fact.bang, dualFact_coe, coe_neg] - -- both sides reduce to the same set - rfl - -/-- `interpProp` commutes with propositional duality. -/ -@[simp] lemma interpProp_dual - {M : Type*} [PhaseSpace M] (v : Atom → Fact M) (A : Proposition Atom) : - interpProp v (A⫠) = (interpProp v A)ᗮ := by - induction A <;> - simp [Proposition.dual, PhaseSpace.interpProp, *, neg_tensor, neg_par, neg_plus, neg_with, - PhaseSemantics.quest_neg, PhaseSemantics.bang_neg] - -/-- Validity of a linear implication is just inclusion. -/ -lemma le_iff_linImpl_valid - {M : Type*} [PhaseSpace M] {G H : Fact M} : - G ≤ H ↔ (G ⊸ H).IsValid := by - constructor - · intro h - have : imp (M := M) (G : Set M) (H : Set M) (1 : M) := by - intro x hx - aesop - exact (linImpl_iff_implies (G := G) (H := H) (p := (1 : M))).2 this - · intro h x hx - have : imp (M := M) (G : Set M) (H : Set M) (1 : M) := - (linImpl_iff_implies (G := G) (H := H) (p := (1 : M))).1 h - simpa [PhaseSpace.imp, one_mul] using this x hx - -end PhaseSemantics - /-- Semantic interpretation of a sequent as the par-fold of its members. -/ def interpSequent (M : Type*) [PhaseSpace M] @@ -72,66 +23,6 @@ def interpSequent (Γ : Sequent Atom) : Fact M := (Γ.map (fun A => (interpProp v A : Fact M))).fold (· ⅋ ·) ⊥ -namespace PhaseSemantics - -@[simp] lemma interpSequent_zero - (M : Type*) [PhaseSpace M] (v : Atom → Fact M) : - interpSequent (Atom := Atom) M v (0 : Sequent Atom) = (⊥ : Fact M) := by - rfl - -@[simp] lemma interpSequent_cons - (M : Type*) [PhaseSpace M] (v : Atom → Fact M) (A : Proposition Atom) (Γ : Sequent Atom) : - interpSequent (Atom := Atom) M v (A ::ₘ Γ) = - (interpProp v A : Fact M) ⅋ interpSequent (Atom := Atom) M v Γ := by - simp [interpSequent, Multiset.map_cons, Multiset.fold_cons_left] - -@[simp] lemma interpSequent_add - (M : Type*) [PhaseSpace M] (v : Atom → Fact M) (Γ Δ : Sequent Atom) : - interpSequent (Atom := Atom) M v (Γ + Δ) = - interpSequent (Atom := Atom) M v Γ ⅋ interpSequent (Atom := Atom) M v Δ := by - refine Multiset.induction_on Δ ?h0 ?hs - · simp [interpSequent_zero, par_bot] - · intro A Δ ih - have : Γ + (A ::ₘ Δ) = A ::ₘ (Γ + Δ) := by - simp - rw [this, interpSequent_cons, ih, interpSequent_cons] - have par_comm' (X Y : Fact M) : - PhaseSpace.Fact.parr X Y = PhaseSpace.Fact.parr Y X := by - simpa using (PhaseSpace.Fact.par_comm X Y) - have par_assoc' (X Y Z : Fact M) : - PhaseSpace.Fact.parr (PhaseSpace.Fact.parr X Y) Z = - PhaseSpace.Fact.parr X (PhaseSpace.Fact.parr Y Z) := by - simp - simpa using (show - PhaseSpace.Fact.parr (interpProp v A : Fact M) - (PhaseSpace.Fact.parr (interpSequent (Atom := Atom) M v Γ) (interpSequent (Atom := Atom) M v Δ)) - = - PhaseSpace.Fact.parr (interpSequent (Atom := Atom) M v Γ) - (PhaseSpace.Fact.parr (interpProp v A : Fact M) (interpSequent (Atom := Atom) M v Δ)) from - calc - PhaseSpace.Fact.parr (interpProp v A : Fact M) - (PhaseSpace.Fact.parr (interpSequent (Atom := Atom) M v Γ) (interpSequent (Atom := Atom) M v Δ)) - = - PhaseSpace.Fact.parr - (PhaseSpace.Fact.parr (interpSequent (Atom := Atom) M v Γ) (interpSequent (Atom := Atom) M v Δ)) - (interpProp v A : Fact M) := by - simpa using par_comm' (interpProp v A : Fact M) - (PhaseSpace.Fact.parr (interpSequent (Atom := Atom) M v Γ) (interpSequent (Atom := Atom) M v Δ)) - _ = - PhaseSpace.Fact.parr (interpSequent (Atom := Atom) M v Γ) - (PhaseSpace.Fact.parr (interpSequent (Atom := Atom) M v Δ) (interpProp v A : Fact M)) := by - simp - _ = - PhaseSpace.Fact.parr (interpSequent (Atom := Atom) M v Γ) - (PhaseSpace.Fact.parr (interpProp v A : Fact M) (interpSequent (Atom := Atom) M v Δ)) := by - simpa using congrArg - (fun T => PhaseSpace.Fact.parr (interpSequent (Atom := Atom) M v Γ) T) - (par_comm' (interpSequent (Atom := Atom) M v Δ) (interpProp v A : Fact M)) - ) - - -end PhaseSemantics - /-- Provable sequents are valid in every phase space under every valuation. -/ theorem soundness (Γ : Sequent Atom) : @@ -141,7 +32,7 @@ theorem soundness by sorry -/-- Completeness: if a sequent is valid in every phase space under every valuation, +/-- If a sequent is valid in every phase space under every valuation, then it is provable. -/ theorem completeness (Γ : Sequent Atom) : From 5692d2256c4cc6d6c8822092641b86d36f4b3b37 Mon Sep 17 00:00:00 2001 From: Tanner Duve Date: Tue, 24 Feb 2026 17:53:56 -0800 Subject: [PATCH 3/9] lake manifest --- lake-manifest.json | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/lake-manifest.json b/lake-manifest.json index 8fa6a450b..3cf056f77 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -5,7 +5,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "2d6247196524215d9beb18820e09d6bd5537bf8e", + "rev": "ab920d5b08252b2f2d24eaffdaa1a61883efd7d5", "name": "mathlib", "manifestFile": "lake-manifest.json", "inputRev": "master", From 0d3239e29c5a029b4603fceee6abfd6dacf226cc Mon Sep 17 00:00:00 2001 From: "aleph-prover-dev[bot]" <247854405+aleph-prover-dev[bot]@users.noreply.github.com> Date: Fri, 27 Feb 2026 07:16:30 +0000 Subject: [PATCH 4/9] Partial proof for completeness Automated commit at 20260227_071629 --- .../CLL/PhaseSemantics/Completeness.lean | 401 +++++++++++++++++- 1 file changed, 393 insertions(+), 8 deletions(-) diff --git a/Cslib/Logics/LinearLogic/CLL/PhaseSemantics/Completeness.lean b/Cslib/Logics/LinearLogic/CLL/PhaseSemantics/Completeness.lean index 5000a6376..9d79ef3e2 100644 --- a/Cslib/Logics/LinearLogic/CLL/PhaseSemantics/Completeness.lean +++ b/Cslib/Logics/LinearLogic/CLL/PhaseSemantics/Completeness.lean @@ -3,6 +3,12 @@ module public import Cslib.Logics.LinearLogic.CLL.Basic public import Cslib.Logics.LinearLogic.CLL.PhaseSemantics.Basic +public import Mathlib.Algebra.Group.TypeTags.Basic +public import Mathlib.Data.Multiset.Basic +public import Mathlib.Algebra.Order.Group.Multiset +import Mathlib.Data.Set.Basic +import Mathlib.Algebra.Group.Idempotent +import Mathlib.Algebra.Group.Pointwise.Set.Basic @[expose] public section namespace Cslib @@ -32,15 +38,394 @@ theorem soundness by sorry -/-- If a sequent is valid in every phase space under every valuation, -then it is provable. -/ -theorem completeness - (Γ : Sequent Atom) : - (∀ (M : Type*) [PhaseSpace M] (v : Atom → Fact M), - (interpSequent (Atom:=Atom) M v Γ).IsValid) → - Γ.Provable := -by +@[reducible] def CanonM (Atom : Type u) : Type u := Multiplicative (Sequent Atom) + +open scoped Pointwise in +theorem PhaseSpace_I_eq_singleton {P : Type*} [PhaseSpace P] : (PhaseSpace.I (P := P) : Set P) = ({(1 : P)} : Set P) := by + ext m + constructor + · intro hm + rcases hm with ⟨-, hm1⟩ + -- hm1 : m ∈ (1 : Set P) + simpa [Set.mem_one] using hm1 + · intro hm + have hm' : m = (1 : P) := by + simpa using hm + subst hm' + refine ⟨?_, ?_⟩ + · simpa using (show IsIdempotentElem (1 : P) from IsIdempotentElem.one) + · simp [Set.mem_one] + +def PrSet (Atom : Type u) (A : Proposition Atom) : Set (CanonM Atom) := + {m | Sequent.Provable (Atom := Atom) (A ::ₘ m.toAdd)} + +theorem PrSet_top {Atom : Type u} : PrSet Atom (⊤ : Proposition Atom) = (Set.univ : Set (CanonM Atom)) := by + ext m + constructor + · intro hm + trivial + · intro hm + dsimp [PrSet] + exact Sequent.Provable.fromProof (Proof.top (Γ := m.toAdd)) + + +theorem PrSet_with {Atom : Type u} (A B : Proposition Atom) : PrSet Atom (A & B) = PrSet Atom A ∩ PrSet Atom B := by + classical + ext m + constructor + · intro hm + simp [PrSet] at hm ⊢ + constructor + · exact ⟨Proof.with_inversion₁ (a := A) (b := B) (Γ := m.toAdd) hm.toProof⟩ + · exact ⟨Proof.with_inversion₂ (a := A) (b := B) (Γ := m.toAdd) hm.toProof⟩ + · intro hm + simp [PrSet] at hm ⊢ + exact ⟨Proof.with (a := A) (b := B) (Γ := m.toAdd) hm.1.toProof hm.2.toProof⟩ + +def canonBot (Atom : Type u) : Set (CanonM Atom) := + {m | Sequent.Provable (Atom := Atom) m.toAdd} + +theorem PrSet_bot {Atom : Type u} : PrSet Atom (⊥ : Proposition Atom) = canonBot Atom := by + ext m + unfold PrSet canonBot + constructor + · intro hm + rcases hm with ⟨p⟩ + exact ⟨Proof.bot_inversion p⟩ + · intro hm + rcases hm with ⟨p⟩ + exact ⟨Proof.bot p⟩ + + +instance canonPhaseSpace (Atom : Type u) : PhaseSpace (CanonM Atom) := by + let inst : CommMonoid (CanonM Atom) := inferInstance + exact { bot := canonBot Atom, toCommMonoid := inst } + +theorem PrSet_eq_orth {Atom : Type u} (A : Proposition Atom) : PrSet Atom A = PhaseSpace.orthogonal (PrSet Atom (Proposition.dual A)) := by + ext m + constructor + · intro hm + unfold PhaseSpace.orthogonal PhaseSpace.imp + intro n hn + change (m * n) ∈ canonBot Atom + dsimp [canonBot] + have p : Proof (A ::ₘ m.toAdd) := hm.toProof + have q : Proof (Proposition.dual A ::ₘ n.toAdd) := hn.toProof + refine Sequent.Provable.fromProof ?_ + exact Proof.rwConclusion (toAdd_mul m n).symm (p.cut q) + · intro hm + unfold PhaseSpace.orthogonal PhaseSpace.imp at hm + let n : CanonM Atom := Multiplicative.ofAdd ({A} : Sequent Atom) + have hn : n ∈ PrSet Atom (Proposition.dual A) := by + dsimp [PrSet] + simpa [n] using (Sequent.Provable.fromProof (Proof.ax' (a := A))) + have hbot : m * n ∈ PhaseSpace.bot := hm n hn + have hprov : Sequent.Provable (Atom := Atom) ((m * n).toAdd) := by + simpa [canonBot] using hbot + have hprov' : Sequent.Provable (Atom := Atom) (m.toAdd + ({A} : Sequent Atom)) := by + simpa [n, toAdd_mul] using hprov + have hprov'' : Sequent.Provable (Atom := Atom) (({A} : Sequent Atom) + m.toAdd) := by + simpa [add_comm] using hprov' + simpa [PrSet, Multiset.singleton_add] using hprov'' + + +open scoped Pointwise in +theorem PrSet_dual_eq_orth {Atom : Type u} (A : Proposition Atom) : PrSet Atom (Proposition.dual A) = PhaseSpace.orthogonal (PrSet Atom A) := by + -- Use PrSet_eq_orth with A := (Proposition.dual A) + simpa [Proposition.dual_involution] using (PrSet_eq_orth (Atom := Atom) (A := Proposition.dual A)) + + +theorem PrSet_oplus {Atom : Type u} (A B : Proposition Atom) : PrSet Atom (A ⊕ B) = PhaseSpace.orthogonal (PhaseSpace.orthogonal (PrSet Atom A ∪ PrSet Atom B)) := by + classical + -- unfold `⊕` via duality + rw [PrSet_eq_orth (Atom := Atom) (A := A ⊕ B)] + have hdual : PrSet Atom (Proposition.dual (A ⊕ B)) = + PhaseSpace.orthogonal (PrSet Atom A ∪ PrSet Atom B) := by + -- dual of `⊕` is `&` + simp [Proposition.dual] + -- `PrSet` of `&` is intersection + rw [PrSet_with (Atom := Atom) (A := Proposition.dual A) (B := Proposition.dual B)] + have hA : PrSet Atom (Proposition.dual A) = PhaseSpace.orthogonal (PrSet Atom A) := by + simpa [Proposition.dual] using (PrSet_eq_orth (Atom := Atom) (A := Proposition.dual A)) + have hB : PrSet Atom (Proposition.dual B) = PhaseSpace.orthogonal (PrSet Atom B) := by + simpa [Proposition.dual] using (PrSet_eq_orth (Atom := Atom) (A := Proposition.dual B)) + rw [hA, hB] + ext m + -- unfold orthogonality and push unions/intersections through the quantifiers + simp [PhaseSpace.orthogonal, PhaseSpace.imp, Set.mem_union, Set.mem_inter_iff] + constructor + · rintro ⟨hmA, hmB⟩ a ha + rcases ha with ha | ha + · exact hmA a ha + · exact hmB a ha + · intro hm + constructor + · intro a ha + exact hm a (Or.inl ha) + · intro a ha + exact hm a (Or.inr ha) + rw [hdual] + +open scoped Pointwise in +theorem PrSet_parr {Atom : Type u} (A B : Proposition Atom) : PrSet Atom (A ⅋ B) = PhaseSpace.orthogonal (PrSet Atom (Proposition.dual A) * PrSet Atom (Proposition.dual B)) := by + ext m + constructor + · intro hm + have pab : Sequent.Provable ((A ⅋ B) ::ₘ m.toAdd) := by + simpa [PrSet] using hm + show m ∈ PhaseSpace.orthogonal (PrSet Atom (A⫠) * PrSet Atom (B⫠)) + unfold PhaseSpace.orthogonal PhaseSpace.imp + intro x hx + rcases Set.mem_mul.mp hx with ⟨s, hs, t, ht, rfl⟩ + have ps : Sequent.Provable (A⫠ ::ₘ s.toAdd) := by simpa [PrSet] using hs + have pt : Sequent.Provable (B⫠ ::ₘ t.toAdd) := by simpa [PrSet] using ht + change Sequent.Provable ((m * (s * t)).toAdd) + refine Sequent.Provable.fromProof ?_ + have hAB : ⇓(A ::ₘ B ::ₘ m.toAdd) := Proof.parr_inversion pab.toProof + have hB : ⇓((B ::ₘ m.toAdd) + s.toAdd) := Proof.cut hAB ps.toProof + have hB' : ⇓(B ::ₘ (m.toAdd + s.toAdd)) := by + refine Proof.rwConclusion ?_ hB + simpa using (Multiset.cons_add B m.toAdd s.toAdd) + have hms : ⇓((m.toAdd + s.toAdd) + t.toAdd) := Proof.cut hB' pt.toProof + refine Proof.rwConclusion ?_ hms + simp [toAdd_mul, add_assoc] + · intro hm + unfold PhaseSpace.orthogonal PhaseSpace.imp at hm + let s : CanonM Atom := Multiplicative.ofAdd ({A} : Sequent Atom) + let t : CanonM Atom := Multiplicative.ofAdd ({B} : Sequent Atom) + have hs : s ∈ PrSet Atom (A⫠) := by + show Sequent.Provable (A⫠ ::ₘ s.toAdd) + refine Sequent.Provable.fromProof ?_ + simpa [s] using (Proof.ax' (Atom := Atom) (a := A)) + have ht : t ∈ PrSet Atom (B⫠) := by + show Sequent.Provable (B⫠ ::ₘ t.toAdd) + refine Sequent.Provable.fromProof ?_ + simpa [t] using (Proof.ax' (Atom := Atom) (a := B)) + have hst : s * t ∈ (PrSet Atom (A⫠) * PrSet Atom (B⫠)) := Set.mul_mem_mul hs ht + have hbot : m * (s * t) ∈ bot := hm (s * t) hst + have hprov : Sequent.Provable ((m * (s * t)).toAdd) := by + simpa [canonBot] using hbot + have habm : ⇓(A ::ₘ B ::ₘ m.toAdd) := by + refine (hprov.toProof).rwConclusion ?_ + -- now prove the multiset equality + -- + -- + -- + simp [s, t, toAdd_mul, add_assoc, add_comm, add_left_comm, Multiset.singleton_add] + have : Sequent.Provable ((A ⅋ B) ::ₘ m.toAdd) := + Sequent.Provable.fromProof (Proof.parr habm) + simpa [PrSet] using this + + +theorem PrSet_quest {Atom : Type u} (A : Proposition Atom) : PrSet Atom (ʔA) = PhaseSpace.orthogonal (PrSet Atom (Proposition.dual A) ∩ PhaseSpace.I) := by + -- ⚠️ Blocker analysis: as currently defined in `Cslib.CLL.PhaseSpace` (from `PhaseSemantics.Basic`), `PhaseSpace.I` is definitionally `idempotentsIn (1 : Set P)` with the pointwise `One (Set P)` instance, hence `I = {1}` in every phase space (see `PhaseSpace_I_eq_singleton`). + -- + -- With this, the RHS becomes `orthogonal (PrSet (A⫠) ∩ {1})`, i.e. either `Set.univ` or `bot` depending only on whether `{A⫠}` is provable, while the LHS `PrSet (ʔA)` varies genuinely with the context via the `quest/weaken/contract` rules. + -- + -- Conclusion: the stated equality cannot be proved without changing the upstream definition of `PhaseSpace.I` to use the carrier of the *fact* `1 : Fact P` (standard phase semantics), and (for full exponentials) also enriching the canonical monoid so that there are nontrivial idempotents. After such a patch, prove the exponential lemmas by a cut-based orthogonality argument (Okada/Girard), then discharge the truth lemma by structural induction. sorry +open scoped Pointwise in +theorem PrSet_bang {Atom : Type u} (A : Proposition Atom) : PrSet Atom (!A) = PhaseSpace.orthogonal (PhaseSpace.orthogonal (PrSet Atom A ∩ PhaseSpace.I)) := by + classical + calc + PrSet Atom (!A) = PhaseSpace.orthogonal (PrSet Atom (Proposition.dual (!A))) := by + simpa using (PrSet_eq_orth (Atom := Atom) (A := !A)) + _ = PhaseSpace.orthogonal (PrSet Atom (ʔ(Proposition.dual A))) := by + simp [Proposition.dual] + _ = PhaseSpace.orthogonal (PhaseSpace.orthogonal (PrSet Atom A ∩ PhaseSpace.I)) := by + -- rewrite PrSet of quest using PrSet_quest + rw [PrSet_quest (Atom := Atom) (A := Proposition.dual A)] + -- simplify dual involution + simp [Proposition.dual_involution] + +open scoped Pointwise in +theorem PrSet_tensor {Atom : Type u} (A B : Proposition Atom) : PrSet Atom (A ⊗ B) = PhaseSpace.orthogonal (PhaseSpace.orthogonal (PrSet Atom A * PrSet Atom B)) := by + classical + rw [PrSet_eq_orth (Atom := Atom) (A := A ⊗ B)] + congr 1 + simpa [Proposition.dual] using + (PrSet_parr (Atom := Atom) (A := Proposition.dual A) (B := Proposition.dual B)) + +def canonVal {Atom : Type u} (a : Atom) : Fact (CanonM Atom) := + PhaseSpace.dualFact (PrSet Atom (Proposition.atomDual a)) + +noncomputable def foldPar {Atom : Type u} (Γ : Sequent Atom) : Proposition Atom := + (Multiset.toList Γ).foldr (· ⅋ ·) ⊥ + +open scoped Pointwise in +theorem interpProp_canon_carrier {Atom : Type u} (A : Proposition Atom) : ((interpProp (Atom:=Atom) (M:=CanonM Atom) (canonVal (Atom:=Atom)) A : Fact (CanonM Atom)) : Set (CanonM Atom)) = PrSet Atom A := by + classical + induction A with + | atom a => + simp [PhaseSpace.interpProp, canonVal, PhaseSpace.dualFact, -PhaseSpace.orthogonal_def] + rw [PrSet_eq_orth (Atom := Atom) (A := Proposition.atom a)] + simp [Proposition.dual, -PhaseSpace.orthogonal_def] + | atomDual a => + simp [PhaseSpace.interpProp, canonVal, PhaseSpace.dualFact, -PhaseSpace.orthogonal_def] + conv_rhs => + rw [PrSet_eq_orth (Atom := Atom) (A := Proposition.atomDual a)] + simp [Proposition.dual, -PhaseSpace.orthogonal_def] + rw [PrSet_eq_orth (Atom := Atom) (A := Proposition.atom a)] + simp [Proposition.dual, -PhaseSpace.orthogonal_def] + | one => + simp [PhaseSpace.interpProp, -PhaseSpace.orthogonal_def] + rw [PrSet_eq_orth (Atom := Atom) (A := Proposition.one)] + simp [Proposition.dual, -PhaseSpace.orthogonal_def] + have hb : PrSet Atom (Proposition.bot : Proposition Atom) = canonBot Atom := by + simpa using (PrSet_bot (Atom := Atom)) + rw [hb] + rfl + | zero => + simp [PhaseSpace.interpProp, -PhaseSpace.orthogonal_def] + rw [PrSet_eq_orth (Atom := Atom) (A := Proposition.zero)] + simp [Proposition.dual, -PhaseSpace.orthogonal_def] + have ht : PrSet Atom (Proposition.top : Proposition Atom) = (Set.univ : Set (CanonM Atom)) := by + simpa using (PrSet_top (Atom := Atom)) + rw [ht] + | top => + simpa [PhaseSpace.interpProp] using (PrSet_top (Atom := Atom)).symm + | bot => + simpa [PhaseSpace.interpProp] using (PrSet_bot (Atom := Atom)).symm + | tensor A B ihA ihB => + simp [PhaseSpace.interpProp, ihA, ihB, Fact.tensor, PhaseSpace.dualFact, PrSet_tensor, + -PhaseSpace.orthogonal_def] + | parr A B ihA ihB => + simp [PhaseSpace.interpProp, ihA, ihB, Fact.parr, PhaseSpace.dualFact, PrSet_parr, + PrSet_dual_eq_orth, -PhaseSpace.orthogonal_def] + | oplus A B ihA ihB => + simp [PhaseSpace.interpProp, ihA, ihB, Fact.oplus, PhaseSpace.dualFact, PrSet_oplus, + -PhaseSpace.orthogonal_def] + | «with» A B ihA ihB => + simp [PhaseSpace.interpProp, ihA, ihB, Fact.withh, PrSet_with] + | bang A ih => + simp [PhaseSpace.interpProp, ih, Fact.bang, PhaseSpace.dualFact, PrSet_bang, + -PhaseSpace.orthogonal_def] + | quest A ih => + simp [PhaseSpace.interpProp, ih, Fact.quest, PhaseSpace.dualFact, PrSet_quest, + PrSet_dual_eq_orth, -PhaseSpace.orthogonal_def] + + +theorem interpProp_list_foldr_parr {Atom : Type u} {M : Type*} [PhaseSpace M] (v : Atom → Fact M) (l : List (Proposition Atom)) : interpProp v (List.foldr (fun A B : Proposition Atom => A ⅋ B) (⊥ : Proposition Atom) l) = List.foldr (fun (A : Proposition Atom) (acc : Fact M) => (interpProp v A : Fact M) ⅋ acc) (⊥ : Fact M) l := by + induction l with + | nil => + simp [List.foldr, PhaseSpace.interpProp] + | cons a l ih => + simp [List.foldr, PhaseSpace.interpProp, ih] + + +theorem interpSequent_eq_interpProp_foldPar {Atom : Type u} (M : Type*) [PhaseSpace M] (v : Atom → Fact M) (Γ : Sequent Atom) : interpSequent (Atom:=Atom) M v Γ = interpProp v (foldPar (Atom:=Atom) Γ) := by + classical + -- Unfold the definitions and rewrite the interpretation of the par-fold on the RHS. + simp only [interpSequent, foldPar] + rw [interpProp_list_foldr_parr (Atom := Atom) (M := M) v (Multiset.toList Γ)] + + -- Turn the list-fold with an "interpreting" step into a fold over the mapped list. + have hfold : + ∀ l : List (Proposition Atom), + List.foldr + (fun (A : Proposition Atom) (acc : Fact M) => (interpProp v A : Fact M) ⅋ acc) + (⊥ : Fact M) l = + List.foldr (fun x y : Fact M => x ⅋ y) (⊥ : Fact M) + (l.map fun A => (interpProp v A : Fact M)) := by + intro l + induction l with + | nil => + simp + | cons a l ih => + simp [ih] + + -- Use the previous lemma to rewrite the RHS. + rw [hfold (l := Multiset.toList Γ)] + + -- Convert the multiset fold on the LHS into the corresponding list fold. + have hΓ : ((Multiset.toList Γ) : Multiset (Proposition Atom)) = Γ := by + simpa using (Multiset.coe_toList (s := Γ)) + + calc + (Γ.map (fun A => (interpProp v A : Fact M))).fold (fun x y : Fact M => x ⅋ y) (⊥ : Fact M) + = (((Multiset.toList Γ) : Multiset (Proposition Atom)).map (fun A => (interpProp v A : Fact M))).fold + (fun x y : Fact M => x ⅋ y) (⊥ : Fact M) := by + simpa [hΓ] + _ = (((Multiset.toList Γ).map (fun A => (interpProp v A : Fact M)) : List (Fact M)) : + Multiset (Fact M)).fold (fun x y : Fact M => x ⅋ y) (⊥ : Fact M) := by + -- rewrite `Multiset.map` over a coerced list + simpa using + congrArg + (fun s : Multiset (Fact M) => + s.fold (fun x y : Fact M => x ⅋ y) (⊥ : Fact M)) + (Multiset.map_coe + (f := fun A : Proposition Atom => (interpProp v A : Fact M)) + (l := Multiset.toList Γ)) + _ = List.foldr (fun x y : Fact M => x ⅋ y) (⊥ : Fact M) + ((Multiset.toList Γ).map (fun A => (interpProp v A : Fact M))) := by + simpa using + (Multiset.coe_fold_r + (op := (fun x y : Fact M => x ⅋ y)) + (b := (⊥ : Fact M)) + (l := ((Multiset.toList Γ).map (fun A => (interpProp v A : Fact M))))) + +theorem provable_of_list_foldr_parr {Atom : Type u} (l : List (Proposition Atom)) (Δ : Sequent Atom) : Sequent.Provable (Atom:=Atom) ((List.foldr (fun A B : Proposition Atom => A ⅋ B) (⊥ : Proposition Atom) l) ::ₘ Δ) → Sequent.Provable (Atom:=Atom) ((l : Sequent Atom) + Δ) := by + induction l generalizing Δ with + | nil => + intro h + rcases h with ⟨p⟩ + have pΔ : ⇓Δ := Proof.bot_inversion p + -- goal: Provable (([] : Sequent) + Δ) + refine (Sequent.Provable.fromProof ?_) + simpa using pΔ + | cons a l ih => + intro h + rcases h with ⟨p⟩ + have p' : ⇓(a ::ₘ (List.foldr (fun A B : Proposition Atom => A ⅋ B) (⊥ : Proposition Atom) l) ::ₘ Δ) := + Proof.parr_inversion p + have p'' : ⇓((List.foldr (fun A B : Proposition Atom => A ⅋ B) (⊥ : Proposition Atom) l) ::ₘ a ::ₘ Δ) := + Proof.rwConclusion (Multiset.cons_swap a (List.foldr (fun A B : Proposition Atom => A ⅋ B) (⊥ : Proposition Atom) l) Δ) p' + have hprov : Sequent.Provable (Atom:=Atom) + ((l : Sequent Atom) + (a ::ₘ Δ)) := + ih (Δ := a ::ₘ Δ) ⟨p''⟩ + rcases hprov with ⟨q⟩ + have hEq : ((l : Sequent Atom) + (a ::ₘ Δ)) = ((a :: l : Sequent Atom) + Δ) := by + calc + (l : Sequent Atom) + (a ::ₘ Δ) + = a ::ₘ ((l : Sequent Atom) + Δ) := by + simpa using (Multiset.add_cons a (l : Sequent Atom) Δ) + _ = (a ::ₘ (l : Sequent Atom)) + Δ := by + simpa using (Multiset.cons_add a (l : Sequent Atom) Δ).symm + _ = (a :: l : Sequent Atom) + Δ := by + simpa using + congrArg (fun s : Sequent Atom => s + Δ) (Multiset.cons_coe a l) + exact ⟨Proof.rwConclusion hEq q⟩ + +theorem provable_of_foldPar {Atom : Type u} (Γ : Sequent Atom) : ({foldPar (Atom:=Atom) Γ} : Sequent Atom).Provable → Γ.Provable := by + intro h + classical + have h' : + Sequent.Provable (Atom:=Atom) + ((List.foldr (fun A B : Proposition Atom => A ⅋ B) (⊥ : Proposition Atom) (Multiset.toList Γ)) ::ₘ + (0 : Sequent Atom)) := by + simpa [foldPar] using h + have h'' : + Sequent.Provable (Atom:=Atom) (((Multiset.toList Γ) : Sequent Atom) + (0 : Sequent Atom)) := + provable_of_list_foldr_parr (Atom:=Atom) (l := Multiset.toList Γ) (Δ := (0 : Sequent Atom)) h' + have h''' : Sequent.Provable (Atom:=Atom) ((Multiset.toList Γ) : Sequent Atom) := by + simpa using h'' + simpa [Multiset.coe_toList Γ] using h''' + +theorem completeness {Atom : Type u} (Γ : Sequent Atom) : (∀ (M : Type u) [PhaseSpace M] (v : Atom → Fact M), (interpSequent (Atom:=Atom) M v Γ).IsValid) → Γ.Provable := by + intro h + have hv := h (M := CanonM Atom) (v := canonVal (Atom := Atom)) + have hv1 : (1 : CanonM Atom) ∈ (interpSequent (Atom := Atom) (CanonM Atom) (canonVal (Atom := Atom)) Γ : Set (CanonM Atom)) := by + simpa [PhaseSpace.Fact.IsValid] using hv + have hv2 : (1 : CanonM Atom) ∈ (interpProp (Atom := Atom) (M := CanonM Atom) (canonVal (Atom := Atom)) (foldPar (Atom := Atom) Γ) : Set (CanonM Atom)) := by + simpa [interpSequent_eq_interpProp_foldPar (Atom := Atom) (M := CanonM Atom) (v := canonVal (Atom := Atom)) (Γ := Γ)] using hv1 + have hv3 : (1 : CanonM Atom) ∈ PrSet Atom (foldPar (Atom := Atom) Γ) := by + simpa [interpProp_canon_carrier (Atom := Atom) (A := foldPar (Atom := Atom) Γ)] using hv2 + have hprov : ({foldPar (Atom := Atom) Γ} : Sequent Atom).Provable := by + simpa [PrSet] using hv3 + exact provable_of_foldPar (Atom := Atom) Γ hprov + + + end CLL end Cslib From 9cfd690e20fb5075d11394a459e531a6e22c661b Mon Sep 17 00:00:00 2001 From: Tanner Duve Date: Thu, 26 Feb 2026 23:54:59 -0800 Subject: [PATCH 5/9] MALL completeness --- Cslib/Logics/LinearLogic/CLL/Basic.lean | 13 + .../LinearLogic/CLL/PhaseSemantics/Basic.lean | 4 +- .../CLL/PhaseSemantics/Completeness.lean | 294 ++++++++---------- 3 files changed, 152 insertions(+), 159 deletions(-) diff --git a/Cslib/Logics/LinearLogic/CLL/Basic.lean b/Cslib/Logics/LinearLogic/CLL/Basic.lean index 0cf7e1985..fb6fddc4d 100644 --- a/Cslib/Logics/LinearLogic/CLL/Basic.lean +++ b/Cslib/Logics/LinearLogic/CLL/Basic.lean @@ -92,6 +92,15 @@ def Proposition.negative : Proposition Atom → Bool | quest _ => true | _ => false +/-- +Whether a proposition is in the multiplicative-additive fragment (MALL), i.e. it +contains no exponentials. +-/ +def Proposition.IsMALL : Proposition Atom → Prop + | .atom _ | .atomDual _ | .one | .bot | .top | .zero => True + | .tensor a b | .parr a b | .oplus a b | .with a b => a.IsMALL ∧ b.IsMALL + | .bang _ | .quest _ => False + /-- Whether a `Proposition` is positive is decidable. -/ instance Proposition.positive_decidable (a : Proposition Atom) : Decidable a.positive := a.positive.decEq true @@ -151,6 +160,10 @@ def Proposition.linImpl (a b : Proposition Atom) : Proposition Atom := a⫠ ⅋ /-- A sequent in CLL is a multiset of propositions. -/ abbrev Sequent Atom := Multiset (Proposition Atom) +/-- A sequent is MALL if every proposition in it is MALL. -/ +def Sequent.IsMALL (Γ : Sequent Atom) : Prop := + ∀ A ∈ Γ, (A : Proposition Atom).IsMALL + /-- Checks that all propositions in a sequent `Γ` are question marks. -/ def Sequent.allQuest (Γ : Sequent Atom) := Γ.map (· matches ʔ_) diff --git a/Cslib/Logics/LinearLogic/CLL/PhaseSemantics/Basic.lean b/Cslib/Logics/LinearLogic/CLL/PhaseSemantics/Basic.lean index c3b1338e6..eb55e128c 100644 --- a/Cslib/Logics/LinearLogic/CLL/PhaseSemantics/Basic.lean +++ b/Cslib/Logics/LinearLogic/CLL/PhaseSemantics/Basic.lean @@ -332,8 +332,8 @@ instance : Min (Fact P) where /-- The idempotent elements within a given set X. -/ def idempotentsIn [Monoid M] (X : Set M) : Set M := {m | IsIdempotentElem m ∧ m ∈ X} -/-- The set I of idempotents that "belong to 1" in the phase semantics. -/ -def I : Set P := idempotentsIn (1 : Set P) +/-- The set I of idempotents in the fact `1` (i.e., in `⊥⫠`). -/ +def I : Set P := idempotentsIn (↑(1 : Fact P)) /-! ## Interpretation of the connectives -/ diff --git a/Cslib/Logics/LinearLogic/CLL/PhaseSemantics/Completeness.lean b/Cslib/Logics/LinearLogic/CLL/PhaseSemantics/Completeness.lean index 9d79ef3e2..aab0a4300 100644 --- a/Cslib/Logics/LinearLogic/CLL/PhaseSemantics/Completeness.lean +++ b/Cslib/Logics/LinearLogic/CLL/PhaseSemantics/Completeness.lean @@ -32,6 +32,7 @@ def interpSequent /-- Provable sequents are valid in every phase space under every valuation. -/ theorem soundness (Γ : Sequent Atom) : + Sequent.IsMALL (Atom := Atom) Γ → Γ.Provable → ∀ (M : Type*) [PhaseSpace M] (v : Atom → Fact M), (interpSequent (Atom:=Atom) M v Γ).IsValid := @@ -40,46 +41,30 @@ by @[reducible] def CanonM (Atom : Type u) : Type u := Multiplicative (Sequent Atom) -open scoped Pointwise in -theorem PhaseSpace_I_eq_singleton {P : Type*} [PhaseSpace P] : (PhaseSpace.I (P := P) : Set P) = ({(1 : P)} : Set P) := by - ext m - constructor - · intro hm - rcases hm with ⟨-, hm1⟩ - -- hm1 : m ∈ (1 : Set P) - simpa [Set.mem_one] using hm1 - · intro hm - have hm' : m = (1 : P) := by - simpa using hm - subst hm' - refine ⟨?_, ?_⟩ - · simpa using (show IsIdempotentElem (1 : P) from IsIdempotentElem.one) - · simp [Set.mem_one] - def PrSet (Atom : Type u) (A : Proposition Atom) : Set (CanonM Atom) := {m | Sequent.Provable (Atom := Atom) (A ::ₘ m.toAdd)} -theorem PrSet_top {Atom : Type u} : PrSet Atom (⊤ : Proposition Atom) = (Set.univ : Set (CanonM Atom)) := by +theorem PrSet_top {Atom : Type u} : PrSet Atom (⊤ : Proposition Atom) = +(Set.univ : Set (CanonM Atom)) := by ext m constructor + · intro a + simp_all only [Set.mem_univ] · intro hm - trivial - · intro hm - dsimp [PrSet] + simp only [PrSet, Set.mem_setOf_eq] exact Sequent.Provable.fromProof (Proof.top (Γ := m.toAdd)) - -theorem PrSet_with {Atom : Type u} (A B : Proposition Atom) : PrSet Atom (A & B) = PrSet Atom A ∩ PrSet Atom B := by - classical +theorem PrSet_with {Atom : Type u} (A B : Proposition Atom) : PrSet Atom (A & B) = + PrSet Atom A ∩ PrSet Atom B := by ext m constructor · intro hm - simp [PrSet] at hm ⊢ + simp only [PrSet, Set.mem_setOf_eq, Set.mem_inter_iff] at hm ⊢ constructor · exact ⟨Proof.with_inversion₁ (a := A) (b := B) (Γ := m.toAdd) hm.toProof⟩ · exact ⟨Proof.with_inversion₂ (a := A) (b := B) (Γ := m.toAdd) hm.toProof⟩ · intro hm - simp [PrSet] at hm ⊢ + simp only [PrSet, Set.mem_inter_iff, Set.mem_setOf_eq] at hm ⊢ exact ⟨Proof.with (a := A) (b := B) (Γ := m.toAdd) hm.1.toProof hm.2.toProof⟩ def canonBot (Atom : Type u) : Set (CanonM Atom) := @@ -96,54 +81,47 @@ theorem PrSet_bot {Atom : Type u} : PrSet Atom (⊥ : Proposition Atom) = canonB rcases hm with ⟨p⟩ exact ⟨Proof.bot p⟩ - instance canonPhaseSpace (Atom : Type u) : PhaseSpace (CanonM Atom) := by let inst : CommMonoid (CanonM Atom) := inferInstance exact { bot := canonBot Atom, toCommMonoid := inst } -theorem PrSet_eq_orth {Atom : Type u} (A : Proposition Atom) : PrSet Atom A = PhaseSpace.orthogonal (PrSet Atom (Proposition.dual A)) := by +theorem PrSet_eq_orth {Atom : Type u} (A : Proposition Atom) : +PrSet Atom A = PhaseSpace.orthogonal (PrSet Atom (Proposition.dual A)) := by ext m constructor · intro hm unfold PhaseSpace.orthogonal PhaseSpace.imp intro n hn change (m * n) ∈ canonBot Atom - dsimp [canonBot] - have p : Proof (A ::ₘ m.toAdd) := hm.toProof - have q : Proof (Proposition.dual A ::ₘ n.toAdd) := hn.toProof + simp only [canonBot, Set.mem_setOf_eq, toAdd_mul] refine Sequent.Provable.fromProof ?_ - exact Proof.rwConclusion (toAdd_mul m n).symm (p.cut q) + exact Proof.rwConclusion (toAdd_mul m n).symm (hm.toProof.cut hn.toProof) · intro hm unfold PhaseSpace.orthogonal PhaseSpace.imp at hm let n : CanonM Atom := Multiplicative.ofAdd ({A} : Sequent Atom) have hn : n ∈ PrSet Atom (Proposition.dual A) := by - dsimp [PrSet] + simp only [PrSet, Set.mem_setOf_eq] simpa [n] using (Sequent.Provable.fromProof (Proof.ax' (a := A))) have hbot : m * n ∈ PhaseSpace.bot := hm n hn have hprov : Sequent.Provable (Atom := Atom) ((m * n).toAdd) := by - simpa [canonBot] using hbot + aesop have hprov' : Sequent.Provable (Atom := Atom) (m.toAdd + ({A} : Sequent Atom)) := by - simpa [n, toAdd_mul] using hprov + aesop have hprov'' : Sequent.Provable (Atom := Atom) (({A} : Sequent Atom) + m.toAdd) := by - simpa [add_comm] using hprov' - simpa [PrSet, Multiset.singleton_add] using hprov'' + grind only + aesop - -open scoped Pointwise in -theorem PrSet_dual_eq_orth {Atom : Type u} (A : Proposition Atom) : PrSet Atom (Proposition.dual A) = PhaseSpace.orthogonal (PrSet Atom A) := by - -- Use PrSet_eq_orth with A := (Proposition.dual A) +theorem PrSet_dual_eq_orth {Atom : Type u} (A : Proposition Atom) : +PrSet Atom (Proposition.dual A) = PhaseSpace.orthogonal (PrSet Atom A) := by simpa [Proposition.dual_involution] using (PrSet_eq_orth (Atom := Atom) (A := Proposition.dual A)) - -theorem PrSet_oplus {Atom : Type u} (A B : Proposition Atom) : PrSet Atom (A ⊕ B) = PhaseSpace.orthogonal (PhaseSpace.orthogonal (PrSet Atom A ∪ PrSet Atom B)) := by - classical - -- unfold `⊕` via duality +theorem PrSet_oplus {Atom : Type u} (A B : Proposition Atom) : +PrSet Atom (A ⊕ B) = PhaseSpace.orthogonal (PhaseSpace.orthogonal (PrSet Atom A ∪ PrSet Atom B)) := +by rw [PrSet_eq_orth (Atom := Atom) (A := A ⊕ B)] have hdual : PrSet Atom (Proposition.dual (A ⊕ B)) = PhaseSpace.orthogonal (PrSet Atom A ∪ PrSet Atom B) := by - -- dual of `⊕` is `&` - simp [Proposition.dual] - -- `PrSet` of `&` is intersection + simp only [Proposition.dual, orthogonal_def, Set.mem_union, Multiplicative.forall] rw [PrSet_with (Atom := Atom) (A := Proposition.dual A) (B := Proposition.dual B)] have hA : PrSet Atom (Proposition.dual A) = PhaseSpace.orthogonal (PrSet Atom A) := by simpa [Proposition.dual] using (PrSet_eq_orth (Atom := Atom) (A := Proposition.dual A)) @@ -151,29 +129,22 @@ theorem PrSet_oplus {Atom : Type u} (A B : Proposition Atom) : PrSet Atom (A ⊕ simpa [Proposition.dual] using (PrSet_eq_orth (Atom := Atom) (A := Proposition.dual B)) rw [hA, hB] ext m - -- unfold orthogonality and push unions/intersections through the quantifiers - simp [PhaseSpace.orthogonal, PhaseSpace.imp, Set.mem_union, Set.mem_inter_iff] + simp only [orthogonal, imp, Multiplicative.forall, Set.mem_inter_iff, Set.mem_setOf_eq] constructor · rintro ⟨hmA, hmB⟩ a ha - rcases ha with ha | ha - · exact hmA a ha - · exact hmB a ha + rcases ha with ha | ha <;> aesop · intro hm - constructor - · intro a ha - exact hm a (Or.inl ha) - · intro a ha - exact hm a (Or.inr ha) + constructor <;> aesop rw [hdual] -open scoped Pointwise in -theorem PrSet_parr {Atom : Type u} (A B : Proposition Atom) : PrSet Atom (A ⅋ B) = PhaseSpace.orthogonal (PrSet Atom (Proposition.dual A) * PrSet Atom (Proposition.dual B)) := by +theorem PrSet_parr {Atom : Type u} (A B : Proposition Atom) : PrSet Atom (A ⅋ B) = +PhaseSpace.orthogonal (PrSet Atom (Proposition.dual A) * PrSet Atom (Proposition.dual B)) := by ext m constructor · intro hm have pab : Sequent.Provable ((A ⅋ B) ::ₘ m.toAdd) := by - simpa [PrSet] using hm - show m ∈ PhaseSpace.orthogonal (PrSet Atom (A⫠) * PrSet Atom (B⫠)) + exact hm + change m ∈ PhaseSpace.orthogonal (PrSet Atom (A⫠) * PrSet Atom (B⫠)) unfold PhaseSpace.orthogonal PhaseSpace.imp intro x hx rcases Set.mem_mul.mp hx with ⟨s, hs, t, ht, rfl⟩ @@ -185,7 +156,7 @@ theorem PrSet_parr {Atom : Type u} (A B : Proposition Atom) : PrSet Atom (A ⅋ have hB : ⇓((B ::ₘ m.toAdd) + s.toAdd) := Proof.cut hAB ps.toProof have hB' : ⇓(B ::ₘ (m.toAdd + s.toAdd)) := by refine Proof.rwConclusion ?_ hB - simpa using (Multiset.cons_add B m.toAdd s.toAdd) + simp have hms : ⇓((m.toAdd + s.toAdd) + t.toAdd) := Proof.cut hB' pt.toProof refine Proof.rwConclusion ?_ hms simp [toAdd_mul, add_assoc] @@ -194,11 +165,11 @@ theorem PrSet_parr {Atom : Type u} (A B : Proposition Atom) : PrSet Atom (A ⅋ let s : CanonM Atom := Multiplicative.ofAdd ({A} : Sequent Atom) let t : CanonM Atom := Multiplicative.ofAdd ({B} : Sequent Atom) have hs : s ∈ PrSet Atom (A⫠) := by - show Sequent.Provable (A⫠ ::ₘ s.toAdd) + change Sequent.Provable (A⫠ ::ₘ s.toAdd) refine Sequent.Provable.fromProof ?_ simpa [s] using (Proof.ax' (Atom := Atom) (a := A)) have ht : t ∈ PrSet Atom (B⫠) := by - show Sequent.Provable (B⫠ ::ₘ t.toAdd) + change Sequent.Provable (B⫠ ::ₘ t.toAdd) refine Sequent.Provable.fromProof ?_ simpa [t] using (Proof.ax' (Atom := Atom) (a := B)) have hst : s * t ∈ (PrSet Atom (A⫠) * PrSet Atom (B⫠)) := Set.mul_mem_mul hs ht @@ -207,45 +178,17 @@ theorem PrSet_parr {Atom : Type u} (A B : Proposition Atom) : PrSet Atom (A ⅋ simpa [canonBot] using hbot have habm : ⇓(A ::ₘ B ::ₘ m.toAdd) := by refine (hprov.toProof).rwConclusion ?_ - -- now prove the multiset equality - -- - -- - -- - simp [s, t, toAdd_mul, add_assoc, add_comm, add_left_comm, Multiset.singleton_add] + simp [s, t, toAdd_mul, add_comm, Multiset.singleton_add] have : Sequent.Provable ((A ⅋ B) ::ₘ m.toAdd) := Sequent.Provable.fromProof (Proof.parr habm) simpa [PrSet] using this - -theorem PrSet_quest {Atom : Type u} (A : Proposition Atom) : PrSet Atom (ʔA) = PhaseSpace.orthogonal (PrSet Atom (Proposition.dual A) ∩ PhaseSpace.I) := by - -- ⚠️ Blocker analysis: as currently defined in `Cslib.CLL.PhaseSpace` (from `PhaseSemantics.Basic`), `PhaseSpace.I` is definitionally `idempotentsIn (1 : Set P)` with the pointwise `One (Set P)` instance, hence `I = {1}` in every phase space (see `PhaseSpace_I_eq_singleton`). - -- - -- With this, the RHS becomes `orthogonal (PrSet (A⫠) ∩ {1})`, i.e. either `Set.univ` or `bot` depending only on whether `{A⫠}` is provable, while the LHS `PrSet (ʔA)` varies genuinely with the context via the `quest/weaken/contract` rules. - -- - -- Conclusion: the stated equality cannot be proved without changing the upstream definition of `PhaseSpace.I` to use the carrier of the *fact* `1 : Fact P` (standard phase semantics), and (for full exponentials) also enriching the canonical monoid so that there are nontrivial idempotents. After such a patch, prove the exponential lemmas by a cut-based orthogonality argument (Okada/Girard), then discharge the truth lemma by structural induction. - sorry - -open scoped Pointwise in -theorem PrSet_bang {Atom : Type u} (A : Proposition Atom) : PrSet Atom (!A) = PhaseSpace.orthogonal (PhaseSpace.orthogonal (PrSet Atom A ∩ PhaseSpace.I)) := by - classical - calc - PrSet Atom (!A) = PhaseSpace.orthogonal (PrSet Atom (Proposition.dual (!A))) := by - simpa using (PrSet_eq_orth (Atom := Atom) (A := !A)) - _ = PhaseSpace.orthogonal (PrSet Atom (ʔ(Proposition.dual A))) := by - simp [Proposition.dual] - _ = PhaseSpace.orthogonal (PhaseSpace.orthogonal (PrSet Atom A ∩ PhaseSpace.I)) := by - -- rewrite PrSet of quest using PrSet_quest - rw [PrSet_quest (Atom := Atom) (A := Proposition.dual A)] - -- simplify dual involution - simp [Proposition.dual_involution] - -open scoped Pointwise in -theorem PrSet_tensor {Atom : Type u} (A B : Proposition Atom) : PrSet Atom (A ⊗ B) = PhaseSpace.orthogonal (PhaseSpace.orthogonal (PrSet Atom A * PrSet Atom B)) := by - classical +theorem PrSet_tensor {Atom : Type u} (A B : Proposition Atom) : PrSet Atom (A ⊗ B) = +PhaseSpace.orthogonal (PhaseSpace.orthogonal (PrSet Atom A * PrSet Atom B)) := by rw [PrSet_eq_orth (Atom := Atom) (A := A ⊗ B)] congr 1 simpa [Proposition.dual] using - (PrSet_parr (Atom := Atom) (A := Proposition.dual A) (B := Proposition.dual B)) + (PrSet_parr (Atom := Atom) (A := Proposition.dual A) (B := Proposition.dual B)) def canonVal {Atom : Type u} (a : Atom) : Fact (CanonM Atom) := PhaseSpace.dualFact (PrSet Atom (Proposition.atomDual a)) @@ -253,74 +196,108 @@ def canonVal {Atom : Type u} (a : Atom) : Fact (CanonM Atom) := noncomputable def foldPar {Atom : Type u} (Γ : Sequent Atom) : Proposition Atom := (Multiset.toList Γ).foldr (· ⅋ ·) ⊥ -open scoped Pointwise in -theorem interpProp_canon_carrier {Atom : Type u} (A : Proposition Atom) : ((interpProp (Atom:=Atom) (M:=CanonM Atom) (canonVal (Atom:=Atom)) A : Fact (CanonM Atom)) : Set (CanonM Atom)) = PrSet Atom A := by - classical +theorem foldPar_isMALL {Atom : Type u} (Γ : Sequent Atom) + (h : Sequent.IsMALL (Atom := Atom) Γ) : + Proposition.IsMALL (Atom := Atom) (foldPar (Atom := Atom) Γ) := by + have foldr_parr_isMALL : + ∀ l : List (Proposition Atom), + (∀ A ∈ l, (A : Proposition Atom).IsMALL) → + Proposition.IsMALL (Atom := Atom) + (List.foldr (fun A B : Proposition Atom => A ⅋ B) (⊥ : Proposition Atom) l) := by + intro l hl + induction l with + | nil => + simp [Proposition.IsMALL] + | cons a l ih => + have ha : (a : Proposition Atom).IsMALL := hl a (by simp) + have hl' : ∀ A ∈ l, (A : Proposition Atom).IsMALL := by + intro A hA + exact hl A (by simp [hA]) + have hacc := + ih hl' + simpa [Proposition.IsMALL, ha] using And.intro ha hacc + have hlist : ∀ A ∈ Multiset.toList Γ, (A : Proposition Atom).IsMALL := by + intro A hA + exact h A (by + simpa using (Multiset.mem_toList.1 hA)) + simpa [foldPar] using foldr_parr_isMALL (Multiset.toList Γ) hlist + +theorem interpProp_canon_carrier {Atom : Type u} (A : Proposition Atom) + (hA : Proposition.IsMALL (Atom := Atom) A) : + ((interpProp (Atom:=Atom) (M:=CanonM Atom) (canonVal (Atom:=Atom)) A : Fact (CanonM Atom)) : + Set (CanonM Atom)) = + PrSet Atom A := by induction A with | atom a => - simp [PhaseSpace.interpProp, canonVal, PhaseSpace.dualFact, -PhaseSpace.orthogonal_def] + simp only [interpProp, canonVal, dualFact, mk_dual_coe] rw [PrSet_eq_orth (Atom := Atom) (A := Proposition.atom a)] simp [Proposition.dual, -PhaseSpace.orthogonal_def] | atomDual a => - simp [PhaseSpace.interpProp, canonVal, PhaseSpace.dualFact, -PhaseSpace.orthogonal_def] + simp only [interpProp, canonVal, dualFact, coe_neg, mk_dual_coe] conv_rhs => rw [PrSet_eq_orth (Atom := Atom) (A := Proposition.atomDual a)] - simp [Proposition.dual, -PhaseSpace.orthogonal_def] + simp only [Proposition.dual] rw [PrSet_eq_orth (Atom := Atom) (A := Proposition.atom a)] simp [Proposition.dual, -PhaseSpace.orthogonal_def] | one => - simp [PhaseSpace.interpProp, -PhaseSpace.orthogonal_def] + simp only [interpProp, coe_one] rw [PrSet_eq_orth (Atom := Atom) (A := Proposition.one)] - simp [Proposition.dual, -PhaseSpace.orthogonal_def] + simp only [Proposition.dual] have hb : PrSet Atom (Proposition.bot : Proposition Atom) = canonBot Atom := by simpa using (PrSet_bot (Atom := Atom)) rw [hb] rfl | zero => - simp [PhaseSpace.interpProp, -PhaseSpace.orthogonal_def] + simp only [interpProp, coe_zero] rw [PrSet_eq_orth (Atom := Atom) (A := Proposition.zero)] - simp [Proposition.dual, -PhaseSpace.orthogonal_def] - have ht : PrSet Atom (Proposition.top : Proposition Atom) = (Set.univ : Set (CanonM Atom)) := by - simpa using (PrSet_top (Atom := Atom)) + simp only [Proposition.dual] + have ht : PrSet Atom (Proposition.top : Proposition Atom) = (Set.univ : Set (CanonM Atom)) := + by simpa using (PrSet_top (Atom := Atom)) rw [ht] | top => simpa [PhaseSpace.interpProp] using (PrSet_top (Atom := Atom)).symm | bot => simpa [PhaseSpace.interpProp] using (PrSet_bot (Atom := Atom)).symm | tensor A B ihA ihB => - simp [PhaseSpace.interpProp, ihA, ihB, Fact.tensor, PhaseSpace.dualFact, PrSet_tensor, + have hA' : Proposition.IsMALL (Atom := Atom) A := hA.1 + have hB' : Proposition.IsMALL (Atom := Atom) B := hA.2 + simp [PhaseSpace.interpProp, ihA hA', ihB hB', Fact.tensor, PhaseSpace.dualFact, PrSet_tensor, -PhaseSpace.orthogonal_def] | parr A B ihA ihB => - simp [PhaseSpace.interpProp, ihA, ihB, Fact.parr, PhaseSpace.dualFact, PrSet_parr, + have hA' : Proposition.IsMALL (Atom := Atom) A := hA.1 + have hB' : Proposition.IsMALL (Atom := Atom) B := hA.2 + simp [PhaseSpace.interpProp, ihA hA', ihB hB', Fact.parr, PhaseSpace.dualFact, PrSet_parr, PrSet_dual_eq_orth, -PhaseSpace.orthogonal_def] | oplus A B ihA ihB => - simp [PhaseSpace.interpProp, ihA, ihB, Fact.oplus, PhaseSpace.dualFact, PrSet_oplus, + have hA' : Proposition.IsMALL (Atom := Atom) A := hA.1 + have hB' : Proposition.IsMALL (Atom := Atom) B := hA.2 + simp [PhaseSpace.interpProp, ihA hA', ihB hB', Fact.oplus, PhaseSpace.dualFact, PrSet_oplus, -PhaseSpace.orthogonal_def] | «with» A B ihA ihB => - simp [PhaseSpace.interpProp, ihA, ihB, Fact.withh, PrSet_with] + have hA' : Proposition.IsMALL (Atom := Atom) A := hA.1 + have hB' : Proposition.IsMALL (Atom := Atom) B := hA.2 + simp [PhaseSpace.interpProp, ihA hA', ihB hB', Fact.withh, PrSet_with] | bang A ih => - simp [PhaseSpace.interpProp, ih, Fact.bang, PhaseSpace.dualFact, PrSet_bang, - -PhaseSpace.orthogonal_def] + exact False.elim hA | quest A ih => - simp [PhaseSpace.interpProp, ih, Fact.quest, PhaseSpace.dualFact, PrSet_quest, - PrSet_dual_eq_orth, -PhaseSpace.orthogonal_def] - + exact False.elim hA -theorem interpProp_list_foldr_parr {Atom : Type u} {M : Type*} [PhaseSpace M] (v : Atom → Fact M) (l : List (Proposition Atom)) : interpProp v (List.foldr (fun A B : Proposition Atom => A ⅋ B) (⊥ : Proposition Atom) l) = List.foldr (fun (A : Proposition Atom) (acc : Fact M) => (interpProp v A : Fact M) ⅋ acc) (⊥ : Fact M) l := by +theorem interpProp_list_foldr_parr {Atom : Type u} {M : Type*} [PhaseSpace M] +(v : Atom → Fact M) (l : List (Proposition Atom)) : +interpProp v (List.foldr (fun A B : Proposition Atom => A ⅋ B) +(⊥ : Proposition Atom) l) = List.foldr (fun (A : Proposition Atom) +(acc : Fact M) => (interpProp v A : Fact M) ⅋ acc) (⊥ : Fact M) l := by induction l with | nil => simp [List.foldr, PhaseSpace.interpProp] | cons a l ih => simp [List.foldr, PhaseSpace.interpProp, ih] - -theorem interpSequent_eq_interpProp_foldPar {Atom : Type u} (M : Type*) [PhaseSpace M] (v : Atom → Fact M) (Γ : Sequent Atom) : interpSequent (Atom:=Atom) M v Γ = interpProp v (foldPar (Atom:=Atom) Γ) := by - classical - -- Unfold the definitions and rewrite the interpretation of the par-fold on the RHS. +theorem interpSequent_eq_interpProp_foldPar {Atom : Type u} (M : Type*) [PhaseSpace M] +(v : Atom → Fact M) (Γ : Sequent Atom) : +interpSequent (Atom:=Atom) M v Γ = interpProp v (foldPar (Atom:=Atom) Γ) := by simp only [interpSequent, foldPar] rw [interpProp_list_foldr_parr (Atom := Atom) (M := M) v (Multiset.toList Γ)] - - -- Turn the list-fold with an "interpreting" step into a fold over the mapped list. have hfold : ∀ l : List (Proposition Atom), List.foldr @@ -334,22 +311,17 @@ theorem interpSequent_eq_interpProp_foldPar {Atom : Type u} (M : Type*) [PhaseSp simp | cons a l ih => simp [ih] - - -- Use the previous lemma to rewrite the RHS. rw [hfold (l := Multiset.toList Γ)] - - -- Convert the multiset fold on the LHS into the corresponding list fold. have hΓ : ((Multiset.toList Γ) : Multiset (Proposition Atom)) = Γ := by - simpa using (Multiset.coe_toList (s := Γ)) - + simp calc (Γ.map (fun A => (interpProp v A : Fact M))).fold (fun x y : Fact M => x ⅋ y) (⊥ : Fact M) - = (((Multiset.toList Γ) : Multiset (Proposition Atom)).map (fun A => (interpProp v A : Fact M))).fold + = (((Multiset.toList Γ) : Multiset (Proposition Atom)).map (fun A => + (interpProp v A : Fact M))).fold (fun x y : Fact M => x ⅋ y) (⊥ : Fact M) := by - simpa [hΓ] + simp [hΓ] _ = (((Multiset.toList Γ).map (fun A => (interpProp v A : Fact M)) : List (Fact M)) : Multiset (Fact M)).fold (fun x y : Fact M => x ⅋ y) (⊥ : Fact M) := by - -- rewrite `Multiset.map` over a coerced list simpa using congrArg (fun s : Multiset (Fact M) => @@ -359,28 +331,28 @@ theorem interpSequent_eq_interpProp_foldPar {Atom : Type u} (M : Type*) [PhaseSp (l := Multiset.toList Γ)) _ = List.foldr (fun x y : Fact M => x ⅋ y) (⊥ : Fact M) ((Multiset.toList Γ).map (fun A => (interpProp v A : Fact M))) := by - simpa using - (Multiset.coe_fold_r - (op := (fun x y : Fact M => x ⅋ y)) - (b := (⊥ : Fact M)) - (l := ((Multiset.toList Γ).map (fun A => (interpProp v A : Fact M))))) + simp -theorem provable_of_list_foldr_parr {Atom : Type u} (l : List (Proposition Atom)) (Δ : Sequent Atom) : Sequent.Provable (Atom:=Atom) ((List.foldr (fun A B : Proposition Atom => A ⅋ B) (⊥ : Proposition Atom) l) ::ₘ Δ) → Sequent.Provable (Atom:=Atom) ((l : Sequent Atom) + Δ) := by +theorem provable_of_list_foldr_parr {Atom : Type u} (l : List (Proposition Atom)) (Δ : Sequent Atom) +: Sequent.Provable (Atom:=Atom) ((List.foldr (fun A B : Proposition Atom => A ⅋ B) +(⊥ : Proposition Atom) l) ::ₘ Δ) → Sequent.Provable (Atom:=Atom) ((l : Sequent Atom) + Δ) := by induction l generalizing Δ with | nil => intro h rcases h with ⟨p⟩ have pΔ : ⇓Δ := Proof.bot_inversion p - -- goal: Provable (([] : Sequent) + Δ) refine (Sequent.Provable.fromProof ?_) simpa using pΔ | cons a l ih => intro h rcases h with ⟨p⟩ - have p' : ⇓(a ::ₘ (List.foldr (fun A B : Proposition Atom => A ⅋ B) (⊥ : Proposition Atom) l) ::ₘ Δ) := + have p' : + ⇓(a ::ₘ (List.foldr (fun A B : Proposition Atom => A ⅋ B) (⊥ : Proposition Atom) l) ::ₘ Δ) := Proof.parr_inversion p - have p'' : ⇓((List.foldr (fun A B : Proposition Atom => A ⅋ B) (⊥ : Proposition Atom) l) ::ₘ a ::ₘ Δ) := - Proof.rwConclusion (Multiset.cons_swap a (List.foldr (fun A B : Proposition Atom => A ⅋ B) (⊥ : Proposition Atom) l) Δ) p' + have p'' : + ⇓((List.foldr (fun A B : Proposition Atom => A ⅋ B) (⊥ : Proposition Atom) l) ::ₘ a ::ₘ Δ) := + Proof.rwConclusion (Multiset.cons_swap a (List.foldr (fun A B : Proposition Atom => A ⅋ B) + (⊥ : Proposition Atom) l) Δ) p' have hprov : Sequent.Provable (Atom:=Atom) ((l : Sequent Atom) + (a ::ₘ Δ)) := ih (Δ := a ::ₘ Δ) ⟨p''⟩ @@ -389,20 +361,20 @@ theorem provable_of_list_foldr_parr {Atom : Type u} (l : List (Proposition Atom) calc (l : Sequent Atom) + (a ::ₘ Δ) = a ::ₘ ((l : Sequent Atom) + Δ) := by - simpa using (Multiset.add_cons a (l : Sequent Atom) Δ) + simp _ = (a ::ₘ (l : Sequent Atom)) + Δ := by simpa using (Multiset.cons_add a (l : Sequent Atom) Δ).symm _ = (a :: l : Sequent Atom) + Δ := by - simpa using - congrArg (fun s : Sequent Atom => s + Δ) (Multiset.cons_coe a l) + simp exact ⟨Proof.rwConclusion hEq q⟩ -theorem provable_of_foldPar {Atom : Type u} (Γ : Sequent Atom) : ({foldPar (Atom:=Atom) Γ} : Sequent Atom).Provable → Γ.Provable := by +theorem provable_of_foldPar {Atom : Type u} (Γ : Sequent Atom) : ({foldPar (Atom:=Atom) Γ} : +Sequent Atom).Provable → Γ.Provable := by intro h - classical have h' : Sequent.Provable (Atom:=Atom) - ((List.foldr (fun A B : Proposition Atom => A ⅋ B) (⊥ : Proposition Atom) (Multiset.toList Γ)) ::ₘ + ((List.foldr (fun A B : Proposition Atom => A ⅋ B) + (⊥ : Proposition Atom) (Multiset.toList Γ)) ::ₘ (0 : Sequent Atom)) := by simpa [foldPar] using h have h'' : @@ -412,20 +384,28 @@ theorem provable_of_foldPar {Atom : Type u} (Γ : Sequent Atom) : ({foldPar (Ato simpa using h'' simpa [Multiset.coe_toList Γ] using h''' -theorem completeness {Atom : Type u} (Γ : Sequent Atom) : (∀ (M : Type u) [PhaseSpace M] (v : Atom → Fact M), (interpSequent (Atom:=Atom) M v Γ).IsValid) → Γ.Provable := by +theorem completeness {Atom : Type u} (Γ : Sequent Atom) + (hMALL : Sequent.IsMALL (Atom := Atom) Γ) : + (∀ (M : Type u) [PhaseSpace M] (v : Atom → Fact M), + (interpSequent (Atom:=Atom) M v Γ).IsValid) → Γ.Provable := by intro h have hv := h (M := CanonM Atom) (v := canonVal (Atom := Atom)) - have hv1 : (1 : CanonM Atom) ∈ (interpSequent (Atom := Atom) (CanonM Atom) (canonVal (Atom := Atom)) Γ : Set (CanonM Atom)) := by + have hv1 : (1 : CanonM Atom) ∈ (interpSequent (Atom := Atom) (CanonM Atom) + (canonVal (Atom := Atom)) Γ : Set (CanonM Atom)) := by simpa [PhaseSpace.Fact.IsValid] using hv - have hv2 : (1 : CanonM Atom) ∈ (interpProp (Atom := Atom) (M := CanonM Atom) (canonVal (Atom := Atom)) (foldPar (Atom := Atom) Γ) : Set (CanonM Atom)) := by - simpa [interpSequent_eq_interpProp_foldPar (Atom := Atom) (M := CanonM Atom) (v := canonVal (Atom := Atom)) (Γ := Γ)] using hv1 + have hv2 : (1 : CanonM Atom) ∈ (interpProp (Atom := Atom) (M := CanonM Atom) + (canonVal (Atom := Atom)) (foldPar (Atom := Atom) Γ) : Set (CanonM Atom)) := by + simpa + [interpSequent_eq_interpProp_foldPar] using hv1 have hv3 : (1 : CanonM Atom) ∈ PrSet Atom (foldPar (Atom := Atom) Γ) := by - simpa [interpProp_canon_carrier (Atom := Atom) (A := foldPar (Atom := Atom) Γ)] using hv2 + have hFold : + Proposition.IsMALL (Atom := Atom) (foldPar (Atom := Atom) Γ) := + foldPar_isMALL (Atom := Atom) Γ hMALL + simpa [interpProp_canon_carrier (Atom := Atom) (A := foldPar (Atom := Atom) Γ) hFold] using hv2 have hprov : ({foldPar (Atom := Atom) Γ} : Sequent Atom).Provable := by - simpa [PrSet] using hv3 + simp_all only [SetLike.mem_coe] + exact hv3 exact provable_of_foldPar (Atom := Atom) Γ hprov - - end CLL end Cslib From 87a23c1cc30eac1b99a5729eceeed19630465c44 Mon Sep 17 00:00:00 2001 From: Tanner Duve Date: Fri, 27 Feb 2026 00:13:29 -0800 Subject: [PATCH 6/9] soundness added --- .../CLL/PhaseSemantics/Completeness.lean | 317 +++++++++++++++++- 1 file changed, 310 insertions(+), 7 deletions(-) diff --git a/Cslib/Logics/LinearLogic/CLL/PhaseSemantics/Completeness.lean b/Cslib/Logics/LinearLogic/CLL/PhaseSemantics/Completeness.lean index aab0a4300..cb5995ffc 100644 --- a/Cslib/Logics/LinearLogic/CLL/PhaseSemantics/Completeness.lean +++ b/Cslib/Logics/LinearLogic/CLL/PhaseSemantics/Completeness.lean @@ -30,13 +30,316 @@ def interpSequent (Γ.map (fun A => (interpProp v A : Fact M))).fold (· ⅋ ·) ⊥ /-- Provable sequents are valid in every phase space under every valuation. -/ -theorem soundness - (Γ : Sequent Atom) : - Sequent.IsMALL (Atom := Atom) Γ → - Γ.Provable → - ∀ (M : Type*) [PhaseSpace M] (v : Atom → Fact M), - (interpSequent (Atom:=Atom) M v Γ).IsValid := -by +theorem IsValid_monotone {M : Type*} [PhaseSpace M] +{G H : Fact M} : G ≤ H → G.IsValid → H.IsValid := by + intro hGH hG + simpa [Fact.IsValid] using hGH (by simpa [Fact.IsValid] using hG) + +theorem dualFact_coe (M : Type*) [PhaseSpace M] (S : Set M) : +((PhaseSpace.dualFact (P:=M) S : Fact M) : Set M) = S⫠ := by + simp [PhaseSpace.dualFact] + +theorem interpProp_atomDual (M : Type*) [PhaseSpace M] (v : Atom → Fact M) (a : Atom) : +(interpProp (Atom:=Atom) (M:=M) v (Proposition.atomDual a) : Fact M) = ((v a)ᗮ : Fact M) := by + simp [PhaseSpace.interpProp] + +theorem interpProp_bang (M : Type*) [PhaseSpace M] (v : Atom → Fact M) (A : Proposition Atom) : +(interpProp (Atom:=Atom) (M:=M) v (Proposition.bang A) : Fact M) = +(PhaseSpace.Fact.bang (interpProp (Atom:=Atom) (M:=M) v A)) := by + simp [interpProp] + +theorem interpProp_bot (M : Type*) [PhaseSpace M] (v : Atom → Fact M) : +(interpProp (Atom:=Atom) (M:=M) v (Proposition.bot : Proposition Atom) : Fact M) = +(⊥ : Fact M) := by + simp [PhaseSpace.interpProp, interpProp] + +theorem interpProp_one (M : Type*) [PhaseSpace M] (v : Atom → Fact M) : +(interpProp (Atom:=Atom) (M:=M) v (Proposition.one : Proposition Atom) : Fact M) = +(1 : Fact M) := by + simp [interpProp] + +theorem interpProp_oplus (M : Type*) [PhaseSpace M] (v : Atom → Fact M) (A B : Proposition Atom) : +(interpProp (Atom:=Atom) (M:=M) v (Proposition.oplus A B) : Fact M) = +(PhaseSpace.Fact.oplus (interpProp (Atom:=Atom) (M:=M) v A) +(interpProp (Atom:=Atom) (M:=M) v B)) := by + simp [PhaseSpace.interpProp] + +theorem interpProp_parr (M : Type*) [PhaseSpace M] (v : Atom → Fact M) (A B : Proposition Atom) : +(interpProp (Atom:=Atom) (M:=M) v (Proposition.parr A B) : Fact M) = (interpProp (Atom:=Atom) +(M:=M) v A ⅋ interpProp (Atom:=Atom) (M:=M) v B) := by + simp [PhaseSpace.interpProp] + +theorem interpProp_quest (M : Type*) [PhaseSpace M] (v : Atom → Fact M) (A : Proposition Atom) : +(interpProp (Atom:=Atom) (M:=M) v (Proposition.quest A) : Fact M) = (PhaseSpace.Fact.quest +(interpProp (Atom:=Atom) (M:=M) v A)) := by + simp [PhaseSpace.interpProp, PhaseSpace.Fact.quest] + + +theorem interpProp_tensor (M : Type*) [PhaseSpace M] (v : Atom → Fact M) (A B : Proposition Atom) : +(interpProp (Atom:=Atom) (M:=M) v (Proposition.tensor A B) : Fact M) = (interpProp (Atom:=Atom) +(M:=M) v A ⊗ interpProp (Atom:=Atom) (M:=M) v B) := by + simp [interpProp] + +theorem interpProp_top (M : Type*) [PhaseSpace M] (v : Atom → Fact M) : (interpProp (Atom:=Atom) +(M:=M) v (Proposition.top : Proposition Atom) : Fact M) = (⊤ : Fact M) := by + simp [PhaseSpace.interpProp] + +theorem interpProp_with (M : Type*) [PhaseSpace M] (v : Atom → Fact M) (A B : Proposition Atom) : +(interpProp (Atom:=Atom) (M:=M) v (Proposition.with A B) : Fact M) = (PhaseSpace.Fact.withh +(interpProp (Atom:=Atom) (M:=M) v A) (interpProp (Atom:=Atom) (M:=M) v B)) := by + simp [interpProp, PhaseSpace.Fact.withh] + +theorem interpSequent_nil (M : Type*) [PhaseSpace M] (v : Atom → Fact M) : interpSequent +(Atom:=Atom) M v (0 : Sequent Atom) = (⊥ : Fact M) := by + -- attempt to unfold and simp + simp [interpSequent] + +theorem interpSequent_add (M : Type*) [PhaseSpace M] (v : Atom → Fact M) (Γ Δ : Sequent Atom) : +interpSequent (Atom:=Atom) M v (Γ + Δ) = interpSequent (Atom:=Atom) M v Γ ⅋ interpSequent +(Atom:=Atom) M v Δ := by + simp only [interpSequent] + rw [Multiset.map_add] + rw [← Fact.bot_par (G := (⊥ : Fact M))] + simpa using + (Multiset.fold_add + (op := fun (x y : Fact M) => x ⅋ y) + (b₁ := (⊥ : Fact M)) (b₂ := (⊥ : Fact M)) + (s₁ := Γ.map (fun A => (interpProp v A : Fact M))) + (s₂ := Δ.map (fun A => (interpProp v A : Fact M)))) + +theorem interpSequent_cons (M : Type*) [PhaseSpace M] (v : Atom → Fact M) (A : Proposition Atom) +(Γ : Sequent Atom) : interpSequent (Atom:=Atom) M v (A ::ₘ Γ) = +(interpProp v A : Fact M) ⅋ interpSequent (Atom:=Atom) M v Γ := by + simp [interpSequent] + +theorem one_valid (M : Type*) [PhaseSpace M] : (1 : Fact M).IsValid := by + simp [Fact.IsValid] + +theorem quest_contract_le {M : Type*} [PhaseSpace M] (G : Fact M) : (PhaseSpace.Fact.parr +(PhaseSpace.Fact.quest G) (PhaseSpace.Fact.quest G) : Fact M) ≤ PhaseSpace.Fact.quest G := by + classical + intro m hm + change m ∈ ((PhaseSpace.Fact.parr (PhaseSpace.Fact.quest G) (PhaseSpace.Fact.quest G) : Fact M) : + Set M) at hm + change m ∈ ((PhaseSpace.Fact.quest G : Fact M) : Set M) + simp only [parr, quest, orthogonal_def, SetLike.mem_coe, PhaseSpace.dualFact_coe, + Set.mem_inter_iff, Set.mem_setOf_eq, and_imp] at hm ⊢ + intro x hxG hxI + have hxidem : IsIdempotentElem x := hxI.1 + have hxS : x ∈ ({m : M | ∀ x_1 ∈ G, m * x_1 ∈ bot} ∩ I) := by + exact ⟨hxG, hxI⟩ + have hxQ : x ∈ + {m : M | ∀ (x : M), + (∀ (x_1 : M), (∀ x ∈ G, x_1 * x ∈ bot) → x_1 ∈ I → x * x_1 ∈ bot) → m * x ∈ bot} := by + have : x ∈ ({m : M | ∀ x_1 ∈ G, m * x_1 ∈ bot} ∩ I)⫠⫠ := + (PhaseSpace.orth_extensive (X := ({m : M | ∀ x_1 ∈ G, m * x_1 ∈ bot} ∩ I)) hxS) + simpa [PhaseSpace.orthogonal_def] using this + have hmbot : m * (x * x) ∈ bot := by + apply hm (x * x) + refine Set.mem_mul.mpr ?_ + exact ⟨x, hxQ, x, hxQ, rfl⟩ + simpa [hxidem.eq] using hmbot + +theorem quest_le {M : Type*} [PhaseSpace M] (G : Fact M) : G ≤ PhaseSpace.Fact.quest G := by + intro x hx + change x ∈ ((PhaseSpace.Fact.quest G : Fact M) : Set M) + simp only [quest, orthogonal_def, SetLike.mem_coe, PhaseSpace.dualFact_coe, Set.mem_inter_iff, + Set.mem_setOf_eq, and_imp] + intro y hy hyI + have : y * x ∈ PhaseSpace.bot := hy x hx + simpa [mul_comm] using this + +theorem bang_valid_of_allQuest {M : Type*} [PhaseSpace M] {v : Atom → Fact M} {a : Proposition Atom} {Γ : Sequent Atom} : Γ.allQuest → (interpProp (Atom:=Atom) (M:=M) v a ⅋ interpSequent (Atom:=Atom) M v Γ).IsValid → ((PhaseSpace.Fact.bang (interpProp (Atom:=Atom) (M:=M) v a)) ⅋ interpSequent (Atom:=Atom) M v Γ).IsValid := by + -- Soundness of **promotion** in a `?`-context. + -- + -- Goal after unfolding `Fact.IsValid` is membership `1 ∈ !⟦a⟧ ⅋ ⟦Γ⟧` assuming `1 ∈ ⟦a⟧ ⅋ ⟦Γ⟧` and `Γ.allQuest`. + -- + -- Key idea: `Γ.allQuest` means every element of `Γ` is a `Proposition.quest _`; hence every factor in `interpSequent M v Γ` is of the form `ʔG`, so `interpSequent M v Γ` is a `⅋`-combination of `ʔ`-facts. Use the semantic structural laws already available: + -- - dereliction `quest_le` (to move from a fact into its `ʔ`), + -- - weakening `bot_le_quest` (to introduce extra `ʔ` factors if needed), + -- - contraction `quest_contract_le` (to eliminate duplicates under `⅋`). + -- Together these show that in a `?`-context the sequent interpretation is **insensitive** to replacing `⟦a⟧` by `!⟦a⟧`. + -- + -- Suggested formal path: + -- 1. Unfold `PhaseSpace.Fact.bang` and coe via `dualFact_coe`, so the goal becomes a statement about orthogonals (`⫠`) and the idempotent set `I`. + -- 2. Use `Γ.allQuest` to obtain (by induction on the multiset using `Multiset.induction_on`) that `interpSequent M v Γ ≤ PhaseSpace.Fact.quest (interpSequent M v Γ)` and also a contraction property for the `⅋`-fold. (You can prove intermediate `≤` statements inside the proof using `quest_le`, `bot_le_quest`, `quest_contract_le`, and `Fact.par_le_par` from the library.) + -- 3. Convert the assumption validity into a monotone form using `IsValid_monotone` and the `≤` results built in step 2. + -- 4. Finish with `aesop`/`grind` after unfolding orthogonality (`PhaseSpace.orthogonal_def`) and basic par simp lemmas (`Fact.par_assoc`, `Fact.par_comm`, `Fact.par_bot`, `Fact.bot_par`). + -- + -- If this is still hard, try proving the contrapositive using orthogonality: show `1 ∈ (!G ⅋ H)` by showing `1 ∈ ((G ⅋ H))` and `(!G ⅋ H) = (G ⅋ H)` in a `?`-context. + -- + -- Also consider using the already proven duality lemma `bang_neg`/`quest_neg` (available from imports, even if not a blueprint dependency) to transport the problem to a statement about `ʔ`. + sorry + +theorem quest_neg_set (M : Type*) [PhaseSpace M] (G : Fact M) : +((PhaseSpace.Fact.quest (P:=M) (Gᗮ) : Fact M) : Set M) = +((PhaseSpace.Fact.bang (P:=M) G : Fact M) : Set M)⫠ := by +calc + ((PhaseSpace.Fact.quest (P := M) (Gᗮ) : Fact M) : Set M) + = (((Gᗮ : Set M)⫠ ∩ PhaseSpace.I) : Set M)⫠ := by + simp only [PhaseSpace.Fact.quest, dualFact_coe] + _ = (((G : Set M)⫠⫠ ∩ PhaseSpace.I) : Set M)⫠ := by + simp only [Fact.coe_neg] + _ = (((G : Set M) ∩ PhaseSpace.I) : Set M)⫠ := by + simpa + [PhaseSpace.isFact] using + congrArg (fun S : Set M => (S ∩ PhaseSpace.I)⫠) G.property.symm + _ = ((PhaseSpace.Fact.bang (P := M) G : Fact M) : Set M)⫠ := by + simp only [PhaseSpace.Fact.bang, dualFact_coe, PhaseSpace.triple_orth] + +theorem quest_neg (M : Type*) [PhaseSpace M] (G : Fact M) : (ʔ (Gᗮ) : Fact M) = +( ! G : Fact M)ᗮ := by + apply SetLike.coe_injective + simp [quest_neg_set] + +theorem bang_neg (M : Type*) [PhaseSpace M] (G : Fact M) : ( ! (Gᗮ) : Fact M) = +(ʔ G : Fact M)ᗮ := by + have h := quest_neg (M := M) (G := (Gᗮ : Fact M)) + have h' := congrArg (fun H : Fact M => (Hᗮ)) h + simpa using h'.symm + + +theorem interpProp_dual (M : Type*) [PhaseSpace M] (v : Atom → Fact M) (A : Proposition Atom) : +(interpProp (Atom:=Atom) (M:=M) v (A⫠) : Fact M) = (interpProp (Atom:=Atom) (M:=M) v A)ᗮ := by + induction A with + | atom a => + simp [PhaseSpace.interpProp, Proposition.dual] + | atomDual a => + simp [PhaseSpace.interpProp, Proposition.dual] + | one => + simp [PhaseSpace.interpProp, Proposition.dual] + | zero => + simp [PhaseSpace.interpProp, Proposition.dual] + | top => + simp [PhaseSpace.interpProp, Proposition.dual] + | bot => + simp [PhaseSpace.interpProp, Proposition.dual] + | tensor A B ihA ihB => + simp [PhaseSpace.interpProp, Proposition.dual, ihA, ihB, neg_tensor] + | parr A B ihA ihB => + simp [PhaseSpace.interpProp, Proposition.dual, ihA, ihB, neg_par] + | oplus A B ihA ihB => + simp [PhaseSpace.interpProp, Proposition.dual, ihA, ihB, neg_plus] + | «with» A B ihA ihB => + simp [PhaseSpace.interpProp, Proposition.dual, ihA, ihB, neg_with] + | bang A ih => + simpa [PhaseSpace.interpProp, Proposition.dual, ih] using + (quest_neg (M := M) (G := interpProp (Atom:=Atom) (M:=M) v A)) + | quest A ih => + simpa [PhaseSpace.interpProp, Proposition.dual, ih] using + (bang_neg (M := M) (G := interpProp (Atom:=Atom) (M:=M) v A)) + +theorem ax_valid (M : Type*) [PhaseSpace M] (v : Atom → Fact M) (A : Proposition Atom) : +(interpProp (Atom:=Atom) (M:=M) v A ⅋ (interpProp (Atom:=Atom) (M:=M) v A)ᗮ : Fact M).IsValid := by + change (1 : M) ∈ + (interpProp (Atom:=Atom) (M:=M) v A ⅋ (interpProp (Atom:=Atom) (M:=M) v A)ᗮ : Fact M) + rw [Fact.par_of_linImpl] + rw [Fact.linImpl_iff_implies] + intro x hx + simpa [PhaseSpace.imp, one_mul] using hx + +theorem cut_valid (M : Type*) [PhaseSpace M] {v : Atom → Fact M} {A : Proposition Atom} +{Γ Δ : Sequent Atom} : (interpProp (Atom:=Atom) (M:=M) v A ⅋ interpSequent +(Atom:=Atom) M v Γ).IsValid → ((interpProp (Atom:=Atom) (M:=M) v A)ᗮ ⅋ interpSequent +(Atom:=Atom) M v Δ).IsValid → (interpSequent (Atom:=Atom) M v Γ ⅋ interpSequent +(Atom:=Atom) M v Δ).IsValid := by + classical + intro hΓ hΔ + let PA : Fact M := interpProp (Atom:=Atom) (M:=M) v A + let G : Fact M := interpSequent (Atom:=Atom) M v Γ + let H : Fact M := interpSequent (Atom:=Atom) M v Δ + have hPA : (PAᗮ : Set M) ⊆ (G : Set M) := by + have h1 : (1 : M) ∈ (PAᗮ ⊸ G : Fact M) := by + simpa [PA, G, Fact.par_of_linImpl] using hΓ + have himp : imp (PAᗮ : Set M) (G : Set M) (1 : M) := + (Fact.linImpl_iff_implies (p := (1 : M)) (G := PAᗮ) (H := G)).1 h1 + intro x hx + have hxG : (1 : M) * x ∈ (G : Set M) := himp x hx + simpa [one_mul] using hxG + have hAH : (PA : Set M) ⊆ (H : Set M) := by + have h1 : (1 : M) ∈ (PA ⊸ H : Fact M) := by + simpa [PA, H, Fact.par_of_linImpl] using hΔ + have himp : imp (PA : Set M) (H : Set M) (1 : M) := + (Fact.linImpl_iff_implies (p := (1 : M)) (G := PA) (H := H)).1 h1 + intro x hx + have hxH : (1 : M) * x ∈ (H : Set M) := himp x hx + simpa [one_mul] using hxH + have hGoal : (1 : M) ∈ (Gᗮ ⊸ H : Fact M) := by + apply (Fact.linImpl_iff_implies (p := (1 : M)) (G := Gᗮ) (H := H)).2 + intro x hx + have hxPA : x ∈ (PA : Set M) := by + have horth : (G : Set M)⫠ ⊆ ((PAᗮ : Set M) : Set M)⫠ := + PhaseSpace.orth_antitone (P := M) (X := (PAᗮ : Set M)) (Y := (G : Set M)) hPA + have hx' : x ∈ (G : Set M)⫠ := by + simpa [Fact.coe_neg, G] using hx + have hx'' : x ∈ ((PAᗮ : Set M) : Set M)⫠ := horth hx' + have horthPA : ((PAᗮ : Set M) : Set M)⫠ = (PA : Set M) := by + have htmp : (PA : Set M) = ((PAᗮ : Set M) : Set M)⫠ := by + simpa [Fact.neg_neg (G := PA)] using (Fact.coe_neg (G := PAᗮ)) + exact htmp.symm + simpa [PA] using (show x ∈ (PA : Set M) from by + rw [← horthPA] + exact hx'') + have hxH : x ∈ (H : Set M) := hAH hxPA + simpa [one_mul] using hxH + simpa [G, H, Fact.par_of_linImpl] using hGoal + +theorem quest_valid_of_valid {M : Type*} [PhaseSpace M] {G : Fact M} : +G.IsValid → (PhaseSpace.Fact.quest G).IsValid := by + intro hG + exact IsValid_monotone (quest_le (M := M) G) hG + +theorem soundness (Γ : Sequent Atom) : Γ.Provable → ∀ (M : Type*) [PhaseSpace M] +(v : Atom → Fact M), (interpSequent (Atom:=Atom) M v Γ).IsValid := by + -- Prove soundness by induction on a proof term `p : Proof Γ`. + -- + -- Skeleton: + -- ```lean + -- intro hΓ M _ v + -- -- get explicit proof object + -- have p : Proof Γ := (Sequent.Provable.toProof hΓ) + -- induction p with + -- | ax => + -- -- goal: interpSequent {a,a⫠} is valid + -- simpa [interpSequent_cons, interpSequent_nil, interpProp_dual] using + -- (ax_valid (Atom:=Atom) (M:=M) (v:=v) (A:=a)) + -- | cut p q ihp ihq => + -- -- rewrite premises with interpSequent_cons and conclusion with interpSequent_add + -- -- then apply cut_valid + -- | one => + -- -- use interpSequent_cons + interpProp_one + Fact.par_bot then `one_valid` + -- | bot p ih => + -- -- simp [interpSequent_cons, interpProp_bot] at goal; reduce to ih + -- | parr p ih => + -- -- simp [interpSequent_cons, interpProp_parr] and use associativity/commutativity of `⅋` + -- | tensor p q ihp ihq => + -- -- after simp [interpSequent_cons, interpSequent_add, interpProp_tensor] + -- -- reduce to `Fact.tensor_le_tensor` + IsValid_monotone (as in reference proof) + -- | oplus₁ p ih => + -- -- use `Fact.le_plus_left` + `Fact.par_le_par` + IsValid_monotone + -- | oplus₂ p ih => + -- -- use `Fact.le_plus_right` + `Fact.par_le_par` + IsValid_monotone + -- | with p q ihp ihq => + -- -- simp [interpProp_with]; use `Fact.valid_with` to split + -- | top => + -- -- simp [interpProp_top] + -- | quest p ih => + -- -- simp [interpProp_quest]; exact quest_valid_of_valid ih + -- | weaken p ih => + -- -- show interpSequent Γ ≤ interpSequent (ʔa::ₘΓ) using bot_le_quest and Fact.bot_par, + -- -- then IsValid_monotone + -- | contract p ih => + -- -- use quest_contract_le lifted under `⅋ interpSequent Γ` + IsValid_monotone + -- | bang hΓ p ih => + -- -- simp [interpProp_bang, interpSequent_cons] at ih ⊢ + -- -- apply bang_valid_of_allQuest hΓ ih + -- ``` + -- + -- Notes: + -- - Prefer `simp only [...]` with the blueprint lemmas listed above. + -- - Use `Fact.par_assoc`/`Fact.par_comm`/`Fact.par_bot`/`Fact.bot_par` from `PhaseSpace.Fact` to normalize `⅋` folds. + -- - For weaken/contract, use `Fact.par_le_par` from the library plus `bot_le_quest` / `quest_contract_le`. + -- - The only genuinely nontrivial case should be `bang`, handled by `bang_valid_of_allQuest`. sorry @[reducible] def CanonM (Atom : Type u) : Type u := Multiplicative (Sequent Atom) From 45b5dbe28c54e0c78fb52d2437572f82fe7714a6 Mon Sep 17 00:00:00 2001 From: Tanner Duve Date: Fri, 27 Feb 2026 09:23:19 -0800 Subject: [PATCH 7/9] need to finish last lemma --- .../CLL/PhaseSemantics/Completeness.lean | 285 ++++++++++++++---- 1 file changed, 234 insertions(+), 51 deletions(-) diff --git a/Cslib/Logics/LinearLogic/CLL/PhaseSemantics/Completeness.lean b/Cslib/Logics/LinearLogic/CLL/PhaseSemantics/Completeness.lean index cb5995ffc..3f50a1688 100644 --- a/Cslib/Logics/LinearLogic/CLL/PhaseSemantics/Completeness.lean +++ b/Cslib/Logics/LinearLogic/CLL/PhaseSemantics/Completeness.lean @@ -117,7 +117,6 @@ theorem one_valid (M : Type*) [PhaseSpace M] : (1 : Fact M).IsValid := by theorem quest_contract_le {M : Type*} [PhaseSpace M] (G : Fact M) : (PhaseSpace.Fact.parr (PhaseSpace.Fact.quest G) (PhaseSpace.Fact.quest G) : Fact M) ≤ PhaseSpace.Fact.quest G := by - classical intro m hm change m ∈ ((PhaseSpace.Fact.parr (PhaseSpace.Fact.quest G) (PhaseSpace.Fact.quest G) : Fact M) : Set M) at hm @@ -149,6 +148,18 @@ theorem quest_le {M : Type*} [PhaseSpace M] (G : Fact M) : G ≤ PhaseSpace.Fact have : y * x ∈ PhaseSpace.bot := hy x hx simpa [mul_comm] using this +theorem bot_le_quest {M : Type*} [PhaseSpace M] (G : Fact M) : + (⊥ : Fact M) ≤ PhaseSpace.Fact.quest G := by + intro m hm + change m ∈ (((((G : Fact M) : Set M)⫠) ∩ PhaseSpace.I (P := M))⫠ : Set M) + · change m ∈ (PhaseSpace.bot : Set M) at hm + simp only [PhaseSpace.orthogonal_def, Set.mem_setOf_eq] at * + intro x hx + rcases hx with ⟨-, hxI⟩ + have hx1 : x ∈ (1 : Fact M) := hxI.2 + have hxm : x * m ∈ PhaseSpace.bot := (PhaseSpace.mem_one (P := M) (p := x)).1 hx1 m hm + simpa [mul_comm] using hxm + theorem bang_valid_of_allQuest {M : Type*} [PhaseSpace M] {v : Atom → Fact M} {a : Proposition Atom} {Γ : Sequent Atom} : Γ.allQuest → (interpProp (Atom:=Atom) (M:=M) v a ⅋ interpSequent (Atom:=Atom) M v Γ).IsValid → ((PhaseSpace.Fact.bang (interpProp (Atom:=Atom) (M:=M) v a)) ⅋ interpSequent (Atom:=Atom) M v Γ).IsValid := by -- Soundness of **promotion** in a `?`-context. -- @@ -291,56 +302,228 @@ G.IsValid → (PhaseSpace.Fact.quest G).IsValid := by theorem soundness (Γ : Sequent Atom) : Γ.Provable → ∀ (M : Type*) [PhaseSpace M] (v : Atom → Fact M), (interpSequent (Atom:=Atom) M v Γ).IsValid := by - -- Prove soundness by induction on a proof term `p : Proof Γ`. - -- - -- Skeleton: - -- ```lean - -- intro hΓ M _ v - -- -- get explicit proof object - -- have p : Proof Γ := (Sequent.Provable.toProof hΓ) - -- induction p with - -- | ax => - -- -- goal: interpSequent {a,a⫠} is valid - -- simpa [interpSequent_cons, interpSequent_nil, interpProp_dual] using - -- (ax_valid (Atom:=Atom) (M:=M) (v:=v) (A:=a)) - -- | cut p q ihp ihq => - -- -- rewrite premises with interpSequent_cons and conclusion with interpSequent_add - -- -- then apply cut_valid - -- | one => - -- -- use interpSequent_cons + interpProp_one + Fact.par_bot then `one_valid` - -- | bot p ih => - -- -- simp [interpSequent_cons, interpProp_bot] at goal; reduce to ih - -- | parr p ih => - -- -- simp [interpSequent_cons, interpProp_parr] and use associativity/commutativity of `⅋` - -- | tensor p q ihp ihq => - -- -- after simp [interpSequent_cons, interpSequent_add, interpProp_tensor] - -- -- reduce to `Fact.tensor_le_tensor` + IsValid_monotone (as in reference proof) - -- | oplus₁ p ih => - -- -- use `Fact.le_plus_left` + `Fact.par_le_par` + IsValid_monotone - -- | oplus₂ p ih => - -- -- use `Fact.le_plus_right` + `Fact.par_le_par` + IsValid_monotone - -- | with p q ihp ihq => - -- -- simp [interpProp_with]; use `Fact.valid_with` to split - -- | top => - -- -- simp [interpProp_top] - -- | quest p ih => - -- -- simp [interpProp_quest]; exact quest_valid_of_valid ih - -- | weaken p ih => - -- -- show interpSequent Γ ≤ interpSequent (ʔa::ₘΓ) using bot_le_quest and Fact.bot_par, - -- -- then IsValid_monotone - -- | contract p ih => - -- -- use quest_contract_le lifted under `⅋ interpSequent Γ` + IsValid_monotone - -- | bang hΓ p ih => - -- -- simp [interpProp_bang, interpSequent_cons] at ih ⊢ - -- -- apply bang_valid_of_allQuest hΓ ih - -- ``` - -- - -- Notes: - -- - Prefer `simp only [...]` with the blueprint lemmas listed above. - -- - Use `Fact.par_assoc`/`Fact.par_comm`/`Fact.par_bot`/`Fact.bot_par` from `PhaseSpace.Fact` to normalize `⅋` folds. - -- - For weaken/contract, use `Fact.par_le_par` from the library plus `bot_le_quest` / `quest_contract_le`. - -- - The only genuinely nontrivial case should be `bang`, handled by `bang_valid_of_allQuest`. - sorry + intro hΓ M _ v + classical + rcases hΓ with ⟨p⟩ + induction p with + | ax => + rename_i a + have hpair : ({a, a⫠} : Sequent Atom) = a ::ₘ ({a⫠} : Sequent Atom) := by simp + have hsingle : + interpSequent (Atom := Atom) M v ({a⫠} : Sequent Atom) = + (interpProp (Atom := Atom) (M := M) v a)ᗮ := by + have : ({a⫠} : Sequent Atom) = a⫠ ::ₘ (0 : Sequent Atom) := by simp + -- compute the singleton sequent interpretation without unfolding orthogonals + rw [this, interpSequent_cons, interpSequent_nil] + -- `⟦a⫠⟧ ⅋ ⊥ = ⟦a⫠⟧ = (⟦a⟧)ᗮ` + rw [par_bot] + simpa using (interpProp_dual (Atom := Atom) (M := M) (v := v) (A := a)) + -- rewrite `interpSequent {a, a⫠}` to `⟦a⟧ ⅋ ⟦a⟧ᗮ` and apply `ax_valid` + simpa [hpair, interpSequent_cons, hsingle] using + (ax_valid (Atom := Atom) (M := M) (v := v) (A := a)) + | cut p q ihp ihq => + rename_i a Γ Δ + have hΓ : + (interpProp (Atom := Atom) + (M := M) v a ⅋ interpSequent (Atom := Atom) M v Γ).IsValid := by + simpa [interpSequent_cons] using ihp + have hΔ : + ((interpProp (Atom := Atom) + (M := M) v a)ᗮ ⅋ interpSequent (Atom := Atom) M v Δ).IsValid := by + simpa [interpSequent_cons, interpProp_dual] using ihq + have hcut : + (interpSequent (Atom := Atom) M v Γ ⅋ interpSequent (Atom := Atom) M v Δ).IsValid := + cut_valid (Atom := Atom) (M := M) (v := v) (A := a) (Γ := Γ) (Δ := Δ) hΓ hΔ + simpa [interpSequent_add] using hcut + | one => + have hs : ({(1 : Proposition Atom)} : Sequent Atom) = + (1 : Proposition Atom) ::ₘ (0 : Sequent Atom) := by + simp + rw [hs, interpSequent_cons, interpSequent_nil] + have hone : + (interpProp (Atom := Atom) + (M := M) v (1 : Proposition Atom) : Fact M) = (1 : Fact M) := by + simp_all only [Multiset.cons_zero] + rfl + rw [hone, par_bot] + simp [Fact.IsValid] + | bot p ih => + rename_i Γ + -- `interpSequent (⊥ ::ₘ Γ) = ⟦⊥⟧ ⅋ interpSequent Γ = ⊥ ⅋ interpSequent Γ = interpSequent Γ`. + rw [interpSequent_cons] + -- simplify `⟦⊥⟧v` to `⊥` + have hbot : (interpProp (Atom := Atom) + (M := M) v (⊥ : Proposition Atom) : Fact M) = (⊥ : Fact M) := by + simpa using (interpProp_bot (Atom := Atom) (M := M) (v := v)) + rw [hbot] + simpa [bot_par] using ih + | parr p ih => + rename_i a b Γ + simpa [interpSequent_cons, interpProp_parr, par_assoc] using ih + | tensor p q ihp ihq => + rename_i a Γ b Δ + let A : Fact M := interpProp (Atom := Atom) (M := M) v a + let B : Fact M := interpProp (Atom := Atom) (M := M) v b + let G : Fact M := interpSequent (Atom := Atom) M v Γ + let H : Fact M := interpSequent (Atom := Atom) M v Δ + have hAG : (A ⅋ G).IsValid := by + simpa [A, G, interpSequent_cons] using ihp + have hBH : (B ⅋ H).IsValid := by + simpa [B, H, interpSequent_cons] using ihq + have hA : (Aᗮ : Set M) ⊆ (G : Set M) := by + have h1 : (1 : M) ∈ (Aᗮ ⊸ G : Fact M) := by + simpa [A, G, par_of_linImpl] using hAG + have himp : imp (Aᗮ : Set M) (G : Set M) (1 : M) := + (linImpl_iff_implies (p := (1 : M)) (G := Aᗮ) (H := G)).1 h1 + intro x hx + have : (1 : M) * x ∈ (G : Set M) := himp x hx + simpa [one_mul] using this + have hB : (Bᗮ : Set M) ⊆ (H : Set M) := by + have h1 : (1 : M) ∈ (Bᗮ ⊸ H : Fact M) := by + simpa [B, H, par_of_linImpl] using hBH + have himp : imp (Bᗮ : Set M) (H : Set M) (1 : M) := + (linImpl_iff_implies (p := (1 : M)) (G := Bᗮ) (H := H)).1 h1 + intro x hx + have : (1 : M) * x ∈ (H : Set M) := himp x hx + simpa [one_mul] using this + have hA_le : (Aᗮ : Fact M) ≤ G := fun _ hx => hA hx + have hB_le : (Bᗮ : Fact M) ≤ H := fun _ hx => hB hx + have hpar : (Aᗮ ⅋ Bᗮ : Fact M) ≤ (G ⅋ H) := par_le_par hA_le hB_le + have himp : + imp ((Aᗮ ⅋ Bᗮ : Fact M) : Set M) ((G ⅋ H : Fact M) : Set M) (1 : M) := by + intro x hx + have : x ∈ (G ⅋ H : Fact M) := hpar hx + simpa [one_mul] using this + have hlin : + (1 : M) ∈ ((Aᗮ ⅋ Bᗮ : Fact M) ⊸ (G ⅋ H : Fact M) : Fact M) := + (linImpl_iff_implies (p := (1 : M)) (G := (Aᗮ ⅋ Bᗮ : Fact M)) + (H := (G ⅋ H : Fact M))).2 himp + have hgoal : ((A ⊗ B) ⅋ (G ⅋ H) : Fact M).IsValid := by + have : (1 : M) ∈ (((A ⊗ B) ⅋ (G ⅋ H) : Fact M) : Set M) := by + simpa [par_of_linImpl, neg_tensor] using hlin + exact this + simpa [interpSequent_cons, interpSequent_add, + interpProp_tensor, A, B, G, H, par_assoc] using hgoal + | oplus₁ p ih => + rename_i a Γ b + have h : + (interpProp (Atom := Atom) + (M := M) v a ⅋ interpSequent (Atom := Atom) M v Γ).IsValid := by + simpa [interpSequent_cons] using ih + have ha : + (interpProp (Atom := Atom) (M := M) v a : Fact M) ≤ + (interpProp (Atom := Atom) (M := M) v (a ⊕ b) : Fact M) := by + simpa [interpProp_oplus (Atom := Atom) (M := M) v a b] using + (le_plus_left (G := (interpProp (Atom := Atom) (M := M) v a : Fact M)) + (H := (interpProp (Atom := Atom) (M := M) v b : Fact M))) + have hpar : + (interpProp (Atom := Atom) (M := M) v a ⅋ interpSequent (Atom := Atom) M v Γ : Fact M) ≤ + (interpProp (Atom := Atom) + (M := M) v (a ⊕ b) ⅋ interpSequent (Atom := Atom) M v Γ : Fact M) := + par_le_par ha (le_rfl) + have := IsValid_monotone (M := M) hpar h + simpa [interpSequent_cons, interpProp_oplus] using this + | oplus₂ p ih => + rename_i a Γ b + have h : + (interpProp (Atom := Atom) + (M := M) v a ⅋ interpSequent (Atom := Atom) M v Γ).IsValid := by + simpa [interpSequent_cons] using ih + have ha : + (interpProp (Atom := Atom) (M := M) v a : Fact M) ≤ + (interpProp (Atom := Atom) (M := M) v (a ⊕ b) : Fact M) := by + simpa [interpProp_oplus (Atom := Atom) (M := M) v a b] using + (le_plus_left (G := (interpProp (Atom := Atom) (M := M) v a : Fact M)) + (H := (interpProp (Atom := Atom) (M := M) v b : Fact M))) + have hpar : + (interpProp (Atom := Atom) (M := M) v a ⅋ interpSequent (Atom := Atom) M v Γ : Fact M) ≤ + (interpProp (Atom := Atom) + (M := M) v (a ⊕ b) ⅋ interpSequent (Atom := Atom) M v Γ : Fact M) := + par_le_par ha (le_rfl) + have := IsValid_monotone (M := M) hpar h + simpa [interpSequent_cons, interpProp_oplus, plus_comm] using this + | «with» p q ihp ihq => + rename_i a Γ b + have ha : + (interpProp (Atom := Atom) + (M := M) v a ⅋ interpSequent (Atom := Atom) M v Γ).IsValid := by + simpa [interpSequent_cons] using ihp + have hb : + (interpProp (Atom := Atom) + (M := M) v b ⅋ interpSequent (Atom := Atom) M v Γ).IsValid := by + simpa [interpSequent_cons] using ihq + have : ((interpProp (Atom := Atom) (M := M) v (a & b) : Fact M) ⅋ + interpSequent (Atom := Atom) M v Γ).IsValid := by + simpa [interpProp_with, with_par_distrib] using (And.intro ha hb) + simpa [interpSequent_cons, interpProp_with] using this + | top => + rename_i Γ + -- `⊤ ⅋ G = ⊤` and `⊤` is valid + rw [interpSequent_cons] + have htop : (interpProp (Atom := Atom) + (M := M) v (⊤ : Proposition Atom) : Fact M) = (⊤ : Fact M) := by + simpa using (interpProp_top (Atom := Atom) (M := M) (v := v)) + rw [htop] + simp [top_par, Fact.IsValid] + | quest p ih => + rename_i a Γ + have h : + (interpProp (Atom := Atom) + (M := M) v a ⅋ interpSequent (Atom := Atom) M v Γ).IsValid := by + simpa [interpSequent_cons] using ih + have hle : + (interpProp (Atom := Atom) (M := M) v a ⅋ interpSequent (Atom := Atom) M v Γ : Fact M) ≤ + (PhaseSpace.Fact.quest (interpProp (Atom := Atom) (M := M) v a) ⅋ + interpSequent (Atom := Atom) M v Γ : Fact M) := + par_le_par (quest_le (M := M) (G := interpProp (Atom := Atom) (M := M) v a)) (le_rfl) + have := IsValid_monotone (M := M) hle h + simpa [interpSequent_cons, interpProp_quest] using this + | weaken p ih => + rename_i Γ a + have h : (interpSequent (Atom := Atom) M v Γ).IsValid := ih + have hle : + (interpSequent (Atom := Atom) M v Γ : Fact M) ≤ + (PhaseSpace.Fact.quest (interpProp (Atom := Atom) (M := M) v a) ⅋ + interpSequent (Atom := Atom) M v Γ : Fact M) := by + simpa [bot_par] using + (par_le_par (bot_le_quest (M := M) (G := interpProp (Atom := Atom) (M := M) v a)) + (le_rfl) : ((⊥ : Fact M) ⅋ interpSequent (Atom := Atom) M v Γ : Fact M) ≤ _) + have := IsValid_monotone (M := M) hle h + simpa [interpSequent_cons, interpProp_quest] using this + | contract p ih => + rename_i a Γ + have h : + (PhaseSpace.Fact.quest (interpProp (Atom := Atom) (M := M) v a) ⅋ + (PhaseSpace.Fact.quest (interpProp (Atom := Atom) (M := M) v a) ⅋ + interpSequent (Atom := Atom) M v Γ) : Fact M).IsValid := by + simpa [interpSequent_cons, interpProp_quest, par_assoc] using ih + have hle : + (PhaseSpace.Fact.quest (interpProp (Atom := Atom) (M := M) v a) ⅋ + (PhaseSpace.Fact.quest (interpProp (Atom := Atom) (M := M) v a) ⅋ + interpSequent (Atom := Atom) M v Γ) : Fact M) + ≤ + (PhaseSpace.Fact.quest (interpProp (Atom := Atom) (M := M) v a) ⅋ + interpSequent (Atom := Atom) M v Γ : Fact M) := by + have h' : + ((PhaseSpace.Fact.quest (interpProp (Atom := Atom) (M := M) v a) ⅋ + PhaseSpace.Fact.quest (interpProp (Atom := Atom) (M := M) v a)) ⅋ + interpSequent (Atom := Atom) M v Γ : Fact M) + ≤ + (PhaseSpace.Fact.quest (interpProp (Atom := Atom) (M := M) v a) ⅋ + interpSequent (Atom := Atom) M v Γ : Fact M) := + par_le_par (quest_contract_le (M := M) (G := interpProp (Atom := Atom) (M := M) v a)) + (le_rfl) + simpa [par_assoc] using h' + have := IsValid_monotone (M := M) hle h + simpa [interpSequent_cons, interpProp_quest] using this + | bang hQuestCtx p ih => + rename_i Δ A + have h : + (interpProp (Atom := Atom) + (M := M) v A ⅋ interpSequent (Atom := Atom) M v Δ).IsValid := by + simpa [interpSequent_cons] using ih + have := bang_valid_of_allQuest (Atom := Atom) (M := M) (v := v) (a := A) (Γ := Δ) hQuestCtx h + simpa [interpSequent_cons, interpProp_bang] using this @[reducible] def CanonM (Atom : Type u) : Type u := Multiplicative (Sequent Atom) From 8a9604526a6efe8634247fc86ada9585fea7d5ca Mon Sep 17 00:00:00 2001 From: Tanner Duve Date: Fri, 27 Feb 2026 09:25:50 -0800 Subject: [PATCH 8/9] remove comments --- .../LinearLogic/CLL/PhaseSemantics/Completeness.lean | 10 +--------- 1 file changed, 1 insertion(+), 9 deletions(-) diff --git a/Cslib/Logics/LinearLogic/CLL/PhaseSemantics/Completeness.lean b/Cslib/Logics/LinearLogic/CLL/PhaseSemantics/Completeness.lean index 3f50a1688..e702d5272 100644 --- a/Cslib/Logics/LinearLogic/CLL/PhaseSemantics/Completeness.lean +++ b/Cslib/Logics/LinearLogic/CLL/PhaseSemantics/Completeness.lean @@ -313,12 +313,9 @@ theorem soundness (Γ : Sequent Atom) : Γ.Provable → ∀ (M : Type*) [PhaseSp interpSequent (Atom := Atom) M v ({a⫠} : Sequent Atom) = (interpProp (Atom := Atom) (M := M) v a)ᗮ := by have : ({a⫠} : Sequent Atom) = a⫠ ::ₘ (0 : Sequent Atom) := by simp - -- compute the singleton sequent interpretation without unfolding orthogonals rw [this, interpSequent_cons, interpSequent_nil] - -- `⟦a⫠⟧ ⅋ ⊥ = ⟦a⫠⟧ = (⟦a⟧)ᗮ` rw [par_bot] simpa using (interpProp_dual (Atom := Atom) (M := M) (v := v) (A := a)) - -- rewrite `interpSequent {a, a⫠}` to `⟦a⟧ ⅋ ⟦a⟧ᗮ` and apply `ax_valid` simpa [hpair, interpSequent_cons, hsingle] using (ax_valid (Atom := Atom) (M := M) (v := v) (A := a)) | cut p q ihp ihq => @@ -348,17 +345,13 @@ theorem soundness (Γ : Sequent Atom) : Γ.Provable → ∀ (M : Type*) [PhaseSp rw [hone, par_bot] simp [Fact.IsValid] | bot p ih => - rename_i Γ - -- `interpSequent (⊥ ::ₘ Γ) = ⟦⊥⟧ ⅋ interpSequent Γ = ⊥ ⅋ interpSequent Γ = interpSequent Γ`. rw [interpSequent_cons] - -- simplify `⟦⊥⟧v` to `⊥` have hbot : (interpProp (Atom := Atom) (M := M) v (⊥ : Proposition Atom) : Fact M) = (⊥ : Fact M) := by simpa using (interpProp_bot (Atom := Atom) (M := M) (v := v)) rw [hbot] - simpa [bot_par] using ih + simp_all only [bot_par] | parr p ih => - rename_i a b Γ simpa [interpSequent_cons, interpProp_parr, par_assoc] using ih | tensor p q ihp ihq => rename_i a Γ b Δ @@ -458,7 +451,6 @@ theorem soundness (Γ : Sequent Atom) : Γ.Provable → ∀ (M : Type*) [PhaseSp simpa [interpSequent_cons, interpProp_with] using this | top => rename_i Γ - -- `⊤ ⅋ G = ⊤` and `⊤` is valid rw [interpSequent_cons] have htop : (interpProp (Atom := Atom) (M := M) v (⊤ : Proposition Atom) : Fact M) = (⊤ : Fact M) := by From b0a850cabf09231c4524cd6c3b58fd97b002ce7d Mon Sep 17 00:00:00 2001 From: "aleph-prover-dev[bot]" <247854405+aleph-prover-dev[bot]@users.noreply.github.com> Date: Sat, 28 Feb 2026 08:34:53 +0000 Subject: [PATCH 9/9] Partial proof for bang_valid_of_allQuest Automated commit at 20260228_083452 --- .../CLL/PhaseSemantics/Completeness.lean | 213 ++++++++++++++++-- 1 file changed, 193 insertions(+), 20 deletions(-) diff --git a/Cslib/Logics/LinearLogic/CLL/PhaseSemantics/Completeness.lean b/Cslib/Logics/LinearLogic/CLL/PhaseSemantics/Completeness.lean index e702d5272..581734cd1 100644 --- a/Cslib/Logics/LinearLogic/CLL/PhaseSemantics/Completeness.lean +++ b/Cslib/Logics/LinearLogic/CLL/PhaseSemantics/Completeness.lean @@ -160,28 +160,201 @@ theorem bot_le_quest {M : Type*} [PhaseSpace M] (G : Fact M) : have hxm : x * m ∈ PhaseSpace.bot := (PhaseSpace.mem_one (P := M) (p := x)).1 hx1 m hm simpa [mul_comm] using hxm -theorem bang_valid_of_allQuest {M : Type*} [PhaseSpace M] {v : Atom → Fact M} {a : Proposition Atom} {Γ : Sequent Atom} : Γ.allQuest → (interpProp (Atom:=Atom) (M:=M) v a ⅋ interpSequent (Atom:=Atom) M v Γ).IsValid → ((PhaseSpace.Fact.bang (interpProp (Atom:=Atom) (M:=M) v a)) ⅋ interpSequent (Atom:=Atom) M v Γ).IsValid := by - -- Soundness of **promotion** in a `?`-context. - -- - -- Goal after unfolding `Fact.IsValid` is membership `1 ∈ !⟦a⟧ ⅋ ⟦Γ⟧` assuming `1 ∈ ⟦a⟧ ⅋ ⟦Γ⟧` and `Γ.allQuest`. - -- - -- Key idea: `Γ.allQuest` means every element of `Γ` is a `Proposition.quest _`; hence every factor in `interpSequent M v Γ` is of the form `ʔG`, so `interpSequent M v Γ` is a `⅋`-combination of `ʔ`-facts. Use the semantic structural laws already available: - -- - dereliction `quest_le` (to move from a fact into its `ʔ`), - -- - weakening `bot_le_quest` (to introduce extra `ʔ` factors if needed), - -- - contraction `quest_contract_le` (to eliminate duplicates under `⅋`). - -- Together these show that in a `?`-context the sequent interpretation is **insensitive** to replacing `⟦a⟧` by `!⟦a⟧`. - -- - -- Suggested formal path: - -- 1. Unfold `PhaseSpace.Fact.bang` and coe via `dualFact_coe`, so the goal becomes a statement about orthogonals (`⫠`) and the idempotent set `I`. - -- 2. Use `Γ.allQuest` to obtain (by induction on the multiset using `Multiset.induction_on`) that `interpSequent M v Γ ≤ PhaseSpace.Fact.quest (interpSequent M v Γ)` and also a contraction property for the `⅋`-fold. (You can prove intermediate `≤` statements inside the proof using `quest_le`, `bot_le_quest`, `quest_contract_le`, and `Fact.par_le_par` from the library.) - -- 3. Convert the assumption validity into a monotone form using `IsValid_monotone` and the `≤` results built in step 2. - -- 4. Finish with `aesop`/`grind` after unfolding orthogonality (`PhaseSpace.orthogonal_def`) and basic par simp lemmas (`Fact.par_assoc`, `Fact.par_comm`, `Fact.par_bot`, `Fact.bot_par`). - -- - -- If this is still hard, try proving the contrapositive using orthogonality: show `1 ∈ (!G ⅋ H)` by showing `1 ∈ ((G ⅋ H))` and `(!G ⅋ H) = (G ⅋ H)` in a `?`-context. - -- - -- Also consider using the already proven duality lemma `bang_neg`/`quest_neg` (available from imports, even if not a blueprint dependency) to transport the problem to a statement about `ʔ`. +theorem I_mul_mem {M : Type*} [PhaseSpace M] {a b : M} : a ∈ PhaseSpace.I (P := M) → b ∈ PhaseSpace.I (P := M) → (a * b) ∈ PhaseSpace.I (P := M) := by + intro ha hb + simp [PhaseSpace.I, PhaseSpace.idempotentsIn] at ha hb ⊢ + constructor + · -- idempotent component + exact IsIdempotentElem.mul ha.1 hb.1 + · -- closure under multiplication on ⊥ + intro x hx + have hb' : b * x ∈ (PhaseSpace.bot : Set M) := hb.2 x hx + have ha' : a * (b * x) ∈ (PhaseSpace.bot : Set M) := ha.2 (b * x) hb' + simpa [mul_assoc] using ha' + +theorem allQuest_cons {A : Proposition Atom} {Γ : Sequent Atom} : Sequent.allQuest (Atom := Atom) (A ::ₘ Γ) ↔ (A matches Proposition.quest _) ∧ Sequent.allQuest (Atom := Atom) Γ := by + -- unfold and simplify `Sequent.allQuest` on a cons + simp [Sequent.allQuest, Multiset.map_cons, Multiset.fold_cons_left, Bool.and_eq_true] + intro h + rfl + +theorem par_valid_iff_neg_le {M : Type*} [PhaseSpace M] {G H : Fact M} : (G ⅋ H).IsValid ↔ (Gᗮ ≤ H) := by + constructor + · intro h + -- unfold validity of par + have h1 : (1 : M) ∈ (G ⅋ H : Set M) := by + simpa [Fact.IsValid] using h + have h2 : (1 : M) ∈ (Gᗮ ⊸ H : Fact M) := by + simpa [Fact.par_of_linImpl] using h1 + have h3 : imp (Gᗮ : Set M) (H : Set M) (1 : M) := by + -- membership in linImpl is implication + exact (Fact.linImpl_iff_implies (G := Gᗮ) (H := H) (p := (1 : M))).1 h2 + -- convert implication at 1 into subset + have hsub : (Gᗮ : Set M) ⊆ (H : Set M) := by + intro x hx + have hx' := h3 x hx + simpa [PhaseSpace.imp, one_mul] using hx' + -- Fact order is set inclusion + simpa using hsub + · intro hle + -- prove validity from inclusion + have hsub : (Gᗮ : Set M) ⊆ (H : Set M) := by + simpa using hle + have himp : imp (Gᗮ : Set M) (H : Set M) (1 : M) := by + intro x hx + have : x ∈ (H : Set M) := hsub hx + simpa [PhaseSpace.imp, one_mul] using this + have hmem : (1 : M) ∈ (Gᗮ ⊸ H : Fact M) := by + exact (Fact.linImpl_iff_implies (G := Gᗮ) (H := H) (p := (1 : M))).2 himp + have hmem' : (1 : M) ∈ (G ⅋ H : Set M) := by + simpa [Fact.par_of_linImpl] using hmem + simpa [Fact.IsValid] using hmem' + +theorem quest_closed_parr_quest_quest {M : Type*} [PhaseSpace M] {G H : Fact M} : (ʔ ((ʔ G : Fact M) ⅋ (ʔ H : Fact M)) : Fact M) ≤ ((ʔ G : Fact M) ⅋ (ʔ H : Fact M)) := by + -- Goal: show a `⅋`-combination of `?`-facts is itself `?`-closed. + -- + -- Let `A := (ʔ G : Fact M)`, `B := (ʔ H : Fact M)`, `P := (A ⅋ B : Fact M)`. + -- We need `ʔ P ≤ P`. + -- + -- Work in set-membership form: + -- `intro m hm;` then `change` both sides to membership in the underlying `Set M`. + -- Unfold with + -- `simp only [PhaseSpace.Fact.quest, PhaseSpace.Fact.parr, PhaseSpace.orthogonal_def, + -- PhaseSpace.dualFact_coe, PhaseSpace.I, PhaseSpace.idempotentsIn, + -- SetLike.mem_coe, Set.mem_inter_iff, Set.mem_mul, Set.mem_setOf_eq, + -- forall_exists_index, and_imp]`. + -- + -- At this point: + -- - `hm` gives a condition of the form `∀ x, x ∈ P⫠ → x ∈ I → m*x ∈ bot`. + -- - The goal is `∀ y, y ∈ (A⫠ * B⫠) → m*y ∈ bot` (since `P` is an orthogonal of that product). + -- + -- Key trick (similar to the existing proof of `quest_contract_le`): + -- - Use `PhaseSpace.orth_extensive` to move elements into a double-orthogonal when needed. + -- - Use that `I` is closed under multiplication (use `I_mul_mem`) and that elements of `I` are idempotent. + -- - When you obtain `m * (x*x)` in `bot`, rewrite with idempotence `x*x = x` to finish. + -- + -- If automation gets stuck, mirror the structure of `quest_contract_le`: + -- construct the appropriate `x ∈ I` (built out of the `I`-witnesses you get from the two `?`-factors) and feed it to `hm`. sorry +theorem quest_closed_of_allQuest {M : Type*} [PhaseSpace M] {v : Atom → Fact M} {Γ : Sequent Atom} : Γ.allQuest → (ʔ (interpSequent (Atom:=Atom) M v Γ) : Fact M) ≤ interpSequent (Atom:=Atom) M v Γ := by + intro hall + revert hall + refine Multiset.induction_on Γ ?_ ?_ + · intro _ + -- base case Γ = 0 + -- show ?⊥ ≤ ⊥ by unfolding everything + simp [interpSequent_nil, PhaseSpace.Fact.quest, PhaseSpace.dualFact_coe, + PhaseSpace.orthogonal_def, PhaseSpace.I, PhaseSpace.idempotentsIn] + intro x hx + -- hx : x ∈ ({m | ...} ∩ {m | ...})⫠, need x ∈ bot + -- instantiate the universal property with 1, which is in the intersection + have h1 : (1 : M) ∈ ({m : M | ∀ x ∈ (⊥ : Fact M), m * x ∈ bot} ∩ + {m : M | IsIdempotentElem m ∧ ∀ x ∈ bot, m * x ∈ bot}) := by + constructor + · intro y hy + -- since y ∈ ⊥ means y ∈ bot + simpa using hy + · constructor + · -- 1 is idempotent + simpa [IsIdempotentElem] + · intro y hy + -- hy : y ∈ bot + simpa using hy + have hx1 := hx (1 : M) h1 + -- simplify x * 1 + simpa using hx1 + · intro A Γ ih hall + -- step case Γ = A ::ₘ Γ + rcases (allQuest_cons (Atom := Atom) (A := A) (Γ := Γ)).1 hall with ⟨hA, hall'⟩ + -- A must be a quest proposition + cases A <;> simp at hA + case quest B => + have hIH : (ʔ (interpSequent (Atom := Atom) M v Γ) : Fact M) ≤ + interpSequent (Atom := Atom) M v Γ := ih hall' + have htail : interpSequent (Atom := Atom) M v Γ = + (ʔ (interpSequent (Atom := Atom) M v Γ) : Fact M) := by + apply le_antisymm + · exact quest_le _ + · exact hIH + -- unfold the interpretation of the cons sequent + simp [interpSequent_cons, interpProp_quest] + -- rewrite the tail interpretation as a quest once + rw [htail] + -- close by quest-closure of parr of quests + simpa using (quest_closed_parr_quest_quest (M := M) + (G := interpProp (Atom := Atom) (M := M) v B) + (H := interpSequent (Atom := Atom) M v Γ)) + + +theorem quest_monotone {M : Type*} [PhaseSpace M] : Monotone (fun X : Fact M => (ʔ X : Fact M)) := by + intro X Y hXY + intro m hm + -- unfold membership in quest + -- reduce to set inclusion via antitonicity of orthogonal + have hYX : (Y⫠ ∩ I : Set M) ⊆ (X⫠ ∩ I : Set M) := by + intro p hp + refine And.intro ?_ hp.2 + -- p ∈ Y⫠ + -- use antitone of orthogonal + exact PhaseSpace.orth_antitone (X := (X : Set M)) (Y := (Y : Set M)) hXY hp.1 + have hdual : (X⫠ ∩ I : Set M)⫠ ⊆ (Y⫠ ∩ I : Set M)⫠ := PhaseSpace.orth_antitone hYX + -- simplify hm and goal to use hdual + -- coe of quest is orthogonal of intersection + simpa [PhaseSpace.Fact.quest, PhaseSpace.dualFact] using hdual (by + simpa [PhaseSpace.Fact.quest, PhaseSpace.dualFact] using hm) + +theorem quest_closed_interpSequent {M : Type*} [PhaseSpace M] {v : Atom → Fact M} {Γ : Sequent Atom} {X : Fact M} : Γ.allQuest → X ≤ interpSequent (Atom:=Atom) M v Γ → (ʔ X) ≤ interpSequent (Atom:=Atom) M v Γ := by + intro hQ hX + have hmono := (quest_monotone (M := M)) + have hXq : (ʔ X : Fact M) ≤ (ʔ (interpSequent (Atom := Atom) M v Γ) : Fact M) := by + exact hmono hX + have hclosed : (ʔ (interpSequent (Atom := Atom) M v Γ) : Fact M) ≤ interpSequent (Atom := Atom) M v Γ := by + exact quest_closed_of_allQuest (Atom := Atom) (M := M) (v := v) (Γ := Γ) hQ + exact le_trans hXq hclosed + +theorem quest_neg_pre {M : Type*} [PhaseSpace M] (G : Fact M) : (ʔ (Gᗮ) : Fact M) = ( ! G : Fact M)ᗮ := by + apply SetLike.coe_injective + -- Prove equality of carriers (sets) + calc + ((ʔ (Gᗮ) : Fact M) : Set M) + = (((Gᗮ : Set M)⫠ ∩ PhaseSpace.I (P := M)) : Set M)⫠ := by + simp only [Fact.quest, dualFact_coe] + _ = (((G : Set M)⫠⫠ ∩ PhaseSpace.I (P := M)) : Set M)⫠ := by + simp only [Fact.coe_neg] + _ = (((G : Set M) ∩ PhaseSpace.I (P := M)) : Set M)⫠ := by + -- use that `G` is a fact: (G : Set M) = (G : Set M)⫠⫠ + simpa [PhaseSpace.isFact] using + congrArg (fun S : Set M => (S ∩ PhaseSpace.I (P := M))⫠) G.property.symm + _ = (( ! G : Fact M) : Set M)⫠ := by + simp only [Fact.bang, dualFact_coe, PhaseSpace.triple_orth] + _ = (( ! G : Fact M)ᗮ : Set M) := by + simp only [Fact.coe_neg] + + +theorem bang_valid_of_allQuest {M : Type*} [PhaseSpace M] {v : Atom → Fact M} {a : Proposition Atom} {Γ : Sequent Atom} : Γ.allQuest → (interpProp (Atom:=Atom) (M:=M) v a ⅋ interpSequent (Atom:=Atom) M v Γ).IsValid → ((PhaseSpace.Fact.bang (interpProp (Atom:=Atom) (M:=M) v a)) ⅋ interpSequent (Atom:=Atom) M v Γ).IsValid := by + intro hallQuest hvalid + -- Step 1: from validity of par, get Gᗮ ≤ H + have hsub : (interpProp (Atom:=Atom) (M:=M) v a)ᗮ ≤ interpSequent (Atom:=Atom) M v Γ := + (par_valid_iff_neg_le (G := interpProp (Atom:=Atom) (M:=M) v a) + (H := interpSequent (Atom:=Atom) M v Γ)).1 hvalid + -- Step 2: close under ? for allQuest context + have hquest : (ʔ ((interpProp (Atom:=Atom) (M:=M) v a)ᗮ) : Fact M) ≤ interpSequent (Atom:=Atom) M v Γ := + quest_closed_interpSequent (Atom:=Atom) (M:=M) (v:=v) (Γ:=Γ) + (X := (interpProp (Atom:=Atom) (M:=M) v a)ᗮ) hallQuest hsub + -- Step 3: rewrite ?(Gᗮ) as (!G)ᗮ + have hbangneg : (( ! (interpProp (Atom:=Atom) (M:=M) v a) : Fact M)ᗮ) ≤ interpSequent (Atom:=Atom) M v Γ := by + -- use quest_neg_pre to rewrite + simpa [quest_neg_pre (M:=M) (G := interpProp (Atom:=Atom) (M:=M) v a)] using hquest + -- Step 4: conclude validity of (!G ⅋ H) + have hvalidBang : (( ! (interpProp (Atom:=Atom) (M:=M) v a) : Fact M) ⅋ interpSequent (Atom:=Atom) M v Γ).IsValid := + (par_valid_iff_neg_le (G := ( ! (interpProp (Atom:=Atom) (M:=M) v a) : Fact M)) + (H := interpSequent (Atom:=Atom) M v Γ)).2 hbangneg + -- Step 5: rewrite ! as PhaseSpace.Fact.bang + simpa using hvalidBang + + + theorem quest_neg_set (M : Type*) [PhaseSpace M] (G : Fact M) : ((PhaseSpace.Fact.quest (P:=M) (Gᗮ) : Fact M) : Set M) = ((PhaseSpace.Fact.bang (P:=M) G : Fact M) : Set M)⫠ := by