diff --git a/Pdl/Completeness.lean b/Pdl/Completeness.lean index 84b59dc..f075739 100644 --- a/Pdl/Completeness.lean +++ b/Pdl/Completeness.lean @@ -1,4 +1,4 @@ --- COMPLETENESS +-- Completeness (Section 7) import Pdl.Soundness import Pdl.TableauGame diff --git a/Pdl/Examples.lean b/Pdl/Examples.lean index 577fbba..25d7fc0 100644 --- a/Pdl/Examples.lean +++ b/Pdl/Examples.lean @@ -6,7 +6,6 @@ import Mathlib.Data.Vector.Snoc import Pdl.Semantics import Pdl.Star -import Pdl.UnfoldBox open HasSat @@ -192,17 +191,3 @@ theorem inductionAxiom (a : Program) (φ : Formula) : tautology ((φ ⋀ ⌈∗a · exact w_aS_u · exact IH · assumption - -/-! ### UnfoldBox example -/ - --- 1 = a --- 2 = b --- 0 = p -def myalpha : Program := ( (·1 : Program) ⋓ (?'(·0 : Formula)) ;' (∗(·2 : Program))) - -def myTP0 : TP myalpha := fun _ => False -def myTP1 : TP myalpha := fun _ => True - --- #eval P myalpha myTP0 -- [[a, b*]] - --- #eval P myalpha myTP1 -- [[a, ∗b], [], [b, ∗b]] diff --git a/Pdl/Interpolation.lean b/Pdl/Interpolation.lean index b7fd082..7d9e98e 100644 --- a/Pdl/Interpolation.lean +++ b/Pdl/Interpolation.lean @@ -1,3 +1,5 @@ +-- Interpolation (Section 8) + import Mathlib.Data.Finset.Basic import Pdl.PartInterpolation diff --git a/Pdl/Modelgraphs.lean b/Pdl/Modelgraphs.lean index a9db28b..64f6e0e 100644 --- a/Pdl/Modelgraphs.lean +++ b/Pdl/Modelgraphs.lean @@ -1,8 +1,8 @@ --- MODELGRAPHS +-- Saturated sets and model graphs (Section 7.1) + import Mathlib.Tactic.ClearExcept import Mathlib.Data.Vector.Basic -import Pdl.Semantics import Pdl.UnfoldBox import Pdl.UnfoldDia diff --git a/Pdl/Substitution.lean b/Pdl/Substitution.lean index 6dc4acf..916893a 100644 --- a/Pdl/Substitution.lean +++ b/Pdl/Substitution.lean @@ -1,9 +1,8 @@ +-- Substitution and Helper Lemmas (Sections 2.1 and 2.2) -import Pdl.Semantics import Pdl.Discon --- ## Single-step replacing --- For simultaneous substition, see below! +/-! ## Single-step replacing -/ mutual /-- Replace atomic proposition `x` by `ψ` in a formula. -/ @@ -220,8 +219,7 @@ theorem repl_in_disMap x ρ (L : List α) (p : α → Prop) (f : α → Formula) simp only [List.map_map] aesop --- ## Substitutions --- Simultaneous +/-! ## Simultaneous Substitutions -/ abbrev Substitution := Nat → Formula @@ -306,7 +304,7 @@ theorem substitutionLemmaRel (σ : Substitution) α {W} (M : KripkeModel W) (w v exact IHφ end --- ## Replacement of Equivalents and similar helpers +/-! ## Semantic Equivalents -/ /- -- This is *not* true because `frm` might be sneaky. @@ -315,7 +313,7 @@ theorem wrong_equiv_repl φ1 φ2 (h : φ1 ≡ φ2) (frm : Formula → Formula) : sorry -/ --- if we replace `frm` with a special case then we get something true: +/-- A true instance of `wrong_equiv_repl`, here we replaced `frm` with a special case. -/ theorem equiv_con {φ1 φ2} (h : φ1 ≡ φ2) ψ : φ1 ⋀ ψ ≡ φ2 ⋀ ψ := by intro W M w diff --git a/dependencies.svg b/dependencies.svg index a1a55e4..ccac2bc 100644 --- a/dependencies.svg +++ b/dependencies.svg @@ -4,400 +4,364 @@ - + %3 - + Soundness - -Soundness + +Soundness Completeness - -Completeness + +Completeness Soundness->Completeness - - + + - + PartInterpolation - -PartInterpolation + +PartInterpolation - + Completeness->PartInterpolation - - + + TableauGame - -TableauGame + +TableauGame TableauGame->Completeness - - + + Modelgraphs - -Modelgraphs + +Modelgraphs Modelgraphs->Completeness - - + + Semantics - -Semantics - - - -Semantics->Modelgraphs - - + +Semantics Discon - -Discon + +Discon Semantics->Discon - - + + Examples - -Examples + +Examples Semantics->Examples - - + + - + SemQuot - -SemQuot + +SemQuot - + Semantics->SemQuot - - + + - + Substitution - -Substitution - - - -Semantics->Substitution - - + +Substitution - + Discon->Substitution - - + + Vocab - -Vocab + +Vocab Vocab->Discon - - + + - + Fresh - -Fresh + +Fresh - + Vocab->Fresh - - + + UnfoldDia - -UnfoldDia + +UnfoldDia - + UnfoldDia->Modelgraphs - - + + Distance - -Distance + +Distance UnfoldDia->Distance - - + + - + LocalTableau - -LocalTableau + +LocalTableau - + UnfoldDia->LocalTableau - - + + - + Distance->PartInterpolation - - + + Star - -Star + +Star - + Star->UnfoldDia - - + + Star->Examples - - + + - + UnfoldBox - -UnfoldBox + +UnfoldBox - + Star->UnfoldBox - - - - - -UnfoldBox->Modelgraphs - - - - - -UnfoldBox->Examples - - - - - -UnfoldBox->LocalTableau - - + + - + Syntax - -Syntax + +Syntax - + Syntax->Semantics - - + + - + Syntax->Vocab - - + + - + FischerLadner - -FischerLadner + +FischerLadner - + Syntax->FischerLadner - - - - - -LoadSplit - -LoadSplit - - - -Syntax->LoadSplit - - + + - + Measures - -Measures + +Measures - + Syntax->Measures - - + + - + FischerLadner->UnfoldBox - - + + - + Fresh->UnfoldDia - - + + - + Fresh->UnfoldBox - - + + - + Interpolation - -Interpolation + +Interpolation - + PartInterpolation->Interpolation - - + + - - -LoadSplit->Soundness - - + + +UnfoldBox->Modelgraphs + + + + + +UnfoldBox->LocalTableau + + - + Tableau - -Tableau + +Tableau - + LocalTableau->Tableau - - + + - + MultisetOrder - -MultisetOrder + +MultisetOrder - + MultisetOrder->LocalTableau - - + + - + Measures->Semantics - - + + - + Tableau->Soundness - - + + - + Tableau->TableauGame - - + + - + Substitution->UnfoldDia - - + + - + Substitution->UnfoldBox - - + + - + Game - -Game + +Game - + Game->TableauGame - - + +