From 3a05743496d583b34c0f6bf963f02f19df0cc618 Mon Sep 17 00:00:00 2001 From: Malvin Gattinger Date: Fri, 3 Nov 2023 10:35:43 +0100 Subject: [PATCH] Bml: shorten Completeness, more about open (iff not closed) tableaux --- Bml/Completeness.lean | 35 ++++++----------- Bml/Tableau.lean | 90 ++++++++++++++++++++++++------------------- 2 files changed, 63 insertions(+), 62 deletions(-) diff --git a/Bml/Completeness.lean b/Bml/Completeness.lean index 5cbda99..fca8517 100644 --- a/Bml/Completeness.lean +++ b/Bml/Completeness.lean @@ -4,8 +4,6 @@ import Bml.Syntax import Bml.Tableau import Bml.Soundness --- TODO: import Bml.modelgraphs - open HasSat -- Each local rule preserves truth "upwards" @@ -176,12 +174,9 @@ theorem locTabEndSatThenSat {X Y} (ltX : LocalTableau X) (Y_endOf_X : Y ∈ endN convert Y_endOf_X; case sim X simpX => aesop -theorem almostCompleteness : ∀ n X, lengthOfSet X = n → Consistent X → Satisfiable X := +theorem almostCompleteness : (X : Finset Formula) → Consistent X → Satisfiable X := by - intro n - induction n using Nat.strong_induction_on - case h n IH => - intro X lX_is_n consX + intro X consX refine' if simpX : Simple X then _ else _ -- CASE 1: X is simple rw [Lemma1_simple_sat_iff_all_projections_sat simpX] @@ -211,12 +206,10 @@ theorem almostCompleteness : ∀ n X, lengthOfSet X = n → Consistent X → Sat exact Classical.choice this · -- show that all projections are sat intro R notBoxR_in_X - apply IH (lengthOfSet (projection X ∪ {~R})) - · -- projection decreases lengthOfSet - subst lX_is_n - exact atmRuleDecreasesLength notBoxR_in_X - · rfl - · exact projOfConsSimpIsCons consX simpX notBoxR_in_X + have : Finset.sum (insert (~R) (projection X)) lengthOfFormula < Finset.sum X lengthOfFormula := by + convert atmRuleDecreasesLength notBoxR_in_X + simp + exact almostCompleteness (projection X ∪ {~R}) (projOfConsSimpIsCons consX simpX notBoxR_in_X) -- CASE 2: X is not simple rename' simpX => notSimpX rcases notSimpleThenLocalRule notSimpX with ⟨B, lrExists⟩ @@ -224,17 +217,14 @@ theorem almostCompleteness : ∀ n X, lengthOfSet X = n → Consistent X → Sat have rest : ∀ Y : Finset Formula, Y ∈ B → LocalTableau Y := by intro Y _ - set N := HasLength.lengthOf Y - exact Classical.choice (existsLocalTableauFor N Y (by rfl)) + exact Classical.choice (existsLocalTableauFor Y) rcases@consToEndNodes X (LocalTableau.byLocalRule lr rest) consX with ⟨E, E_endOf_X, consE⟩ 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 + have := endNodesOfLocalRuleLT E_endOf_X + exact almostCompleteness E consE exact locTabEndSatThenSat (LocalTableau.byLocalRule lr rest) E_endOf_X satE +termination_by + almostCompleteness X _ => lengthOfSet X -- Theorem 4, page 37 theorem completeness : ∀ X, Consistent X ↔ Satisfiable X := @@ -242,8 +232,7 @@ theorem completeness : ∀ X, Consistent X ↔ Satisfiable X := intro X constructor · intro X_is_consistent - let n := lengthOfSet X - apply almostCompleteness n X (by rfl) X_is_consistent + apply almostCompleteness X X_is_consistent -- use Theorem 2: exact correctness X diff --git a/Bml/Tableau.lean b/Bml/Tableau.lean index 061b4c3..a327878 100644 --- a/Bml/Tableau.lean +++ b/Bml/Tableau.lean @@ -89,8 +89,7 @@ theorem projection_set_length_leq : ∀ X, lengthOfSet (projection X) ≤ length unfold projection ext1 g simp - · - calc + · calc (projection (insert f S)).sum lengthOfFormula = (projection (insert f S)).sum lengthOfFormula := refl _ @@ -146,8 +145,7 @@ theorem localRulesDecreaseLength {X : Finset Formula} {B : Finset (Finset Formul all_goals intro β inB; simp at * case neg ϕ notnot_in_X => subst inB - · - calc + · calc lengthOfSet (insert ϕ (X.erase (~~ϕ))) ≤ lengthOfSet (X.erase (~~ϕ)) + lengthOf ϕ := by apply lengthOf_insert_leq_plus _ < lengthOfSet (X.erase (~~ϕ)) + lengthOf ϕ + 2 := by simp @@ -155,8 +153,7 @@ theorem localRulesDecreaseLength {X : Finset Formula} {B : Finset (Finset Formul _ = lengthOfSet X := lengthRemove X (~~ϕ) notnot_in_X case Con ϕ ψ in_X => subst inB - · - calc + · calc lengthOf (insert ϕ (insert ψ (X.erase (ϕ⋀ψ)))) ≤ lengthOf (insert ψ (X.erase (ϕ⋀ψ))) + lengthOf ϕ := by apply lengthOf_insert_leq_plus @@ -195,8 +192,7 @@ theorem atmRuleDecreasesLength {X : Finset Formula} {ϕ} : ext1 phi rw [proj]; rw [proj] simp - · - calc + · calc lengthOfSet (insert (~ϕ) (projection X)) ≤ lengthOfSet (projection X) + lengthOf (~ϕ) := lengthOf_insert_leq_plus _ = lengthOfSet (projection X) + 1 + lengthOf ϕ := by simp; ring @@ -213,12 +209,8 @@ inductive LocalTableau : Finset Formula → Type | byLocalRule {X B} (_ : LocalRule X B) (next : ∀ Y ∈ B, LocalTableau Y) : LocalTableau X | sim {X} : Simple X → LocalTableau X -def existsLocalTableauFor : ∀ N α, N = lengthOf α → Nonempty (LocalTableau α) := +def existsLocalTableauFor α : Nonempty (LocalTableau α) := by - intro N - induction N using Nat.strong_induction_on - case h n IH => - intro α nDef cases em ¬∃ B, Nonempty (LocalRule α B) case inl canApplyRule => constructor @@ -232,32 +224,28 @@ def existsLocalTableauFor : ∀ N α, N = lengthOf α → Nonempty (LocalTableau cases' r_exists with r cases r case bot h => - have t := LocalTableau.byLocalRule (LocalRule.bot h) ?_; use t + use (LocalTableau.byLocalRule (LocalRule.bot h) ?_) intro Y; intro Y_in_empty; tauto case Not h => - have t := LocalTableau.byLocalRule (LocalRule.Not h) ?_; use t + use (LocalTableau.byLocalRule (LocalRule.Not h) ?_) intro Y; intro Y_in_empty; tauto case neg f h => - have t := LocalTableau.byLocalRule (LocalRule.neg h) ?_; use t + use (LocalTableau.byLocalRule (LocalRule.neg h) ?_) intro Y Y_def - have rDec := localRulesDecreaseLength (LocalRule.neg h) Y Y_def - subst nDef - specialize IH (lengthOf Y) rDec Y (refl _) - apply Classical.choice IH + have := localRulesDecreaseLength (LocalRule.neg h) Y Y_def + apply Classical.choice (existsLocalTableauFor Y) case Con f g h => - have t := LocalTableau.byLocalRule (LocalRule.Con h) ?_; use t + use (LocalTableau.byLocalRule (LocalRule.Con h) ?_) intro Y Y_def - have rDec := localRulesDecreaseLength (LocalRule.Con h) Y Y_def - subst nDef - specialize IH (lengthOf Y) rDec Y (refl _) - apply Classical.choice IH + have := localRulesDecreaseLength (LocalRule.Con h) Y Y_def + apply Classical.choice (existsLocalTableauFor Y) case nCo f g h => - have t := LocalTableau.byLocalRule (LocalRule.nCo h) ?_; use t + use (LocalTableau.byLocalRule (LocalRule.nCo h) ?_) intro Y Y_def - have rDec := localRulesDecreaseLength (LocalRule.nCo h) Y Y_def - subst nDef - specialize IH (lengthOf Y) rDec Y (refl _) - apply Classical.choice IH + have := localRulesDecreaseLength (LocalRule.nCo h) Y Y_def + apply Classical.choice (existsLocalTableauFor Y) +termination_by + existsLocalTableauFor α => lengthOf α open LocalTableau @@ -374,11 +362,42 @@ inductive Tableau : Finset Formula → Type | atm {X ϕ} : ~(□ϕ) ∈ X → Simple X → Tableau (projection X ∪ {~ϕ}) → Tableau X | opn {X} : Simple X → (∀ φ, ~(□φ) ∈ X → IsEmpty (ClosedTableau (projection X ∪ {~φ}))) → Tableau X +def isOpen : Tableau X → Prop + | (Tableau.loc lt next) => ∃ Y, ∃ h : Y ∈ endNodesOf ⟨X, lt⟩, isOpen (next Y h) -- mwah?! + | (Tableau.atm _ _ t_proj) => isOpen t_proj + | (Tableau.opn _ _) => True + +def isClosed : Tableau X → Prop + | (Tableau.loc lt next) => ∀ Y, ∀ h : Y ∈ endNodesOf ⟨X, lt⟩, isClosed (next Y h) -- mwah?! + | (Tableau.atm _ _ t_proj) => isClosed t_proj + | (Tableau.opn _ _) => False + +theorem open_iff_notClosed {X} {t : Tableau X} : isOpen t ↔ ¬ isClosed t := + by + induction t + all_goals + simp [isOpen, isClosed] + try assumption + case loc Y ltY next IH => + constructor + · rintro ⟨Z, Z_in, Z_isOp⟩ + specialize IH Z Z_in + use Z, Z_in + rw [← IH] + exact Z_isOp + · rintro ⟨Z, Z_in, Z_notClosed⟩ + specialize IH Z Z_in + use Z, Z_in + rw [IH] + exact Z_notClosed + +def OpenTableau (X : Finset Formula) : Type := { t : Tableau X // isOpen t } + def injectTab : ClosedTableau X → Tableau X | (ClosedTableau.loc lt ends) => Tableau.loc lt (λ _ Y_in => injectTab (ends _ Y_in)) | (ClosedTableau.atm nB_in_X simX ctProj) => Tableau.atm nB_in_X simX (injectTab ctProj) -theorem existsTableauFor {α} : Nonempty (Tableau α) := +def existsTableauFor {α} : Nonempty (Tableau α) := by cases em (∃ B, Nonempty (LocalRule α B)) case inl canApplyRule => @@ -387,7 +406,7 @@ theorem existsTableauFor {α} : Nonempty (Tableau α) := constructor apply Tableau.loc (LocalTableau.byLocalRule lr _) _ · intro Y _ - exact Classical.choice (existsLocalTableauFor (lengthOf Y) Y rfl) + exact Classical.choice (existsLocalTableauFor Y) · intro Y Y_in_ends apply Classical.choice have : lengthOf Y < lengthOf α := endNodesOfLocalRuleLT Y_in_ends @@ -406,10 +425,3 @@ theorem existsTableauFor {α} : Nonempty (Tableau α) := exact ⟨Tableau.atm nBf_in_a is_simp (injectTab ct_notf)⟩ termination_by existsTableauFor α => lengthOf α - -def isOpen : Tableau X → Prop - | (Tableau.loc lt next) => ∃ Y, ∃ h : Y ∈ endNodesOf ⟨X, lt⟩, isOpen (next Y h) -- mwah?! - | (Tableau.atm _ _ t_proj) => isOpen t_proj - | (Tableau.opn _ _) => True - -def OpenTableau (X : Finset Formula) : Type := { t : Tableau X // isOpen t }