diff --git a/Foundation/Modal/ComplementClosedConsistentFinset.lean b/Foundation/Modal/ComplementClosedConsistentFinset.lean index 4bcfd4cdd..638fa0818 100644 --- a/Foundation/Modal/ComplementClosedConsistentFinset.lean +++ b/Foundation/Modal/ComplementClosedConsistentFinset.lean @@ -72,26 +72,6 @@ lemma intro_union_consistent (h : ∀ {Γ₁ Γ₂ : FormulaFinset _}, (Γ₁ apply iff_theory_consistent_formulae_consistent.mp; simpa using FormulaSet.intro_union_consistent h; -/- -lemma intro_triunion_consistent - (h : ∀ {Γ₁ Γ₂ Γ₃ : List (Formula α)}, (∀ φ ∈ Γ₁, φ ∈ P₁) ∧ (∀ φ ∈ Γ₂, φ ∈ P₂) ∧ (∀ φ ∈ Γ₃, φ ∈ P₃) → 𝓢 ⊬ ⋀Γ₁ ⋏ ⋀Γ₂ ⋏ ⋀Γ₃ ➝ ⊥) - : FormulaFinset.Consistent 𝓢 (P₁ ∪ P₂ ∪ P₃) := by - rw [←iff_theory_consistent_formulae_consistent]; - convert FormulaSet.intro_triunion_consistent h; - ext; - constructor; - . simp only [Finset.coe_union, Set.mem_union, Finset.mem_coe]; - rintro ((hp₁ | hp₂) | hp₃); - . left; left; assumption; - . left; right; assumption; - . right; assumption; - . simp only [Set.mem_union, Finset.coe_union, Finset.mem_coe]; - rintro ((hp₁ | hp₂) | hp₃); - . left; left; assumption; - . left; right; assumption; - . right; assumption; --/ - end diff --git a/Foundation/Modal/Entailment/K.lean b/Foundation/Modal/Entailment/K.lean index 295d75796..191f3f0a6 100644 --- a/Foundation/Modal/Entailment/K.lean +++ b/Foundation/Modal/Entailment/K.lean @@ -594,6 +594,24 @@ lemma provable_iff_boxed : (X.box) *⊢[𝓢]! φ ↔ ∃ Δ : List F, (∀ ψ apply Context.provable_iff.mpr; use Δ.box; +lemma provable_iff_boxed_finset : (X.box) *⊢[𝓢]! φ ↔ ∃ Δ : Finset F, (Δ.box.toSet ⊆ X.box) ∧ (Δ.box) *⊢[𝓢]! φ := by + apply Iff.trans provable_iff_boxed; + constructor; + . rintro ⟨Δ, hΔ₁, hΔ₂⟩; + use Δ.toFinset; + constructor; + . intro ψ hψ; + apply hΔ₁ ψ; + sorry; + . sorry; + . rintro ⟨Δ, hΔ₁, hΔ₂⟩; + use Δ.toList; + constructor; + . intro ψ hψ; + apply hΔ₁; + sorry; + . sorry; + lemma nec! {Γ : Set F} (h : Γ *⊢[𝓢]! φ) : Γ.box *⊢[𝓢]! □φ := by apply Context.provable_iff.mpr; obtain ⟨Δ, hΔ₁, hΔ₂⟩ := Context.provable_iff.mp h; diff --git a/Foundation/Modal/Kripke/Basic.lean b/Foundation/Modal/Kripke/Basic.lean index d15ae7685..d969a0485 100644 --- a/Foundation/Modal/Kripke/Basic.lean +++ b/Foundation/Modal/Kripke/Basic.lean @@ -204,39 +204,13 @@ lemma multidia_def : x ⊧ ◇^[n]φ ↔ ∃ y, x ≺^[n] y ∧ y ⊧ φ := by . apply ih.mpr; use y; -lemma disj_def : x ⊧ ⋁Γ ↔ ∃ φ ∈ Γ, x ⊧ φ := by - induction Γ using List.induction_with_singleton with - | hcons φ Γ hΓ ih => - suffices x ⊧ φ ∨ x ⊧ ⋁Γ ↔ x ⊧ φ ∨ ∃ a ∈ Γ, x ⊧ a by simpa [List.disj₂_cons_nonempty hΓ]; - constructor; - . rintro (_ | h) - . tauto; - . right; exact ih.mp h; - . rintro (_ | h); - . tauto; - . right; exact ih.mpr h; - | _ => simp; - -lemma conj_def : x ⊧ ⋀Γ ↔ ∀ φ ∈ Γ, x ⊧ φ := by - induction Γ using List.induction_with_singleton with - | hcons φ Γ hΓ ih => - suffices (x ⊧ φ ∧ x ⊧ ⋀Γ) ↔ (x ⊧ φ ∧ ∀ φ ∈ Γ, x ⊧ φ) by simpa [List.conj₂_cons_nonempty hΓ]; - constructor; - . intro ⟨_, hΓ⟩; - constructor; - . assumption; - . exact ih.mp hΓ; - . intro ⟨_, hΓ⟩; - constructor; - . assumption; - . apply ih.mpr hΓ; - | _ => simp; +lemma disj_def {Γ : List _} : x ⊧ Γ.disj ↔ ∃ φ ∈ Γ, x ⊧ φ := by simp; + +lemma conj_def {Γ : List _} : x ⊧ Γ.conj ↔ ∀ φ ∈ Γ, x ⊧ φ := by simp; -lemma fconj_def {Γ : Finset _} : x ⊧ Γ.conj ↔ ∀ φ ∈ Γ, x ⊧ φ := by - simp only [Semantics.realize_finset_conj, Satisfies.iff_models]; +lemma fconj_def {Γ : Finset _} : x ⊧ Γ.conj ↔ ∀ φ ∈ Γ, x ⊧ φ := by simp; -lemma fdisj_def {Γ : Finset _} : x ⊧ Γ.disj ↔ ∃ φ ∈ Γ, x ⊧ φ := by - simp only [Semantics.realize_finset_disj, Satisfies.iff_models]; +lemma fdisj_def {Γ : Finset _} : x ⊧ Γ.disj ↔ ∃ φ ∈ Γ, x ⊧ φ := by simp; lemma trans (hpq : x ⊧ φ ➝ ψ) (hqr : x ⊧ ψ ➝ χ) : x ⊧ φ ➝ χ := by simp_all; diff --git a/Foundation/Modal/MaximalConsistentSet.lean b/Foundation/Modal/MaximalConsistentSet.lean index 4ca285a10..e9ca822e0 100644 --- a/Foundation/Modal/MaximalConsistentSet.lean +++ b/Foundation/Modal/MaximalConsistentSet.lean @@ -228,58 +228,6 @@ lemma intro_union_consistent(h : ∀ {Γ₁ Γ₂ : FormulaFinset _}, (Γ₁.toS have : φ ∈ T₁ ∪ T₂ := hΔ hφ; simp_all [Δ₁, Δ₂]; -/- -omit [DecidableEq α] in -open Classical in -lemma intro_union_consistent - (h : ∀ {Γ₁ Γ₂ : List (Formula α)}, (∀ φ ∈ Γ₁, φ ∈ T₁) ∧ (∀ φ ∈ Γ₂, φ ∈ T₂) → 𝓢 ⊬ ⋀Γ₁ ⋏ ⋀Γ₂ ➝ ⊥) - : Consistent 𝓢 (T₁ ∪ T₂) := by - apply def_consistent.mpr; - intro Δ hΔ; - let Δ₁ := (Δ.filter (· ∈ T₁)); - let Δ₂ := (Δ.filter (· ∈ T₂)); - have : 𝓢 ⊬ ⋀Δ₁ ⋏ ⋀Δ₂ ➝ ⊥ := @h Δ₁ Δ₂ ⟨(by intro _ h; simpa using List.of_mem_filter h), (by intro _ h; simpa using List.of_mem_filter h)⟩; - exact unprovable_C!_trans (by - apply FiniteContext.deduct'!; - apply Conj₂!_iff_forall_provable.mpr; - intro ψ hq; - cases (hΔ ψ hq); - . exact Conj₂!_iff_forall_provable.mp (K!_left FiniteContext.id!) ψ $ List.mem_filter_of_mem hq (by simpa); - . exact Conj₂!_iff_forall_provable.mp (K!_right FiniteContext.id!) ψ $ List.mem_filter_of_mem hq (by simpa); - ) this; - -open Classical in -lemma intro_triunion_consistent - (h : ∀ {Γ₁ Γ₂ Γ₃ : List (Formula α)}, (∀ φ ∈ Γ₁, φ ∈ T₁) ∧ (∀ φ ∈ Γ₂, φ ∈ T₂) ∧ (∀ φ ∈ Γ₃, φ ∈ T₃) → 𝓢 ⊬ ⋀Γ₁ ⋏ ⋀Γ₂ ⋏ ⋀Γ₃ ➝ ⊥) - : Consistent 𝓢 (T₁ ∪ T₂ ∪ T₃) := by - apply intro_union_consistent; - rintro Γ₁₂ Γ₃ ⟨h₁₂, h₃⟩; - simp at h₁₂; - let Γ₁ := (Γ₁₂.filter (· ∈ T₁)); - let Γ₂ := (Γ₁₂.filter (· ∈ T₂)); - apply unprovable_C!_trans (φ := ⋀Γ₁ ⋏ ⋀Γ₂ ⋏ ⋀Γ₃); - . exact C!_trans (K!_right $ K!_assoc) $ by - apply CKK!_of_C!; - apply CConj₂Append!_iff_CKConj₂Conj₂!.mp; - apply CConj₂Conj₂!_of_subset; - intro φ hp; - simp [Γ₁, Γ₂]; - rcases h₁₂ φ hp with (h₁ | h₂); - . left; exact ⟨hp, h₁⟩; - . right; exact ⟨hp, h₂⟩; - . apply h; - refine ⟨?_, ?_, h₃⟩; - . intro φ hp; - rcases h₁₂ φ (List.mem_of_mem_filter hp) with (_ | _) - . assumption; - . simpa using List.of_mem_filter hp; - . intro φ hp; - rcases h₁₂ φ (List.mem_of_mem_filter hp) with (_ | _) - . have := List.of_mem_filter hp; simp at this; - simpa using List.of_mem_filter hp; - . assumption; --/ - lemma exists_consistent_maximal_of_consistent (T_consis : Consistent 𝓢 T) : ∃ Z, Consistent 𝓢 Z ∧ T ⊆ Z ∧ ∀ U, U *⊬[𝓢] ⊥ → Z ⊆ U → U = Z := by obtain ⟨Z, h₁, ⟨h₂, h₃⟩⟩ := zorn_subset_nonempty { T : FormulaSet α | Consistent 𝓢 T} (by diff --git a/Foundation/Modal/Tableau.lean b/Foundation/Modal/Tableau.lean index 900f4240d..50933afc1 100644 --- a/Foundation/Modal/Tableau.lean +++ b/Foundation/Modal/Tableau.lean @@ -529,67 +529,41 @@ lemma iff_mem₂_and : φ ⋏ ψ ∈ t.1.2 ↔ (φ ∈ t.1.2 ∨ ψ ∈ t.1.2) : rcases of_mem₁_and $ iff_not_mem₂_mem₁.mp hφψ with ⟨hφ, hψ⟩; constructor <;> { apply iff_not_mem₂_mem₁.mpr; assumption; }; -lemma iff_mem₁_conj₂ {Γ : List (Formula α)} : ⋀Γ ∈ t.1.1 ↔ ∀ φ ∈ Γ, φ ∈ t.1.1 := by - induction Γ using List.induction_with_singleton with - | hcons φ Γ Γ_nil ih => - simp only [(List.conj₂_cons_nonempty Γ_nil), List.mem_cons]; - constructor; - . rintro h φ (rfl | hp); - . exact iff_mem₁_and.mp h |>.1; - . exact ih.mp (iff_mem₁_and.mp h |>.2) _ hp; - . intro h; - apply iff_mem₁_and.mpr; - simp_all; - | _ => simp; +lemma iff_mem₁_conj {Γ : List (Formula α)} : Γ.conj ∈ t.1.1 ↔ ∀ φ ∈ Γ, φ ∈ t.1.1 := by induction Γ <;> simp_all [iff_mem₁_and] lemma iff_mem₁_fconj {Γ : Finset (Formula α)} : Γ.conj ∈ t.1.1 ↔ ↑Γ ⊆ t.1.1 := by constructor; . intro h φ hφ; - apply iff_mem₁_conj₂ (Γ := Γ.toList) (t := t) |>.mp; - . apply mdp_mem₁_provable ?_ h; simp; + apply iff_mem₁_conj (Γ := Γ.toList) (t := t) |>.mp; + . apply mdp_mem₁_provable ?_ h; + sorry; . simpa; . intro h; - apply mdp_mem₁_provable ?_ $ iff_mem₁_conj₂ (Γ := Γ.toList) (t := t) |>.mpr $ by - intro φ hφ; + apply mdp_mem₁_provable ?_ $ iff_mem₁_conj (Γ := Γ.toList) (t := t) |>.mpr ?_ + . sorry; + . intro φ hφ; apply h; simp_all; - simp; -lemma iff_mem₂_conj₂ {Γ : List _} : ⋀Γ ∈ t.1.2 ↔ (∃ φ ∈ Γ, φ ∈ t.1.2) := by - induction Γ using List.induction_with_singleton with - | hcons φ Γ hΓ ih => - rw [List.conj₂_cons_nonempty hΓ]; - constructor; - . intro h; - rcases iff_mem₂_and.mp h with (hφ | hΓ); - . exact ⟨φ, by tauto, hφ⟩; - . obtain ⟨ψ, hψ₁, hψ₂⟩ := ih.mp hΓ; - exact ⟨ψ, by tauto, hψ₂⟩; - . rintro ⟨ψ, (hψ₁ | hψ₁), hψ₂⟩; - . apply iff_mem₂_and.mpr; - left; - assumption; - . apply iff_mem₂_and.mpr; - right; - apply ih.mpr; - exact ⟨ψ, by simpa, hψ₂⟩; - | _ => simp; +lemma iff_mem₂_conj {Γ : List _} : Γ.conj ∈ t.1.2 ↔ (∃ φ ∈ Γ, φ ∈ t.1.2) := by induction Γ <;> simp_all [iff_mem₂_and] lemma iff_mem₂_fconj {Γ : Finset (Formula α)} : Γ.conj ∈ t.1.2 ↔ (∃ φ ∈ Γ, φ ∈ t.1.2) := by constructor; . intro h; - obtain ⟨φ, hφ₁, hφ₂⟩ := iff_mem₂_conj₂ (Γ := Γ.toList) (t := t) |>.mp $ by - apply mdp_mem₂_provable (ψ := Γ.conj); - . simp; - . assumption; - use φ; - constructor; - . simpa using hφ₁; - . simpa; + obtain ⟨φ, hφ₁, hφ₂⟩ := iff_mem₂_conj (Γ := Γ.toList) (t := t) |>.mp $ by + apply mdp_mem₂_provable ?_ h; + sorry; + . use φ; + constructor; + . simpa using hφ₁; + . simpa; . rintro ⟨ψ, hψ₁, hψ₂⟩; - apply iff_mem₂_conj₂.mpr; - use ψ; - constructor <;> simpa; + apply mdp_mem₂_provable ?_ $ iff_mem₂_conj (Γ := Γ.toList) (t := t) |>.mpr ?_ + . sorry; + . use ψ; + constructor; + . simpa using hψ₁; + . simpa; omit [Encodable α] in private lemma of_mem₁_or : φ ⋎ ψ ∈ t.1.1 → (φ ∈ t.1.1 ∨ ψ ∈ t.1.1) := by @@ -632,59 +606,23 @@ lemma iff_mem₂_or : φ ⋎ ψ ∈ t.1.2 ↔ (φ ∈ t.1.2 ∧ ψ ∈ t.1.2) := . have := iff_not_mem₂_mem₁.mpr hφ; contradiction; . exact iff_not_mem₂_mem₁.mpr hψ; -lemma iff_mem₁_disj {Γ : List _} : ⋁Γ ∈ t.1.1 ↔ (∃ φ ∈ Γ, φ ∈ t.1.1) := by - induction Γ using List.induction_with_singleton with - | hcons φ Γ hΓ ih => - rw [List.disj₂_cons_nonempty hΓ]; - constructor; - . intro h; - rcases iff_mem₁_or.mp h with (hφ | hΓ); - . exact ⟨φ, by tauto, hφ⟩; - . obtain ⟨ψ, hψ₁, hψ₂⟩ := ih.mp hΓ; - exact ⟨ψ, by tauto, hψ₂⟩; - . rintro ⟨ψ, (hψ₁ | hψ₁), hψ₂⟩; - . apply iff_mem₁_or.mpr; - left; - assumption; - . apply iff_mem₁_or.mpr; - right; - apply ih.mpr; - exact ⟨ψ, by simpa, hψ₂⟩; - | _ => simp; - -lemma iff_mem₂_disj {Γ : List _} : ⋁Γ ∈ t.1.2 ↔ (∀ φ ∈ Γ, φ ∈ t.1.2) := by - induction Γ using List.induction_with_singleton with - | hcons φ Γ hΓ ih => - rw [List.disj₂_cons_nonempty hΓ]; - constructor; - . intro h; - rcases iff_mem₂_or.mp h with ⟨hφ, hΓ⟩; - rintro ψ (hψ | hΓ); - . assumption; - . apply ih.mp hΓ; - assumption; - . intro h; - apply iff_mem₂_or.mpr; - constructor; - . apply h; tauto; - . apply ih.mpr; - intro ψ hψ; - apply h; - tauto; - | _ => simp; +lemma iff_mem₁_disj {Γ : List _} : Γ.disj ∈ t.1.1 ↔ (∃ φ ∈ Γ, φ ∈ t.1.1) := by induction Γ <;> simp_all [iff_mem₁_or]; + +lemma iff_mem₂_disj {Γ : List _} : Γ.disj ∈ t.1.2 ↔ (∀ φ ∈ Γ, φ ∈ t.1.2) := by induction Γ <;> simp_all [iff_mem₂_or]; lemma iff_mem₂_fdisj {Γ : Finset _} : Γ.disj ∈ t.1.2 ↔ (↑Γ ⊆ t.1.2) := by constructor; . intro h φ hφ; apply iff_mem₂_disj (Γ := Γ.toList) (t := t) |>.mp; - . apply mdp_mem₂_provable ?_ h; simp; + . apply mdp_mem₂_provable ?_ h; + sorry; . simpa; . intro h; apply mdp_mem₂_provable ?_ $ iff_mem₂_disj (Γ := Γ.toList) (t := t) |>.mpr $ by intro φ hφ; apply h; simp_all; - simp; + sorry; omit [Encodable α] in private lemma of_mem₁_imp : φ ➝ ψ ∈ t.1.1 → (φ ∈ t.1.2 ∨ ψ ∈ t.1.1) := by diff --git a/Foundation/Propositional/ConsistentTableau.lean b/Foundation/Propositional/ConsistentTableau.lean index b2ccaeff6..5ebaaec74 100644 --- a/Foundation/Propositional/ConsistentTableau.lean +++ b/Foundation/Propositional/ConsistentTableau.lean @@ -118,8 +118,6 @@ lemma consistent_either (hCon : t.Consistent 𝓢) (φ : Formula α) : Tableau.C . simp only [Finset.coe_union, Set.union_subset_iff]; tauto; . simp only [Finset.coe_union, Set.union_subset_iff]; tauto; - -- have : 𝓢 ⊢! ⋀(Γ₁ ++ Γ₂) ➝ ⋁(Δ₁ ++ Δ₂) := C!_trans (K!_left EConj₂AppendKConj₂Conj₂!) $ C!_trans (cut! h₁ h₂) (K!_right EDisj₂AppendADisj₂Disj₂!); - end Consistent end @@ -489,31 +487,22 @@ lemma iff_mem₁_and [DecidableEq α] : φ ⋏ ψ ∈ t.1.1 ↔ φ ∈ t.1.1 ∧ apply Set.doubleton_subset.mpr; tauto; -lemma iff_mem₁_conj₂ [DecidableEq α] {Γ : List (Formula α)} : ⋀Γ ∈ t.1.1 ↔ ∀ φ ∈ Γ, φ ∈ t.1.1 := by - induction Γ using List.induction_with_singleton with - | hcons φ Γ Γ_nil ih => - simp only [(List.conj₂_cons_nonempty Γ_nil), List.mem_cons]; - constructor; - . rintro h φ (rfl | hp); - . exact iff_mem₁_and.mp h |>.1; - . exact ih.mp (iff_mem₁_and.mp h |>.2) _ hp; - . intro h; - apply iff_mem₁_and.mpr; - simp_all; - | _ => simp; +lemma iff_mem₁_conj₂ [DecidableEq α] {Γ : List (Formula α)} : Γ.conj ∈ t.1.1 ↔ ∀ φ ∈ Γ, φ ∈ t.1.1 := by + induction Γ <;> simp_all [iff_mem₁_and]; lemma iff_mem₁_fconj [DecidableEq α] {Γ : Finset (Formula α)} : Γ.conj ∈ t.1.1 ↔ ↑Γ ⊆ t.1.1 := by constructor; . intro h φ hφ; apply iff_mem₁_conj₂ (Γ := Γ.toList) (t := t) |>.mp; - . apply mdp_mem₁_provable ?_ h; simp; + . apply mdp_mem₁_provable ?_ h; + sorry; . simpa; . intro h; apply mdp_mem₁_provable ?_ $ iff_mem₁_conj₂ (Γ := Γ.toList) (t := t) |>.mpr $ by intro φ hφ; apply h; simp_all; - simp; + sorry; private lemma of_mem₁_or [DecidableEq α] : φ ⋎ ψ ∈ t.1.1 → (φ ∈ t.1.1 ∨ ψ ∈ t.1.1) := by intro h; @@ -553,24 +542,18 @@ lemma iff_mem₂_or [DecidableEq α] : φ ⋎ ψ ∈ t.1.2 ↔ φ ∈ t.1.2 ∧ . have := iff_not_mem₂_mem₁.mpr hφ; contradiction; . exact iff_not_mem₂_mem₁.mpr hψ; -lemma iff_mem₂_disj [DecidableEq α] {Γ : List (Formula α)} : ⋁Γ ∈ t.1.2 ↔ ∀ φ ∈ Γ, φ ∈ t.1.2 := by - induction Γ using List.induction_with_singleton with - | hcons φ Γ Γ_nil ih => - simp only [(List.disj₂_cons_nonempty Γ_nil), List.mem_cons]; - constructor; - . rintro h φ (rfl | hp); - . exact iff_mem₂_or.mp h |>.1; - . exact ih.mp (iff_mem₂_or.mp h |>.2) _ hp; - . intro h; - apply iff_mem₂_or.mpr; - simp_all; - | _ => simp; +lemma iff_mem₂_disj [DecidableEq α] {Γ : List (Formula α)} : Γ.disj ∈ t.1.2 ↔ ∀ φ ∈ Γ, φ ∈ t.1.2 := by + induction Γ <;> simp_all [iff_mem₂_or]; lemma iff_mem₂_fdisj [DecidableEq α] {Γ : Finset (Formula α)} : Γ.disj ∈ t.1.2 ↔ ↑Γ ⊆ t.1.2 := by + + sorry; + /- apply Iff.trans $ show Γ.disj ∈ t.1.2 ↔ ⋁Γ.toList ∈ t.1.2 by constructor <;> apply mdp_mem₂_provable $ by simp; apply Iff.trans iff_mem₂_disj; simp_all only [Finset.mem_toList]; rfl; + -/ lemma of_mem₁_imp [DecidableEq α] : φ ➝ ψ ∈ t.1.1 → (φ ∈ t.1.2 ∨ ψ ∈ t.1.1) := by intro h;