From 37b160144261cecb301c60a6cb7ae7b98e932638 Mon Sep 17 00:00:00 2001 From: Malvin Gattinger Date: Mon, 27 Nov 2023 21:15:53 +0100 Subject: [PATCH] first definitions for dagger tableau --- Pdl/DagTableau.lean | 241 ++++++++++++++++++++++++++++++++++++++++++++ Pdl/Syntax.lean | 1 + Pdl/Tableau.lean | 16 +-- 3 files changed, 252 insertions(+), 6 deletions(-) create mode 100644 Pdl/DagTableau.lean diff --git a/Pdl/DagTableau.lean b/Pdl/DagTableau.lean new file mode 100644 index 0000000..7e9978a --- /dev/null +++ b/Pdl/DagTableau.lean @@ -0,0 +1,241 @@ +import Mathlib.Data.Finset.Basic + +import Pdl.Syntax +import Pdl.Discon +import Pdl.Semantics +import Pdl.Star + +-- IDEA: adjust the type to forbid atomic program on (neg)top level? + +inductive DagFormula : Type + | bottom : DagFormula + | atom_prop : Char → DagFormula + | neg : DagFormula → DagFormula + | and : DagFormula → DagFormula → DagFormula + | box : Program → DagFormula → DagFormula + | dag : Program → DagFormula → DagFormula + deriving Repr + +def DagFormula.boxes : List Program → DagFormula → DagFormula + | [], f => f + | (p :: ps), f => DagFormula.box p (DagFormula.boxes ps f) + +/- +def decDagFormula (f g : DagFormula) : Decidable (f = g) := + match f,g with + | DagFormula.atom_prop A, DagFormula.atom_prop B => + dite (A = B) (fun h => isTrue (by rw [h])) (fun h => isFalse (by simp; exact h)) + | DagFormula.atom_prop _, _ => isFalse (by intro; contradiction) + +-- TODO: many many cases +-/ +instance : DecidableEq DagFormula := sorry -- decDagFormula? - or can a newer Lean version derive this? + + +local notation "·" c => DagFormula.atom_prop c +local prefix:11 "~" => DagFormula.neg + +local notation "⊥" => DagFormula.bottom +local infixr:66 "⋀" => DagFormula.and +local infixr:60 "⋁" => DagFormula.or + +local notation "⌈" α "⌉" P => DagFormula.box α P +local notation "⌈⌈" α "⌉⌉" P => DagFormula.boxes α P +local notation "⌈" α "†⌉" P => DagFormula.dag α P + +-- THE f FUNCTION +-- | Borzechowski's f function, sort of. + +def undag : DagFormula → Formula + | ⊥ => ⊥ + | ~f => ~(undag f) + | ·c => ·c + | φ⋀ψ => undag φ ⋀ undag ψ + | ⌈α⌉ φ => ⌈α⌉ (undag φ) + | ⌈α†⌉ φ => ⌈∗α⌉ (undag φ) + +-- instance : Coe Nat Int := ⟨Int.ofNat⟩ + +@[simp] +def inject : Formula → DagFormula + | ⊥ => ⊥ + | ~f => ~ inject f + | ·c => ·c + | φ⋀ψ => inject φ ⋀ inject ψ + | ⌈α⌉φ => ⌈α⌉(inject φ) + +-- | Borzechowski's f function, sort of. +@[simp] +def containsDag : DagFormula → Bool + | ⊥ => False + | ~f => containsDag f + | ·_ => False + | φ⋀ψ => containsDag φ ∧ containsDag ψ + | ⌈_⌉φ => containsDag φ + | ⌈_†⌉ _ => True + +@[simp] +lemma undag_inject {f} : undag (inject f) = f := + by + cases f + all_goals simp [undag] + case neg f => + rw [@undag_inject f] + case and f g => + rw [@undag_inject f] + rw [@undag_inject g] + exact ⟨rfl,rfl⟩ + case box a f => + apply undag_inject + +@[simp] +lemma inject_never_containsDag : ∀ f, containsDag (inject f) = false := + by + apply Formula.rec + case bottom => simp + case atom_prop => simp + case neg => + intro f + simp + case and => + intro g h + simp [containsDag] + tauto + case box => + intro a f + simp + -- The recursor introduces program cases which we do not care about. + case motive_2 => + intro _ + exact True + all_goals { simp } + +-- MEASURE +@[simp] +def mOfDagFormula : DagFormula → Nat + | ⊥ => 0 + | ~⊥ => 0 + | ·_ => 0 -- missing in borze? + | ~·_ => 0 + | ~~φ => 1 + mOfDagFormula φ + | φ⋀ψ => 1 + mOfDagFormula φ + mOfDagFormula ψ + | ~φ⋀ψ => 1 + mOfDagFormula (~φ) + mOfDagFormula (~ψ) + | ⌈α⌉ φ => mOfProgram α + mOfDagFormula φ + | ⌈_†⌉φ => mOfDagFormula φ + | ~⌈α⌉ φ => mOfProgram α + mOfDagFormula (~φ) + | ~⌈_†⌉φ => mOfDagFormula (~φ) + +-- Daggered Tableau + +structure DagTabNode where + fs : Finset Formula + dfs : Finset DagFormula -- for diamond this is actually a singleton? + deriving DecidableEq + +inductive dagRule : DagTabNode → Finset (DagTabNode) → Type + -- Diamond rules + | notUndag (h : ((~⌈·A⌉φ : DagFormula) ∈ X.dfs)) : + dagRule X { ⟨X.fs ∪ {undag (~⌈·A⌉φ)}, X.dfs \ {~⌈·A⌉φ}⟩ } + + | notUnion {α β φ} (h : ((~⌈α⋓β⌉φ : DagFormula) ∈ X.dfs)) : + dagRule X { ⟨X.fs, X.dfs \ {~⌈α ⋓ b⌉φ} ∪ {~⌈α⌉φ}⟩ + , ⟨X.fs, X.dfs \ {~⌈α ⋓ b⌉φ} ∪ {~⌈β⌉φ}⟩ } + + | notTest (h : ((⌈?'ψ⌉φ : DagFormula) ∈ X.dfs)) : + dagRule X { ⟨X.fs ∪ {ψ}, X.dfs \ {⌈?'ψ⌉φ} ∪ {φ}⟩ } + + | notSequence (h : ((~⌈α;'β⌉φ : DagFormula) ∈ X.dfs)) : + dagRule X { ⟨X.fs, X.dfs \ {~⌈α⌉⌈b⌉φ}⟩ } + + | notStar (h : ((~⌈∗α⌉φ : DagFormula) ∈ X.dfs)) : + dagRule X { ⟨X.fs, X.dfs \ {~⌈∗α⌉φ} ∪ {~⌈α⌉φ}⟩ + , ⟨X.fs, X.dfs \ {~⌈∗α⌉φ} ∪ {~⌈α⌉⌈α†⌉φ}⟩ } + + | notDag (h : ((~⌈α†⌉φ : DagFormula) ∈ X.dfs)) : + dagRule X { } -- ×, i.e. delete branch + + -- Box rules + | undag (h : ((⌈·A⌉φ : DagFormula) ∈ X.dfs)) : + dagRule X { ⟨X.fs ∪ {undag (⌈·A⌉φ)}, X.dfs \ {⌈·A⌉φ}⟩ } + + | union {α β φ} (h : ((⌈α⋓β⌉φ : DagFormula) ∈ X.dfs)) : + dagRule X { ⟨X.fs, X.dfs \ {⌈α ⋓ b⌉φ} ∪ {⌈α⌉φ, ⌈β⌉φ}⟩ } + + | test (h : ((⌈?'ψ⌉φ : DagFormula) ∈ X.dfs)) : + dagRule X { ⟨X.fs ∪ {~ψ}, X.dfs \ {⌈?'ψ⌉φ}⟩ + , ⟨X.fs, X.dfs \ {⌈?'ψ⌉φ} ∪ {φ}⟩ } + + | sequence (h : ((⌈α;'β⌉φ : DagFormula) ∈ X.dfs)) : + dagRule X { ⟨X.fs, X.dfs \ {⌈α⌉⌈b⌉φ}⟩ } + + | star (h : ((~⌈∗α⌉φ : DagFormula) ∈ X.dfs)) : + dagRule X { ⟨X.fs, X.dfs \ {~⌈∗α⌉φ} ∪ {~⌈α⌉φ}⟩ + , ⟨X.fs, X.dfs \ {~⌈∗α⌉φ} ∪ {~⌈α⌉⌈α†⌉φ}⟩ } + +inductive DagTab : DagTabNode → Type + | byRule {X B} (_ : dagRule X B) (next : ∀ Y ∈ B, DagTab Y) : DagTab X + | stop {X} (_ : X.dfs = ∅) : DagTab X + +def endNodesOf : DagTab X -> List (List Formula) := sorry -- TODO +-- (or have it -> List (DagTabNode) and prove that dfs will be empty? + +-- Given a proper dagger formula, define the *unique* DagTab for it? +-- More generally, given a DagTabNode, how to continue? +def theTabFor (N : DagTabNode) : DagTab N := sorry + +-- all weak successors of a node in a DagTab, i.e. itself, immediate and later successors. +def successors : (t : DagTab N) → Finset DagTabNode + | @DagTab.byRule X B (_ : dagRule X B) next => {N} ∪ B.attach.biUnion (fun ⟨Y, h⟩ => successors (next Y h)) + | DagTab.stop _ => {N} + +instance modelCanSemImplyDagTabNode {W : Type} : vDash (KripkeModel W × W) (DagTabNode) := + vDash.mk (λ ⟨M,w⟩ Δ => ∀ φ ∈ Δ.fs ∪ (Δ.dfs.image undag) , @evaluate W M w φ) + + +theorem notStarSoundness M (a : Program) (v w : W) (Δ : DagTabNode) + (φ : DagFormula) (in_D : (~⌈a⌉φ) ∈ Δ.dfs) (t : DagTab Δ) + -- TODO: containsDag φ -- needed? + (v_D : (M, v) ⊨ Δ) (v_a_w : relate M a v w) (w_nP : (M, w) ⊨ (~undag φ)) : + ∃ Γ ∈ successors t, + (M, v) ⊨ Γ ∧ ( ( ∃ (a : Char) (as : List Program), (~ ⌈·a⌉⌈⌈as⌉⌉(undag φ)) ∈ Γ.fs + ∧ relate M (Program.steps ([Program.atom_prog a] ++ as)) v w ) + ∨ ((~φ) ∈ Γ.dfs ∧ v = w) ) := by + cases a + case atom_prog A => + -- NOTE: do we really want Γ = Δ here, what about the step done by "undag" rule? + use Δ + constructor + · cases t + all_goals simp [successors] + · constructor + · assumption + · left + use A, [] + simp at * + constructor + · + -- TODO: by contradiction / do not allow A in dfs? + sorry + · exact v_a_w + + case sequence α β => + sorry + + case union α β => + -- NOTE: how to ensure that notUnion is "eventually" applied in t (: DagTab Δ)? + -- May need to redefine DagTab to make it fully deterministic. + -- That should work here, but probably not for boxes? + simp at v_a_w + cases v_a_w + · have := notStarSoundness M α v w ?_ φ + · sorry + sorry + · have := notStarSoundness M α v w ?_ φ + · sorry + sorry + + case star α => + sorry + + case test ψ => + sorry diff --git a/Pdl/Syntax.lean b/Pdl/Syntax.lean index 653a227..8ce333e 100644 --- a/Pdl/Syntax.lean +++ b/Pdl/Syntax.lean @@ -47,6 +47,7 @@ infixr:60 "⋁" => Formula.or notation:55 φ:56 " ↣ " ψ:55 => ~φ ⋀ (~ψ) notation:55 φ:56 " ⟷ " ψ:55 => (φ↣ψ) ⋀ (φ↣φ) notation "⌈" α "⌉" P => Formula.box α P +notation "⌈⌈" as "⌉⌉" P => Formula.boxes as P infixl:33 ";'" => Program.sequence -- avoiding plain ";" which has a meaning in Lean 4 infixl:33 "⋓" => Program.union diff --git a/Pdl/Tableau.lean b/Pdl/Tableau.lean index c1af972..9159cbb 100644 --- a/Pdl/Tableau.lean +++ b/Pdl/Tableau.lean @@ -200,7 +200,7 @@ lemma localRuleTruth {W} {M : KripkeModel W} {w : W} {X B} : -- STAR RULES case nSt a f naSf_in_X => constructor - · rintro ⟨Y, Y_in, MwY⟩ -- invertibility + · rintro ⟨Y, Y_in, MwY⟩ -- invertibility, should be easy simp at Y_in rcases Y_in with ⟨FS,FS_in,Y_def⟩ subst Y_def @@ -222,14 +222,14 @@ lemma localRuleTruth {W} {M : KripkeModel W} {w : W} {X B} : right exact List.mem_of_mem_head? rfl case inr FS_in_unrav => - simp [unravel] at FS_in_unrav + sorry case inr g_neq_nsSf => apply MwY simp left exact ⟨g_in_X, g_neq_nsSf⟩ - · intro Mw_X -- soundness + · intro Mw_X -- soundness, needs Lemma have w_adiamond_f := Mw_X (~⌈∗a⌉f) naSf_in_X simp at w_adiamond_f rcases w_adiamond_f with ⟨v, w_aS_v, v_nF⟩ @@ -275,7 +275,7 @@ lemma localRuleTruth {W} {M : KripkeModel W} {w : W} {X B} : · intro g g_in; simp at g_in; apply Mw_ZX; tauto case sta a f aSf_in_X => constructor - · rintro ⟨Y, Y_in, w_Y⟩ -- invertibility + · rintro ⟨Y, Y_in, w_Y⟩ -- invertibility, needs Lemma 4 3/4 simp at Y_in rcases Y_in with ⟨Z, Z_in_unrav, Y_def⟩ subst Y_def @@ -285,14 +285,18 @@ lemma localRuleTruth {W} {M : KripkeModel W} {w : W} {X B} : subst g_def simp intro v w_a_v + have := lemmaFourAndThreeQuarters M -- use here? sorry case inr g_not => apply w_Y simp tauto - · intro w_X -- soundness + · intro w_X -- soundness, should be easy + simp + specialize w_X (⌈∗a⌉f) aSf_in_X + simp at w_X simp - have := lemmaFourAndThreeQuarters M -- use here? + use (X \ {⌈∗a⌉f} ∪ (List.toFinset {f} ∪ List.toFinset a_1)) sorry -- OTHER PDL RULES