generalise Uplus notation for Lists² and Finsets²

Pdl/Discon.lean

@@ -106,19 +106,28 @@ theorem disconEval {W M} {w : W} :
 -- UPLUS
 
 @[simp]
-def pairunion : List (List Formula) → List (List Formula) → List (List Formula)
+def pairunionList : List (List Formula) → List (List Formula) → List (List Formula)
   | xls, yls => List.join (xls.map fun xl => yls.map fun yl => xl ++ yl)
 
+@[simp]
 def pairunionFinset : Finset (Finset Formula) → Finset (Finset Formula) → Finset (Finset Formula)
   | X, Y => {X.biUnion fun ga => Y.biUnion fun gb => ga ∪ gb}
 
-infixl:77 "⊎" => pairunion
+class HasUplus (α : Type → Type) where
+  pairunion : α (α Formula) → α (α Formula) → α (α Formula)
+
+infixl:77 "⊎" => HasUplus.pairunion
+
+@[simp]
+instance listHasUplus : HasUplus List := ⟨pairunionList⟩
+@[simp]
+instance finsetHasUplus : HasUplus Finset := ⟨pairunionFinset⟩
 
-theorem disconAnd {XS YS} : discon (XS⊎YS)≡discon XS⋀discon YS :=
+theorem disconAnd {XS YS} : discon (XS ⊎ YS) ≡ discon XS ⋀ discon YS :=
   by
   unfold semEquiv
   intro W M w
-  rw [disconEval (XS⊎YS) (by rfl)]
+  rw [disconEval (XS ⊎ YS) (by rfl)]
   simp
   rw [disconEval XS (by rfl)]
   rw [disconEval YS (by rfl)]

Pdl/Examples.lean

@@ -6,41 +6,38 @@ import Mathlib.Tactic.FinCases
 open Vector
 
 -- some simple silly stuff
-theorem mytaut1 (p : Char) : tautology (Formula.atom_prop p↣Formula.atom_prop p) :=
+theorem mytaut1 (p : Char) : tautology ((·p) ↣ (·p)) :=
   by
-  unfold tautology evaluatePoint evaluate
+  unfold tautology
   intro W M w
-  sorry -- tauto
+  simp
 
 open Classical
 
 theorem mytaut2 (p : Char) : tautology ((~~·p)↣·p) :=
   by
   unfold tautology evaluatePoint evaluate
   intro W M w
-  classical
-  tauto
+  simp
 
 def myModel : KripkeModel ℕ where
   val _ _ := True
   Rel _ _ v := HEq v 1
 
 theorem mysat (p : Char) : satisfiable (·p) :=
   by
-  unfold satisfiable
-  exists ℕ
-  exists myModel
-  exists 1
-  unfold evaluatePoint evaluate
+  use ℕ, myModel, 1
+  unfold myModel
+  simp
 
 -- Segerberg's axioms
 
 -- A1: all propositional tautologies
 
 theorem A2 (a : Program) (X Y : Formula) : tautology (⌈a⌉ ⊤) :=
   by
-  unfold tautology evaluatePoint evaluate
-  sorry -- tauto
+  unfold tautology
+  simp
 
 theorem A3 (a : Program) (X Y : Formula) : tautology ((⌈a⌉(X⋀Y)) ↣ (⌈a⌉X) ⋀ (⌈a⌉Y)) :=
   by
@@ -67,7 +64,7 @@ theorem A4 (a b : Program) (p : Char) : tautology ((⌈a;b⌉(·p)) ⟷ (⌈a⌉
     intro v w_a_v v1 v_b_v1
     specialize hl v1
     apply hl
-    unfold Relate
+    simp
     use v
     constructor
     · exact w_a_v
@@ -77,7 +74,7 @@ theorem A4 (a b : Program) (p : Char) : tautology ((⌈a;b⌉(·p)) ⟷ (⌈a⌉
     cases' hyp with hl hr
     contrapose! hr
     intro v2 w_ab_v2
-    unfold Relate at w_ab_v2 
+    simp at w_ab_v2
     rcases w_ab_v2 with ⟨v1, w_a_v1, v1_b_v2⟩
     exact hl v1 w_a_v1 v2 v1_b_v2
 
@@ -94,16 +91,16 @@ theorem A5 (a b : Program) (X : Formula) : tautology ((⌈a ∪ b⌉X) ⟷((⌈a
     · -- show ⌈α⌉X
       intro v
       specialize lhs v
-      intro (w_a_v : Relate M a w v)
-      unfold Relate at lhs 
+      intro (w_a_v : relate M a w v)
+      unfold relate at lhs
       apply lhs
       left
       exact w_a_v
     · -- show ⌈β⌉X
       intro v
       specialize lhs v
-      intro (w_b_v : Relate M b w v)
-      unfold Relate at lhs 
+      intro (w_b_v : relate M b w v)
+      unfold relate at lhs
       apply lhs
       right
       exact w_b_v
@@ -115,7 +112,7 @@ theorem A5 (a b : Program) (X : Formula) : tautology ((⌈a ∪ b⌉X) ⟷((⌈a
     intro v; intro m_ab_v
     specialize rhs_a v
     specialize rhs_b v
-    unfold Relate at m_ab_v 
+    unfold relate at m_ab_v
     cases m_ab_v
     · apply rhs_a m_ab_v
     · apply rhs_b m_ab_v
@@ -133,30 +130,27 @@ theorem A6 (a : Program) (X : Formula) : tautology ((⌈∗a⌉X) ⟷ (X ⋀ (
     constructor
     · -- show X using refl:
       apply starAX
-      unfold Relate
       simp
       exact StarCat.refl w
     · -- show [α][α∗]X using star.step:
       intro v w_a_v v_1 v_aS_v1
       apply starAX
-      unfold Relate
+      unfold relate
       apply StarCat.step w v v_1
       exact w_a_v
-      unfold Relate at v_aS_v1 
+      unfold relate at v_aS_v1
       exact v_aS_v1
   · -- right to left
     by_contra hyp
     cases' hyp with hl hr
     contrapose! hr
     cases' hl with w_X w_aSaX
     intro v w_aStar_v
-    unfold Relate at w_aStar_v 
-    simp at w_aStar_v 
+    simp at w_aStar_v
     cases w_aStar_v
     case refl => exact w_X
     case step w y v w_a_y y_aS_v =>
-      unfold Relate at w_aSaX 
-      simp at w_aSaX 
+      simp at w_aSaX
       exact w_aSaX y w_a_y v y_aS_v
 
 example (a b : Program) (X : Formula) :
@@ -169,9 +163,9 @@ example (a b : Program) (X : Formula) :
 
 -- related via star ==> related via a finite chain
 theorem starIsFinitelyManySteps {W : Type} {M : KripkeModel W} {x z : W} {α : Program} :
-    StarCat (Relate M α) x z →
+    StarCat (relate M α) x z →
       ∃ (n : ℕ) (ys : Vector W n.succ),
-        x = ys.headI ∧ z = ys.getLast ∧ ∀ i : Fin n, Relate M α (get ys i) (get ys (i + 1)) :=
+        x = ys.headI ∧ z = ys.getLast ∧ ∀ i : Fin n, relate M α (get ys i) (get ys (i + 1)) :=
   by
   intro x_aS_z
   induction x_aS_z
@@ -227,7 +221,7 @@ theorem starIsFinitelyManySteps {W : Type} {M : KripkeModel W} {x z : W} {α : P
 theorem finitelyManyStepsIsStar {W : Type} {M : KripkeModel W} {α : Program} {n : ℕ}
     {ys : Vector W (Nat.succ n)} :
     (∀ i : Fin n, relate M α (get ys i) (get ys (i + 1))) →
-      StarCat (relate M α) ys.headI ys.getLast :=
+      StarCat (relate M α) ys.head ys.last :=
   by
   simp
   induction n
@@ -241,7 +235,7 @@ theorem finitelyManyStepsIsStar {W : Type} {M : KripkeModel W} {α : Program} {n
     intro lhs
     apply StarCat.step
     · -- ys has at least two elements now
-      show Relate M α ys.head ys.tail.head
+      show relate M α ys.head ys.tail.head
       specialize lhs 0
       simp at lhs 
       have foo : ys.nth 1 = ys.tail.head :=
@@ -267,9 +261,9 @@ theorem finitelyManyStepsIsStar {W : Type} {M : KripkeModel W} {α : Program} {n
 
 -- related via star <=> related via a finite chain
 theorem starIffFinitelyManySteps (W : Type) (M : KripkeModel W) (x z : W) (α : Program) :
-    StarCat (Relate M α) x z ↔
+    StarCat (relate M α) x z ↔
       ∃ (n : ℕ) (ys : Vector W n.succ),
-        x = ys.headI ∧ z = ys.getLast ∧ ∀ i : Fin n, Relate M α (get ys i) (get ys (i + 1)) :=
+        x = ys.head ∧ z = ys.last ∧ ∀ i : Fin n, relate M α (get ys i) (get ys (i + 1)) :=
   by
   constructor
   apply starIsFinitelyManySteps
@@ -331,17 +325,15 @@ theorem stepStarIsStarStepBoxes {a : Program} {φ : Formula} : tautology ((⌈a;
   apply lhs
 
 -- Example 1 in Borzechowski
-theorem inductionAxiom (a : Program) (φ : Formula) : tautology (φ ⋀ (⌈∗a⌉(φ ↣ (⌈a⌉φ)) ↣ (⌈∗a⌉φ))) :=
+theorem inductionAxiom (a : Program) (φ : Formula) : tautology ((φ ⋀ ⌈∗a⌉(φ ↣ (⌈a⌉φ))) ↣ (⌈∗a⌉φ)) :=
   by
   simp
   intro W M w
   simp
   intro Mwφ
   intro MwStarImpHyp
   intro x w_starA_x
-  unfold Relate at w_starA_x 
-  simp at w_starA_x 
-  rw [starIffFinitelyManySteps] at w_starA_x 
+  rw [starIffFinitelyManySteps] at w_starA_x
   rcases w_starA_x with ⟨n, ys, w_is_head, x_is_last, i_a_isucc⟩
   have claim : ∀ i : Fin n.succ, Evaluate M (ys.nth ↑i) φ :=
     by

Pdl/Syntax.lean

@@ -156,10 +156,9 @@ def vocabOfSetFormula : Finset Formula → Finset Char
 class HasVocabulary (α : Type) where
   voc : α → Finset Char
 
-instance formulaHasVocabulary : HasVocabulary Formula := ⟨ vocabOfFormula⟩
-instance programHasVocabulary : HasVocabulary Program := ⟨ vocabOfProgram ⟩
-instance finsetFormulaHasVocabulary : HasVocabulary (Finset Formula) := ⟨ vocabOfSetFormula ⟩
-
+instance formulaHasVocabulary : HasVocabulary Formula := ⟨vocabOfFormula⟩
+instance programHasVocabulary : HasVocabulary Program := ⟨vocabOfProgram⟩
+instance finsetFormulaHasVocabulary : HasVocabulary (Finset Formula) := ⟨vocabOfSetFormula⟩
 
 lemma boxes_last : ∀ {a as P} , (~⌈a⌉Formula.boxes (as ++ [c]) P) = (~⌈a⌉Formula.boxes as (⌈c⌉P)) :=
   by

Pdl/Tableau.lean

@@ -12,6 +12,10 @@ import Pdl.Unravel
 -- TODO: Can we use variables below without making them arguments of localRule?
 -- variable (X : Finset Formula) (f g : Formula) (a b : Program)
 
+@[simp]
+def listsToSets : List (List Formula) → Finset (Finset Formula)
+| LS => (LS.map List.toFinset).toFinset
+
 -- Local rules: given this set, we get these sets as child nodes
 inductive localRule : Finset Formula → Finset (Finset Formula) → Type
   -- PROP LOGIC
@@ -36,24 +40,34 @@ inductive localRule : Finset Formula → Finset (Finset Formula) → Type
   | nUn {a b f} (h : (~⌈a ∪ b⌉f) ∈ X) : localRule X { X \ {~⌈a ∪ b⌉f} ∪ {~⌈a⌉f}
                                                     , X \ {~⌈a ∪ b⌉f} ∪ {~⌈b⌉f} }
   -- STAR
-  | sta {X a f} (h : (⌈∗a⌉f) ∈ X) : localRule X (pairunionFinset { X \ {⌈∗a⌉f} } ((unravel (⌈∗a⌉f)).map List.toFinset).toFinset)
-  | nSt {a f} (h : (~⌈∗a⌉f) ∈ X) : localRule X (pairunionFinset { X \ {~⌈∗a⌉f} } ((unravel (~⌈∗a⌉f)).map List.toFinset).toFinset)
+  | sta {X a f} (h : (⌈∗a⌉f) ∈ X) : localRule X ({ X \ {⌈∗a⌉f} } ⊎ (listsToSets (unravel (⌈∗a⌉f))))
+  | nSt {a f} (h : (~⌈∗a⌉f) ∈ X) : localRule X ({ X \ {~⌈∗a⌉f} } ⊎ (listsToSets (unravel (~⌈∗a⌉f))))
 
   -- TODO which rules need and modify markings?
   -- TODO only apply * if there is a marking.
 
 
 -- TODO: rephrase this like Lemma 5 of MB with both directions / invertible?
-lemma localRuleTruth {W : Type} {M : KripkeModel W} {w : W} {X : Finset Formula} {B : Finset (Finset Formula)} :
-  localRule X B → (∃ Y ∈ B, (M,w) ⊨ Y) → (M,w) ⊨ X := sorry
+lemma localRuleTruth {W} {M : KripkeModel W} {w : W} {X B} :
+  localRule X B → ((∃ Y ∈ B, (M,w) ⊨ Y) ↔ (M,w) ⊨ X) :=
+  by
+  intro locR
+  cases locR
+  case nSt a f aSf_in_X =>
+    have := likeLemmaFour M (∗ a)
+    simp at *
+    -- TODO
+    sorry
+  -- TODO
+  all_goals { sorry }
 
 
 -- TODO inductive LocalTableau
 
 
 -- TABLEAUX
 
-inductive Tableau
+inductive Tableau -- to be rewritten as in tablean?
   | leaf : Set Formula → Tableau
   | Rule : Rule → List (Set Formula) → Tableau