Bml: Examples, Vocabulary, Soundness, Tableauexamples, Completeness

Bml.lean

@@ -5,10 +5,10 @@ import «Bml».Semantics
 import «Bml».Setsimp
 import «Bml».Modelgraphs
 import «Bml».Tableau
--- TODO import «Bml».Examples
--- TODO import «Bml».Vocabulary
--- TODO import «Bml».Soundness
--- TODO import «Bml».Tableauexamples
--- TODO import «Bml».Completeness
+import «Bml».Examples
+import «Bml».Vocabulary
+import «Bml».Soundness
+import «Bml».Tableauexamples
+import «Bml».Completeness
 -- TODO import «Bml».Partitions
 -- TODO import «Bml».Interpolation

Bml/Completeness.lean

@@ -1,12 +1,11 @@
 -- COMPLETENESS
-import Syntax
-import Tableau
-import Soundness
 
-#align_import completeness
+import Bml.Syntax
+import Bml.Tableau
+import Bml.Soundness
+
+-- TODO: import Bml.modelgraphs
 
--- import modelgraphs
--- import modelgraphs
 open HasSat
 
 -- Each local rule preserves truth "upwards"
@@ -16,17 +15,17 @@ theorem localRuleTruth {W : Type} {M : KripkeModel W} {w : W} {X : Finset Formul
   intro r
   cases r
   case bot => simp
-  case not => simp
-  case neg a f notnotf_in_a =>
+  case Not => simp
+  case neg f notnotf_in_a =>
     intro hyp
     rcases hyp with ⟨b, b_in_B, w_sat_b⟩
     intro phi phi_in_a
-    have b_is_af : b = insert f (a \ {~~f}) := by simp at *; subst b_in_B
+    have b_is_af : b = insert f (X \ {~~f}) := by simp at *; subst b_in_B; tauto
     have phi_in_b_or_is_f : phi ∈ b ∨ phi = ~~f :=
       by
       rw [b_is_af]
       simp
-      finish
+      sorry
     cases' phi_in_b_or_is_f with phi_in_b phi_is_notnotf
     · apply w_sat_b
       exact phi_in_b
@@ -37,17 +36,17 @@ theorem localRuleTruth {W : Type} {M : KripkeModel W} {w : W} {X : Finset Formul
       apply w_sat_b
       rw [b_is_af]
       simp at *
-  case con a f g fandg_in_a =>
+  case Con f g fandg_in_a =>
     intro hyp
     rcases hyp with ⟨b, b_in_B, w_sat_b⟩
     intro phi phi_in_a
     simp at b_in_B 
-    have b_is_fga : b = insert f (insert g (a \ {f⋏g})) := by subst b_in_B; ext1; simp
-    have phi_in_b_or_is_fandg : phi ∈ b ∨ phi = f⋏g :=
+    have b_is_fga : b = insert f (insert g (X \ {f⋀g})) := by subst b_in_B; ext1; simp
+    have phi_in_b_or_is_fandg : phi ∈ b ∨ phi = f⋀g :=
       by
       rw [b_is_fga]
       simp
-      finish
+      sorry
     cases' phi_in_b_or_is_fandg with phi_in_b phi_is_fandg
     · apply w_sat_b
       exact phi_in_b
@@ -56,39 +55,32 @@ theorem localRuleTruth {W : Type} {M : KripkeModel W} {w : W} {X : Finset Formul
       constructor
       · apply w_sat_b; rw [b_is_fga]; simp
       · apply w_sat_b; rw [b_is_fga]; simp
-  case nCo a f g not_fandg_in_a =>
+  case nCo f g not_fandg_in_a =>
     intro hyp
     rcases hyp with ⟨b, b_in_B, w_sat_b⟩
     intro phi phi_in_a
     simp at *
-    have phi_in_b_or_is_notfandg : phi ∈ b ∨ phi = ~(f⋏g) := by
-      cases b_in_B <;> · rw [b_in_B]; simp; finish
+    have phi_in_b_or_is_notfandg : phi ∈ b ∨ phi = ~(f⋀g) := by
+      cases b_in_B
+      case inl b_in_B => rw [b_in_B]; simp; tauto
+      case inr b_in_B => rw [b_in_B]; simp; tauto
     cases b_in_B
-    · -- b contains ~f
+    case inl b_in_B => -- b contains ~f
       cases' phi_in_b_or_is_notfandg with phi_in_b phi_def
       · exact w_sat_b phi phi_in_b
       · rw [phi_def]
         unfold Evaluate
         rw [b_in_B] at w_sat_b 
         specialize w_sat_b (~f)
-        rw [not_and_or]
-        left
-        unfold Evaluate at w_sat_b 
-        apply w_sat_b
-        finish
-    · -- b contains ~g
+        aesop
+    case inr b_in_B => -- b contains ~g
       cases' phi_in_b_or_is_notfandg with phi_in_b phi_def
       · exact w_sat_b phi phi_in_b
       · rw [phi_def]
         unfold Evaluate
         rw [b_in_B] at w_sat_b 
         specialize w_sat_b (~g)
-        rw [not_and_or]
-        right
-        unfold Evaluate at w_sat_b 
-        apply w_sat_b
-        finish
-#align localRuleTruth localRuleTruth
+        aesop
 
 -- Each local rule is "complete", i.e. preserves satisfiability "upwards"
 theorem localRuleCompleteness {X : Finset Formula} {B : Finset (Finset Formula)} :
@@ -97,12 +89,11 @@ theorem localRuleCompleteness {X : Finset Formula} {B : Finset (Finset Formula)}
   intro lr
   intro sat_B
   rcases sat_B with ⟨Y, Y_in_B, sat_Y⟩
-  unfold satisfiable at *
+  unfold Satisfiable at *
   rcases sat_Y with ⟨W, M, w, w_sat_Y⟩
   use W, M, w
   apply localRuleTruth lr
   tauto
-#align localRuleCompleteness localRuleCompleteness
 
 -- Lemma 11 (but rephrased to be about local tableau!?)
 theorem inconsUpwards {X} {ltX : LocalTableau X} :
@@ -114,7 +105,6 @@ theorem inconsUpwards {X} {ltX : LocalTableau X} :
     (lhs Y YinEnds).some
   constructor
   exact ClosedTableau.loc ltX leafTableaus
-#align inconsUpwards inconsUpwards
 
 -- Converse of Lemma 11
 theorem consToEndNodes {X} {ltX : LocalTableau X} :
@@ -125,23 +115,20 @@ theorem consToEndNodes {X} {ltX : LocalTableau X} :
   have claim := Not.imp consX (@inconsUpwards X ltX)
   simp at claim 
   tauto
-#align consToEndNodes consToEndNodes
 
 def projOfConsSimpIsCons :
     ∀ {X ϕ}, Consistent X → Simple X → ~(□ϕ) ∈ X → Consistent (projection X ∪ {~ϕ}) :=
   by
   intro X ϕ consX simpX notBoxPhi_in_X
   unfold Consistent at *
   unfold Inconsistent at *
-  by_contra h
+  contrapose consX
   simp at *
-  cases' h with ctProj
-  have ctX : ClosedTableau X :=
-    by
-    apply ClosedTableau.atm notBoxPhi_in_X simpX
-    simp; exact ctProj
-  cases consX; tauto
-#align projOfConsSimpIsCons projOfConsSimpIsCons
+  cases' consX with ctProj
+  constructor
+  apply ClosedTableau.atm notBoxPhi_in_X simpX
+  simp
+  exact ctProj
 
 theorem locTabEndSatThenSat {X Y} (ltX : LocalTableau X) (Y_endOf_X : Y ∈ endNodesOf ⟨X, ltX⟩) :
     Satisfiable Y → Satisfiable X := by
@@ -152,51 +139,61 @@ theorem locTabEndSatThenSat {X Y} (ltX : LocalTableau X) (Y_endOf_X : Y ∈ endN
     cases lr
     case bot W bot_in_W =>
       simp at *
-      exact Y_endOf_X
-    case not _ ϕ h =>
+    case Not ϕ h =>
       simp at *
-      exact Y_endOf_X
-    case neg Z ϕ notNotPhi_inX =>
+    case neg ϕ notNotPhi_inX =>
       simp at *
-      specialize IH (insert ϕ (Z.erase (~~ϕ)))
-      simp at IH 
+      specialize IH (insert ϕ (X.erase (~~ϕ)))
+      simp at IH
       apply IH
       rcases Y_endOf_X with ⟨W, W_def, Y_endOf_W⟩
       subst W_def
       exact Y_endOf_W
-    case con Z ϕ ψ _ =>
+    case Con ϕ ψ _ =>
       simp at *
-      specialize IH (insert ϕ (insert ψ (Z.erase (ϕ⋏ψ))))
+      specialize IH (insert ϕ (insert ψ (X.erase (ϕ⋀ψ))))
       simp at IH 
       apply IH
       rcases Y_endOf_X with ⟨W, W_def, Y_endOf_W⟩
       subst W_def
       exact Y_endOf_W
-    case nCo Z ϕ ψ _ =>
+    case nCo ϕ ψ _ =>
       simp at *
-      rcases Y_endOf_X with ⟨W, W_def, Y_endOf_W⟩
-      cases W_def
-      all_goals subst W_def
-      · specialize IH (insert (~ϕ) (Z.erase (~(ϕ⋏ψ))))
+      cases Y_endOf_X
+      case inl Y_endOf_X =>
+        left
+        simp at *
+        sorry
+        /-
+        rcases Y_endOf_X with ⟨W, W_def, Y_endOf_W⟩
+        subst W_def
+        specialize IH (insert (~ϕ) (X.erase (~(ϕ⋀ψ))))
         simp at IH 
-        use insert (~ϕ) (Z.erase (~(ϕ⋏ψ)))
+        use insert (~ϕ) (X.erase (~(ϕ⋀ψ)))
         constructor
         · left; rfl
         · apply IH; exact Y_endOf_W
-      · specialize IH (insert (~ψ) (Z.erase (~(ϕ⋏ψ))))
+        -/
+      case inr Y_endOf_X =>
+        right
+        sorry
+        /-
+        rcases Y_endOf_X with ⟨W, W_def, Y_endOf_W⟩
+        subst W_def
+        specialize IH (insert (~ψ) (X.erase (~(ϕ⋀ψ))))
         simp at IH 
-        use insert (~ψ) (Z.erase (~(ϕ⋏ψ)))
+        use insert (~ψ) (X.erase (~(ϕ⋀ψ)))
         constructor
         · right; rfl
         · apply IH; exact Y_endOf_W
-  case sim X simpX => finish
-#align locTabEndSatThenSat locTabEndSatThenSat
+        -/
+  case sim X simpX => aesop
 
 theorem almostCompleteness : ∀ n X, lengthOfSet X = n → Consistent X → Satisfiable X :=
   by
   intro n
-  apply Nat.strong_induction_on n
-  intro n IH
+  induction n using Nat.strong_induction_on
+  case h n IH =>
   intro X lX_is_n consX
   refine' if simpX : Simple X then _ else _
   -- CASE 1: X is simple
@@ -207,22 +204,23 @@ theorem almostCompleteness : ∀ n X, lengthOfSet X = n → Consistent X → Sat
     unfold Consistent at consX 
     unfold Inconsistent at consX 
     simp at consX 
-    cases consX; apply consX
+    cases' consX with myfalse
+    apply myfalse
     unfold Closed at h 
     refine' if botInX : ⊥ ∈ X then _ else _
     · apply ClosedTableau.loc; rotate_left; apply LocalTableau.byLocalRule
       exact LocalRule.bot botInX
-      intro Y YinEmpty; cases YinEmpty
-      rw [botNoEndNodes]; intro Y YinEmpty; cases YinEmpty
-    · have f1 : ∃ (f : Formula) (H : f ∈ X), ~f ∈ X := by tauto
+      intro Y YinEmpty; exfalso; cases YinEmpty
+      rw [botNoEndNodes]; intro Y YinEmpty; exfalso; cases YinEmpty
+    · have f1 : ∃ (f : Formula) (_ : f ∈ X), ~f ∈ X := by tauto
       have : Nonempty (ClosedTableau X) :=
         by
         rcases f1 with ⟨f, f_in_X, notf_in_X⟩
         fconstructor
         apply ClosedTableau.loc; rotate_left; apply LocalTableau.byLocalRule
-        apply LocalRule.not ⟨f_in_X, notf_in_X⟩
-        intro Y YinEmpty; cases YinEmpty
-        rw [notNoEndNodes]; intro Y YinEmpty; cases YinEmpty
+        apply LocalRule.Not ⟨f_in_X, notf_in_X⟩
+        intro Y YinEmpty; exfalso; cases YinEmpty
+        rw [notNoEndNodes]; intro Y YinEmpty; exfalso; cases YinEmpty
       exact Classical.choice this
   · -- show that all projections are sat
     intro R notBoxR_in_X
@@ -238,19 +236,18 @@ theorem almostCompleteness : ∀ n X, lengthOfSet X = n → Consistent X → Sat
   have lr := Classical.choice lrExists
   have rest : ∀ Y : Finset Formula, Y ∈ B → LocalTableau Y :=
     by
-    intro Y Y_in_B
+    intro Y _
     set N := HasLength.lengthOf Y
     exact Classical.choice (existsLocalTableauFor N Y (by rfl))
   rcases@consToEndNodes X (LocalTableau.byLocalRule lr rest) consX with ⟨E, E_endOf_X, consE⟩
-  have satE : satisfiable E := by
+  have satE : Satisfiable E := by
     apply IH (lengthOfSet E)
     · -- end Node of local rule is LT
       subst lX_is_n
       apply endNodesOfLocalRuleLT E_endOf_X
     · rfl
     · exact consE
   exact locTabEndSatThenSat (LocalTableau.byLocalRule lr rest) E_endOf_X satE
-#align almostCompleteness almostCompleteness
 
 -- Theorem 4, page 37
 theorem completeness : ∀ X, Consistent X ↔ Satisfiable X :=
@@ -262,13 +259,10 @@ theorem completeness : ∀ X, Consistent X ↔ Satisfiable X :=
     apply almostCompleteness n X (by rfl) X_is_consistent
   -- use Theorem 2:
   exact correctness X
-#align completeness completeness
 
 theorem singletonCompleteness : ∀ φ, Consistent {φ} ↔ Satisfiable φ :=
   by
   intro f
   have := completeness {f}
   simp only [singletonSat_iff_sat] at *
   tauto
-#align singletonCompleteness singletonCompleteness
-

Bml/Examples.lean

@@ -1,17 +1,14 @@
 -- EXAMPLES
-import Syntax
-import Semantics
-
-#align_import examples
+import Bml.Syntax
+import Bml.Semantics
 
 open HasSat
 
 theorem mytaut1 (p : Char) : Tautology ((·p)↣·p) :=
   by
   unfold Tautology Evaluate
   intro W M w
-  simp; unfold Evaluate; tauto
-#align mytaut1 mytaut1
+  simp
 
 open Classical
 
@@ -21,42 +18,33 @@ theorem mytaut2 (p : Char) : Tautology ((~~·p)↣·p) :=
   intro W M w
   classical
   simp
-  unfold Evaluate
-  tauto
-#align mytaut2 mytaut2
 
 def myModel : KripkeModel ℕ where
   val _ _ := True
   Rel _ v := HEq v 1
-#align myModel myModel
 
 theorem mysat (p : Char) : Satisfiable (·p) :=
   by
-  unfold satisfiable
+  unfold Satisfiable
   exists ℕ
   exists myModel
   exists 1
-  unfold Evaluate
-#align mysat mysat
 
 -- Some validities of basic modal logic
+
 theorem boxTop : Tautology (□⊤) := by
   unfold Tautology Evaluate
   tauto
-#align boxTop boxTop
 
-theorem A3 (X Y : Formula) : Tautology (□(X⋏Y)↣□X⋏□Y) :=
+theorem A3 (X Y : Formula) : Tautology (□(X⋀Y) ↣ □X⋀□Y) :=
   by
   unfold Tautology Evaluate
   intro W M w
   by_contra hyp
   simp at hyp 
-  unfold Evaluate at hyp 
-  simp at hyp 
+  unfold Evaluate at hyp
   cases' hyp with hl hr
   contrapose! hr
   constructor
   · intro v1 ass; exact (hl v1 ass).1
   · intro v2 ass; exact (hl v2 ass).2
-#align A3 A3
-