comments, cleaning, update dependency graph

m4lvin · Dec 23, 2024 · 2f05d43 · 2f05d43
1 parent 820872f
commit 2f05d43
Show file tree

Hide file tree

Showing 6 changed files with 176 additions and 227 deletions.
diff --git 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
@@ -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
@@ -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
@@ -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
@@ -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