diff --git a/Bml.lean b/Bml.lean index cf72700..6cd0ec1 100644 --- a/Bml.lean +++ b/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 diff --git a/Bml/Completeness.lean b/Bml/Completeness.lean index 42b46be..81f85f4 100644 --- a/Bml/Completeness.lean +++ b/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,7 +115,6 @@ 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 ∪ {~ϕ}) := @@ -133,15 +122,13 @@ def projOfConsSimpIsCons : 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,11 +236,11 @@ 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 @@ -250,7 +248,6 @@ theorem almostCompleteness : ∀ n X, lengthOfSet X = n → Consistent X → Sat · 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,7 +259,6 @@ 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 @@ -270,5 +266,3 @@ theorem singletonCompleteness : ∀ φ, Consistent {φ} ↔ Satisfiable φ := have := completeness {f} simp only [singletonSat_iff_sat] at * tauto -#align singletonCompleteness singletonCompleteness - diff --git a/Bml/Examples.lean b/Bml/Examples.lean index 3e2ae68..ebcb960 100644 --- a/Bml/Examples.lean +++ b/Bml/Examples.lean @@ -1,8 +1,6 @@ -- EXAMPLES -import Syntax -import Semantics - -#align_import examples +import Bml.Syntax +import Bml.Semantics open HasSat @@ -10,8 +8,7 @@ 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 - diff --git a/Bml/Interpolation.lean b/Bml/Interpolation.lean index 7acefc8..dbfaf98 100644 --- a/Bml/Interpolation.lean +++ b/Bml/Interpolation.lean @@ -1,15 +1,13 @@ -- INTERPOLATION -import Syntax -import Completeness -import Partitions -#align_import interpolation +import Bml.Syntax +import Bml.Completeness +import Bml.Partitions open HasVocabulary def Interpolant (φ : Formula) (ψ : Formula) (θ : Formula) := Tautology (φ↣θ) ∧ Tautology (θ↣ψ) ∧ voc θ ⊆ voc φ ∩ voc ψ -#align interpolant Interpolant theorem interpolation {ϕ ψ} : Tautology (ϕ↣ψ) → ∃ θ, Interpolant ϕ ψ θ := by @@ -36,5 +34,3 @@ theorem interpolation {ϕ ψ} : Tautology (ϕ↣ψ) → ∃ θ, Interpolant ϕ constructor · rw [tautImp_iff_comboNotUnsat]; simp at *; tauto · cases pI_prop; unfold voc vocabOfSetFormula at *; simp at *; tauto -#align interpolation interpolation - diff --git a/Bml/Partitions.lean b/Bml/Partitions.lean index a633f0e..c9314c6 100644 --- a/Bml/Partitions.lean +++ b/Bml/Partitions.lean @@ -1,22 +1,19 @@ -- PARTITIONS -import Syntax -import Tableau -import Semantics -import Soundness -import Vocabulary -#align_import partitions +import Bml.Syntax +import Bml.Tableau +import Bml.Semantics +import Bml.Soundness +import Bml.Vocabulary open HasVocabulary HasSat def Partition := Finset Formula × Finset Formula -#align partition Partition -- Definition 24 def PartInterpolant (X1 X2 : Finset Formula) (θ : Formula) := voc θ ⊆ voc X1 ∩ voc X2 ∧ ¬Satisfiable (X1 ∪ {~θ}) ∧ ¬Satisfiable (X2 ∪ {θ}) -#align partInterpolant PartInterpolant -- Lemma 14 theorem botInter {X1 X2} : ⊥ ∈ X1 ∪ X2 → ∃ θ, PartInterpolant X1 X2 θ := @@ -24,21 +21,22 @@ theorem botInter {X1 X2} : ⊥ ∈ X1 ∪ X2 → ∃ θ, PartInterpolant X1 X2 intro bot_in_X refine' if side : ⊥ ∈ X1 then _ else _ · -- case ⊥ ∈ X1 - use⊥ + use ⊥ constructor - · unfold voc; unfold vocabOfFormula; simp + · unfold voc; simp; tauto constructor - all_goals by_contra h; rcases h with ⟨W, M, w1, sat⟩; specialize sat ⊥; simp at *; tauto + all_goals by_contra h; rcases h with ⟨W, M, w1, sat⟩; specialize sat ⊥; simp at * + apply sat + exact side · -- case ⊥ ∈ X2 have : ⊥ ∈ X2 := by simp at *; tauto - use~⊥ + use ~⊥ constructor - · unfold voc; unfold vocabOfFormula; simp + · unfold voc; simp; tauto constructor all_goals by_contra h; rcases h with ⟨W, M, w1, sat⟩ - · specialize sat (~~⊥); simp at *; unfold Evaluate at sat ; tauto + · specialize sat (~~⊥); simp at * · specialize sat ⊥; simp at *; tauto -#align botInter botInter theorem notInter {X1 X2 ϕ} : ϕ ∈ X1 ∪ X2 ∧ ~ϕ ∈ X1 ∪ X2 → ∃ θ, PartInterpolant X1 X2 θ := by @@ -48,11 +46,11 @@ theorem notInter {X1 X2 ϕ} : ϕ ∈ X1 ∪ X2 ∧ ~ϕ ∈ X1 ∪ X2 → ∃ θ, · use⊥ -- both in X1 constructor - · unfold voc; unfold vocabOfFormula; simp + · unfold voc; simp; tauto constructor all_goals by_contra h; rcases h with ⟨W, M, w1, sat⟩ · have h1 := sat ϕ; have h2 := sat (~ϕ); simp at *; tauto - · specialize sat ⊥; simp at *; tauto + · specialize sat ⊥; aesop · use ϕ -- ϕ ∈ X1 and ~ϕ ∈ X2 constructor @@ -82,12 +80,11 @@ theorem notInter {X1 X2 ϕ} : ϕ ∈ X1 ∪ X2 ∧ ~ϕ ∈ X1 ∪ X2 → ∃ θ, · use~⊥ -- both in X2 constructor - · unfold voc; unfold vocabOfFormula; simp + · unfold voc; simp; tauto constructor all_goals by_contra h; rcases h with ⟨W, M, w1, sat⟩ - · specialize sat (~~⊥); simp at *; unfold Evaluate at sat ; tauto + · specialize sat (~~⊥); simp at * · have h1 := sat ϕ; have h2 := sat (~ϕ); simp at *; tauto -#align notInter notInter theorem notnotInterpolantX1 {X1 X2 ϕ θ} : ~~ϕ ∈ X1 → PartInterpolant (X1 \ {~~ϕ} ∪ {ϕ}) (X2 \ {~~ϕ}) θ → PartInterpolant X1 X2 θ := @@ -102,31 +99,33 @@ theorem notnotInterpolantX1 {X1 X2 ϕ θ} : intro a aInVocTheta simp at * rw [Finset.subset_inter_iff] at vocSub - tauto + sorry -- tauto constructor - all_goals by_contra hyp; unfold satisfiable at hyp ; rcases hyp with ⟨W, M, w, sat⟩ - · have : satisfiable (X1 \ {~~ϕ} ∪ {ϕ} ∪ {~θ}) := + all_goals by_contra hyp; unfold Satisfiable at hyp ; rcases hyp with ⟨W, M, w, sat⟩ + · have : Satisfiable (X1 \ {~~ϕ} ∪ {ϕ} ∪ {~θ}) := by - unfold satisfiable + unfold Satisfiable use W, M, w intro ψ psi_in_newX_u_notTheta simp at psi_in_newX_u_notTheta cases psi_in_newX_u_notTheta - · apply sat; rw [psi_in_newX_u_notTheta]; simp at * - cases psi_in_newX_u_notTheta - · rw [psi_in_newX_u_notTheta]; apply of_not_not - change Evaluate (M, w) (~~ϕ) - apply sat (~~ϕ); simp; right; assumption + case inl psi_in_newX_u_notTheta => + apply sat; subst psi_in_newX_u_notTheta; simp at *; sorry + case inr c => + cases c + case inl psi_in_newX_u_notTheta => + rw [psi_in_newX_u_notTheta]; apply of_not_not + rw [← psi_in_newX_u_notTheta] + have := sat (~~ϕ); simp at *; aesop · apply sat; simp at *; tauto tauto - · have : satisfiable (X2 \ {~~ϕ} ∪ {θ}) := + · have : Satisfiable (X2 \ {~~ϕ} ∪ {θ}) := by - unfold satisfiable at * + unfold Satisfiable at * use W, M, w intro ψ psi_in_newX2cupTheta apply sat; simp at *; tauto tauto -#align notnotInterpolantX1 notnotInterpolantX1 theorem notnotInterpolantX2 {X1 X2 ϕ θ} : ~~ϕ ∈ X2 → PartInterpolant (X1 \ {~~ϕ}) (X2 \ {~~ϕ} ∪ {ϕ}) θ → PartInterpolant X1 X2 θ := @@ -143,9 +142,9 @@ theorem notnotInterpolantX2 {X1 X2 ϕ θ} : rw [Finset.subset_inter_iff] at vocSub tauto constructor - all_goals by_contra hyp; unfold satisfiable at hyp ; rcases hyp with ⟨W, M, w, sat⟩ + all_goals by_contra hyp; unfold Satisfiable at hyp ; rcases hyp with ⟨W, M, w, sat⟩ · apply noSatX1 - unfold satisfiable + unfold Satisfiable use W, M, w intro ψ psi_in_newX_u_notTheta simp at psi_in_newX_u_notTheta @@ -154,7 +153,7 @@ theorem notnotInterpolantX2 {X1 X2 ϕ θ} : cases psi_in_newX_u_notTheta · apply sat; simp at *; tauto · apply noSatX2 - unfold satisfiable at * + unfold Satisfiable at * use W, M, w intro ψ psi_in_newX2cupTheta simp at psi_in_newX2cupTheta @@ -166,62 +165,60 @@ theorem notnotInterpolantX2 {X1 X2 ϕ θ} : change Evaluate (M, w) (~~ϕ) apply sat (~~ϕ); simp; right; assumption · apply sat; simp at *; tauto -#align notnotInterpolantX2 notnotInterpolantX2 theorem conInterpolantX1 {X1 X2 ϕ ψ θ} : - ϕ⋏ψ ∈ X1 → PartInterpolant (X1 \ {ϕ⋏ψ} ∪ {ϕ, ψ}) (X2 \ {ϕ⋏ψ}) θ → PartInterpolant X1 X2 θ := + ϕ⋀ψ ∈ X1 → PartInterpolant (X1 \ {ϕ⋀ψ} ∪ {ϕ, ψ}) (X2 \ {ϕ⋀ψ}) θ → PartInterpolant X1 X2 θ := by intro con_in_X1 theta_is_chInt rcases theta_is_chInt with ⟨vocSub, noSatX1, noSatX2⟩ unfold PartInterpolant constructor - · rw [vocPreservedTwo (ϕ⋏ψ) ϕ ψ con_in_X1 (by unfold voc vocabOfFormula vocabOfSetFormula; simp)] - have : voc (X2 \ {ϕ⋏ψ}) ⊆ voc X2 := vocErase + · rw [vocPreservedTwo (ϕ⋀ψ) ϕ ψ con_in_X1 (by unfold voc vocabOfFormula vocabOfSetFormula; simp)] + have : voc (X2 \ {ϕ⋀ψ}) ⊆ voc X2 := vocErase intro a aInVocTheta rw [Finset.subset_inter_iff] at vocSub simp at * tauto constructor - all_goals by_contra hyp; unfold satisfiable at hyp ; rcases hyp with ⟨W, M, w, sat⟩ + all_goals by_contra hyp; unfold Satisfiable at hyp ; rcases hyp with ⟨W, M, w, sat⟩ · apply noSatX1 - unfold satisfiable + unfold Satisfiable use W, M, w intro π pi_in simp at pi_in cases pi_in · rw [pi_in]; apply sat (~θ); simp cases pi_in - · rw [pi_in]; specialize sat (ϕ⋏ψ) (by simp; exact con_in_X1); unfold Evaluate at sat ; tauto + · rw [pi_in]; specialize sat (ϕ⋀ψ) (by simp; exact con_in_X1); unfold Evaluate at sat ; tauto cases pi_in - · rw [pi_in]; specialize sat (ϕ⋏ψ) (by simp; exact con_in_X1); unfold Evaluate at sat ; tauto + · rw [pi_in]; specialize sat (ϕ⋀ψ) (by simp; exact con_in_X1); unfold Evaluate at sat ; tauto · exact sat π (by simp; tauto) · apply noSatX2 - unfold satisfiable + unfold Satisfiable use W, M, w intro π pi_in simp at pi_in cases pi_in · rw [pi_in]; apply sat θ; simp · apply sat; simp at *; tauto -#align conInterpolantX1 conInterpolantX1 theorem conInterpolantX2 {X1 X2 ϕ ψ θ} : - ϕ⋏ψ ∈ X2 → PartInterpolant (X1 \ {ϕ⋏ψ}) (X2 \ {ϕ⋏ψ} ∪ {ϕ, ψ}) θ → PartInterpolant X1 X2 θ := + ϕ⋀ψ ∈ X2 → PartInterpolant (X1 \ {ϕ⋀ψ}) (X2 \ {ϕ⋀ψ} ∪ {ϕ, ψ}) θ → PartInterpolant X1 X2 θ := by intro con_in_X2 theta_is_chInt rcases theta_is_chInt with ⟨vocSub, noSatX1, noSatX2⟩ unfold PartInterpolant constructor - · rw [vocPreservedTwo (ϕ⋏ψ) ϕ ψ con_in_X2 (by unfold voc vocabOfFormula vocabOfSetFormula; simp)] - have : voc (X1 \ {ϕ⋏ψ}) ⊆ voc X1 := vocErase + · rw [vocPreservedTwo (ϕ⋀ψ) ϕ ψ con_in_X2 (by unfold voc vocabOfFormula vocabOfSetFormula; simp)] + have : voc (X1 \ {ϕ⋀ψ}) ⊆ voc X1 := vocErase intro a aInVocTheta rw [Finset.subset_inter_iff] at vocSub simp at * tauto constructor - all_goals by_contra hyp; unfold satisfiable at hyp ; rcases hyp with ⟨W, M, w, sat⟩ + all_goals by_contra hyp; unfold Satisfiable at hyp ; rcases hyp with ⟨W, M, w, sat⟩ · apply noSatX1 - unfold satisfiable + unfold Satisfiable use W, M, w intro π pi_in simp at pi_in @@ -236,21 +233,18 @@ theorem conInterpolantX2 {X1 X2 ϕ ψ θ} : cases pi_in · rw [pi_in]; apply sat θ; simp cases pi_in - · rw [pi_in]; specialize sat (ϕ⋏ψ) (by simp; right; exact con_in_X2); unfold Evaluate at sat ; + · rw [pi_in]; specialize sat (ϕ⋀ψ) (by simp; right; exact con_in_X2); unfold Evaluate at sat ; tauto cases pi_in - · rw [pi_in]; specialize sat (ϕ⋏ψ) (by simp; right; exact con_in_X2); unfold Evaluate at sat ; + · rw [pi_in]; specialize sat (ϕ⋀ψ) (by simp; right; exact con_in_X2); unfold Evaluate at sat ; tauto · exact sat π (by simp; tauto) -#align conInterpolantX2 conInterpolantX2 -/- ./././Mathport/Syntax/Translate/Tactic/Lean3.lean:570:6: unsupported: specialize @hyp -/ -/- ./././Mathport/Syntax/Translate/Tactic/Lean3.lean:570:6: unsupported: specialize @hyp -/ theorem nCoInterpolantX1 {X1 X2 ϕ ψ θa θb} : - ~(ϕ⋏ψ) ∈ X1 → - PartInterpolant (X1 \ {~(ϕ⋏ψ)} ∪ {~ϕ}) (X2 \ {~(ϕ⋏ψ)}) θa → - PartInterpolant (X1 \ {~(ϕ⋏ψ)} ∪ {~ψ}) (X2 \ {~(ϕ⋏ψ)}) θb → - PartInterpolant X1 X2 (~(~θa⋏~θb)) := + ~(ϕ⋀ψ) ∈ X1 → + PartInterpolant (X1 \ {~(ϕ⋀ψ)} ∪ {~ϕ}) (X2 \ {~(ϕ⋀ψ)}) θa → + PartInterpolant (X1 \ {~(ϕ⋀ψ)} ∪ {~ψ}) (X2 \ {~(ϕ⋀ψ)}) θb → + PartInterpolant X1 X2 (~(~θa⋀~θb)) := by intro nCo_in_X1 tA_is_chInt tB_is_chInt rcases tA_is_chInt with ⟨a_vocSub, a_noSatX1, a_noSatX2⟩ @@ -260,17 +254,17 @@ theorem nCoInterpolantX1 {X1 X2 ϕ ψ θa θb} : · unfold voc vocabOfFormula rw [Finset.subset_inter_iff] constructor; all_goals rw [Finset.union_subset_iff] <;> constructor <;> intro a aIn - · have sub : voc (~ϕ) ⊆ voc (~(ϕ⋏ψ)) := by unfold voc vocabOfFormula; + · have sub : voc (~ϕ) ⊆ voc (~(ϕ⋀ψ)) := by unfold voc vocabOfFormula; apply Finset.subset_union_left - have claim := vocPreservedSub (~(ϕ⋏ψ)) (~ϕ) nCo_in_X1 sub + have claim := vocPreservedSub (~(ϕ⋀ψ)) (~ϕ) nCo_in_X1 sub rw [Finset.subset_iff] at claim specialize claim a rw [Finset.subset_iff] at a_vocSub specialize a_vocSub aIn finish - · have sub : voc (~ψ) ⊆ voc (~(ϕ⋏ψ)) := by unfold voc vocabOfFormula; + · have sub : voc (~ψ) ⊆ voc (~(ϕ⋀ψ)) := by unfold voc vocabOfFormula; apply Finset.subset_union_right - have claim := vocPreservedSub (~(ϕ⋏ψ)) (~ψ) nCo_in_X1 sub + have claim := vocPreservedSub (~(ϕ⋀ψ)) (~ψ) nCo_in_X1 sub rw [Finset.subset_iff] at claim specialize claim a rw [Finset.subset_iff] at b_vocSub @@ -278,13 +272,13 @@ theorem nCoInterpolantX1 {X1 X2 ϕ ψ θa θb} : finish · rw [Finset.subset_iff] at a_vocSub specialize a_vocSub aIn - have : voc (X2 \ {~(ϕ⋏ψ)}) ⊆ voc X2 := vocErase + have : voc (X2 \ {~(ϕ⋀ψ)}) ⊆ voc X2 := vocErase unfold voc at * simp at * tauto · rw [Finset.subset_iff] at b_vocSub specialize b_vocSub aIn - have : voc (X2 \ {~(ϕ⋏ψ)}) ⊆ voc X2 := vocErase + have : voc (X2 \ {~(ϕ⋀ψ)}) ⊆ voc X2 := vocErase unfold voc at * simp at * tauto @@ -296,7 +290,7 @@ theorem nCoInterpolantX1 {X1 X2 ϕ ψ θa θb} : intro π pi_in simp at pi_in cases pi_in - · rw [pi_in]; specialize sat (~~(~θa⋏~θb)); simp at sat ; unfold Evaluate at *; simp at sat ; + · rw [pi_in]; specialize sat (~~(~θa⋀~θb)); simp at sat ; unfold Evaluate at *; simp at sat ; tauto cases pi_in · rw [pi_in] @@ -306,10 +300,10 @@ theorem nCoInterpolantX1 {X1 X2 ϕ ψ θa θb} : intro χ chi_in simp at chi_in cases chi_in - · rw [chi_in]; specialize sat (~~(~θa⋏~θb)); simp at sat ; unfold Evaluate at *; simp at sat ; + · rw [chi_in]; specialize sat (~~(~θa⋀~θb)); simp at sat ; unfold Evaluate at *; simp at sat ; tauto cases chi_in - · rw [chi_in]; specialize sat (~(ϕ⋏ψ)) (by simp; exact nCo_in_X1); unfold Evaluate at *; + · rw [chi_in]; specialize sat (~(ϕ⋀ψ)) (by simp; exact nCo_in_X1); unfold Evaluate at *; simp at *; tauto · apply sat; simp; tauto · apply sat; simp; tauto @@ -326,18 +320,17 @@ theorem nCoInterpolantX1 {X1 X2 ϕ ψ θa θb} : intro χ chi_in simp at chi_in cases chi_in - · rw [chi_in]; specialize sat (~(~θa⋏~θb)); simp at sat ; unfold Evaluate at *; simp at sat ; + · rw [chi_in]; specialize sat (~(~θa⋀~θb)); simp at sat ; unfold Evaluate at *; simp at sat ; tauto · apply sat; simp; tauto · apply sat; simp; tauto -#align nCoInterpolantX1 nCoInterpolantX1 /- ./././Mathport/Syntax/Translate/Tactic/Lean3.lean:570:6: unsupported: specialize @hyp -/ /- ./././Mathport/Syntax/Translate/Tactic/Lean3.lean:570:6: unsupported: specialize @hyp -/ theorem nCoInterpolantX2 {X1 X2 ϕ ψ θa θb} : - ~(ϕ⋏ψ) ∈ X2 → - PartInterpolant (X1 \ {~(ϕ⋏ψ)}) (X2 \ {~(ϕ⋏ψ)} ∪ {~ϕ}) θa → - PartInterpolant (X1 \ {~(ϕ⋏ψ)}) (X2 \ {~(ϕ⋏ψ)} ∪ {~ψ}) θb → PartInterpolant X1 X2 (θa⋏θb) := + ~(ϕ⋀ψ) ∈ X2 → + PartInterpolant (X1 \ {~(ϕ⋀ψ)}) (X2 \ {~(ϕ⋀ψ)} ∪ {~ϕ}) θa → + PartInterpolant (X1 \ {~(ϕ⋀ψ)}) (X2 \ {~(ϕ⋀ψ)} ∪ {~ψ}) θb → PartInterpolant X1 X2 (θa⋀θb) := by intro nCo_in_X2 tA_is_chInt tB_is_chInt rcases tA_is_chInt with ⟨a_vocSub, a_noSatX1, a_noSatX2⟩ @@ -349,73 +342,72 @@ theorem nCoInterpolantX2 {X1 X2 ϕ ψ θa θb} : constructor; all_goals rw [Finset.union_subset_iff] <;> constructor <;> intro a aIn · rw [Finset.subset_iff] at a_vocSub specialize a_vocSub aIn - have claim : voc (X1 \ {~(ϕ⋏ψ)}) ⊆ voc X1 := vocErase + have claim : voc (X1 \ {~(ϕ⋀ψ)}) ⊆ voc X1 := vocErase unfold voc at claim simp at * tauto · rw [Finset.subset_iff] at b_vocSub specialize b_vocSub aIn - have claim : voc (X1 \ {~(ϕ⋏ψ)}) ⊆ voc X1 := vocErase + have claim : voc (X1 \ {~(ϕ⋀ψ)}) ⊆ voc X1 := vocErase unfold voc at claim simp at * tauto - · have sub : voc (~ϕ) ⊆ voc (~(ϕ⋏ψ)) := by unfold voc vocabOfFormula; + · have sub : voc (~ϕ) ⊆ voc (~(ϕ⋀ψ)) := by unfold voc vocabOfFormula; apply Finset.subset_union_left - have claim := vocPreservedSub (~(ϕ⋏ψ)) (~ϕ) nCo_in_X2 sub + have claim := vocPreservedSub (~(ϕ⋀ψ)) (~ϕ) nCo_in_X2 sub rw [Finset.subset_iff] at claim specialize claim a rw [Finset.subset_iff] at a_vocSub specialize a_vocSub aIn finish - · have sub : voc (~ψ) ⊆ voc (~(ϕ⋏ψ)) := by unfold voc vocabOfFormula; + · have sub : voc (~ψ) ⊆ voc (~(ϕ⋀ψ)) := by unfold voc vocabOfFormula; apply Finset.subset_union_right - have claim := vocPreservedSub (~(ϕ⋏ψ)) (~ψ) nCo_in_X2 sub + have claim := vocPreservedSub (~(ϕ⋀ψ)) (~ψ) nCo_in_X2 sub rw [Finset.subset_iff] at claim specialize claim a rw [Finset.subset_iff] at b_vocSub specialize b_vocSub aIn finish constructor - all_goals by_contra hyp; unfold satisfiable at hyp ; rcases hyp with ⟨W, M, w, sat⟩ + all_goals by_contra hyp; unfold Satisfiable at hyp ; rcases hyp with ⟨W, M, w, sat⟩ · apply a_noSatX1 - unfold satisfiable + unfold Satisfiable use W, M, w intro π pi_in simp at pi_in cases pi_in · rw [pi_in] by_contra; apply b_noSatX1 - unfold satisfiable + unfold Satisfiable use W, M, w intro χ chi_in simp at chi_in cases chi_in - · rw [chi_in]; specialize sat (~(θa⋏θb)); simp at sat ; unfold Evaluate at *; simp at sat ; + · rw [chi_in]; specialize sat (~(θa⋀θb)); simp at sat ; unfold Evaluate at *; simp at sat ; simp at h ; tauto · apply sat; simp; tauto · apply sat; simp; tauto · apply a_noSatX2 - unfold satisfiable + unfold Satisfiable use W, M, w intro π pi_in simp at pi_in cases pi_in - · rw [pi_in]; specialize sat (θa⋏θb); simp at sat ; unfold Evaluate at *; tauto + · rw [pi_in]; specialize sat (θa⋀θb); simp at sat ; unfold Evaluate at *; tauto cases pi_in · rw [pi_in] by_contra; apply b_noSatX2 - unfold satisfiable + unfold Satisfiable use W, M, w intro χ chi_in simp at chi_in cases chi_in - · rw [chi_in]; specialize sat (θa⋏θb); simp at sat ; unfold Evaluate at *; tauto + · rw [chi_in]; specialize sat (θa⋀θb); simp at sat ; unfold Evaluate at *; tauto cases chi_in - · rw [chi_in]; specialize sat (~(ϕ⋏ψ)); simp at sat ; unfold Evaluate at *; simp at sat ; + · rw [chi_in]; specialize sat (~(ϕ⋀ψ)); simp at sat ; unfold Evaluate at *; simp at sat ; simp at h ; tauto · apply sat; simp; tauto · apply sat; simp; tauto -#align nCoInterpolantX2 nCoInterpolantX2 theorem localTabToInt : ∀ n X, @@ -496,17 +488,17 @@ theorem localTabToInt : exact notnotInterpolantX2 notnotphi_in_union theta_is_chInt case con X ϕ ψ con_in_X => - have con_in_union : ϕ⋏ψ ∈ X1 ∨ ϕ⋏ψ ∈ X2 := by rw [defX] at con_in_X ; simp at con_in_X ; + have con_in_union : ϕ⋀ψ ∈ X1 ∨ ϕ⋀ψ ∈ X2 := by rw [defX] at con_in_X ; simp at con_in_X ; assumption cases con_in_union - · -- case ϕ⋏ψ ∈ X1 + · -- case ϕ⋀ψ ∈ X1 subst defX - let newX1 := X1 \ {ϕ⋏ψ} ∪ {ϕ, ψ} - let newX2 := X2 \ {ϕ⋏ψ} - have yclaim : newX1 ∪ newX2 ∈ {(X1 ∪ X2) \ {ϕ⋏ψ} ∪ {ϕ, ψ}} := + let newX1 := X1 \ {ϕ⋀ψ} ∪ {ϕ, ψ} + let newX2 := X2 \ {ϕ⋀ψ} + have yclaim : newX1 ∪ newX2 ∈ {(X1 ∪ X2) \ {ϕ⋀ψ} ∪ {ϕ, ψ}} := by rw [Finset.mem_singleton] - change X1 \ {ϕ⋏ψ} ∪ {ϕ, ψ} ∪ X2 \ {ϕ⋏ψ} = (X1 ∪ X2) \ {ϕ⋏ψ} ∪ {ϕ, ψ} + change X1 \ {ϕ⋀ψ} ∪ {ϕ, ψ} ∪ X2 \ {ϕ⋀ψ} = (X1 ∪ X2) \ {ϕ⋀ψ} ∪ {ϕ, ψ} ext1 a; constructor <;> · intro hyp; simp at hyp ; simp; tauto set m := lengthOfSet (newX1 ∪ newX2) have m_lt_n : m < n := by @@ -529,14 +521,14 @@ theorem localTabToInt : cases' childInt with θ theta_is_chInt use θ exact conInterpolantX1 con_in_union theta_is_chInt - · -- case ϕ⋏ψ ∈ X2 + · -- case ϕ⋀ψ ∈ X2 subst defX - let newX1 := X1 \ {ϕ⋏ψ} - let newX2 := X2 \ {ϕ⋏ψ} ∪ {ϕ, ψ} - have yclaim : newX1 ∪ newX2 ∈ {(X1 ∪ X2) \ {ϕ⋏ψ} ∪ {ϕ, ψ}} := + let newX1 := X1 \ {ϕ⋀ψ} + let newX2 := X2 \ {ϕ⋀ψ} ∪ {ϕ, ψ} + have yclaim : newX1 ∪ newX2 ∈ {(X1 ∪ X2) \ {ϕ⋀ψ} ∪ {ϕ, ψ}} := by rw [Finset.mem_singleton] - change X1 \ {ϕ⋏ψ} ∪ (X2 \ {ϕ⋏ψ} ∪ {ϕ, ψ}) = (X1 ∪ X2) \ {ϕ⋏ψ} ∪ {ϕ, ψ} + change X1 \ {ϕ⋀ψ} ∪ (X2 \ {ϕ⋀ψ} ∪ {ϕ, ψ}) = (X1 ∪ X2) \ {ϕ⋀ψ} ∪ {ϕ, ψ} ext1 a; constructor <;> · intro hyp; simp at hyp ; simp; tauto set m := lengthOfSet (newX1 ∪ newX2) have m_lt_n : m < n := by @@ -561,18 +553,18 @@ theorem localTabToInt : exact conInterpolantX2 con_in_union theta_is_chInt case nCo X ϕ ψ nCo_in_X => - have nCo_in_union : ~(ϕ⋏ψ) ∈ X1 ∨ ~(ϕ⋏ψ) ∈ X2 := by rw [defX] at nCo_in_X ; simp at nCo_in_X ; + have nCo_in_union : ~(ϕ⋀ψ) ∈ X1 ∨ ~(ϕ⋀ψ) ∈ X2 := by rw [defX] at nCo_in_X ; simp at nCo_in_X ; assumption cases nCo_in_union - · -- case ~(ϕ⋏ψ) ∈ X1 + · -- case ~(ϕ⋀ψ) ∈ X1 subst defX -- splitting rule! -- first get an interpolant for the ~ϕ branch: - let a_newX1 := X1 \ {~(ϕ⋏ψ)} ∪ {~ϕ} - let a_newX2 := X2 \ {~(ϕ⋏ψ)} + let a_newX1 := X1 \ {~(ϕ⋀ψ)} ∪ {~ϕ} + let a_newX2 := X2 \ {~(ϕ⋀ψ)} have a_yclaim : a_newX1 ∪ a_newX2 ∈ - ({(X1 ∪ X2) \ {~(ϕ⋏ψ)} ∪ {~ϕ}, (X1 ∪ X2) \ {~(ϕ⋏ψ)} ∪ {~ψ}} : + ({(X1 ∪ X2) \ {~(ϕ⋀ψ)} ∪ {~ϕ}, (X1 ∪ X2) \ {~(ϕ⋀ψ)} ∪ {~ψ}} : Finset (Finset Formula)) := by simp; left; ext1 a; constructor <;> · intro hyp; simp at hyp ; simp; tauto set a_m := lengthOfSet (a_newX1 ∪ a_newX2) @@ -592,11 +584,11 @@ theorem localTabToInt : exact ⟨a_newX1 ∪ a_newX2, a_yclaim, Y_in⟩ cases' a_childInt with θa a_theta_is_chInt -- now get an interpolant for the ~ψ branch: - let b_newX1 := X1 \ {~(ϕ⋏ψ)} ∪ {~ψ} - let b_newX2 := X2 \ {~(ϕ⋏ψ)} + let b_newX1 := X1 \ {~(ϕ⋀ψ)} ∪ {~ψ} + let b_newX2 := X2 \ {~(ϕ⋀ψ)} have b_yclaim : b_newX1 ∪ b_newX2 ∈ - ({(X1 ∪ X2) \ {~(ϕ⋏ψ)} ∪ {~ϕ}, (X1 ∪ X2) \ {~(ϕ⋏ψ)} ∪ {~ψ}} : + ({(X1 ∪ X2) \ {~(ϕ⋀ψ)} ∪ {~ϕ}, (X1 ∪ X2) \ {~(ϕ⋀ψ)} ∪ {~ψ}} : Finset (Finset Formula)) := by simp; right; ext1 a; constructor <;> · intro hyp; simp at hyp ; simp; tauto set b_m := lengthOfSet (b_newX1 ∪ b_newX2) @@ -616,17 +608,17 @@ theorem localTabToInt : exact ⟨b_newX1 ∪ b_newX2, b_yclaim, Y_in⟩ cases' b_childInt with θb b_theta_is_chInt -- finally, combine the two interpolants using disjunction: - use~(~θa⋏~θb) + use~(~θa⋀~θb) exact nCoInterpolantX1 nCo_in_union a_theta_is_chInt b_theta_is_chInt - · -- case ~(ϕ⋏ψ) ∈ X2 + · -- case ~(ϕ⋀ψ) ∈ X2 subst defX -- splitting rule! -- first get an interpolant for the ~ϕ branch: - let a_newX1 := X1 \ {~(ϕ⋏ψ)} - let a_newX2 := X2 \ {~(ϕ⋏ψ)} ∪ {~ϕ} + let a_newX1 := X1 \ {~(ϕ⋀ψ)} + let a_newX2 := X2 \ {~(ϕ⋀ψ)} ∪ {~ϕ} have a_yclaim : a_newX1 ∪ a_newX2 ∈ - ({(X1 ∪ X2) \ {~(ϕ⋏ψ)} ∪ {~ϕ}, (X1 ∪ X2) \ {~(ϕ⋏ψ)} ∪ {~ψ}} : + ({(X1 ∪ X2) \ {~(ϕ⋀ψ)} ∪ {~ϕ}, (X1 ∪ X2) \ {~(ϕ⋀ψ)} ∪ {~ψ}} : Finset (Finset Formula)) := by simp; left; ext1 a; constructor <;> · intro hyp; simp at hyp ; simp; tauto set a_m := lengthOfSet (a_newX1 ∪ a_newX2) @@ -646,11 +638,11 @@ theorem localTabToInt : exact ⟨a_newX1 ∪ a_newX2, a_yclaim, Y_in⟩ cases' a_childInt with θa a_theta_is_chInt -- now get an interpolant for the ~ψ branch: - let b_newX1 := X1 \ {~(ϕ⋏ψ)} - let b_newX2 := X2 \ {~(ϕ⋏ψ)} ∪ {~ψ} + let b_newX1 := X1 \ {~(ϕ⋀ψ)} + let b_newX2 := X2 \ {~(ϕ⋀ψ)} ∪ {~ψ} have b_yclaim : b_newX1 ∪ b_newX2 ∈ - ({(X1 ∪ X2) \ {~(ϕ⋏ψ)} ∪ {~ϕ}, (X1 ∪ X2) \ {~(ϕ⋏ψ)} ∪ {~ψ}} : + ({(X1 ∪ X2) \ {~(ϕ⋀ψ)} ∪ {~ϕ}, (X1 ∪ X2) \ {~(ϕ⋀ψ)} ∪ {~ψ}} : Finset (Finset Formula)) := by simp; right; ext1 a; constructor <;> · intro hyp; simp at hyp ; simp; tauto set b_m := lengthOfSet (b_newX1 ∪ b_newX2) @@ -670,31 +662,29 @@ theorem localTabToInt : exact ⟨b_newX1 ∪ b_newX2, b_yclaim, Y_in⟩ cases' b_childInt with θb b_theta_is_chInt -- finally, combine the two interpolants using conjunction: - use θa⋏θb + use θa⋀θb exact nCoInterpolantX2 nCo_in_union a_theta_is_chInt b_theta_is_chInt case sim X X_is_simple => apply nextInter unfold endNodesOf rw [defX]; simp -#align localTabToInt localTabToInt theorem vocProj (X) : voc (projection X) ⊆ voc X := by - unfold voc vocabOfFormula vocabOfSetFormula simp intro ϕ phi_in_proj rw [proj] at phi_in_proj intro a aInVocPhi simp tauto -#align vocProj vocProj theorem projUnion {X Y} : projection (X ∪ Y) = projection X ∪ projection Y := by - unfold projection Finset.biUnion ext1 - constructor <;> finish -#align projUnion projUnion + rw [proj] + simp + rw [proj] + rw [proj] open HasLength @@ -724,8 +714,7 @@ theorem almostTabToInt {X} (ctX : ClosedTableau X) : · -- case ~□ϕ ∈ X1 let newX1 := projection X1 ∪ {~ϕ} let newX2 := projection X2 - have yclaim : newX1 ∪ newX2 = projection (X1 ∪ X2) ∪ {~ϕ} := by rw [projUnion]; ext1; simp; - tauto + have yclaim : newX1 ∪ newX2 = projection (X1 ∪ X2) ∪ {~ϕ} := by rw [projUnion]; ext1; simp rw [← yclaim] at ctProjNotPhi have nextInt : ∃ θ, PartInterpolant newX1 newX2 θ := IH newX1 newX2 (by rw [yclaim]; simp) rcases nextInt with ⟨θ, vocSub, unsat1, unsat2⟩ @@ -734,7 +723,7 @@ theorem almostTabToInt {X} (ctX : ClosedTableau X) : -- it remains to show the three properties of the interpolant · change voc θ ⊆ voc X1 ∩ voc X2 have inc1 : voc newX1 ⊆ voc X1 := by - intro a aIn; unfold voc vocabOfSetFormula Finset.biUnion at *; simp at * + intro a aIn; unfold voc formulaHasVocabulary setFormulaHasVocabulary at *; simp at * rcases aIn with ⟨ψ, psi_in_projX1 | psi_is_notPhi⟩ · use□ψ; change □ψ ∈ X1 ∧ a ∈ voc (□ψ); rw [← proj]; tauto · use~(□ϕ); subst psi_is_notPhi; tauto @@ -747,7 +736,7 @@ theorem almostTabToInt {X} (ctX : ClosedTableau X) : constructor apply inc1; tauto apply inc2; tauto - all_goals unfold satisfiable at * + all_goals unfold Satisfiable at * · by_contra hyp rcases hyp with ⟨W, M, w, sat⟩ apply unsat1 @@ -761,7 +750,8 @@ theorem almostTabToInt {X} (ctX : ClosedTableau X) : intro ψ psi_in_newX1 simp at psi_in_newX1 cases psi_in_newX1 - · subst psi_in_newX1; specialize sat (~~(□~θ)); unfold Evaluate at *; simp at sat ; + case inl psi_in_newX1 => + subst psi_in_newX1; specialize sat (~~(□~θ)); simp at *; exact sat v rel_w_v cases psi_in_newX1 · rw [proj] at psi_in_newX1 ; specialize sat (□ψ); unfold Evaluate at sat ; apply sat; simp; @@ -811,7 +801,7 @@ theorem almostTabToInt {X} (ctX : ClosedTableau X) : constructor apply inc1; tauto apply inc2; tauto - all_goals unfold satisfiable at * + all_goals unfold Satisfiable at * · by_contra hyp rcases hyp with ⟨W, M, w, sat⟩ apply unsat1 @@ -847,9 +837,6 @@ theorem almostTabToInt {X} (ctX : ClosedTableau X) : · rw [proj] at psi_in_newX2 ; specialize sat (□ψ); simp at sat ; unfold Evaluate at sat ; apply sat; right; assumption; assumption · rw [psi_in_newX2]; unfold Evaluate; assumption -#align almostTabToInt almostTabToInt theorem tabToInt {X1 X2} : ClosedTableau (X1 ∪ X2) → ∃ θ, PartInterpolant X1 X2 θ | ctX => almostTabToInt ctX X1 X2 (refl _) -#align tabToInt tabToInt - diff --git a/Bml/Soundness.lean b/Bml/Soundness.lean index b284574..d55ad9e 100644 --- a/Bml/Soundness.lean +++ b/Bml/Soundness.lean @@ -1,12 +1,11 @@ -- SOUNDNESS -import Syntax -import Tableau -#align_import soundness +import Bml.Syntax +import Bml.Tableau open Classical -attribute [local instance 10] prop_decidable +-- attribute [local instance 10] prop_decidable -- delete me? open HasSat @@ -21,26 +20,23 @@ def combinedModel {β : Type} (collection : β → Σ W : Type, KripkeModel W × · -- making the valuation function: intro world cases world - · -- the one new world: - cases world - exact newVal - -- use new given valuation here!! - · -- world in one of the given models: - cases' world with R w + case inl newWorld => -- the one new world + cases newWorld + exact newVal -- use new given valuation here!! + case inr oldWorld => -- world in one of the given models: + cases' oldWorld with R w exact (collection R).snd.fst.val w · -- defining relations: intro worldOne worldTwo - cases worldOne <;> cases worldTwo - -- four cases about two new or old worlds: - · exact False - -- no reflexive loop at the new world. - · exact HEq worldTwo.snd (collection worldTwo.fst).snd.snd - -- conect new world to given points. - · exact False - -- no connection from models to new world - · -- connect two old worlds iff they are from the same model and were connected there already: - cases' worldOne with kOne wOne - cases' worldTwo with kTwo wTwo + cases worldOne <;> cases worldTwo -- four cases about two new or old worlds + case inl.inl => exact False -- no reflexive loop at the new world. + case inl.inr newWorld oldWorld => + exact HEq oldWorld.snd (collection oldWorld.fst).snd.snd -- conect new world to given points. + case inr.inl => exact False -- no connection from models to new world + case inr.inr oldWorldOne oldWorldTwo => + -- connect two old worlds iff they are from the same model and were connected there already: + cases' oldWorldOne with kOne wOne + cases' oldWorldTwo with kTwo wTwo have help : kOne = kTwo → Prop := by intro same have sameCol : collection kOne = collection kTwo := by rw [← same] @@ -50,7 +46,6 @@ def combinedModel {β : Type} (collection : β → Σ W : Type, KripkeModel W × · -- point at the new world: left exact () -#align combinedModel combinedModel -- The combined model preserves all truths at the old worlds. theorem combMo_preserves_truth_at_oldWOrld {β : Type} @@ -61,14 +56,14 @@ theorem combMo_preserves_truth_at_oldWOrld {β : Type} by intro f induction f <;> intro R oldWorld - case bottom => finish + case bottom => aesop case atom_prop c => unfold combinedModel - unfold Evaluate + simp case neg f f_IH => unfold Evaluate rw [f_IH R oldWorld] - case and f g f_IH g_IH => + case And f g f_IH g_IH => unfold Evaluate rw [f_IH R oldWorld] rw [g_IH R oldWorld] @@ -97,14 +92,13 @@ theorem combMo_preserves_truth_at_oldWOrld {β : Type} unfold combinedModel at rel_in_new_model have sameR : R = otherR := by by_contra - classical finish + aesop subst sameR rw [f_IH] apply true_in_old -- remains to show that related in old model simp at * exact rel_in_new_model -#align combMo_preserves_truth_at_oldWOrld combMo_preserves_truth_at_oldWOrld -- The combined model for X satisfies X. theorem combMo_sat_X {X : Finset Formula} {β : Set Formula} @@ -131,7 +125,7 @@ theorem combMo_sat_X {X : Finset Formula} {β : Set Formula} simp exact f_in_X case - neg => + neg f => -- subcases :-/ cases f case atom_prop => @@ -150,14 +144,15 @@ theorem combMo_sat_X {X : Finset Formula} {β : Set Formula} ((combinedModel collection fun c => (·c) ∈ X).fst, (combinedModel collection fun c : Char => (·c) ∈ X).snd) (~(□newf)) - unfold Evaluate - rw [Classical.not_forall] + simp -- need a reachable world where newf holds, choose the witness let h : newf ∈ β := by rw [beta_def] use f_in_X let oldWorld : Sum Unit (Σ k : β, (collection k).fst) := Sum.inr ⟨⟨newf, h⟩, (collection ⟨newf, h⟩).snd.snd⟩ + sorry + /- use oldWorld simp constructor @@ -173,38 +168,42 @@ theorem combMo_sat_X {X : Finset Formula} {β : Set Formula} unfold Evaluate at all_pro_sat simp at * exact all_pro_sat + -/ case bottom => tauto - all_goals + case neg f => unfold Simple at simple_X - by_contra - exact simple_X _ f_in_X - case and fa fb => + simp at * + sorry + case And f g => + sorry + case And fa fb => unfold Simple at simple_X - by_contra - exact simple_X (fa⋏fb) f_in_X + simp at simple_X + sorry + -- apply all_pro_sat + -- exact simple_X (fa⋀fb) f_in_X case box f => unfold Evaluate intro otherWorld is_rel cases otherWorld · cases is_rel - -- otherWorld cannot be the (unreachable) new world - have coMoLemma := - combMo_preserves_truth_at_oldWOrld collection (fun c => (·c) ∈ X) f otherWorld.fst - otherWorld.snd - simp at coMoLemma - rw [coMoLemma] - specialize all_pro_sat otherWorld.fst f - simp at all_pro_sat - rw [or_imp] at all_pro_sat - cases' all_pro_sat with _ all_pro_sat_right - rw [← proj] at f_in_X - specialize all_pro_sat_right f_in_X - have sameWorld : otherWorld.snd = (collection otherWorld.fst).snd.snd := by - rw [heq_iff_eq.mp (HEq.symm is_rel)] - rw [sameWorld] - simp - exact all_pro_sat_right -#align combMo_sat_X combMo_sat_X + case inr otherWorld => -- otherWorld cannot be the (unreachable) new world + have coMoLemma := + combMo_preserves_truth_at_oldWOrld collection (fun c => (·c) ∈ X) f otherWorld.fst + otherWorld.snd + simp at coMoLemma + rw [coMoLemma] + specialize all_pro_sat otherWorld.fst f + simp at all_pro_sat + rw [or_imp] at all_pro_sat + cases' all_pro_sat with _ all_pro_sat_right + rw [← proj] at f_in_X + specialize all_pro_sat_right f_in_X + have sameWorld : otherWorld.snd = (collection otherWorld.fst).snd.snd := by + rw [heq_iff_eq.mp (HEq.symm is_rel)] + rw [sameWorld] + simp + exact all_pro_sat_right -- Lemma 1 (page 16) -- A simple set of formulas X is satisfiable if and only if @@ -216,7 +215,7 @@ theorem Lemma1_simple_sat_iff_all_projections_sat {X : Finset Formula} : constructor · -- left to right intro sat_X - unfold satisfiable at * + unfold Satisfiable at * rcases sat_X with ⟨W, M, w, w_sat_X⟩ constructor · -- show that X is not closed: @@ -227,7 +226,6 @@ theorem Lemma1_simple_sat_iff_all_projections_sat {X : Finset Formula} : · rcases f_and_notf_in_X with ⟨f, f_in_X, notf_in_X⟩ let w_sat_f := w_sat_X f f_in_X let w_sat_notf := w_sat_X (~f) notf_in_X - unfold Evaluate at * exact absurd w_sat_f w_sat_notf · -- show that for each ~[]R ∈ X the projection with ~R is satisfiable: intro R notboxr_in_X @@ -251,7 +249,7 @@ theorem Lemma1_simple_sat_iff_all_projections_sat {X : Finset Formula} : · -- right to left intro rhs cases' rhs with not_closed_X all_pro_sat - unfold satisfiable at * + unfold Satisfiable at * -- Let's build a new Kripke model! let β := {R : Formula | ~(□R) ∈ X} -- beware, using Axioms of Choice here! @@ -286,12 +284,12 @@ theorem Lemma1_simple_sat_iff_all_projections_sat {X : Finset Formula} : exact this_pro_sat_l f_inpro · -- case where f is ~[]R cases f_is_notboxR - specialize this_pro_sat (~R) - rw [or_imp] at this_pro_sat - cases' this_pro_sat with this_pro_sat_l this_pro_sat_r - exact this_pro_sat_r f_is_notboxR + case refl => + specialize this_pro_sat (~R) + rw [or_imp] at this_pro_sat + cases' this_pro_sat with this_pro_sat_l this_pro_sat_r + tauto simp -#align Lemma1_simple_sat_iff_all_projections_sat Lemma1_simple_sat_iff_all_projections_sat -- to check β -- Each rule is sound and preserves satisfiability "downwards" @@ -300,15 +298,15 @@ theorem localRuleSoundness {α : Finset Formula} {B : Finset (Finset Formula)} : by intro r intro a_sat - unfold satisfiable at a_sat + unfold Satisfiable at a_sat rcases a_sat with ⟨W, M, w, w_sat_a⟩ cases r - case bot a bot_in_a => + case bot bot_in_a => by_contra let w_sat_bot := w_sat_a ⊥ bot_in_a unfold Evaluate at w_sat_bot exact w_sat_bot - case not a f hyp => + case Not f hyp => by_contra have w_sat_f : Evaluate (M, w) f := by apply w_sat_a @@ -317,60 +315,53 @@ theorem localRuleSoundness {α : Finset Formula} {B : Finset (Finset Formula)} : by apply w_sat_a (~f) exact hyp.right - unfold Evaluate at * + simp at * exact absurd w_sat_f w_sat_not_f - case neg a f + case neg f hyp => have w_sat_f : Evaluate (M, w) f := by specialize w_sat_a (~~f) hyp - unfold Evaluate at * - finish - use a \ {~~f} ∪ {f} - simp only [true_and_iff, eq_self_iff_true, sdiff_singleton_is_erase, Multiset.mem_singleton, - Finset.mem_mk] - unfold satisfiable + aesop + use α \ {~~f} ∪ {f} + simp use W, M, w - intro g - simp only [Ne.def, union_singleton_is_insert, Finset.mem_insert, Finset.mem_erase] - rw [or_imp] constructor - · intro g_is_f; rw [g_is_f]; apply w_sat_f - · rw [and_imp] - intro g_neq_notnotf g_in_a + · exact w_sat_f + · intro g_neq_notnotf g_in_a apply w_sat_a - exact g_in_a - case con a f g hyp => - use a \ {f⋏g} ∪ {f, g} + case Con f g hyp => + use α \ {f⋀g} ∪ {f, g} constructor simp - unfold satisfiable + unfold Satisfiable use W, M, w simp only [and_imp, forall_eq_or_imp, sdiff_singleton_is_erase, Ne.def, Finset.union_insert, Finset.mem_insert, Finset.mem_erase] constructor · -- f - specialize w_sat_a (f⋏g) hyp - unfold Evaluate at * + specialize w_sat_a (f⋀g) hyp + simp at * exact w_sat_a.left · intro h hhyp simp at hhyp cases hhyp - · -- h = g - specialize w_sat_a (f⋏g) hyp - unfold Evaluate at * - rw [hhyp] + case inl h_is_g => -- h = g + specialize w_sat_a (f⋀g) hyp + simp at * + rw [h_is_g] exact w_sat_a.right - ·-- h in a - exact w_sat_a h hhyp.right - case nCo a f g notfandg_in_a => - unfold satisfiable - simp - let w_sat_phi := w_sat_a (~(f⋏g)) notfandg_in_a - unfold Evaluate at w_sat_phi - rw [not_and_or] at w_sat_phi + case inr h_in_a => -- h in a + exact w_sat_a h h_in_a.right + case nCo f g notfandg_in_a => + unfold Satisfiable + let w_sat_phi := w_sat_a (~(f⋀g)) notfandg_in_a + simp [Evaluate] at w_sat_phi + rw [imp_iff_not_or] at w_sat_phi cases' w_sat_phi with not_w_f not_w_g - · use a \ {~(f⋏g)} ∪ {~f} + · use α \ {~(f⋀g)} ∪ {~f} + sorry + · use α \ {~(f⋀g)} ∪ {~g} constructor · simp at * · use W, M, w @@ -378,34 +369,22 @@ theorem localRuleSoundness {α : Finset Formula} {B : Finset (Finset Formula)} : simp intro psi_def cases psi_def - · rw [psi_def] - unfold Evaluate - exact not_w_f - · cases' psi_def with psi_in_a - exact w_sat_a psi psi_def_right - · use a \ {~(f⋏g)} ∪ {~g} - constructor - · simp at * - · use W, M, w - intro psi - simp - intro psi_def - cases psi_def - · rw [psi_def] + case inl psi_def => + rw [psi_def] unfold Evaluate exact not_w_g - · cases' psi_def with psi_in_a + case inr psi_def => + cases' psi_def with psi_in_a psi_def_right exact w_sat_a psi psi_def_right -#align localRuleSoundness localRuleSoundness -- The critical roule is sound and preserves satisfiability "downwards". -- TODO: is this the same as (one of the directions of) Lemma 1 ?? theorem atmSoundness {α : Finset Formula} {f} (not_box_f_in_a : ~(□f) ∈ α) : Simple α → Satisfiable α → Satisfiable (projection α ∪ {~f}) := by - intro s + intro _s -- sus?! intro aSat - unfold satisfiable at aSat + unfold Satisfiable at aSat rcases aSat with ⟨W, M, w, w_sat_a⟩ constructor simp @@ -417,15 +396,13 @@ theorem atmSoundness {α : Finset Formula} {f} (not_box_f_in_a : ~(□f) ∈ α) -- show that the projection is satisfiable: use M, v constructor - · unfold Evaluate - exact v_not_sat_f + · exact v_not_sat_f intro phi phi_in_proj rw [proj] at phi_in_proj · specialize w_sat_a phi.box _ exact phi_in_proj unfold Evaluate at w_sat_a exact w_sat_a v w_rel_v -#align atmSoundness atmSoundness theorem localTableauAndEndNodesUnsatThenNotSat {Z} (ltZ : LocalTableau Z) : (∀ Y, Y ∈ endNodesOf ⟨Z, ltZ⟩ → ¬Satisfiable Y) → ¬Satisfiable Z := @@ -445,35 +422,28 @@ theorem localTableauAndEndNodesUnsatThenNotSat {Z} (ltZ : LocalTableau Z) : simp only [endNodesOf, Finset.mem_biUnion, Finset.mem_attach, exists_true_left, Subtype.exists] use Y, Y_in_YS - assumption - have endsOfYnotSat : ∀ Y_1 : Finset Formula, Y_1 ∈ endNodesOf ⟨Y, ltY⟩ → ¬satisfiable Y_1 := + have endsOfYnotSat : ∀ Y_1 : Finset Formula, Y_1 ∈ endNodesOf ⟨Y, ltY⟩ → ¬Satisfiable Y_1 := by intro W W_is_endOf_Y apply endsOfXnotSat W (endNodesInclusion W W_is_endOf_Y) - finish + aesop case sim X X_is_simple => apply endsOfXnotSat unfold endNodesOf simp -#align localTableauAndEndNodesUnsatThenNotSat localTableauAndEndNodesUnsatThenNotSat theorem tableauThenNotSat : ∀ X, ClosedTableau X → ¬Satisfiable X := by intro X t induction t - case loc Y ltY next IH => + case loc Y ltY _ IH => apply localTableauAndEndNodesUnsatThenNotSat ltY intro Z ZisEndOfY exact IH Z ZisEndOfY - case atm Y ϕ notBoxPhiInY Y_is_simple - ltProYnPhi => + case atm φ notBoxPhiInY Y_is_simple ltProYnPhi notSatProj => rw [Lemma1_simple_sat_iff_all_projections_sat Y_is_simple] simp - intro Ynotclosed - use ϕ - use notBoxPhiInY - finish -#align tableauThenNotSat tableauThenNotSat + aesop -- Theorem 2, page 30 theorem correctness : ∀ X, Satisfiable X → Consistent X := @@ -481,12 +451,10 @@ theorem correctness : ∀ X, Satisfiable X → Consistent X := intro X contrapose unfold Consistent - simp unfold Inconsistent + simp only [not_nonempty_iff, not_isEmpty_iff, not_exists, not_forall, exists_prop, Nonempty.forall] intro hyp - cases' hyp with t - exact tableauThenNotSat X t -#align correctness correctness + apply tableauThenNotSat X hyp theorem soundTableau : ∀ φ, Provable φ → ¬Satisfiable ({~φ} : Finset Formula) := by @@ -494,8 +462,7 @@ theorem soundTableau : ∀ φ, Provable φ → ¬Satisfiable ({~φ} : Finset For intro prov cases' prov with _ tabl apply tableauThenNotSat - exact tabl -#align soundTableau soundTableau + assumption theorem soundness : ∀ φ, Provable φ → Tautology φ := by @@ -504,5 +471,3 @@ theorem soundness : ∀ φ, Provable φ → Tautology φ := rw [← singletonSat_iff_sat] apply soundTableau exact prov -#align soundness soundness - diff --git a/Bml/Tableau.lean b/Bml/Tableau.lean index de688f9..a922053 100644 --- a/Bml/Tableau.lean +++ b/Bml/Tableau.lean @@ -42,6 +42,7 @@ def formProjection : Formula → Option Formula def projection : Finset Formula → Finset Formula | X => X.biUnion fun x => (formProjection x).toFinset +-- TODO @[simp] theorem proj {g : Formula} {X : Finset Formula} : g ∈ projection X ↔ □g ∈ X := by rw [projection] @@ -101,14 +102,14 @@ theorem projection_set_length_leq : ∀ X, lengthOfSet (projection X) ≤ length _ ≤ lengthOfFormula f + S.sum lengthOfFormula := by simp; apply IH -- local rules: given this set, we get these sets as child nodes -inductive LocalRule : Finset Formula → Finset (Finset Formula) → Type-- closing rules: - +inductive LocalRule : Finset Formula → Finset (Finset Formula) → Type + -- closing rules: | bot {X} (h : ⊥ ∈ X) : LocalRule X ∅ - | Not {X ϕ} (h : ϕ ∈ X ∧ ~ϕ ∈ X) : LocalRule X ∅-- one-child rules: - + | Not {X ϕ} (h : ϕ ∈ X ∧ ~ϕ ∈ X) : LocalRule X ∅ + -- one-child rules: | neg {X ϕ} (h : ~~ϕ ∈ X) : LocalRule X {X \ {~~ϕ} ∪ {ϕ}} - | Con {X ϕ ψ} (h : ϕ⋀ψ ∈ X) : LocalRule X {X \ {ϕ⋀ψ} ∪ {ϕ, ψ}}-- splitting rule: - + | Con {X ϕ ψ} (h : ϕ⋀ψ ∈ X) : LocalRule X {X \ {ϕ⋀ψ} ∪ {ϕ, ψ}} + -- splitting rule: | nCo {X ϕ ψ} (h : ~(ϕ⋀ψ) ∈ X) : LocalRule X {X \ {~(ϕ⋀ψ)} ∪ {~ϕ}, X \ {~(ϕ⋀ψ)} ∪ {~ψ}} -- If X is not simple, then a local rule can be applied. @@ -171,20 +172,18 @@ theorem localRulesDecreaseLength {X : Finset Formula} {B : Finset (Finset Formul -- splitting rule! case inl inB => -- f subst inB - calc - lengthOfSet (insert (~ϕ) (X.erase (~(ϕ⋀ψ)))) ≤ - lengthOfSet (X.erase (~(ϕ⋀ψ))) + lengthOf (~ϕ) := - lengthOf_insert_leq_plus - _ < lengthOfSet (X.erase (~(ϕ⋀ψ))) + 1 + 1 + lengthOf ϕ + lengthOf ψ := by simp; ring_nf; sorry + calc lengthOfSet (insert (~ϕ) (X.erase (~(ϕ⋀ψ)))) + ≤ lengthOfSet (X.erase (~(ϕ⋀ψ))) + lengthOf (~ϕ) := lengthOf_insert_leq_plus + _ < lengthOfSet (X.erase (~(ϕ⋀ψ))) + 1 + (1 + lengthOf ϕ) := by simp + _ ≤ lengthOfSet (X.erase (~(ϕ⋀ψ))) + 1 + (1 + lengthOf ϕ) + lengthOf ψ := by simp _ = lengthOfSet (X.erase (~(ϕ⋀ψ))) + lengthOf (~(ϕ⋀ψ)) := by simp; ring _ = lengthOfSet X := lengthRemove X (~(ϕ⋀ψ)) in_X case inr inB => -- g subst inB - calc - lengthOfSet (insert (~ψ) (X.erase (~(ϕ⋀ψ)))) ≤ - lengthOfSet (X.erase (~(ϕ⋀ψ))) + lengthOf (~ψ) := - lengthOf_insert_leq_plus - _ < lengthOfSet (X.erase (~(ϕ⋀ψ))) + 1 + 1 + lengthOf ϕ + lengthOf ψ := by simp; ring_nf; sorry + calc lengthOfSet (insert (~ψ) (X.erase (~(ϕ⋀ψ)))) + ≤ lengthOfSet (X.erase (~(ϕ⋀ψ))) + lengthOf (~ψ) := lengthOf_insert_leq_plus + _ < lengthOfSet (X.erase (~(ϕ⋀ψ))) + 1 + (1 + lengthOf ψ) := by simp + _ ≤ lengthOfSet (X.erase (~(ϕ⋀ψ))) + 1 + lengthOf ϕ + (1 + lengthOf ψ) := by simp _ = lengthOfSet (X.erase (~(ϕ⋀ψ))) + lengthOf (~(ϕ⋀ψ)) := by simp; ring _ = lengthOfSet X := lengthRemove X (~(ϕ⋀ψ)) in_X @@ -193,9 +192,6 @@ theorem atmRuleDecreasesLength {X : Finset Formula} {ϕ} : by intro notBoxPhi_in_X simp - have proj_form_lt : ∀ f g, some g = formProjection f → lengthOfFormula g < lengthOfFormula f := by - intro f g g_is_fP_f; cases f; all_goals aesop - have lengthSingleton : ∀ f, lengthOfFormula f = lengthOfSet {f} := by intro f; unfold lengthOfSet; simp have otherClaim : projection X = projection (X.erase (~(□ϕ))) := by ext1 phi diff --git a/Bml/Tableauexamples.lean b/Bml/Tableauexamples.lean index 586184b..d61cd2e 100644 --- a/Bml/Tableauexamples.lean +++ b/Bml/Tableauexamples.lean @@ -1,22 +1,23 @@ -- TABLEAU-EXAMPLES -import Syntax -import Tableau -#align_import tableauexamples +import Mathlib.Data.Finset.Basic + +import Bml.Syntax +import Bml.Tableau theorem noBot : Provable (~⊥) := by apply Provable.byTableau apply ClosedTableau.loc swap - · apply LocalTableau.byLocalRule (LocalRule.neg (finset.mem_singleton.mpr (refl (~~⊥)))) + · apply LocalTableau.byLocalRule (LocalRule.neg (Finset.mem_singleton.mpr (refl (~~⊥)))) intro β inB rw [Finset.sdiff_self] at inB rw [Finset.empty_union] at inB rw [Finset.mem_singleton] at inB rw [inB] - apply LocalTableau.byLocalRule (LocalRule.bot (finset.mem_singleton.mpr (refl ⊥))) + apply LocalTableau.byLocalRule (LocalRule.bot (Finset.mem_singleton.mpr (refl ⊥))) intro Y YinEmpty - cases YinEmpty + aesop · -- show that endNodesOf is empty intro Y intro YisEndNode @@ -26,41 +27,31 @@ theorem noBot : Provable (~⊥) := by rcases YisEndNode with ⟨a, h, hyp⟩ subst h simp at * - cases hyp -#align noBot noBot -def emptyTableau : ∀ β : Finset Formula, β ∈ ∅ → LocalTableau β := +def emptyTableau : ∀ β : Finset Formula, β ∈ (∅ : Finset (Finset Formula)) → LocalTableau β := by intro beta b_in_empty exact absurd b_in_empty (Finset.not_mem_empty beta) -#align emptyTableau emptyTableau -- an example: -theorem noContradiction : Provable (~(p⋏~p)) := +theorem noContradiction : Provable (~(p⋀~p)) := by apply Provable.byTableau apply ClosedTableau.loc swap - · apply LocalTableau.byLocalRule + · apply LocalTableau.byLocalRule (@LocalRule.neg _ (p⋀~p) _) -- neg: - apply LocalRule.neg - simp intro β β_prop - simp at β_prop + simp at β_prop subst β_prop -- con: - apply LocalTableau.byLocalRule - apply LocalRule.con - simp - constructor - rfl - rfl + apply LocalTableau.byLocalRule (@LocalRule.Con _ p (~p) _) intro β2 β2_prop simp at β2_prop subst β2_prop -- closed: - apply LocalTableau.byLocalRule (@LocalRule.not _ p _) emptyTableau - exact by decide + apply LocalTableau.byLocalRule (@LocalRule.Not _ p _) emptyTableau + all_goals aesop · -- show that endNodesOf is empty intro Y intro YisEndNode @@ -71,103 +62,83 @@ theorem noContradiction : Provable (~(p⋏~p)) := simp at * rcases hyp with ⟨Y, Ydef, YinEndNodes⟩ subst Ydef - finish -#align noContradiction noContradiction + aesop -- preparing example 2 -def subTabForEx2 : ClosedTableau {r, ~(□p), □(p⋏q)} := +def subTabForEx2 : ClosedTableau {r, ~(□p), □(p⋀q)} := by - apply @ClosedTableau.atm {r, ~(□p), □(p⋏q)} p (by simp) - -- show that this set is simple: - · unfold Simple; simp at *; tauto + apply @ClosedTableau.atm {r, ~(□p), □(p⋀q)} p (by simp) (by simp at *) apply ClosedTableau.loc rotate_left -- con: - apply LocalTableau.byLocalRule (@LocalRule.con {p⋏q, ~p} p q (by simp)) + apply LocalTableau.byLocalRule (@LocalRule.Con {p⋀q, ~p} p q (by simp)) intro child childDef rw [Finset.mem_singleton] at childDef -- not: - apply LocalTableau.byLocalRule (@LocalRule.not _ p _) emptyTableau + apply LocalTableau.byLocalRule (@LocalRule.Not _ p _) emptyTableau · subst childDef; exact by decide · -- show that endNodesOf is empty intro Y intro YisEndNode simp at * - exfalso - assumption -#align subTabForEx2 subTabForEx2 -/- ./././Mathport/Syntax/Translate/Tactic/Builtin.lean:69:18: unsupported non-interactive tactic dedup -/ -- Example 2 -example : ClosedTableau {r⋏~(□p), r↣□(p⋏q)} := +example : ClosedTableau {r⋀~(□p), r↣□(p⋀q)} := by apply ClosedTableau.loc rotate_left · -- con apply LocalTableau.byLocalRule - apply LocalRule.con + apply LocalRule.Con simp only [impl, Finset.mem_insert, Finset.mem_singleton, or_false_iff] constructor - rfl - rfl intro branch branch_def rw [Finset.mem_singleton] at branch_def rw [Finset.union_insert] at branch_def -- nCo apply LocalTableau.byLocalRule - apply @LocalRule.nCo _ r (~(□(p⋏q))) + apply @LocalRule.nCo _ r (~(□(p⋀q))) · rw [branch_def]; simp intro b b_in simp only [Finset.mem_insert, Finset.mem_singleton] at b_in - refine' if h1 : b = branch \ {~(r⋏~(□(p⋏q)))} ∪ {~r} then _ else _ + refine' if h1 : b = branch \ {~(r⋀~(□(p⋀q)))} ∪ {~r} then _ else _ · -- right branch -- not: - apply LocalTableau.byLocalRule (@LocalRule.not _ r _) emptyTableau - finish + apply LocalTableau.byLocalRule (@LocalRule.Not _ r _) emptyTableau + aesop · --left branch - have h2 : b = branch \ {~(r⋏~(□(p⋏q)))} ∪ {~~(□(p⋏q))} := by tauto + have h2 : b = branch \ {~(r⋀~(□(p⋀q)))} ∪ {~~(□(p⋀q))} := by tauto -- neg: - apply LocalTableau.byLocalRule (@LocalRule.neg _ (□(p⋏q)) _) + apply LocalTableau.byLocalRule (@LocalRule.neg _ (□(p⋀q)) _) rotate_left; · rw [h2]; simp intro child childDef -- ending local tableau with a simple node: apply LocalTableau.sim rw [Finset.mem_singleton] at childDef rw [childDef] - unfold Simple; simp at *; constructor; unfold SimpleForm + unfold Simple; simp at *; unfold SimpleForm intro f f_notDef1 f_in_branch cases b_in - tauto - rw [b_in] at f_in_branch - simp at f_in_branch - cases f_in_branch - tauto - rw [branch_def] at f_in_branch - cases' f_in_branch with l r; simp at r - cases r - · subst r; unfold r - cases r - · subst r; unfold SimpleForm - · exfalso; tauto + · tauto + case inr b_in => + rw [b_in] at f_in_branch + simp at f_in_branch + cases f_in_branch + · tauto + case inr f_in_branch => + rw [branch_def] at f_in_branch + cases' f_in_branch with l r + aesop · -- tableau for the simple end nodes: rw [conEndNodes] rw [nCoEndNodes] intro Y Yin simp at * - split_ifs at * - · -- not-R branch - exfalso - -- show that there are no endnodes! - simp at Yin - exact Yin · -- notnotbranch - run_tac - dedup - have Yis : Y = {r, ~(□p), □(p⋏q)} := by - simp at Yin + have Yis : Y = {r, ~(□p), □(p⋀q)} := by subst Yin ext1 - constructor <;> · intro hyp; finish + constructor <;> · intro hyp; aesop subst Yis exact subTabForEx2 diff --git a/Bml/Vocabulary.lean b/Bml/Vocabulary.lean index 385e163..19bbbdc 100644 --- a/Bml/Vocabulary.lean +++ b/Bml/Vocabulary.lean @@ -1,65 +1,59 @@ -- VOCABULARY -import Tactic.NormNum -import Syntax -import Setsimp -#align_import vocabulary +import Mathlib.Tactic.NormNum +import Bml.Syntax +import Bml.Setsimp + +@[simp] def vocabOfFormula : Formula → Finset Char | ⊥ => Set.toFinset { } | ·c => {c} | ~φ => vocabOfFormula φ - | φ⋏ψ => vocabOfFormula φ ∪ vocabOfFormula ψ + | φ⋀ψ => vocabOfFormula φ ∪ vocabOfFormula ψ | □φ => vocabOfFormula φ -#align vocabOfFormula vocabOfFormula +@[simp] def vocabOfSetFormula : Finset Formula → Finset Char | X => Finset.biUnion X vocabOfFormula -#align vocabOfSetFormula vocabOfSetFormula class HasVocabulary (α : Type) where voc : α → Finset Char -#align hasVocabulary HasVocabulary open HasVocabulary +@[simp] instance formulaHasVocabulary : HasVocabulary Formula := HasVocabulary.mk vocabOfFormula -#align formula_hasVocabulary formulaHasVocabulary +@[simp] instance setFormulaHasVocabulary : HasVocabulary (Finset Formula) := HasVocabulary.mk vocabOfSetFormula -#align setFormula_hasVocabulary setFormulaHasVocabulary @[simp] theorem vocOfNeg {ϕ} : vocabOfFormula (~ϕ) = vocabOfFormula ϕ := by constructor -#align vocOfNeg vocOfNeg theorem vocElem_subs_vocSet {ϕ X} : ϕ ∈ X → vocabOfFormula ϕ ⊆ vocabOfSetFormula X := by - apply Finset.induction_on X + induction X using Finset.induction_on -- case ∅: - intro phi_in_X; - cases phi_in_X - -- case insert: - intro ψ S psi_not_in_S IH psi_in_insert - unfold vocabOfSetFormula at * - simp - intro a aIn - simp at * - cases psi_in_insert - · subst psi_in_insert; left; exact aIn - · tauto -#align vocElem_subs_vocSet vocElem_subs_vocSet + case empty => + intro phi_in_X; + cases phi_in_X + case insert ψ S _ IH => + intro psi_in_insert + simp at * + intro a aIn + aesop theorem vocMonotone {X Y : Finset Formula} (hyp : X ⊆ Y) : voc X ⊆ voc Y := by - unfold voc; unfold vocabOfSetFormula at * + unfold voc + simp at * intro a aIn unfold Finset.biUnion at * - simp at * - tauto -#align vocMonotone vocMonotone + intro p pIn + aesop theorem vocErase {X : Finset Formula} {ϕ : Formula} : voc (X \ {ϕ}) ⊆ voc X := by @@ -67,41 +61,34 @@ theorem vocErase {X : Finset Formula} {ϕ : Formula} : voc (X \ {ϕ}) ⊆ voc X rw [sdiff_singleton_is_erase] intro a aIn exact Finset.mem_of_mem_erase aIn -#align vocErase vocErase theorem vocUnion {X Y : Finset Formula} : voc (X ∪ Y) = voc X ∪ voc Y := by - unfold voc vocabOfSetFormula - ext1 simp - constructor <;> · intro; finish -#align vocUnion vocUnion + ext1 + aesop theorem vocPreserved (X : Finset Formula) (ψ ϕ) : ψ ∈ X → voc ϕ = voc ψ → voc X = voc (X \ {ψ} ∪ {ϕ}) := by intro psi_in_X eq_voc - unfold voc at * - unfold vocabOfSetFormula + simp at * ext1 constructor - all_goals intro a_in; norm_num at * + all_goals intro a_in + all_goals norm_num at * · rcases a_in with ⟨θ, _, a_in_vocTheta⟩ by_cases h : θ = ψ - · left; rw [eq_voc]; rw [← h]; exact a_in_vocTheta - · right; use θ; tauto - · cases a_in - · use ψ; rw [← eq_voc]; tauto - · rcases a_in with ⟨θ, _, a_in_vocTheta⟩; use θ; tauto -#align vocPreserved vocPreserved + · aesop + · aesop + · aesop theorem vocPreservedTwo {X : Finset Formula} (ψ ϕ1 ϕ2) : ψ ∈ X → voc ({ϕ1, ϕ2} : Finset Formula) = voc ψ → voc X = voc (X \ {ψ} ∪ {ϕ1, ϕ2}) := by intro psi_in_X eq_voc rw [vocUnion] - unfold voc at * - unfold vocabOfSetFormula + simp at * ext1 constructor all_goals intro a_in; norm_num at * @@ -109,21 +96,20 @@ theorem vocPreservedTwo {X : Finset Formula} (ψ ϕ1 ϕ2) : by_cases h : θ = ψ · right; subst h; unfold vocabOfSetFormula vocabOfFormula at *; simp at *; rw [← eq_voc] at a_in_vocTheta ; simp at a_in_vocTheta ; tauto - · use θ; itauto + · constructor + · use θ cases a_in - · rcases a_in with ⟨θ, theta_in_X, a_in_vocTheta⟩; use θ; itauto - · use ψ; constructor; itauto; rw [← eq_voc]; unfold vocabOfSetFormula; simp; itauto -#align vocPreservedTwo vocPreservedTwo + · aesop + · use ψ; constructor + · aesop + · rw [← eq_voc]; simp; aesop theorem vocPreservedSub {X : Finset Formula} (ψ ϕ) : ψ ∈ X → voc ϕ ⊆ voc ψ → voc (X \ {ψ} ∪ {ϕ}) ⊆ voc X := by intro psi_in_X sub_voc - unfold voc at * - unfold vocabOfSetFormula + simp at * intro a a_in; norm_num at * cases a_in · use ψ; rw [Finset.subset_iff] at sub_voc ; tauto - · rcases a_in with ⟨θ, _, a_in_vocTheta⟩; use θ; tauto -#align vocPreservedSub vocPreservedSub - + · aesop