From d0d6cde52816a510aa557ddf113aed36fd731a11 Mon Sep 17 00:00:00 2001 From: Fabrizio Montesi Date: Tue, 3 Mar 2026 10:20:29 +0100 Subject: [PATCH 01/19] feat: change context notation to <[] --- Cslib/Foundations/Syntax/Congruence.lean | 2 +- Cslib/Foundations/Syntax/Context.lean | 2 +- Cslib/Languages/CCS/Basic.lean | 8 ++++---- 3 files changed, 6 insertions(+), 6 deletions(-) diff --git a/Cslib/Foundations/Syntax/Congruence.lean b/Cslib/Foundations/Syntax/Congruence.lean index 9d3774f97..0e710b147 100644 --- a/Cslib/Foundations/Syntax/Congruence.lean +++ b/Cslib/Foundations/Syntax/Congruence.lean @@ -15,6 +15,6 @@ namespace Cslib /-- An equivalence relation preserved by all contexts. -/ class Congruence (α : Type*) [HasContext α] (r : α → α → Prop) extends - IsEquiv α r, covariant : CovariantClass (HasContext.Context α) α (·[·]) r + IsEquiv α r, covariant : CovariantClass (HasContext.Context α) α (·<[·]) r end Cslib diff --git a/Cslib/Foundations/Syntax/Context.lean b/Cslib/Foundations/Syntax/Context.lean index 017abadbe..d4ae23789 100644 --- a/Cslib/Foundations/Syntax/Context.lean +++ b/Cslib/Foundations/Syntax/Context.lean @@ -19,6 +19,6 @@ class HasContext (Term : Sort*) where /-- Replaces the hole in the context with a term. -/ fill (c : Context) (t : Term) : Term -@[inherit_doc] notation:max c "[" t "]" => HasContext.fill c t +@[inherit_doc] notation:max c "<[" t "]" => HasContext.fill c t end Cslib diff --git a/Cslib/Languages/CCS/Basic.lean b/Cslib/Languages/CCS/Basic.lean index 76bc92e3d..1c3a71ef7 100644 --- a/Cslib/Languages/CCS/Basic.lean +++ b/Cslib/Languages/CCS/Basic.lean @@ -123,14 +123,14 @@ instance : HasContext (Process Name Constant) := ⟨Context Name Constant, Conte /-- Definition of context filling. -/ @[scoped grind =] -theorem isContext_def (c : Context Name Constant) (p : Process Name Constant) : - c[p] = c.fill p := rfl +theorem hasContext_def (c : Context Name Constant) (p : Process Name Constant) : + c<[p] = c.fill p := rfl /-- Any `Process` can be obtained by filling a `Context` with an atom. This proves that `Context` is a complete formalisation of syntactic contexts for CCS. -/ theorem Context.complete (p : Process Name Constant) : - ∃ c : Context Name Constant, p = c[Process.nil] ∨ - ∃ k : Constant, p = c[Process.const k] := by + ∃ c : Context Name Constant, p = c<[Process.nil] ∨ + ∃ k : Constant, p = c<[Process.const k] := by induction p case nil => exists hole From 3c97c1f3670c1bc6c250ebfaae306d823b9f9f2e Mon Sep 17 00:00:00 2001 From: Fabrizio Montesi Date: Tue, 3 Mar 2026 13:23:11 +0100 Subject: [PATCH 02/19] feat: contexts for CLL --- Cslib/Logics/LinearLogic/CLL/Basic.lean | 39 +++++++++++++++++++++++++ 1 file changed, 39 insertions(+) diff --git a/Cslib/Logics/LinearLogic/CLL/Basic.lean b/Cslib/Logics/LinearLogic/CLL/Basic.lean index c7cb4558e..68900c7e1 100644 --- a/Cslib/Logics/LinearLogic/CLL/Basic.lean +++ b/Cslib/Logics/LinearLogic/CLL/Basic.lean @@ -7,6 +7,7 @@ Authors: Fabrizio Montesi module public import Cslib.Init +public import Cslib.Foundations.Syntax.Context public import Mathlib.Data.Multiset.Fold @[expose] public section @@ -68,6 +69,44 @@ instance : Bot (Proposition Atom) := ⟨.bot⟩ @[inherit_doc] scoped prefix:95 "!" => Proposition.bang @[inherit_doc] scoped prefix:95 "ʔ" => Proposition.quest +/-- Propositional contexts (single-hole contexts for propositions). -/ +inductive Proposition.Context (Atom : Type u) : Type u where + | hole + | tensorL (c : Context Atom) (b : Proposition Atom) + | tensorR (a : Proposition Atom) (c : Context Atom) + | parrL (c : Context Atom) (b : Proposition Atom) + | parrR (a : Proposition Atom) (c : Context Atom) + | oplusL (c : Context Atom) (b : Proposition Atom) + | oplusR (a : Proposition Atom) (c : Context Atom) + | withL (c : Context Atom) (b : Proposition Atom) + | withR (a : Proposition Atom) (c : Context Atom) + | bang (c : Context Atom) + | quest (c : Context Atom) +deriving DecidableEq, BEq + +/-- Replaces the hole in a propositional context with a propositions. -/ +def Proposition.Context.fill (c : Context Atom) (a : Proposition Atom) : Proposition Atom := + match c with + | hole => a + | tensorL c b => .tensor (c.fill a) b + | tensorR b c => .tensor b (c.fill a) + | parrL c b => .parr (c.fill a) b + | parrR b c => .parr b (c.fill a) + | oplusL c b => .oplus (c.fill a) b + | oplusR b c => .oplus b (c.fill a) + | withL c b => .with (c.fill a) b + | withR b c => .with b (c.fill a) + | bang c => .bang (c.fill a) + | quest c => .quest (c.fill a) + +instance : HasContext (Proposition Atom) := + ⟨Proposition.Context Atom, Proposition.Context.fill⟩ + +/-- Definition of context filling. -/ +@[scoped grind =] +theorem Proposition.hasContext_def (c : Proposition.Context Atom) (a : Proposition Atom) : + c<[a] = c.fill a := rfl + /-- Positive propositions. -/ def Proposition.positive : Proposition Atom → Bool | atom _ => true From 7d277582f138857f6bcfc913650f94ecd37d5744 Mon Sep 17 00:00:00 2001 From: Fabrizio Montesi Date: Tue, 3 Mar 2026 19:04:26 +0100 Subject: [PATCH 03/19] feat: class for logical equivalence. Almost there! --- Cslib/Foundations/Syntax/Congruence.lean | 2 +- Cslib/Foundations/Syntax/Context.lean | 16 ++- Cslib/Languages/CCS/Basic.lean | 5 +- Cslib/Logics/LinearLogic/CLL/Basic.lean | 110 +++++++++--------- .../LinearLogic/CLL/CutElimination.lean | 4 +- .../Logics/LinearLogic/CLL/EtaExpansion.lean | 11 +- 6 files changed, 84 insertions(+), 64 deletions(-) diff --git a/Cslib/Foundations/Syntax/Congruence.lean b/Cslib/Foundations/Syntax/Congruence.lean index 0e710b147..b32ab53e9 100644 --- a/Cslib/Foundations/Syntax/Congruence.lean +++ b/Cslib/Foundations/Syntax/Congruence.lean @@ -13,7 +13,7 @@ public import Mathlib.Algebra.Order.Monoid.Unbundled.Defs namespace Cslib -/-- An equivalence relation preserved by all contexts. -/ +/-- An equivalence relation on `α` preserved by all contexts `Ctx`. -/ class Congruence (α : Type*) [HasContext α] (r : α → α → Prop) extends IsEquiv α r, covariant : CovariantClass (HasContext.Context α) α (·<[·]) r diff --git a/Cslib/Foundations/Syntax/Context.lean b/Cslib/Foundations/Syntax/Context.lean index d4ae23789..e3ffc4a36 100644 --- a/Cslib/Foundations/Syntax/Context.lean +++ b/Cslib/Foundations/Syntax/Context.lean @@ -12,10 +12,20 @@ public import Cslib.Init namespace Cslib -/-- Class for types (`Term`) that have a notion of (single-hole) contexts (`Context`). -/ -class HasContext (Term : Sort*) where +/-- Class for types with a canonical notion of heterogeneous single-hole contexts. -/ +class HasHContext (α : Type u) (β : Type v) where /-- The type of contexts. -/ - Context : Sort* + Context : Type* + /-- Replaces the hole in the context with a term, resulting in a new value. -/ + fill (c : Context) (b : β) : α + +@[inherit_doc] notation:max c "<[" t "]" => HasHContext.fill c t + +/-- Class for types (`Term`) that have a canonical notion of homogeneous single-hole contexts +(`Context`). -/ +class HasContext (Term : Type*) where + /-- The type of contexts. -/ + Context : Type* /-- Replaces the hole in the context with a term. -/ fill (c : Context) (t : Term) : Term diff --git a/Cslib/Languages/CCS/Basic.lean b/Cslib/Languages/CCS/Basic.lean index 1c3a71ef7..17dce26f5 100644 --- a/Cslib/Languages/CCS/Basic.lean +++ b/Cslib/Languages/CCS/Basic.lean @@ -119,11 +119,12 @@ def Context.fill (c : Context Name Constant) (p : Process Name Constant) : Proce | choiceR r c => Process.choice r (c.fill p) | res a c => Process.res a (c.fill p) -instance : HasContext (Process Name Constant) := ⟨Context Name Constant, Context.fill⟩ +instance : IsContext (Context Name Constant) (Process Name Constant) (Process Name Constant) := + ⟨Context.fill⟩ /-- Definition of context filling. -/ @[scoped grind =] -theorem hasContext_def (c : Context Name Constant) (p : Process Name Constant) : +theorem context_fill_def (c : Context Name Constant) (p : Process Name Constant) : c<[p] = c.fill p := rfl /-- Any `Process` can be obtained by filling a `Context` with an atom. This proves that `Context` diff --git a/Cslib/Logics/LinearLogic/CLL/Basic.lean b/Cslib/Logics/LinearLogic/CLL/Basic.lean index 68900c7e1..04bb45df8 100644 --- a/Cslib/Logics/LinearLogic/CLL/Basic.lean +++ b/Cslib/Logics/LinearLogic/CLL/Basic.lean @@ -8,6 +8,8 @@ module public import Cslib.Init public import Cslib.Foundations.Syntax.Context +public import Cslib.Foundations.Logic.InferenceSystem +public import Cslib.Foundations.Logic.LogicalEquivalence public import Mathlib.Data.Multiset.Fold @[expose] public section @@ -99,12 +101,11 @@ def Proposition.Context.fill (c : Context Atom) (a : Proposition Atom) : Proposi | bang c => .bang (c.fill a) | quest c => .quest (c.fill a) -instance : HasContext (Proposition Atom) := - ⟨Proposition.Context Atom, Proposition.Context.fill⟩ +instance : HasContext (Proposition Atom) := ⟨Proposition.Context Atom, Proposition.Context.fill⟩ /-- Definition of context filling. -/ @[scoped grind =] -theorem Proposition.hasContext_def (c : Proposition.Context Atom) (a : Proposition Atom) : +theorem Proposition.context_fill_def (c : Context Atom) (a : Proposition Atom) : c<[a] = c.fill a := rfl /-- Positive propositions. -/ @@ -191,6 +192,15 @@ def Sequent.allQuest (Γ : Sequent Atom) := Γ.map (· matches ʔ_) |> Multiset.fold Bool.and true +/-- Judgemental contexts for CLL. -/ +def Sequent.Context Atom := Multiset (Proposition Atom) × Unit + +/-- Filling a judgemental context returns a sequent. -/ +def Sequent.Context.fill (Γc : Sequent.Context Atom) (a : Proposition Atom) := a ::ₘ Γc.1 + +instance : HasHContext (Sequent Atom) (Proposition Atom) := + ⟨Sequent.Context Atom, Sequent.Context.fill⟩ + open Proposition in /-- A proof in the sequent calculus for classical linear logic. -/ inductive Proof : Sequent Atom → Type u where @@ -210,34 +220,19 @@ inductive Proof : Sequent Atom → Type u where | bang {Γ : Sequent Atom} {a} : Γ.allQuest → Proof (a ::ₘ Γ) → Proof ((!a) ::ₘ Γ) -- No rule for zero. -@[inherit_doc] -scoped notation "⇓" Γ:90 => Proof Γ +open Logic -/-- Rewrites the conclusion of a proof into an equal one. -/ -@[scoped grind =] -def Proof.rwConclusion (h : Γ = Δ) (p : ⇓Γ) : ⇓Δ := h ▸ p - -/-- A sequent is provable if there exists a proof that concludes it. -/ -@[scoped grind =] -def Sequent.Provable (Γ : Sequent Atom) := Nonempty (⇓Γ) +instance : InferenceSystem (Sequent Atom) := ⟨Proof⟩ -/-- Having a proof of Γ shows that it is provable. -/ -theorem Sequent.Provable.fromProof {Γ : Sequent Atom} (p : ⇓Γ) : Γ.Provable := ⟨p⟩ +open InferenceSystem -/-- Having a proof of Γ shows that it is provable. -/ +/-- Convenience definition for rewriting conclusions in proofs. -/ @[scoped grind =] -noncomputable def Sequent.Provable.toProof {Γ : Sequent Atom} (p : Γ.Provable) : ⇓Γ := - Classical.choice p - -instance : Coe (Proof Γ) (Γ.Provable) where - coe p := Sequent.Provable.fromProof p - -noncomputable instance : Coe (Γ.Provable) (Proof Γ) where - coe p := p.toProof +def Proof.rwConclusion {Γ Δ : Sequent Atom} (h : Γ = Δ) (p : ⇓Γ) := InferenceSystem.rwConclusion h p /-- The axiom, but where the order of propositions is reversed. -/ @[scoped grind <=] -def Proof.ax' {a : Proposition Atom} : ⇓{a⫠, a} := +def Proof.ax' {a : Proposition Atom} : ⇓({a⫠, a} : Sequent Atom) := Multiset.pair_comm a (a⫠) ▸ Proof.ax /-- Cut, but where the premises are reversed. -/ @@ -274,27 +269,29 @@ section LogicalEquiv /-- Two propositions are equivalent if one implies the other and vice versa. Proof-relevant version. -/ -def Proposition.equiv (a b : Proposition Atom) := ⇓{a⫠, b} × ⇓{b⫠, a} - -open Sequent in -/-- Propositional equivalence, proof-irrelevant version (`Prop`). -/ -def Proposition.Equiv (a b : Proposition Atom) := Provable {a⫠, b} ∧ Provable {b⫠, a} - -/-- Conversion from proof-relevant to proof-irrelevant versions of propositional -equivalence. -/ -theorem Proposition.equiv.toProp (h : Proposition.equiv a b) : Proposition.Equiv a b := by - obtain ⟨p, q⟩ := h - exact ⟨p, q⟩ +def Proposition.equiv (a b : Proposition Atom) := + ⇓({a⫠, b} : Sequent Atom) × ⇓({b⫠, a} : Sequent Atom) @[inherit_doc] scoped infix:29 " ≡⇓ " => Proposition.equiv +open Sequent in +/-- Propositional equivalence, proof-irrelevant version (`Prop`). -/ +def Proposition.Equiv (a b : Proposition Atom) := + Derivable ({a⫠, b} : Sequent Atom) ∧ Derivable ({b⫠, a} : Sequent Atom) + @[inherit_doc] scoped infix:29 " ≡ " => Proposition.Equiv +/-- Conversion from proof-relevant to proof-irrelevant versions of propositional +equivalence. -/ +theorem Proposition.equiv.toProp (h : a ≡⇓ b) : a ≡ b := ⟨h.1, h.2⟩ + /-- Proof-relevant equivalence is coerciable into proof-irrelevant equivalence. -/ -instance {a b : Proposition Atom} : Coe (a ≡⇓ b) (a ≡ b) where - coe := Proposition.equiv.toProp +instance : Coe (a ≡⇓ b) (a ≡ b) := ⟨Proposition.equiv.toProp⟩ + +/-- Transforms a proof-irrelevant equivalence into a proof-relevant one (this is not computable). -/ +noncomputable def chooseEquiv (h : a ≡ b) : a ≡⇓ b := ⟨h.1, h.2⟩ namespace Proposition @@ -302,8 +299,7 @@ open Sequent /-- Proof-relevant equivalence is reflexive. -/ @[scoped grind =] -def equiv.refl (a : Proposition Atom) : a.equiv a := - ⟨Proof.ax', Proof.ax'⟩ +def equiv.refl (a : Proposition Atom) : a ≡⇓ a := ⟨Proof.ax', Proof.ax'⟩ /-- Proof-relevant equivalence is symmetric. -/ @[scoped grind =] @@ -326,21 +322,17 @@ theorem Equiv.symm {a b : Proposition Atom} (h : a ≡ b) : b ≡ a := ⟨h.2, h /-- Proof-irrelevant equivalence is transitive. -/ @[scoped grind →] theorem Equiv.trans {a b c : Proposition Atom} (hab : a ≡ b) (hbc : b ≡ c) : a ≡ c := - ⟨ - Provable.fromProof - (Proof.cut (hab.1.toProof.rwConclusion (Multiset.pair_comm _ _)) hbc.1.toProof), - Provable.fromProof - (Proof.cut (hbc.2.toProof.rwConclusion (Multiset.pair_comm _ _)) hab.2.toProof) - ⟩ - -/-- Transforms a proof-irrelevant equivalence into a proof-relevant one (this is not computable). -/ -noncomputable def chooseEquiv (h : a ≡ b) : a ≡⇓ b := - ⟨h.1.toProof, h.2.toProof⟩ + equiv.trans (chooseEquiv hab) (chooseEquiv hbc) /-- The canonical equivalence relation for propositions. -/ def propositionSetoid : Setoid (Proposition Atom) := ⟨Equiv, Equiv.refl, Equiv.symm, Equiv.trans⟩ +instance : IsEquiv (Proposition Atom) Proposition.Equiv where + refl := Equiv.refl + symm a b := Equiv.symm (a := a) (b := b) + trans a b c := Equiv.trans (a := a) (b := b) (c := c) + /-- !⊤ ≡⇓ 1 -/ @[scoped grind =] def bang_top_eqv_one : (!⊤ : Proposition Atom) ≡⇓ 1 := @@ -349,8 +341,8 @@ def bang_top_eqv_one : (!⊤ : Proposition Atom) ≡⇓ 1 := /-- ʔ0 ≡⇓ ⊥ -/ @[scoped grind =] def quest_zero_eqv_bot : (ʔ0 : Proposition Atom) ≡⇓ ⊥ := - ⟨.rwConclusion (Multiset.pair_comm ..) <| .bot (.bang rfl .top), - .rwConclusion (Multiset.pair_comm ..) <| .weaken .one⟩ + ⟨rwConclusion (Multiset.pair_comm ..) <| .bot (.bang rfl .top), + rwConclusion (Multiset.pair_comm ..) <| .weaken .one⟩ /-- a ⊗ 0 ≡⇓ 0 -/ @[scoped grind =] @@ -405,6 +397,18 @@ open scoped Multiset in def subst_eqv {Γ Δ : Sequent Atom} (heqv : a ≡⇓ b) (p : ⇓(Γ + {a} + Δ)) : ⇓(Γ + {b} + Δ) := add_middle_eq_cons ▸ subst_eqv_head heqv (add_middle_eq_cons ▸ p) +instance : Congruence (Proposition Atom) Proposition.Equiv where + elim : + Covariant (Proposition.Context Atom) (Proposition Atom) (Proposition.Context.fill) + Proposition.Equiv := by + sorry + +instance : LogicalEquivalence (Proposition Atom) (Sequent Atom) Proof where + eqv := Proposition.Equiv + eqv_fill_valid {a b : Proposition Atom} (heqv : a.Equiv b) + (c : HasHContext.Context (Sequent Atom) (Proposition Atom)) + (h : ⇓c<[a]) : ⇓c<[b] := sorry + /-- Tensor is commutative. -/ @[scoped grind =] def tensor_symm {a b : Proposition Atom} : a ⊗ b ≡⇓ b ⊗ a := @@ -426,8 +430,8 @@ def tensor_assoc {a b c : Proposition Atom} : a ⊗ (b ⊗ c) ≡⇓ (a ⊗ b) show a⫠ ::ₘ b⫠ ::ₘ c⫠ ::ₘ {a ⊗ (b ⊗ c)} = ((a ⊗ (b ⊗ c)) ::ₘ {a⫠} + ({b⫠} + {c⫠})) by grind ▸ (.tensor .ax <| .tensor .ax .ax)⟩ -instance {Γ : Sequent Atom} : Std.Symm (fun a b => Sequent.Provable ((a ⊗ b) ::ₘ Γ)) where - symm _ _ h := Sequent.Provable.fromProof (subst_eqv_head tensor_symm h.toProof) +instance {Γ : Sequent Atom} : Std.Symm (fun a b => Derivable ((a ⊗ b) ::ₘ Γ)) where + symm _ _ h := Derivable.fromDerivation (subst_eqv_head tensor_symm (Derivable.toDerivation h)) /-- ⊕ is idempotent. -/ @[scoped grind =] diff --git a/Cslib/Logics/LinearLogic/CLL/CutElimination.lean b/Cslib/Logics/LinearLogic/CLL/CutElimination.lean index 7969a7d69..cc435d544 100644 --- a/Cslib/Logics/LinearLogic/CLL/CutElimination.lean +++ b/Cslib/Logics/LinearLogic/CLL/CutElimination.lean @@ -18,8 +18,10 @@ universe u variable {Atom : Type u} +open Cslib.Logic.InferenceSystem + /-- A proof is cut-free if it does not contain any applications of rule cut. -/ -def Proof.cutFree (p : ⇓Γ) : Bool := +def Proof.cutFree {Γ : Sequent Atom} (p : ⇓Γ) : Bool := match p with | ax => true | one => true diff --git a/Cslib/Logics/LinearLogic/CLL/EtaExpansion.lean b/Cslib/Logics/LinearLogic/CLL/EtaExpansion.lean index ab891c49d..de4cfdb95 100644 --- a/Cslib/Logics/LinearLogic/CLL/EtaExpansion.lean +++ b/Cslib/Logics/LinearLogic/CLL/EtaExpansion.lean @@ -25,10 +25,12 @@ attribute [local grind =] Multiset.add_comm attribute [local grind =] Multiset.add_assoc attribute [local grind =] Multiset.insert_eq_cons +open Cslib.Logic.InferenceSystem + /-- The η-expansion of a proposition `a` is a `Proof` of `{a, a⫠}` that applies the axiom only to atomic propositions. -/ @[scoped grind =] -def Proposition.expand (a : Proposition Atom) : ⇓{a, a⫠} := +def Proposition.expand (a : Proposition Atom) : ⇓({a, a⫠} : Sequent Atom):= match a with | atom x | atomDual x => Proof.ax @@ -80,7 +82,7 @@ decreasing_by /-- A `Proof` has only atomic axioms if all its instances of the axiom treat atomic propositions. -/ @[scoped grind =] -def Proof.onlyAtomicAxioms (p : ⇓Γ) : Bool := +def Proof.onlyAtomicAxioms {Γ : Sequent Atom} (p : ⇓Γ) : Bool := match p with | @ax _ a => (a matches Proposition.atom _) || (a matches Proposition.atomDual _) | cut p q => p.onlyAtomicAxioms && q.onlyAtomicAxioms @@ -98,8 +100,9 @@ def Proof.onlyAtomicAxioms (p : ⇓Γ) : Bool := | bang _ p => p.onlyAtomicAxioms /-- `Proof.onlyAtomicAxioms` is preserved by `Proof.rwConclusion`. -/ -theorem Proof.onlyAtomicAxioms_rwConclusion {heq : Γ = Δ} {p : ⇓Γ} (h : p.onlyAtomicAxioms) : - (p.rwConclusion heq).onlyAtomicAxioms := by grind +theorem Proof.onlyAtomicAxioms_rwConclusion {Γ Δ : Sequent Atom} {heq : Γ = Δ} {p : ⇓Γ} + (h : p.onlyAtomicAxioms) : + (rwConclusion heq p).onlyAtomicAxioms := by grind open Proposition Proof in @[local grind →] From ec6392b27921a6e0be435aab9cc053253d85fb7c Mon Sep 17 00:00:00 2001 From: Fabrizio Montesi Date: Tue, 3 Mar 2026 19:04:45 +0100 Subject: [PATCH 04/19] forgot some files --- Cslib/Foundations/Logic/InferenceSystem.lean | 47 +++++++++++++++++++ .../Foundations/Logic/LogicalEquivalence.lean | 33 +++++++++++++ 2 files changed, 80 insertions(+) create mode 100644 Cslib/Foundations/Logic/InferenceSystem.lean create mode 100644 Cslib/Foundations/Logic/LogicalEquivalence.lean diff --git a/Cslib/Foundations/Logic/InferenceSystem.lean b/Cslib/Foundations/Logic/InferenceSystem.lean new file mode 100644 index 000000000..ef10f8358 --- /dev/null +++ b/Cslib/Foundations/Logic/InferenceSystem.lean @@ -0,0 +1,47 @@ +/- +Copyright (c) 2026 Fabrizio Montesi. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Fabrizio Montesi +-/ + +module + +@[expose] public section + +namespace Cslib.Logic + +/-- +The notation typeclass for inference systems. +This enables the notation `⇓a`, where `a : α` is a derivable value. +-/ +class InferenceSystem (α : Type u) where + /-- + `⇓a` is a derivation of `a`, that is, a witness that `a` is derivable. + The meaning of this notation is type-dependent. + -/ + derivation (s : α) : Sort v + +namespace InferenceSystem + +@[inherit_doc] scoped notation "⇓" a:90 => InferenceSystem.derivation a + +/-- Rewrites the conclusion of a proof into an equal one. -/ +@[scoped grind =] +def rwConclusion [InferenceSystem α] {Γ Δ : α} (h : Γ = Δ) (p : ⇓Γ) : ⇓Δ := h ▸ p + +/-- `a` is derivable if it is the conclusion of some derivation. -/ +def Derivable [InferenceSystem α] (a : α) := Nonempty (⇓a) + +/-- Shows derivability from a derivation. -/ +def Derivable.fromDerivation [InferenceSystem α] {a : α} (d : ⇓a) : Derivable a := Nonempty.intro d + +instance [InferenceSystem α] {a : α} : Coe (⇓a) (Derivable a) := ⟨Derivable.fromDerivation⟩ + +/-- Extracts (noncomputably) a derivation from the fact that a conclusion is derivable. -/ +noncomputable def Derivable.toDerivation [InferenceSystem α] {a : α} (d : Derivable a) : ⇓a := Classical.choice d + +noncomputable instance [InferenceSystem α] {a : α} : Coe (Derivable a) (⇓a) := ⟨Derivable.toDerivation⟩ + +end InferenceSystem + +end Cslib.Logic diff --git a/Cslib/Foundations/Logic/LogicalEquivalence.lean b/Cslib/Foundations/Logic/LogicalEquivalence.lean new file mode 100644 index 000000000..b361c65a4 --- /dev/null +++ b/Cslib/Foundations/Logic/LogicalEquivalence.lean @@ -0,0 +1,33 @@ +/- +Copyright (c) 2026 Fabrizio Montesi. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Fabrizio Montesi +-/ + +module + +public import Cslib.Foundations.Syntax.Context +public import Cslib.Foundations.Syntax.Congruence + +@[expose] public section + +namespace Cslib.Logic + +/-- A logical equivalence for a given type of `Judgement`s is a congruence on propositions that +preserves validity of judgements. -/ +class LogicalEquivalence + (Proposition : Type u) [HasContext Proposition] + (Judgement : Type v) [HasHContext Judgement Proposition] + (Valid : Judgement → Sort w) where + /-- The logical equivalence relation. -/ + eqv (a b : Proposition) : Prop + /-- Proof that `eqv` is a congruence. -/ + [congruence : Congruence Proposition eqv] + /-- Validity is preserved for any judgemental context. -/ + eqv_fill_valid (heqv : eqv a b) (c : HasHContext.Context Judgement Proposition) + (h : Valid (c<[a])) : Valid (c<[b]) + +@[inherit_doc] +scoped infix:29 " ≡ " => LogicalEquivalence.eqv + +end Cslib.Logic From 5b433ab5c7d5c311b87c9d098258c189e4b16315 Mon Sep 17 00:00:00 2001 From: Fabrizio Montesi Date: Wed, 4 Mar 2026 18:54:25 +0100 Subject: [PATCH 05/19] logical equivalence for HML --- .../Foundations/Logic/LogicalEquivalence.lean | 2 +- Cslib/Foundations/Syntax/Context.lean | 10 +- Cslib/Logics/HML/LogicalEquivalence.lean | 107 ++++++++++++++++++ Cslib/Logics/LinearLogic/CLL/Basic.lean | 57 +++++++++- 4 files changed, 167 insertions(+), 9 deletions(-) create mode 100644 Cslib/Logics/HML/LogicalEquivalence.lean diff --git a/Cslib/Foundations/Logic/LogicalEquivalence.lean b/Cslib/Foundations/Logic/LogicalEquivalence.lean index b361c65a4..d24628559 100644 --- a/Cslib/Foundations/Logic/LogicalEquivalence.lean +++ b/Cslib/Foundations/Logic/LogicalEquivalence.lean @@ -14,7 +14,7 @@ public import Cslib.Foundations.Syntax.Congruence namespace Cslib.Logic /-- A logical equivalence for a given type of `Judgement`s is a congruence on propositions that -preserves validity of judgements. -/ +preserves validity of judgements under any judgemental context. -/ class LogicalEquivalence (Proposition : Type u) [HasContext Proposition] (Judgement : Type v) [HasHContext Judgement Proposition] diff --git a/Cslib/Foundations/Syntax/Context.lean b/Cslib/Foundations/Syntax/Context.lean index e3ffc4a36..ef367cef7 100644 --- a/Cslib/Foundations/Syntax/Context.lean +++ b/Cslib/Foundations/Syntax/Context.lean @@ -16,19 +16,19 @@ namespace Cslib class HasHContext (α : Type u) (β : Type v) where /-- The type of contexts. -/ Context : Type* - /-- Replaces the hole in the context with a term, resulting in a new value. -/ + /-- Replaces the hole in the context with a value, resulting in a new value. -/ fill (c : Context) (b : β) : α @[inherit_doc] notation:max c "<[" t "]" => HasHContext.fill c t -/-- Class for types (`Term`) that have a canonical notion of homogeneous single-hole contexts +/-- Class for types (`α`) that have a canonical notion of homogeneous single-hole contexts (`Context`). -/ -class HasContext (Term : Type*) where +class HasContext (α : Type*) where /-- The type of contexts. -/ Context : Type* /-- Replaces the hole in the context with a term. -/ - fill (c : Context) (t : Term) : Term + fill (c : Context) (a : α) : α -@[inherit_doc] notation:max c "<[" t "]" => HasContext.fill c t +instance [inst : HasContext α] : HasHContext α α := ⟨inst.Context, inst.fill⟩ end Cslib diff --git a/Cslib/Logics/HML/LogicalEquivalence.lean b/Cslib/Logics/HML/LogicalEquivalence.lean new file mode 100644 index 000000000..4e1d83af1 --- /dev/null +++ b/Cslib/Logics/HML/LogicalEquivalence.lean @@ -0,0 +1,107 @@ +/- +Copyright (c) 2026 Fabrizio Montesi. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Fabrizio Montesi +-/ + +module + +public import Cslib.Logics.HML.Basic +public import Cslib.Foundations.Logic.LogicalEquivalence + +@[expose] public section + +/-! # Logical Equivalence in HML + +This module defines logical equivalence for HML propositions and instantiates `LogicalEquivalence`. +-/ + +namespace Cslib.Logic.HML + +/-- Logical equivalence for HML propositions. -/ +@[scoped grind =] +def Proposition.Equiv {State : Type u} {Label : Type v} (a b : Proposition Label) : Prop := + ∀ lts : LTS State Label, a.denotation lts = b.denotation lts + +/-- Propositional contexts. -/ +inductive Proposition.Context (Label : Type u) : Type u where + | hole + | andL (c : Context Label) (φ : Proposition Label) + | andR (φ : Proposition Label) (c : Context Label) + | orL (c : Context Label) (φ : Proposition Label) + | orR (φ : Proposition Label) (c : Context Label) + | diamond (μ : Label) (c : Context Label) + | box (μ : Label) (c : Context Label) + +/-- Replaces a hole in a propositional context with a proposition. -/ +@[scoped grind =] +def Proposition.Context.fill (c : Context Label) (φ : Proposition Label) := + match c with + | hole => φ + | andL c φ' => (c.fill φ).and φ' + | andR φ' c => φ'.and (c.fill φ) + | orL c φ' => (c.fill φ).or φ' + | orR φ' c => φ'.or (c.fill φ) + | diamond μ c => .diamond μ (c.fill φ) + | box μ c => .box μ (c.fill φ) + +instance : HasContext (Proposition Label) := ⟨Proposition.Context Label, Proposition.Context.fill⟩ + +open scoped Proposition Proposition.Context + +instance : IsEquiv (Proposition Label) (Proposition.Equiv (State := State) (Label := Label)) where + refl := by grind + symm := by grind + trans := by grind + +instance {State : Type u} {Label : Type v} : + Congruence (Proposition Label) (Proposition.Equiv (State := State) (Label := Label)) where + elim : + Covariant (Proposition.Context Label) (Proposition Label) (Proposition.Context.fill) + Proposition.Equiv := by + intro ctx a b hab lts + specialize hab lts + induction ctx + <;> simp only [Proposition.Context.fill, Proposition.denotation] + <;> grind + +/-- Bundled version of a judgement for `Satisfy`. -/ +structure Satisfies.Judgement (State : Type u) (Label : Type v) where + lts : LTS State Label + state : State + φ : Proposition Label + +/-- `Satisfies` variant using bundled judgements. -/ +def Satisfies.Bundled (j : Satisfies.Judgement State Label) := Satisfies j.lts j.state j.φ + +@[scoped grind =] +theorem Satisfies.bundled_char : Satisfies.Bundled j ↔ Satisfies j.lts j.state j.φ := by rfl + +/-- Judgemental contexts. -/ +structure Satisfies.Context (State : Type u) (Label : Type v) where + lts : LTS State Label + state : State + +/-- Fills a judgemental context with a proposition. -/ +def Satisfies.Context.fill (c : Satisfies.Context State Label) (φ : Proposition Label) : + Satisfies.Judgement State Label := { + lts := c.lts + state := c.state + φ := φ +} + +instance judgementalContext : + HasHContext (Satisfies.Judgement State Label) (Proposition Label) := + ⟨Satisfies.Context State Label, Satisfies.Context.fill⟩ + +instance : LogicalEquivalence + (Proposition Label) (Satisfies.Judgement State Label) (Satisfies.Bundled) where + eqv := Proposition.Equiv + eqv_fill_valid {a b : Proposition Label} (heqv : a.Equiv (State := State) b) + (c : HasHContext.Context (Satisfies.Judgement State Label) (Proposition Label)) + (h : Satisfies.Bundled c<[a]) : Satisfies.Bundled c<[b] := by + simp only [Satisfies.bundled_char, HasHContext.fill, Satisfies.Context.fill] + simp only [Satisfies.bundled_char, HasHContext.fill, Satisfies.Context.fill] at h + grind + +end Cslib.Logic.HML diff --git a/Cslib/Logics/LinearLogic/CLL/Basic.lean b/Cslib/Logics/LinearLogic/CLL/Basic.lean index 04bb45df8..91e2d2a92 100644 --- a/Cslib/Logics/LinearLogic/CLL/Basic.lean +++ b/Cslib/Logics/LinearLogic/CLL/Basic.lean @@ -87,6 +87,7 @@ inductive Proposition.Context (Atom : Type u) : Type u where deriving DecidableEq, BEq /-- Replaces the hole in a propositional context with a propositions. -/ +@[scoped grind =] def Proposition.Context.fill (c : Context Atom) (a : Proposition Atom) : Proposition Atom := match c with | hole => a @@ -397,17 +398,67 @@ open scoped Multiset in def subst_eqv {Γ Δ : Sequent Atom} (heqv : a ≡⇓ b) (p : ⇓(Γ + {a} + Δ)) : ⇓(Γ + {b} + Δ) := add_middle_eq_cons ▸ subst_eqv_head heqv (add_middle_eq_cons ▸ p) +open scoped Context + +@[local grind .] +private lemma Proposition.equiv_tensor₁ {a a' b : Proposition Atom} (h : a ≡ a') : + a ⊗ b ≡ a' ⊗ b := by sorry + -- obtain ⟨h₁, h₂⟩ := h + -- obtain h₁ := h₁.some + -- obtain h₂ := h₂.some + -- constructor + -- case left => + -- constructor + +@[local grind .] +private lemma Proposition.equiv_tensor₂ {a b b' : Proposition Atom} (h : b ≡ b') : + a ⊗ b ≡ a ⊗ b' := by sorry + +@[local grind .] +private lemma Proposition.equiv_parr₁ {a a' b : Proposition Atom} (h : a ≡ a') : + a ⅋ b ≡ a' ⅋ b := by sorry + +@[local grind .] +private lemma Proposition.equiv_parr₂ {a b b' : Proposition Atom} (h : b ≡ b') : + a ⅋ b ≡ a ⅋ b' := by sorry + +@[local grind .] +private lemma Proposition.equiv_oplus₁ {a a' b : Proposition Atom} (h : a ≡ a') : + a ⊕ b ≡ a' ⊕ b := by sorry + +@[local grind .] +private lemma Proposition.equiv_oplus₂ {a b b' : Proposition Atom} (h : b ≡ b') : + a ⊕ b ≡ a ⊕ b' := by sorry + +@[local grind .] +private lemma Proposition.equiv_with₁ {a a' b : Proposition Atom} (h : a ≡ a') : + a & b ≡ a' & b := by sorry + +@[local grind .] +private lemma Proposition.equiv_with₂ {a b b' : Proposition Atom} (h : b ≡ b') : + a & b ≡ a & b' := by sorry + +@[local grind .] +private lemma Proposition.equiv_bang {a a' : Proposition Atom} (h : a ≡ a') : + !a ≡ !a' := by sorry + +@[local grind .] +private lemma Proposition.equiv_quest {a a' : Proposition Atom} (h : a ≡ a') : + ʔa ≡ ʔa' := by sorry + instance : Congruence (Proposition Atom) Proposition.Equiv where elim : Covariant (Proposition.Context Atom) (Proposition Atom) (Proposition.Context.fill) Proposition.Equiv := by - sorry + intro ctx a b hab + induction ctx <;> grind -instance : LogicalEquivalence (Proposition Atom) (Sequent Atom) Proof where +noncomputable instance : LogicalEquivalence (Proposition Atom) (Sequent Atom) Proof where eqv := Proposition.Equiv eqv_fill_valid {a b : Proposition Atom} (heqv : a.Equiv b) (c : HasHContext.Context (Sequent Atom) (Proposition Atom)) - (h : ⇓c<[a]) : ⇓c<[b] := sorry + (h : ⇓c<[a]) : ⇓c<[b] := by + apply subst_eqv_head (chooseEquiv heqv) h /-- Tensor is commutative. -/ @[scoped grind =] From d2761314297fade0e6889f00f02d31bed3ed2eb0 Mon Sep 17 00:00:00 2001 From: Fabrizio Montesi Date: Thu, 5 Mar 2026 08:41:15 +0100 Subject: [PATCH 06/19] minor fixes --- Cslib/Foundations/Syntax/Context.lean | 2 +- Cslib/Logics/HML/LogicalEquivalence.lean | 3 +-- 2 files changed, 2 insertions(+), 3 deletions(-) diff --git a/Cslib/Foundations/Syntax/Context.lean b/Cslib/Foundations/Syntax/Context.lean index ef367cef7..5316fd8d4 100644 --- a/Cslib/Foundations/Syntax/Context.lean +++ b/Cslib/Foundations/Syntax/Context.lean @@ -13,7 +13,7 @@ public import Cslib.Init namespace Cslib /-- Class for types with a canonical notion of heterogeneous single-hole contexts. -/ -class HasHContext (α : Type u) (β : Type v) where +class HasHContext (α β : Type*) where /-- The type of contexts. -/ Context : Type* /-- Replaces the hole in the context with a value, resulting in a new value. -/ diff --git a/Cslib/Logics/HML/LogicalEquivalence.lean b/Cslib/Logics/HML/LogicalEquivalence.lean index 4e1d83af1..17db3a313 100644 --- a/Cslib/Logics/HML/LogicalEquivalence.lean +++ b/Cslib/Logics/HML/LogicalEquivalence.lean @@ -84,11 +84,10 @@ structure Satisfies.Context (State : Type u) (Label : Type v) where /-- Fills a judgemental context with a proposition. -/ def Satisfies.Context.fill (c : Satisfies.Context State Label) (φ : Proposition Label) : - Satisfies.Judgement State Label := { + Satisfies.Judgement State Label where lts := c.lts state := c.state φ := φ -} instance judgementalContext : HasHContext (Satisfies.Judgement State Label) (Proposition Label) := From 0b4a0ccec4505e2024f5fb7f7d5da30545e31832 Mon Sep 17 00:00:00 2001 From: Fabrizio Montesi Date: Thu, 5 Mar 2026 11:04:36 +0100 Subject: [PATCH 07/19] parr1 --- Cslib/Logics/LinearLogic/CLL/Basic.lean | 72 +++++++++++++++++++++---- 1 file changed, 63 insertions(+), 9 deletions(-) diff --git a/Cslib/Logics/LinearLogic/CLL/Basic.lean b/Cslib/Logics/LinearLogic/CLL/Basic.lean index 91e2d2a92..c633a6469 100644 --- a/Cslib/Logics/LinearLogic/CLL/Basic.lean +++ b/Cslib/Logics/LinearLogic/CLL/Basic.lean @@ -402,21 +402,75 @@ open scoped Context @[local grind .] private lemma Proposition.equiv_tensor₁ {a a' b : Proposition Atom} (h : a ≡ a') : - a ⊗ b ≡ a' ⊗ b := by sorry - -- obtain ⟨h₁, h₂⟩ := h - -- obtain h₁ := h₁.some - -- obtain h₂ := h₂.some - -- constructor - -- case left => - -- constructor + a ⊗ b ≡ a' ⊗ b := by + obtain ⟨h₁, h₂⟩ := h + obtain h₁ := h₁.some + obtain h₂ := h₂.some + constructor + case left => + constructor + simp only [Proposition.dual] + apply Proof.parr + rw [show (a⫠ ::ₘ b⫠ ::ₘ {a' ⊗ b}) = ((a' ⊗ b) ::ₘ ({a⫠} + {b⫠})) by grind] + apply Proof.tensor + · apply h₁.rwConclusion (by grind) + · exact Proof.ax + case right => + constructor + simp only [Proposition.dual] + apply Proof.parr + rw [show (a'⫠ ::ₘ b⫠ ::ₘ {a ⊗ b}) = ((a ⊗ b) ::ₘ ({a'⫠} + {b⫠})) by grind] + apply Proof.tensor + · apply h₂.rwConclusion (by grind) + · exact Proof.ax @[local grind .] private lemma Proposition.equiv_tensor₂ {a b b' : Proposition Atom} (h : b ≡ b') : - a ⊗ b ≡ a ⊗ b' := by sorry + a ⊗ b ≡ a ⊗ b' := by + obtain ⟨h₁, h₂⟩ := h + obtain h₁ := h₁.some + obtain h₂ := h₂.some + constructor + case left => + constructor + simp only [Proposition.dual] + apply Proof.parr + rw [show (a⫠ ::ₘ b⫠ ::ₘ {a ⊗ b'}) = ((a ⊗ b') ::ₘ ({a⫠} + {b⫠})) by grind] + apply Proof.tensor + · exact Proof.ax + · apply h₁.rwConclusion (by grind) + case right => + constructor + simp only [Proposition.dual] + apply Proof.parr + rw [show (a⫠ ::ₘ b'⫠ ::ₘ {a ⊗ b}) = ((a ⊗ b) ::ₘ ({a⫠} + {b'⫠})) by grind] + apply Proof.tensor + · exact Proof.ax + · apply h₂.rwConclusion (by grind) @[local grind .] private lemma Proposition.equiv_parr₁ {a a' b : Proposition Atom} (h : a ≡ a') : - a ⅋ b ≡ a' ⅋ b := by sorry + a ⅋ b ≡ a' ⅋ b := by + obtain ⟨h₁, h₂⟩ := h + obtain h₁ := h₁.some + obtain h₂ := h₂.some + constructor + case left => + constructor + simp only [Proposition.dual] + apply Proof.parr + rw [show (a⫠ ::ₘ b⫠ ::ₘ {a ⊗ b'}) = ((a ⊗ b') ::ₘ ({a⫠} + {b⫠})) by grind] + apply Proof.tensor + · exact Proof.ax + · apply h₁.rwConclusion (by grind) + case right => + constructor + simp only [Proposition.dual] + apply Proof.parr + rw [show (a⫠ ::ₘ b'⫠ ::ₘ {a ⊗ b}) = ((a ⊗ b) ::ₘ ({a⫠} + {b'⫠})) by grind] + apply Proof.tensor + · exact Proof.ax + · apply h₂.rwConclusion (by grind) @[local grind .] private lemma Proposition.equiv_parr₂ {a b b' : Proposition Atom} (h : b ≡ b') : From 91e8f596c454efd0a0c0c8af4fcfbc107c845eb0 Mon Sep 17 00:00:00 2001 From: Fabrizio Montesi Date: Thu, 5 Mar 2026 14:07:37 +0100 Subject: [PATCH 08/19] some cases of congruence for logical equivalence in CLL --- Cslib/Logics/LinearLogic/CLL/Basic.lean | 158 ++++++++++++++++++++++-- 1 file changed, 148 insertions(+), 10 deletions(-) diff --git a/Cslib/Logics/LinearLogic/CLL/Basic.lean b/Cslib/Logics/LinearLogic/CLL/Basic.lean index c633a6469..caf7e5ec0 100644 --- a/Cslib/Logics/LinearLogic/CLL/Basic.lean +++ b/Cslib/Logics/LinearLogic/CLL/Basic.lean @@ -458,43 +458,181 @@ private lemma Proposition.equiv_parr₁ {a a' b : Proposition Atom} (h : a ≡ a case left => constructor simp only [Proposition.dual] + rw [show {a⫠ ⊗ b⫠, a' ⅋ b} = (a' ⅋ b) ::ₘ {a⫠ ⊗ b⫠} by grind] apply Proof.parr - rw [show (a⫠ ::ₘ b⫠ ::ₘ {a ⊗ b'}) = ((a ⊗ b') ::ₘ ({a⫠} + {b⫠})) by grind] + rw [show (a' ::ₘ b ::ₘ {a⫠ ⊗ b⫠}) = ((a⫠ ⊗ b⫠) ::ₘ ({a'} + {b})) by grind] apply Proof.tensor - · exact Proof.ax · apply h₁.rwConclusion (by grind) + · exact Proof.ax' case right => constructor simp only [Proposition.dual] + rw [show {a'⫠ ⊗ b⫠, a ⅋ b} = (a ⅋ b) ::ₘ {a'⫠ ⊗ b⫠} by grind] apply Proof.parr - rw [show (a⫠ ::ₘ b'⫠ ::ₘ {a ⊗ b}) = ((a ⊗ b) ::ₘ ({a⫠} + {b'⫠})) by grind] + rw [show (a ::ₘ b ::ₘ {a'⫠ ⊗ b⫠}) = ((a'⫠ ⊗ b⫠) ::ₘ ({a} + {b})) by grind] apply Proof.tensor - · exact Proof.ax · apply h₂.rwConclusion (by grind) + · exact Proof.ax' @[local grind .] private lemma Proposition.equiv_parr₂ {a b b' : Proposition Atom} (h : b ≡ b') : - a ⅋ b ≡ a ⅋ b' := by sorry + a ⅋ b ≡ a ⅋ b' := by + obtain ⟨h₁, h₂⟩ := h + obtain h₁ := h₁.some + obtain h₂ := h₂.some + constructor + case left => + constructor + simp only [Proposition.dual] + rw [show {a⫠ ⊗ b⫠, a ⅋ b'} = (a ⅋ b') ::ₘ {a⫠ ⊗ b⫠} by grind] + apply Proof.parr + rw [show (a ::ₘ b' ::ₘ {a⫠ ⊗ b⫠}) = ((a⫠ ⊗ b⫠) ::ₘ ({a} + {b'})) by grind] + apply Proof.tensor + · exact Proof.ax' + · apply h₁.rwConclusion (by grind) + case right => + constructor + simp only [Proposition.dual] + rw [show {a⫠ ⊗ b'⫠, a ⅋ b} = (a ⅋ b) ::ₘ {a⫠ ⊗ b'⫠} by grind] + apply Proof.parr + rw [show (a ::ₘ b ::ₘ {a⫠ ⊗ b'⫠}) = ((a⫠ ⊗ b'⫠) ::ₘ ({a} + {b})) by grind] + apply Proof.tensor + · exact Proof.ax' + · apply h₂.rwConclusion (by grind) @[local grind .] private lemma Proposition.equiv_oplus₁ {a a' b : Proposition Atom} (h : a ≡ a') : - a ⊕ b ≡ a' ⊕ b := by sorry + a ⊕ b ≡ a' ⊕ b := by + obtain ⟨h₁, h₂⟩ := h + obtain h₁ := h₁.some + obtain h₂ := h₂.some + constructor + case left => + constructor + simp only [Proposition.dual] + apply Proof.with + · rw [show a⫠ ::ₘ {a' ⊕ b} = (a' ⊕ b) ::ₘ {a⫠} by grind] + apply Proof.oplus₁ + apply h₁.rwConclusion (by grind) + · rw [show b⫠ ::ₘ {a' ⊕ b} = (a' ⊕ b) ::ₘ {b⫠} by grind] + apply Proof.oplus₂ + exact Proof.ax + case right => + constructor + simp only [Proposition.dual] + apply Proof.with + · rw [show a'⫠ ::ₘ {a ⊕ b} = (a ⊕ b) ::ₘ {a'⫠} by grind] + apply Proof.oplus₁ + apply h₂.rwConclusion (by grind) + · rw [show b⫠ ::ₘ {a ⊕ b} = (a ⊕ b) ::ₘ {b⫠} by grind] + apply Proof.oplus₂ + exact Proof.ax @[local grind .] private lemma Proposition.equiv_oplus₂ {a b b' : Proposition Atom} (h : b ≡ b') : - a ⊕ b ≡ a ⊕ b' := by sorry + a ⊕ b ≡ a ⊕ b' := by + obtain ⟨h₁, h₂⟩ := h + obtain h₁ := h₁.some + obtain h₂ := h₂.some + constructor + case left => + constructor + simp only [Proposition.dual] + apply Proof.with + · rw [show a⫠ ::ₘ {a ⊕ b'} = (a ⊕ b') ::ₘ {a⫠} by grind] + apply Proof.oplus₁ + exact Proof.ax + · rw [show b⫠ ::ₘ {a ⊕ b'} = (a ⊕ b') ::ₘ {b⫠} by grind] + apply Proof.oplus₂ + apply h₁.rwConclusion (by grind) + case right => + constructor + simp only [Proposition.dual] + apply Proof.with + · rw [show a⫠ ::ₘ {a ⊕ b} = (a ⊕ b) ::ₘ {a⫠} by grind] + apply Proof.oplus₁ + exact Proof.ax + · rw [show b'⫠ ::ₘ {a ⊕ b} = (a ⊕ b) ::ₘ {b'⫠} by grind] + apply Proof.oplus₂ + apply h₂.rwConclusion (by grind) @[local grind .] private lemma Proposition.equiv_with₁ {a a' b : Proposition Atom} (h : a ≡ a') : - a & b ≡ a' & b := by sorry + a & b ≡ a' & b := by + obtain ⟨h₁, h₂⟩ := h + obtain h₁ := h₁.some + obtain h₂ := h₂.some + constructor + case left => + constructor + simp only [Proposition.dual] + rw [show {a⫠ ⊕ b⫠, a' & b} = (a' & b) ::ₘ {a⫠ ⊕ b⫠} by grind] + apply Proof.with + · rw [show a' ::ₘ {a⫠ ⊕ b⫠} = (a⫠ ⊕ b⫠) ::ₘ {a'} by grind] + apply Proof.oplus₁ + apply h₁.rwConclusion (by grind) + · rw [show b ::ₘ {a⫠ ⊕ b⫠} = (a⫠ ⊕ b⫠) ::ₘ {b} by grind] + apply Proof.oplus₂ + exact Proof.ax' + case right => + constructor + simp only [Proposition.dual] + rw [show {a'⫠ ⊕ b⫠, a & b} = (a & b) ::ₘ {a'⫠ ⊕ b⫠} by grind] + apply Proof.with + · rw [show a ::ₘ {a'⫠ ⊕ b⫠} = (a'⫠ ⊕ b⫠) ::ₘ {a} by grind] + apply Proof.oplus₁ + apply h₂.rwConclusion (by grind) + · rw [show b ::ₘ {a'⫠ ⊕ b⫠} = (a'⫠ ⊕ b⫠) ::ₘ {b} by grind] + apply Proof.oplus₂ + exact Proof.ax' @[local grind .] private lemma Proposition.equiv_with₂ {a b b' : Proposition Atom} (h : b ≡ b') : - a & b ≡ a & b' := by sorry + a & b ≡ a & b' := by + obtain ⟨h₁, h₂⟩ := h + obtain h₁ := h₁.some + obtain h₂ := h₂.some + constructor + case left => + constructor + simp only [Proposition.dual] + rw [show {a⫠ ⊕ b⫠, a & b'} = (a & b') ::ₘ {a⫠ ⊕ b⫠} by grind] + apply Proof.with + · rw [show a ::ₘ {a⫠ ⊕ b⫠} = (a⫠ ⊕ b⫠) ::ₘ {a} by grind] + apply Proof.oplus₁ + exact Proof.ax' + · rw [show b' ::ₘ {a⫠ ⊕ b⫠} = (a⫠ ⊕ b⫠) ::ₘ {b'} by grind] + apply Proof.oplus₂ + apply h₁.rwConclusion (by grind) + case right => + constructor + simp only [Proposition.dual] + rw [show {a⫠ ⊕ b'⫠, a & b} = (a & b) ::ₘ {a⫠ ⊕ b'⫠} by grind] + apply Proof.with + · rw [show a ::ₘ {a⫠ ⊕ b'⫠} = (a⫠ ⊕ b'⫠) ::ₘ {a} by grind] + apply Proof.oplus₁ + exact Proof.ax' + · rw [show b ::ₘ {a⫠ ⊕ b'⫠} = (a⫠ ⊕ b'⫠) ::ₘ {b} by grind] + apply Proof.oplus₂ + apply h₂.rwConclusion (by grind) @[local grind .] private lemma Proposition.equiv_bang {a a' : Proposition Atom} (h : a ≡ a') : - !a ≡ !a' := by sorry + !a ≡ !a' := by + obtain ⟨h₁, h₂⟩ := h + obtain h₁ := h₁.some + obtain h₂ := h₂.some + constructor + case left => + constructor + simp only [Proposition.dual] + rw [show {ʔa⫠, !a'} = (!a') ::ₘ {ʔa⫠} by grind] + apply Proof.bang + · simp [allQuest, Multiset.fold] + · rw [show a' ::ₘ {ʔa⫠} = ʔa⫠ ::ₘ {a'} by grind] + apply Proof.quest + apply h₁.rwConclusion (by grind) + case right => sorry @[local grind .] private lemma Proposition.equiv_quest {a a' : Proposition Atom} (h : a ≡ a') : From 869e9104c21bb81b41e3f9c419a6ea3e00ccabac Mon Sep 17 00:00:00 2001 From: Fabrizio Montesi Date: Thu, 5 Mar 2026 14:43:37 +0100 Subject: [PATCH 09/19] done with congruence cases for logical equivalence in CLL --- Cslib/Languages/CCS/Basic.lean | 3 +-- Cslib/Logics/LinearLogic/CLL/Basic.lean | 32 +++++++++++++++++++++++-- 2 files changed, 31 insertions(+), 4 deletions(-) diff --git a/Cslib/Languages/CCS/Basic.lean b/Cslib/Languages/CCS/Basic.lean index 17dce26f5..b6299cb4d 100644 --- a/Cslib/Languages/CCS/Basic.lean +++ b/Cslib/Languages/CCS/Basic.lean @@ -119,8 +119,7 @@ def Context.fill (c : Context Name Constant) (p : Process Name Constant) : Proce | choiceR r c => Process.choice r (c.fill p) | res a c => Process.res a (c.fill p) -instance : IsContext (Context Name Constant) (Process Name Constant) (Process Name Constant) := - ⟨Context.fill⟩ +instance : HasContext (Process Name Constant) := ⟨Context Name Constant, Context.fill⟩ /-- Definition of context filling. -/ @[scoped grind =] diff --git a/Cslib/Logics/LinearLogic/CLL/Basic.lean b/Cslib/Logics/LinearLogic/CLL/Basic.lean index caf7e5ec0..14def9834 100644 --- a/Cslib/Logics/LinearLogic/CLL/Basic.lean +++ b/Cslib/Logics/LinearLogic/CLL/Basic.lean @@ -632,11 +632,39 @@ private lemma Proposition.equiv_bang {a a' : Proposition Atom} (h : a ≡ a') : · rw [show a' ::ₘ {ʔa⫠} = ʔa⫠ ::ₘ {a'} by grind] apply Proof.quest apply h₁.rwConclusion (by grind) - case right => sorry + case right => + constructor + simp only [Proposition.dual] + rw [show {ʔa'⫠, !a} = (!a) ::ₘ {ʔa'⫠} by grind] + apply Proof.bang + · simp [allQuest, Multiset.fold] + · rw [show a ::ₘ {ʔa'⫠} = ʔa'⫠ ::ₘ {a} by grind] + apply Proof.quest + apply h₂.rwConclusion (by grind) @[local grind .] private lemma Proposition.equiv_quest {a a' : Proposition Atom} (h : a ≡ a') : - ʔa ≡ ʔa' := by sorry + ʔa ≡ ʔa' := by + obtain ⟨h₁, h₂⟩ := h + obtain h₁ := h₁.some + obtain h₂ := h₂.some + constructor + case left => + constructor + simp only [Proposition.dual] + apply Proof.bang + · simp [allQuest, Multiset.fold] + · rw [show a⫠ ::ₘ {ʔa'} = ʔa' ::ₘ {a⫠} by grind] + apply Proof.quest + apply h₁.rwConclusion (by grind) + case right => + constructor + simp only [Proposition.dual] + apply Proof.bang + · simp [allQuest, Multiset.fold] + · rw [show a'⫠ ::ₘ {ʔa} = ʔa ::ₘ {a'⫠} by grind] + apply Proof.quest + apply h₂.rwConclusion (by grind) instance : Congruence (Proposition Atom) Proposition.Equiv where elim : From 44d95ae945cac429a1b5299ee127ca465b835a58 Mon Sep 17 00:00:00 2001 From: Fabrizio Montesi Date: Thu, 5 Mar 2026 15:11:30 +0100 Subject: [PATCH 10/19] fix: type hint --- Cslib/Languages/CCS/Basic.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/Cslib/Languages/CCS/Basic.lean b/Cslib/Languages/CCS/Basic.lean index b6299cb4d..54fe7181a 100644 --- a/Cslib/Languages/CCS/Basic.lean +++ b/Cslib/Languages/CCS/Basic.lean @@ -129,8 +129,8 @@ theorem context_fill_def (c : Context Name Constant) (p : Process Name Constant) /-- Any `Process` can be obtained by filling a `Context` with an atom. This proves that `Context` is a complete formalisation of syntactic contexts for CCS. -/ theorem Context.complete (p : Process Name Constant) : - ∃ c : Context Name Constant, p = c<[Process.nil] ∨ - ∃ k : Constant, p = c<[Process.const k] := by + ∃ c : Context Name Constant, p = c<[(Process.nil : Process Name Constant)] ∨ + ∃ k : Constant, p = c<[(Process.const k : Process Name Constant)] := by induction p case nil => exists hole From d5d4d163eff3391475466d7be16750a84ec20c80 Mon Sep 17 00:00:00 2001 From: Fabrizio Montesi Date: Thu, 5 Mar 2026 15:17:18 +0100 Subject: [PATCH 11/19] remove unnecessary unit --- Cslib/Logics/LinearLogic/CLL/Basic.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/Cslib/Logics/LinearLogic/CLL/Basic.lean b/Cslib/Logics/LinearLogic/CLL/Basic.lean index 14def9834..a429d112f 100644 --- a/Cslib/Logics/LinearLogic/CLL/Basic.lean +++ b/Cslib/Logics/LinearLogic/CLL/Basic.lean @@ -194,10 +194,10 @@ def Sequent.allQuest (Γ : Sequent Atom) := |> Multiset.fold Bool.and true /-- Judgemental contexts for CLL. -/ -def Sequent.Context Atom := Multiset (Proposition Atom) × Unit +def Sequent.Context Atom := Sequent Atom /-- Filling a judgemental context returns a sequent. -/ -def Sequent.Context.fill (Γc : Sequent.Context Atom) (a : Proposition Atom) := a ::ₘ Γc.1 +def Sequent.Context.fill (Γc : Sequent.Context Atom) (a : Proposition Atom) := a ::ₘ Γc instance : HasHContext (Sequent Atom) (Proposition Atom) := ⟨Sequent.Context Atom, Sequent.Context.fill⟩ From cc75b32e69b94c3a45dcd223feca7710eeea3918 Mon Sep 17 00:00:00 2001 From: Fabrizio Montesi Date: Thu, 5 Mar 2026 15:31:01 +0100 Subject: [PATCH 12/19] separate characterisation theorem for logical equivalence in HML --- Cslib/Logics/HML/LogicalEquivalence.lean | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) diff --git a/Cslib/Logics/HML/LogicalEquivalence.lean b/Cslib/Logics/HML/LogicalEquivalence.lean index 17db3a313..708889d33 100644 --- a/Cslib/Logics/HML/LogicalEquivalence.lean +++ b/Cslib/Logics/HML/LogicalEquivalence.lean @@ -19,10 +19,14 @@ This module defines logical equivalence for HML propositions and instantiates `L namespace Cslib.Logic.HML /-- Logical equivalence for HML propositions. -/ -@[scoped grind =] def Proposition.Equiv {State : Type u} {Label : Type v} (a b : Proposition Label) : Prop := ∀ lts : LTS State Label, a.denotation lts = b.denotation lts +@[scoped grind =] +theorem Proposition.equiv_def {State : Type u} {Label : Type v} (a b : Proposition Label) : + Equiv (State := State) a b ↔ + (∀ lts : LTS State Label, a.denotation lts = b.denotation lts) := by rfl + /-- Propositional contexts. -/ inductive Proposition.Context (Label : Type u) : Type u where | hole From 7ee600c7f5258a5ff368ce9d35500345ef2f97ba Mon Sep 17 00:00:00 2001 From: Fabrizio Montesi Date: Thu, 5 Mar 2026 15:37:19 +0100 Subject: [PATCH 13/19] fix errors --- Cslib/Foundations/Logic/InferenceSystem.lean | 2 ++ CslibTests/CLL.lean | 2 ++ 2 files changed, 4 insertions(+) diff --git a/Cslib/Foundations/Logic/InferenceSystem.lean b/Cslib/Foundations/Logic/InferenceSystem.lean index ef10f8358..0f244c311 100644 --- a/Cslib/Foundations/Logic/InferenceSystem.lean +++ b/Cslib/Foundations/Logic/InferenceSystem.lean @@ -6,6 +6,8 @@ Authors: Fabrizio Montesi module +public import Cslib.Init + @[expose] public section namespace Cslib.Logic diff --git a/CslibTests/CLL.lean b/CslibTests/CLL.lean index 4864a9299..a4d81a42f 100644 --- a/CslibTests/CLL.lean +++ b/CslibTests/CLL.lean @@ -71,6 +71,8 @@ example : (a⫠ = b⫠) ↔ (a = b) := Proposition.dual_inj a b /-! ## Basic proof tests -/ +open scoped Cslib.Logic.InferenceSystem + -- Axiom: ⊢ a, a⫠ example : ⇓({a, a⫠} : Sequent Nat) := Proof.ax example : ⇓({a⫠, a} : Sequent Nat) := Proof.ax' From e882e710ad5c938cbaeb9315ee2bd779bc4a1eef Mon Sep 17 00:00:00 2001 From: Fabrizio Montesi Date: Thu, 5 Mar 2026 15:38:40 +0100 Subject: [PATCH 14/19] line lengths --- Cslib/Foundations/Logic/InferenceSystem.lean | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) diff --git a/Cslib/Foundations/Logic/InferenceSystem.lean b/Cslib/Foundations/Logic/InferenceSystem.lean index 0f244c311..8f42df51a 100644 --- a/Cslib/Foundations/Logic/InferenceSystem.lean +++ b/Cslib/Foundations/Logic/InferenceSystem.lean @@ -40,9 +40,11 @@ def Derivable.fromDerivation [InferenceSystem α] {a : α} (d : ⇓a) : Derivabl instance [InferenceSystem α] {a : α} : Coe (⇓a) (Derivable a) := ⟨Derivable.fromDerivation⟩ /-- Extracts (noncomputably) a derivation from the fact that a conclusion is derivable. -/ -noncomputable def Derivable.toDerivation [InferenceSystem α] {a : α} (d : Derivable a) : ⇓a := Classical.choice d +noncomputable def Derivable.toDerivation [InferenceSystem α] {a : α} (d : Derivable a) : ⇓a := + Classical.choice d -noncomputable instance [InferenceSystem α] {a : α} : Coe (Derivable a) (⇓a) := ⟨Derivable.toDerivation⟩ +noncomputable instance [InferenceSystem α] {a : α} : Coe (Derivable a) (⇓a) := + ⟨Derivable.toDerivation⟩ end InferenceSystem From b51c654f538b1addfdaeb1d2c81cf72d74b337c5 Mon Sep 17 00:00:00 2001 From: Chris Henson Date: Thu, 5 Mar 2026 10:31:52 -0500 Subject: [PATCH 15/19] abbrev for HasContext --- Cslib/Foundations/Syntax/Context.lean | 9 ++------- 1 file changed, 2 insertions(+), 7 deletions(-) diff --git a/Cslib/Foundations/Syntax/Context.lean b/Cslib/Foundations/Syntax/Context.lean index 5316fd8d4..475ca53d1 100644 --- a/Cslib/Foundations/Syntax/Context.lean +++ b/Cslib/Foundations/Syntax/Context.lean @@ -23,12 +23,7 @@ class HasHContext (α β : Type*) where /-- Class for types (`α`) that have a canonical notion of homogeneous single-hole contexts (`Context`). -/ -class HasContext (α : Type*) where - /-- The type of contexts. -/ - Context : Type* - /-- Replaces the hole in the context with a term. -/ - fill (c : Context) (a : α) : α - -instance [inst : HasContext α] : HasHContext α α := ⟨inst.Context, inst.fill⟩ +abbrev HasContext (α : Type*) := HasHContext α α +def HasContext.Context (α : Type*) [HasContext α] : Type* := HasHContext.Context α α end Cslib From 874396a40a899aac38466ec06bbc10cdbe1394dc Mon Sep 17 00:00:00 2001 From: Chris Henson Date: Thu, 5 Mar 2026 10:49:32 -0500 Subject: [PATCH 16/19] forgot docstring --- Cslib/Foundations/Syntax/Context.lean | 2 ++ 1 file changed, 2 insertions(+) diff --git a/Cslib/Foundations/Syntax/Context.lean b/Cslib/Foundations/Syntax/Context.lean index 475ca53d1..bff8f952f 100644 --- a/Cslib/Foundations/Syntax/Context.lean +++ b/Cslib/Foundations/Syntax/Context.lean @@ -24,6 +24,8 @@ class HasHContext (α β : Type*) where /-- Class for types (`α`) that have a canonical notion of homogeneous single-hole contexts (`Context`). -/ abbrev HasContext (α : Type*) := HasHContext α α + +@[inherit_doc HasHContext.Context] def HasContext.Context (α : Type*) [HasContext α] : Type* := HasHContext.Context α α end Cslib From 8b2ae244dafbb4d8b16016b71352edfaaeaf4397 Mon Sep 17 00:00:00 2001 From: Fabrizio Montesi Date: Thu, 5 Mar 2026 17:01:18 +0100 Subject: [PATCH 17/19] def should be a theorem --- Cslib/Foundations/Logic/InferenceSystem.lean | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/Cslib/Foundations/Logic/InferenceSystem.lean b/Cslib/Foundations/Logic/InferenceSystem.lean index 8f42df51a..3a9eda6f1 100644 --- a/Cslib/Foundations/Logic/InferenceSystem.lean +++ b/Cslib/Foundations/Logic/InferenceSystem.lean @@ -35,7 +35,8 @@ def rwConclusion [InferenceSystem α] {Γ Δ : α} (h : Γ = Δ) (p : ⇓Γ) : def Derivable [InferenceSystem α] (a : α) := Nonempty (⇓a) /-- Shows derivability from a derivation. -/ -def Derivable.fromDerivation [InferenceSystem α] {a : α} (d : ⇓a) : Derivable a := Nonempty.intro d +theorem Derivable.fromDerivation [InferenceSystem α] {a : α} (d : ⇓a) : Derivable a := + Nonempty.intro d instance [InferenceSystem α] {a : α} : Coe (⇓a) (Derivable a) := ⟨Derivable.fromDerivation⟩ From 0c959a57b5d76cf4896bd5afe388de0ed5c24592 Mon Sep 17 00:00:00 2001 From: Fabrizio Montesi Date: Thu, 5 Mar 2026 17:21:51 +0100 Subject: [PATCH 18/19] mk_all --- Cslib.lean | 3 +++ 1 file changed, 3 insertions(+) diff --git a/Cslib.lean b/Cslib.lean index a9d5ffc3e..fcb0b0a8b 100644 --- a/Cslib.lean +++ b/Cslib.lean @@ -54,6 +54,8 @@ public import Cslib.Foundations.Data.Relation public import Cslib.Foundations.Data.Set.Saturation public import Cslib.Foundations.Data.StackTape public import Cslib.Foundations.Lint.Basic +public import Cslib.Foundations.Logic.InferenceSystem +public import Cslib.Foundations.Logic.LogicalEquivalence public import Cslib.Foundations.Semantics.FLTS.Basic public import Cslib.Foundations.Semantics.FLTS.FLTSToLTS public import Cslib.Foundations.Semantics.FLTS.LTSToFLTS @@ -94,6 +96,7 @@ public import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.LcAt public import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.Properties public import Cslib.Languages.LambdaCalculus.Named.Untyped.Basic public import Cslib.Logics.HML.Basic +public import Cslib.Logics.HML.LogicalEquivalence public import Cslib.Logics.LinearLogic.CLL.Basic public import Cslib.Logics.LinearLogic.CLL.CutElimination public import Cslib.Logics.LinearLogic.CLL.EtaExpansion From 8e3d6da7b0392d4d0b9f8d8808f77f7586ae5bfb Mon Sep 17 00:00:00 2001 From: Fabrizio Montesi Date: Thu, 5 Mar 2026 18:40:37 +0100 Subject: [PATCH 19/19] docstrings --- Cslib/Logics/HML/LogicalEquivalence.lean | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/Cslib/Logics/HML/LogicalEquivalence.lean b/Cslib/Logics/HML/LogicalEquivalence.lean index 708889d33..a82181134 100644 --- a/Cslib/Logics/HML/LogicalEquivalence.lean +++ b/Cslib/Logics/HML/LogicalEquivalence.lean @@ -71,8 +71,11 @@ instance {State : Type u} {Label : Type v} : /-- Bundled version of a judgement for `Satisfy`. -/ structure Satisfies.Judgement (State : Type u) (Label : Type v) where + /-- The state transition system to consider. -/ lts : LTS State Label + /-- The state to check the proposition against. -/ state : State + /-- The proposition to check. -/ φ : Proposition Label /-- `Satisfies` variant using bundled judgements. -/ @@ -83,7 +86,9 @@ theorem Satisfies.bundled_char : Satisfies.Bundled j ↔ Satisfies j.lts j.state /-- Judgemental contexts. -/ structure Satisfies.Context (State : Type u) (Label : Type v) where + /-- The state transition system to consider. -/ lts : LTS State Label + /-- The state to check propositions against. -/ state : State /-- Fills a judgemental context with a proposition. -/