From 81794993cae2c7b4cc7c7dfeb191b82b52252006 Mon Sep 17 00:00:00 2001 From: Malvin Gattinger Date: Wed, 1 Nov 2023 16:13:50 +0100 Subject: [PATCH] PDL Tableau with an idea how to represent repeats in inductive types --- Pdl.lean | 1 + Pdl/Measures.lean | 68 ++++++++++++++++++++++++++++ Pdl/Semantics.lean | 1 + Pdl/Syntax.lean | 55 +---------------------- Pdl/Tableau.lean | 110 ++++++++++++++++++++++++++++++++++++++------- 5 files changed, 164 insertions(+), 71 deletions(-) create mode 100644 Pdl/Measures.lean diff --git a/Pdl.lean b/Pdl.lean index 734efe2..a87ecdb 100644 --- a/Pdl.lean +++ b/Pdl.lean @@ -1,6 +1,7 @@ -- This module serves as the root of the `Pdl` library. -- Import modules here that should be built as part of the library. import «Pdl».Syntax +import «Pdl».Measures import «Pdl».Vocab import «Pdl».Semantics import «Pdl».Star diff --git a/Pdl/Measures.lean b/Pdl/Measures.lean new file mode 100644 index 0000000..6cea920 --- /dev/null +++ b/Pdl/Measures.lean @@ -0,0 +1,68 @@ +-- MEASURES + +import Mathlib.Algebra.BigOperators.Basic +import Mathlib.Data.Finset.Basic + +import Pdl.Syntax + +-- COMPLEXITY + +mutual + def lengthOfProgram : Program → Nat + | ·_ => 1 + | α;β => 1 + lengthOfProgram α + lengthOfProgram β + | α⋓β => 1 + lengthOfProgram α + lengthOfProgram β + | ∗α => 1 + lengthOfProgram α + | ✓φ => 1 + lengthOfFormula φ + def lengthOfFormula : Formula → Nat + | Formula.bottom => 1 + | ·_ => 1 + | ~φ => 1 + lengthOfFormula φ + | φ⋀ψ => 1 + lengthOfFormula φ + lengthOfFormula ψ + | ⌈α⌉φ => 1 + lengthOfProgram α + lengthOfFormula φ +end +termination_by -- silly but needed?! + lengthOfProgram p => sizeOf p + lengthOfFormula f => sizeOf f + +-- mwah +@[simp] +def lengthOfEither : PSum Program Formula → Nat + | PSum.inl p => lengthOfProgram p + | PSum.inr f => lengthOfFormula f + +class HasLength (α : Type) where + lengthOf : α → ℕ + +open HasLength +@[simp] +instance formulaHasLength : HasLength Formula := ⟨lengthOfFormula⟩ +@[simp] +instance setFormulaHasLength : HasLength (Finset Formula) := ⟨fun X => X.sum lengthOfFormula⟩ + +-- MEASURE +mutual + @[simp] + def mOfProgram : Program → Nat + | ·_ => 0 + | ✓ φ => 1 + mOfFormula φ + | α;β => 1 + mOfProgram α + mOfProgram β + 1 -- TODO: max (mOfFormula φ) (mOfFormula (~φ)) + | α⋓β => 1 + mOfProgram α + mOfProgram β + 1 + | ∗α => 1 + mOfProgram α + @[simp] + def mOfFormula : Formula → Nat + | ⊥ => 0 + | ~⊥ => 0 + |-- missing in borze? + ·_ => + 0 + | ~·_ => 0 + | ~~φ => 1 + mOfFormula φ + | φ⋀ψ => 1 + mOfFormula φ + mOfFormula ψ + | ~φ⋀ψ => 1 + mOfFormula (~φ) + mOfFormula (~ψ) + | ⌈α⌉ φ => mOfProgram α + mOfFormula φ + | ~⌈α⌉ φ => mOfProgram α + mOfFormula (~φ) +end +termination_by -- silly but needed?! + mOfProgram p => sizeOf p + mOfFormula f => sizeOf f diff --git a/Pdl/Semantics.lean b/Pdl/Semantics.lean index 96f75e7..92024cc 100644 --- a/Pdl/Semantics.lean +++ b/Pdl/Semantics.lean @@ -5,6 +5,7 @@ import Mathlib.Order.CompleteLattice import Mathlib.Order.FixedPoints import Pdl.Syntax +import Pdl.Measures -- Kripke Models aka Labelled Transition Systems structure KripkeModel (W : Type) : Type where diff --git a/Pdl/Syntax.lean b/Pdl/Syntax.lean index 0f2dbdb..988ee82 100644 --- a/Pdl/Syntax.lean +++ b/Pdl/Syntax.lean @@ -14,7 +14,7 @@ mutual | union : Program → Program → Program | star : Program → Program | test : Formula → Program - deriving Repr, DecidableEq -- is not derivable here? + deriving Repr, DecidableEq end -- Notation and abbreviations @@ -53,59 +53,6 @@ infixl:33 "⋓" => Program.union prefix:33 "∗" => Program.star prefix:33 "✓" => Program.test -- avoiding "?" which has a meaning in Lean 4 - --- COMPLEXITY -mutual - def lengthOfProgram : Program → Nat - | ·_ => 1 - | α;β => 1 + lengthOfProgram α + lengthOfProgram β - | α⋓β => 1 + lengthOfProgram α + lengthOfProgram β - | ∗α => 1 + lengthOfProgram α - | ✓φ => 1 + lengthOfFormula φ - def lengthOfFormula : Formula → Nat - | Formula.bottom => 1 - | ·_ => 1 - | ~φ => 1 + lengthOfFormula φ - | φ⋀ψ => 1 + lengthOfFormula φ + lengthOfFormula ψ - | ⌈α⌉φ => 1 + lengthOfProgram α + lengthOfFormula φ -end -termination_by -- silly but needed?! - lengthOfProgram p => sizeOf p - lengthOfFormula f => sizeOf f - --- mwah -@[simp] -def lengthOfEither : PSum Program Formula → Nat - | PSum.inl p => lengthOfProgram p - | PSum.inr f => lengthOfFormula f - --- MEASURE -mutual - @[simp] - def mOfProgram : Program → Nat - | ·_ => 0 - | ✓ φ => 1 + mOfFormula φ - | α;β => 1 + mOfProgram α + mOfProgram β + 1 -- TODO: max (mOfFormula φ) (mOfFormula (~φ)) - | α⋓β => 1 + mOfProgram α + mOfProgram β + 1 - | ∗α => 1 + mOfProgram α - @[simp] - def mOfFormula : Formula → Nat - | ⊥ => 0 - | ~⊥ => 0 - |-- missing in borze? - ·_ => - 0 - | ~·_ => 0 - | ~~φ => 1 + mOfFormula φ - | φ⋀ψ => 1 + mOfFormula φ + mOfFormula ψ - | ~φ⋀ψ => 1 + mOfFormula (~φ) + mOfFormula (~ψ) - | ⌈α⌉ φ => mOfProgram α + mOfFormula φ - | ~⌈α⌉ φ => mOfProgram α + mOfFormula (~φ) -end -termination_by -- silly but needed?! - mOfProgram p => sizeOf p - mOfFormula f => sizeOf f - theorem boxes_last : (~⌈a⌉Formula.boxes (as ++ [c]) P) = (~⌈a⌉Formula.boxes as (⌈c⌉P)) := by induction as diff --git a/Pdl/Tableau.lean b/Pdl/Tableau.lean index 01608b1..d90e51a 100644 --- a/Pdl/Tableau.lean +++ b/Pdl/Tableau.lean @@ -1,21 +1,26 @@ +-- TABLEAU + +import Mathlib.Data.Finset.Basic +import Mathlib.Data.Finset.Option + import Pdl.Syntax +import Pdl.Measures import Pdl.Semantics import Pdl.Discon import Pdl.Unravel --- NOTE: Much here should be replaced with extended versions of --- https://github.com/m4lvin/tablean/blob/main/src/tableau.lean --- but maybe we should mathport that project to Lean 4 first? - --- LOCAL TABLEAU - --- TODO: Can we use variables below without making them arguments of localRule? --- variable (X : Finset Formula) (f g : Formula) (a b : Program) +-- HELPER FUNCTIONS @[simp] def listsToSets : List (List Formula) → Finset (Finset Formula) | LS => (LS.map List.toFinset).toFinset +-- LOCAL TABLEAU + +-- Definition 9, page 15 +-- A set X is closed iff 0 ∈ X or X contains a formula and its negation. +def Closed : Finset Formula → Prop := fun X => ⊥ ∈ X ∨ ∃ f ∈ X, (~f) ∈ X + -- Local rules: given this set, we get these sets as child nodes inductive localRule : Finset Formula → Finset (Finset Formula) → Type -- PROP LOGIC @@ -314,19 +319,90 @@ lemma localRuleTruth {W} {M : KripkeModel W} {w : W} {X B} : -- split TODO sorry +-- A set X is simple iff all P ∈ X are (negated) atoms or [A]_ or ¬[A]_. +@[simp] +def SimpleForm : Formula → Bool + | ⊥ => True + | ~⊥ => True + | ·_ => True + | ~·_ => True + | ⌈·_⌉_ => True + | ~⌈·_⌉_ => True + | _ => False --- TODO inductive LocalTableau +def Simple : Finset Formula → Bool + | X => ∀ P ∈ X, SimpleForm P +-- Definition 8, page 14 +-- mixed with Definition 11 (with all PDL stuff missing for now) +-- a local tableau for X, must be maximal +inductive LocalTableau : Finset Formula → Type + | byLocalRule {X B} (_ : localRule X B) (next : ∀ Y ∈ B, LocalTableau Y) : LocalTableau X + | sim {X} : Simple X → LocalTableau X --- TABLEAUX +open LocalTableau + +open HasLength + +-- needed for endNodesOf +instance localTableauHasSizeof : SizeOf (Σ X, LocalTableau X) := + ⟨fun ⟨X, _⟩ => lengthOf X⟩ + +-- open end nodes of a given localTableau +@[simp] +def endNodesOf : (Σ X, LocalTableau X) → Finset (Finset Formula) + | ⟨X, @byLocalRule _ B lr next⟩ => + B.attach.biUnion fun ⟨Y, h⟩ => + have : lengthOf Y < lengthOf X := sorry -- localRulesDecreaseLength lr Y h + endNodesOf ⟨Y, next Y h⟩ + | ⟨X, sim _⟩ => {X} -inductive Tableau -- to be rewritten as in tablean? - | leaf : Set Formula → Tableau - | Rule : Rule → List (Set Formula) → Tableau +-- PROJECTIONS -def projection : Char → Formula → Option Formula - | a, ⌈·b⌉ f => if a = b then some f else none +@[simp] +def formProjection : Char → Formula → Option Formula + | A, ⌈·B⌉φ => if A == B then some φ else none | _, _ => none --- TODO inductive globalRule : ... --- | nSt {a f} (h : (~⌈·a⌉f) ∈ X) : localRule X { X \ {~⌈·a⌉f} ∪ {~f} } -- TODO projection!! +def projection : Char → Finset Formula → Finset Formula + | A, X => X.biUnion fun x => (formProjection A x).toFinset + +@[simp] +theorem proj : g ∈ projection A X ↔ (⌈·A⌉g) ∈ X := + by + rw [projection] + simp + constructor + · intro lhs + rcases lhs with ⟨boxg, boxg_in_X, projboxg_is_g⟩ + cases boxg + repeat' aesop + · intro rhs + use ⌈·A⌉g + simp + exact rhs + +theorem projSet : projection A X = {ϕ | (⌈·A⌉ϕ) ∈ X} := + by + ext1 + simp + +-- TABLEAUX + +-- Definition 16, page 29 +-- TODO: do we want a ClosedTableau or more general Tableau type? +-- If more general, do we want an "open" constructor with(out) arguments/proofs? +inductive ClosedTableau : List (Finset Formula) → Finset Formula → Type + | loc {X} (lt : LocalTableau X) : (∀ Y ∈ endNodesOf ⟨X, lt⟩, ClosedTableau Hist Y) → ClosedTableau Hist X + | atm {A X ϕ} : (~⌈·A⌉ϕ) ∈ X → Simple X → ClosedTableau (X :: Hist) (projection A X ∪ {~ϕ}) → ClosedTableau Hist X + | repeat {X} : X ∈ Hist → ClosedTableau Hist X + +inductive Provable : Formula → Prop + | byTableau {φ : Formula} : ClosedTableau _ {~φ} → Provable φ + +-- Definition 17, page 30 +def Inconsistent : Finset Formula → Prop + | X => Nonempty (ClosedTableau [] X) + +def Consistent : Finset Formula → Prop + | X => ¬Inconsistent X