perf(Incompleteness): factor costly definability and frame proofs

LeanPool/Incompleteness/Arith/D1.lean

@@ -154,7 +154,10 @@ lemma quote_derivation_def
 
 @[simp] lemma fstidx_quote
     {Γ : Finset (SyntacticFormula L)} (d : T ⊢₂ Γ) : fstIdx (⌜d⌝ : V) = ⌜Γ⌝ := by
-  induction d <;> simp [quote_derivation_def, codeIn]
+  induction d <;>
+    simp only [quote_derivation_def, codeIn, fstIdx_axL, fstIdx_root, fstIdx_verumIntro,
+      fstIdx_andIntro, fstIdx_orIntro, fstIdx_allIntro, fstIdx_exIntro, fstIdx_wkRule,
+      fstIdx_shiftRule, fstIdx_cutRule]
 
 end Derivation2
 

LeanPool/Incompleteness/Arithmetization/Basic/IOpen.lean

@@ -8,7 +8,6 @@ module
 public import LeanPool.Incompleteness.Arithmetization.Basic.Ind
 public import LeanPool.Incompleteness.Arithmetization.Basic.PeanoMinus
 import LeanPool.Incompleteness.Arithmetization.Definability.Init
-import Mathlib.Algebra.Order.Sub.Basic
 import Mathlib.Data.Nat.Cast.Order.Basic
 
 /-! # IOpen -/

LeanPool/Incompleteness/Arithmetization/Basic/Ind.lean

@@ -9,7 +9,6 @@ public import LeanPool.Incompleteness.Arithmetization.Definability.Boldface
 import LeanPool.Incompleteness.Arithmetization.Basic.PeanoMinus
 import LeanPool.Incompleteness.Arithmetization.Definability.Init
 import LeanPool.Incompleteness.Foundation.FirstOrder.Completeness.Corollaries
-import Mathlib.Algebra.Order.Sub.Basic
 
 /-! # Ind -/
 

LeanPool/Incompleteness/Arithmetization/ISigmaOne/HFS/Seq.lean

@@ -8,7 +8,6 @@ module
 public import LeanPool.Incompleteness.Arithmetization.ISigmaOne.HFS.Basic
 import LeanPool.Incompleteness.Arithmetization.Definability.Absoluteness
 import LeanPool.Incompleteness.Arithmetization.Definability.Init
-import Mathlib.Algebra.Order.Sub.Basic
 
 /-!
 
@@ -432,8 +431,21 @@ section «lp_section_4»
 def _root_.LO.FirstOrder.Arith.mkSeq₁Def : Sg0.Semisentence 2 := .mkSigma
   “s x. !seqConsDef s 0 x” (by simp)
 
+-- Keeping the function abstract prevents conversion from unfolding encoded sequence operations.
+omit [V ⊧ₘ* 𝐈Sg1] in
+private lemma defined_zero_left (f : V → V → V) (φ : Sg0.Semisentence 3)
+    (hφ : Sg0-Function₂ f via φ) :
+    Sg0-Function₁ (fun x ↦ f ∅ x) via
+      (.mkSigma “s x. !φ s 0 x” (by simp)) := by
+  intro v
+  simp only [Fin.isValue, Fin.succ_zero_eq_one, Nat.reduceAdd, Nat.succ_eq_add_one,
+    HierarchySymbol.Semiformula.val_mkSigma, Semiformula.eval_substs, hφ.df.iff,
+    Matrix.vecCons_zero, Semiterm.val_bvar, Matrix.cons_val_one,
+    Semiterm.val_const, Structure.numeral_eq_numeral, ORingStruc.zero_eq_zero]
+  rfl
+
 lemma mkSeq₁_defined : Sg0-Function₁ (fun x : V ↦ !⟦x⟧) via mkSeq₁Def := by
-  intro v; simp [mkSeq₁Def]; rfl
+  simpa only [mkSeq₁Def] using defined_zero_left seqCons seqConsDef seqCons_defined
 
 @[simp] lemma eval_mkSeq₁Def (v) :
     Semiformula.Evalbm V v mkSeq₁Def.val ↔ v 0 = !⟦v 1⟧ := mkSeq₁_defined.df.iff v

LeanPool/Incompleteness/Arithmetization/ISigmaOne/Metamath/Formula/Basic.lean

@@ -1273,19 +1273,21 @@ lemma uformula_result_induction {P : V → V → V → Prop} (hP : Sg1-Relation
   rcases hp.case with
     (⟨k, r, v, hkr, hv, rfl⟩ | ⟨k, r, v, hkr, hv, rfl⟩ | rfl | rfl | ⟨p₁, p₂, hp₁, hp₂,
       rfl⟩ | ⟨p₁, p₂, hp₁, hp₂, rfl⟩ | ⟨p₁, hp₁, rfl⟩ | ⟨p₁, hp₁, rfl⟩)
-  · simpa [hkr, hv] using hRel param k r v hkr hv
-  · simpa [hkr, hv] using hNRel param k r v hkr hv
-  · simpa using hverum param
-  · simpa using hfalsum param
-  · simpa [c.result_and hp₁ hp₂] using
-      hand param p₁ p₂ hp₁ hp₂ (ih p₁ (by simp) param (by simp [f]) hp₁) (ih p₂ (by simp) param (by
-        simp [f]) hp₂)
-  · simpa [c.result_or hp₁ hp₂] using
-      hor param p₁ p₂ hp₁ hp₂ (ih p₁ (by simp) param (by simp [f]) hp₁) (ih p₂ (by simp) param (by
-        simp [f]) hp₂)
-  · simpa [c.result_all hp₁] using
+  · simpa only [c.result_rel hkr hv] using hRel param k r v hkr hv
+  · simpa only [c.result_nrel hkr hv] using hNRel param k r v hkr hv
+  · simpa only [c.result_verum] using hverum param
+  · simpa only [c.result_falsum] using hfalsum param
+  · simpa only [c.result_and hp₁ hp₂] using
+      hand param p₁ p₂ hp₁ hp₂
+        (ih p₁ (by simp) param (by simp [f]) hp₁)
+        (ih p₂ (by simp) param (by simp [f]) hp₂)
+  · simpa only [c.result_or hp₁ hp₂] using
+      hor param p₁ p₂ hp₁ hp₂
+        (ih p₁ (by simp) param (by simp [f]) hp₁)
+        (ih p₂ (by simp) param (by simp [f]) hp₂)
+  · simpa only [c.result_all hp₁] using
       hall param p₁ hp₁ (ih p₁ (by simp) (c.allChanges param) (by simp [f]) hp₁)
-  · simpa [c.result_ex hp₁] using
+  · simpa only [c.result_ex hp₁] using
       hex param p₁ hp₁ (ih p₁ (by simp) (c.exChanges param) (by simp [f]) hp₁)
 
 
@@ -1715,22 +1717,22 @@ lemma semiformula_result_induction {P : V → V → V → V → Prop} (hP : Sg1-
   rcases Language.IsSemiformula.case_iff.mp hp with
     (⟨k, R, v, hR, hv, rfl⟩ | ⟨k, R, v, hR, hv, rfl⟩ | rfl | rfl | ⟨p₁, p₂, h₁, h₂, rfl⟩ | ⟨p₁,
       p₂, h₁, h₂, rfl⟩ | ⟨p₁, h₁, rfl⟩ | ⟨p₁, h₁, rfl⟩)
-  · simpa [hR, hv.isUTerm] using hRel n param k R v hR hv
-  · simpa [hR, hv.isUTerm] using hNRel n param k R v hR hv
-  · simpa using hverum n param
-  · simpa using hfalsum n param
-  · simpa [h₁.isUFormula, h₂.isUFormula] using
+  · simpa only [c.result_rel hR hv.isUTerm] using hRel n param k R v hR hv
+  · simpa only [c.result_nrel hR hv.isUTerm] using hNRel n param k R v hR hv
+  · simpa only [c.result_verum] using hverum n param
+  · simpa only [c.result_falsum] using hfalsum n param
+  · simpa only [c.result_and h₁.isUFormula h₂.isUFormula] using
       hand n param p₁ p₂ h₁ h₂
         (ih p₁ (by simp) param (by simp [f]) n (by simp [g]) h₁)
         (ih p₂ (by simp) param (by simp [f]) n (by simp [g]) h₂)
-  · simpa [h₁.isUFormula, h₂.isUFormula] using
+  · simpa only [c.result_or h₁.isUFormula h₂.isUFormula] using
       hor n param p₁ p₂ h₁ h₂
         (ih p₁ (by simp) param (by simp [f]) n (by simp [g]) h₁)
         (ih p₂ (by simp) param (by simp [f]) n (by simp [g]) h₂)
-  · simpa [h₁.isUFormula] using
+  · simpa only [c.result_all h₁.isUFormula] using
       hall n param p₁ h₁
         (ih p₁ (by simp) (c.allChanges param) (by simp [f]) (n + 1) (by simp [g]) h₁)
-  · simpa [h₁.isUFormula] using
+  · simpa only [c.result_ex h₁.isUFormula] using
       hex n param p₁ h₁
         (ih p₁ (by simp) (c.exChanges param) (by simp [f]) (n + 1) (by simp [g]) h₁)
 

LeanPool/Incompleteness/Arithmetization/ISigmaOne/Metamath/Proof/Derivation.lean

@@ -8,7 +8,6 @@ module
 public import LeanPool.Incompleteness.Arithmetization.ISigmaOne.Metamath.Proof.Thy
 public import LeanPool.Incompleteness.Arithmetization.ISigmaOne.Metamath.Formula.Iteration
 import LeanPool.Incompleteness.Arithmetization.Definability.Init
-import Mathlib.Algebra.Order.Sub.Basic
 
 /-! # Derivation -/
 

LeanPool/Incompleteness/Arithmetization/ISigmaOne/Metamath/Term/Functions.lean

@@ -7,7 +7,6 @@ module
 
 public import LeanPool.Incompleteness.Arithmetization.ISigmaOne.Metamath.Term.Basic
 import LeanPool.Incompleteness.Arithmetization.Definability.Init
-import Mathlib.Algebra.Order.Sub.Basic
 import Mathlib.Data.Nat.Cast.Order.Basic
 
 /-! # Functions -/

LeanPool/Incompleteness/Foundation/FirstOrder/Arith/Theory.lean

@@ -232,23 +232,9 @@ example (a b : ℕ) : Set.Finite {a, b} := by simp only [Set.finite_singleton, S
     ext φ; constructor
     · rintro ⟨⟩
       case equal => left; assumption
-      case addZero => tauto
-      case addAssoc => tauto
-      case addComm => tauto
-      case addEqOfLt => tauto
-      case zeroLe => tauto
-      case zeroLtOne => tauto
-      case oneLeOfZeroLt => tauto
-      case addLtAdd => tauto
-      case mulZero => tauto
-      case mulOne => tauto
-      case mulAssoc => tauto
-      case mulComm => tauto
-      case mulLtMul => tauto
-      case distr => tauto
-      case ltIrrefl => tauto
-      case ltTrans => tauto
-      case ltTri => tauto
+      all_goals
+        right
+        simp only [Set.mem_insert_iff, Set.mem_singleton_iff, or_true, true_or]
     · rintro (h | rfl | rfl | rfl | rfl | rfl | rfl | rfl | rfl | rfl | rfl | rfl | rfl | rfl | rfl
       | rfl | rfl | rfl)
       · exact PeanoMinus.equal _ h

LeanPool/Incompleteness/Foundation/FirstOrder/Completeness/SubLanguage.lean

@@ -84,21 +84,7 @@ def toSubLanguage' (pf : ∀ k, L.Func k → Prop) (pr : ∀ k, L.Rel k → Prop
     | bvar x => rfl
     | fvar x => rfl
     | func f v ih =>
-      have hv : (fun i => (toSubLanguage' pf pr (v i)
-          (fun k' f' h' => h k' f' (lang_func_ss f v i h'))).lMap L.ofSubLanguage) = v := by
-        funext i
-        exact ih i _
-      calc
-        (toSubLanguage' pf pr (func f v) h).lMap L.ofSubLanguage =
-            func ((L.ofSubLanguage).func ⟨f, h _ f (lang_func f v)⟩)
-              (fun i => (toSubLanguage' pf pr (v i)
-                (fun k' f' h' => h k' f' (lang_func_ss f v i h'))).lMap
-                  L.ofSubLanguage) := rfl
-        _ = func f (fun i => (toSubLanguage' pf pr (v i)
-              (fun k' f' h' => h k' f' (lang_func_ss f v i h'))).lMap
-                L.ofSubLanguage) := by
-          rfl
-        _ = func f v := congrArg (func f) hv
+      exact congrArg (func f) (funext fun i ↦ ih i _)
 
 end Semiterm
 
@@ -188,18 +174,7 @@ def toSubLanguage' (pf : ∀ k, L.Func k → Prop) (pr : ∀ k, L.Rel k → Prop
         (fun k f h => hf k f (langFunc_rel_ss r v i h))).lMap L.ofSubLanguage) = v := by
       funext i
       exact Semiterm.lMap_toSubLanguage' pf pr (v i) _
-    calc
-      lMap L.ofSubLanguage (toSubLanguage' pf pr (nrel r v) hf hr) =
-          nrel (L.ofSubLanguage.rel
-            ⟨r, hr _ r (by simp only [langRel, Finset.mem_singleton])⟩)
-            (fun i => ((v i).toSubLanguage' pf pr
-              (fun k f h => hf k f (langFunc_rel_ss r v i h))).lMap
-                L.ofSubLanguage) := rfl
-      _ = nrel r (fun i => ((v i).toSubLanguage' pf pr
-            (fun k f h => hf k f (langFunc_rel_ss r v i h))).lMap
-              L.ofSubLanguage) := by
-        rfl
-      _ = nrel r v := congrArg (nrel r) hv
+    exact congrArg (nrel r) hv
   case hall φ ih =>
     calc
       lMap L.ofSubLanguage (toSubLanguage' pf pr (∀' φ) hf hr) =
@@ -210,7 +185,13 @@ def toSubLanguage' (pf : ∀ k, L.Func k → Prop) (pr : ∀ k, L.Rel k → Prop
       lMap L.ofSubLanguage (toSubLanguage' pf pr (∃' φ) hf hr) =
           ∃' lMap L.ofSubLanguage (toSubLanguage' pf pr φ hf hr) := rfl
       _ = ∃' φ := congrArg Semiformula.ex (ih hf hr)
-  all_goals simp_all [toSubLanguage']
+  all_goals simp only [toSubLanguage']
+  case hverum => rfl
+  case hfalsum => rfl
+  case hand φ ψ ihp ihq =>
+    exact congrArg₂ Semiformula.and (ihp _ _) (ihq _ _)
+  case hor φ ψ ihp ihq =>
+    exact congrArg₂ Semiformula.or (ihp _ _) (ihq _ _)
 
 /-- Imported declaration from the Incompleteness formalization. -/
 noncomputable def languageFuncIndexed (φ : Semiformula L μ n) (k) : Finset (L.Func k) :=

LeanPool/Incompleteness/Foundation/Modal/Entailment/K5.lean

@@ -7,10 +7,6 @@ module
 
 public import LeanPool.Incompleteness.Foundation.Modal.Entailment.K
 
-import Mathlib.Data.Finset.Attr
-import Mathlib.Tactic.Bound.Init
-import Mathlib.Tactic.Finiteness.Attr
-import Mathlib.Tactic.SetLike
 
 /-! # K5 -/
 

LeanPool/Incompleteness/Foundation/Modal/Kripke/Completeness.lean

@@ -37,7 +37,7 @@ namespace canonicalFrame
 
 variable {Ω₁ Ω₂ : (canonicalFrame 𝓢).World}
 
-@[simp] lemma rel_def_box : Ω₁ ≺ Ω₂ ↔ ∀ {φ}, □φ ∈ Ω₁ → φ ∈ Ω₂ := by simp [Frame.Rel']; aesop;
+@[simp] lemma rel_def_box : Ω₁ ≺ Ω₂ ↔ ∀ {φ}, □φ ∈ Ω₁ → φ ∈ Ω₂ := Iff.rfl
 
 lemma multirel_def_multibox : Ω₁ ≺^[n] Ω₂ ↔ ∀ {φ}, □^[n]φ ∈ Ω₁.1 → φ ∈ Ω₂.1 := by
   induction n generalizing Ω₁ Ω₂ with
@@ -91,10 +91,8 @@ lemma multirel_def_multibox : Ω₁ ≺^[n] Ω₂ ↔ ∀ {φ}, □^[n]φ ∈ Ω
         apply hΩ;
         simp_all;
 
-lemma multirel_def_multibox' : Ω₁ ≺^[n] Ω₂ ↔ ∀ {φ}, φ ∈ (□''⁻¹^[n]Ω₁.1) → φ ∈ Ω₂.1 := by
-  constructor;
-  · intro h φ hp; exact multirel_def_multibox.mp h hp;
-  · intro h; apply multirel_def_multibox.mpr; assumption;
+lemma multirel_def_multibox' : Ω₁ ≺^[n] Ω₂ ↔ ∀ {φ}, φ ∈ (□''⁻¹^[n]Ω₁.1) → φ ∈ Ω₂.1 :=
+  multirel_def_multibox
 
 lemma multirel_def_multidia : Ω₁ ≺^[n] Ω₂ ↔ ∀ {φ}, (φ ∈ Ω₂.1 → ◇^[n]φ ∈ Ω₁.1) :=
   Iff.trans multirel_def_multibox multibox_multidia

LeanPool/Incompleteness/Foundation/Modal/Kripke/Hilbert/GL/Completeness.lean

@@ -42,15 +42,16 @@ namespace miniCanonicalFrame
 
 lemma is_irreflexive : Std.Irrefl (miniCanonicalFrame φ).Rel := by
   constructor
-  simp_all
+  rintro X ⟨_, χ, _, hnot, hmem⟩
+  exact hnot hmem
 
 lemma is_transitive : IsTrans (miniCanonicalFrame φ).World (miniCanonicalFrame φ).Rel := by
   constructor
-  rintro X Y Z ⟨RXY, ⟨χ, _, _, _⟩⟩ ⟨RYZ, _⟩;
-  constructor;
-  · simp_all
-  · use χ;
-    simp_all
+  rintro X Y Z ⟨RXY, ⟨χ, hχ, hnot, hmem⟩⟩ ⟨RYZ, _⟩
+  constructor
+  · intro ψ hψ hX
+    exact RYZ ψ hψ (RXY ψ hψ hX).2
+  · exact ⟨χ, hχ, hnot, (RYZ χ hχ hmem).2⟩
 
 end miniCanonicalFrame
 
@@ -64,24 +65,21 @@ abbrev miniCanonicalModel (φ : Formula ℕ) : Kripke.Model where
 lemma truthlemma_lemma1
   {X : ComplementClosedConsistentFinset Hilbert.GL φ.subformulas} (hq : □ψ ∈ φ.subformulas)
   : ((X.1.prebox ∪ X.1.prebox.modalBox) ∪ {□ψ, -ψ}) ⊆ φ.subformulas⁻ := by
-  intro χ hr;
-  replace hr : χ = □ψ ∨ χ = -ψ ∨ □χ ∈ X ∨ (∃ a, □a ∈ X ∧ □a = χ) := by simp at hr; tauto;
-  rcases hr with (rfl | rfl | hp | ⟨χ, hr, rfl⟩);
-  · apply Finset.mem_union.mpr;
-    tauto;
-  · apply Finset.mem_union.mpr;
-    right;
-    apply Finset.mem_image.mpr;
-    use ψ;
-    constructor;
-    · exact subformulas.mem_box hq;
-    · tauto;
-  · have := X.closed.subset hp;
-    have := FormulaFinset.complementary_mem_box (by apply subformulas.mem_imp₁) this;
-    apply Finset.mem_union.mpr;
-    left;
-    exact subformulas.mem_box this;
-  · exact X.closed.subset hr;
+  intro χ hr
+  simp only [Finset.mem_union, Finset.mem_insert, Finset.mem_singleton] at hr
+  rcases hr with (hprebox | hbox) | rfl | rfl
+  · have hp : □χ ∈ X.1 := by
+      simpa only [Finset.eq_prebox_premultibox_one, Finset.mem_preimage,
+        Function.iterate_one] using hprebox
+    have := X.closed.subset hp
+    have := FormulaFinset.complementary_mem_box (by apply subformulas.mem_imp₁) this
+    exact Finset.mem_union_left _ (subformulas.mem_box this)
+  · obtain ⟨χ, hχ, rfl⟩ := Finset.mem_image.mp hbox
+    apply X.closed.subset
+    simpa only [Finset.eq_prebox_premultibox_one, Finset.mem_preimage,
+      Function.iterate_one] using hχ
+  · exact Finset.mem_union_left _ hq
+  · exact Finset.mem_union_right _ (Finset.mem_image.mpr ⟨ψ, subformulas.mem_box hq, rfl⟩)
 
 
 lemma truthlemma_lemma2
@@ -92,14 +90,14 @@ lemma truthlemma_lemma2
   apply FormulaFinset.intro_union_consistent;
   rintro Γ₁ Γ₂ ⟨hΓ₁, hΓ₂⟩;
   replace hΓ₂ : ∀ χ ∈ Γ₂, χ = □ψ ∨ χ = -ψ := by
-    simp_all
+    simpa only [Finset.mem_insert, Finset.mem_singleton] using hΓ₂
   by_contra hC;
   have : Γ₁ ⊢[_]! ⋀Γ₂ ==> ⊥ := provable_iff.mpr <| and_imply_iff_imply_imply'!.mp hC;
   have : Γ₁ ⊢[_]! (□ψ ⋏ -ψ) ==> ⊥ := imp_trans''! (by
     suffices Γ₁ ⊢[Hilbert.GL]! ⋀[□ψ, -ψ] ==> ⋀Γ₂ by
-      simp_all
-    apply conjconj_subset!;
-    simpa using hΓ₂;
+      simpa only [List.conj₂_doubleton] using this
+    apply conjconj_subset!
+    simpa only [List.mem_cons, List.not_mem_nil, or_false] using hΓ₂
   ) this;
   have : Γ₁ ⊢[_]! □ψ ==> -ψ ==> ⊥ := and_imply_iff_imply_imply'!.mp this;
   have : Γ₁ ⊢[Hilbert.GL]! □ψ ==> ψ := by
@@ -112,8 +110,9 @@ lemma truthlemma_lemma2
   have : _ ⊢! ⋀□'Γ₁ ==> □ψ := provable_iff.mp this;
   have : _ ⊢! ⋀□'(X.1.prebox ∪ X.1.prebox.modalBox |>.toList) ==> □ψ :=
     imp_trans''! (conjconj_subset! (by
-    simp_all
-  )) this;
+      intro χ hχ
+      exact List.box_subset_mono (fun {ψ} hψ ↦ Finset.mem_toList.mpr (hΓ₁ ψ hψ)) hχ
+    )) this;
   have : _ ⊢! ⋀□'(X.1.prebox.toList) ==> □ψ := imp_trans''! (conjconj_provable! (by
     suffices ∀ χ, (□χ ∈ X ∨ ∃ χ', □χ' ∈ X ∧ □χ' =
       χ) → (□'^[1](Finset.premultibox 1 X).toList) ⊢[Hilbert.GL]! □χ by simpa;
@@ -174,9 +173,14 @@ lemma truthlemma {X : (miniCanonicalModel φ).World} (q_sub : ψ ∈ φ.subformu
       push Not;
       use Y;
       constructor;
-      · constructor;
-        · aesop;
-        · aesop;
+      · constructor
+        · intro χ hχ hBox
+          have hprebox : χ ∈ X.1.prebox := by
+            change □χ ∈ X.1 at hBox
+            simpa only [Finset.eq_prebox_premultibox_one, Finset.mem_preimage,
+              Function.iterate_one] using hBox
+          exact ⟨hY₁.1.1 hprebox, hY₁.1.2 (Finset.mem_image.mpr ⟨χ, hprebox, rfl⟩)⟩
+        · exact ⟨ψ, q_sub, h, hY₁.2 (Finset.mem_insert_self _ _)⟩
       · apply ih ?_ |>.not.mpr;
         · apply iff_mem_compl (subformulas.mem_box q_sub) |>.not.mpr;
           push Not;

LeanPool/Incompleteness/Foundation/Modal/Kripke/Hilbert/GL/Tree.lean

@@ -9,7 +9,6 @@ public import LeanPool.Incompleteness.Foundation.Modal.Kripke.Tree
 public import LeanPool.Incompleteness.Foundation.Modal.Hilbert.WellKnown
 public import LeanPool.Incompleteness.Foundation.Modal.Kripke.AxiomL
 import LeanPool.Incompleteness.Foundation.Modal.Kripke.Hilbert.GL.Completeness
-import LeanPool.Incompleteness.Foundation.Modal.Kripke.Hilbert.GL.Soundness
 
 /-! # Tree -/