complete

FormalizedFormalLogic · Nov 24, 2024 · 83d8ebd · 83d8ebd
1 parent d4b6d72
commit 83d8ebd
Show file tree

Hide file tree

Showing 8 changed files with 105 additions and 78 deletions.
diff --git a/Arithmetization/ISigmaOne/Ind.lean b/Arithmetization/ISigmaOne/Ind.lean
@@ -56,16 +56,15 @@ lemma order_induction_sigma_or_pi {P Q : V → Prop} (hP : 𝚺-[m]-Predicate P)
       apply LO.FirstOrder.Arith.HierarchySymbol.Boldface.imp
       · simp_all only [SigmaPiDelta.alt_sigma, Fin.isValue]
         apply LO.FirstOrder.Arith.HierarchySymbol.Boldface.comp₂
-        · simp_all only [zero_add, Fin.isValue, HierarchySymbol.BoldfaceFunction.var]
-        · simp_all only [zero_add, HierarchySymbol.BoldfaceFunction.const]
-      · simp_all only [Fin.isValue]
-        apply LO.FirstOrder.Arith.HierarchySymbol.Boldface.or
+        · simp [Fin.isValue, HierarchySymbol.BoldfaceFunction.var]
+        · simp [HierarchySymbol.BoldfaceFunction.const]
+      · apply LO.FirstOrder.Arith.HierarchySymbol.Boldface.or
         · apply LO.FirstOrder.Arith.HierarchySymbol.Boldface.comp₂
-          · simp_all only [zero_add, Fin.isValue, HierarchySymbol.BoldfaceFunction.var]
-          · simp_all only [zero_add, HierarchySymbol.BoldfaceFunction.const]
+          · simp [Fin.isValue, HierarchySymbol.BoldfaceFunction.var]
+          · simp [HierarchySymbol.BoldfaceFunction.const]
         · apply LO.FirstOrder.Arith.HierarchySymbol.Boldface.comp₂
-          · simp_all only [zero_add, Fin.isValue, HierarchySymbol.BoldfaceFunction.var]
-          · simp_all only [zero_add, HierarchySymbol.BoldfaceFunction.const]
+          · simp [Fin.isValue, HierarchySymbol.BoldfaceFunction.var]
+          · simp [HierarchySymbol.BoldfaceFunction.const]
     case ind z ih =>
       have : P z ∨ Q z :=
         ind z (fun y hy ↦ by

diff --git a/Arithmetization/ISigmaOne/Metamath/Coding.lean b/Arithmetization/ISigmaOne/Metamath/Coding.lean
diff --git a/Arithmetization/ISigmaOne/Metamath/Formula/Basic.lean b/Arithmetization/ISigmaOne/Metamath/Formula/Basic.lean
@@ -1285,8 +1285,8 @@ def blueprint (pL : LDef) : Language.UformulaRec1.Blueprint pL where
   nrel := .mkSigma “y param k R v. ∃ M, !pL.termBVVecDef M k v ∧ !listMaxDef y M” (by simp)
   verum := .mkSigma “y param. y = 0” (by simp)
   falsum := .mkSigma “y param. y = 0” (by simp)
-  and := .mkSigma “y param p₁ p₂ y₁ y₂. !max y y₁ y₂” (by simp)
-  or := .mkSigma “y param p₁ p₂ y₁ y₂. !max y y₁ y₂” (by simp)
+  and := .mkSigma “y param p₁ p₂ y₁ y₂. !Arith.max y y₁ y₂” (by simp)
+  or := .mkSigma “y param p₁ p₂ y₁ y₂. !Arith.max y y₁ y₂” (by simp)
   all := .mkSigma “y param p₁ y₁. !subDef y y₁ 1” (by simp)
   ex := .mkSigma “y param p₁ y₁. !subDef y y₁ 1” (by simp)
   allChanges := .mkSigma “param' param. param' = 0” (by simp)
@@ -1311,8 +1311,8 @@ def construction : Language.UformulaRec1.Construction V L (blueprint pL) where
   falsum_defined := by intro v; simp [blueprint]
   and_defined := by intro v; simp [blueprint]; rfl
   or_defined := by intro v; simp [blueprint]; rfl
-  all_defined := by intro v; simp [blueprint]; rfl
-  ex_defined := by intro v; simp [blueprint]; rfl
+  all_defined := by intro v; simp [blueprint]
+  ex_defined := by intro v; simp [blueprint]
   allChanges_defined := by intro v; simp [blueprint]
   exChanges_defined := by intro v; simp [blueprint]
 

diff --git a/Arithmetization/ISigmaOne/Metamath/Formula/Functions.lean b/Arithmetization/ISigmaOne/Metamath/Formula/Functions.lean
@@ -46,8 +46,8 @@ def construction : Language.UformulaRec1.Construction V L (blueprint pL) where
   falsum_defined := by intro v; simp [blueprint]
   and_defined := by intro v; simp [blueprint]; rfl
   or_defined := by intro v; simp [blueprint]; rfl
-  all_defined := by intro v; simp [blueprint]; rfl
-  ex_defined := by intro v; simp [blueprint]; rfl
+  all_defined := by intro v; simp [blueprint]
+  ex_defined := by intro v; simp [blueprint]
   allChanges_defined := by intro v; simp [blueprint]
   exChanges_defined := by intro v; simp [blueprint]
 
@@ -271,8 +271,8 @@ def construction : Language.UformulaRec1.Construction V L (blueprint pL) where
   falsum_defined := by intro v; simp [blueprint]
   and_defined := by intro v; simp [blueprint]; rfl
   or_defined := by intro v; simp [blueprint]; rfl
-  all_defined := by intro v; simp [blueprint]; rfl
-  ex_defined := by intro v; simp [blueprint]; rfl
+  all_defined := by intro v; simp [blueprint]
+  ex_defined := by intro v; simp [blueprint]
   allChanges_defined := by intro v; simp [blueprint]
   exChanges_defined := by intro v; simp [blueprint]
 
@@ -434,8 +434,8 @@ def construction : Language.UformulaRec1.Construction V L (blueprint pL) where
   falsum_defined := by intro v; simp [blueprint]
   and_defined := by intro v; simp [blueprint]; rfl
   or_defined := by intro v; simp [blueprint]; rfl
-  all_defined := by intro v; simp [blueprint]; rfl
-  ex_defined := by intro v; simp [blueprint]; rfl
+  all_defined := by intro v; simp [blueprint]
+  ex_defined := by intro v; simp [blueprint]
   allChanges_defined := by intro v; simp [blueprint, L.qVec_defined.df.iff]
   exChanges_defined := by intro v; simp [blueprint, L.qVec_defined.df.iff]
 

diff --git a/Arithmetization/ISigmaOne/Metamath/Formula/Iteration.lean b/Arithmetization/ISigmaOne/Metamath/Formula/Iteration.lean
@@ -36,7 +36,7 @@ def construction : VecRec.Construction V blueprint where
   nil _ := ^⊤
   cons _ p _ ih := p ^⋏ ih
   nil_defined := by intro v; simp [blueprint]
-  cons_defined := by intro v; simp [blueprint]; rfl
+  cons_defined := by intro v; simp [blueprint]
 
 end QQConj
 
@@ -105,7 +105,7 @@ def construction : VecRec.Construction V blueprint where
   nil _ := ^⊥
   cons _ p _ ih := p ^⋎ ih
   nil_defined := by intro v; simp [blueprint]
-  cons_defined := by intro v; simp [blueprint]; rfl
+  cons_defined := by intro v; simp [blueprint]
 
 end QQDisj
 
@@ -188,7 +188,7 @@ section
 def _root_.LO.FirstOrder.Arith.substItrDef : 𝚺₁.Semisentence 4 := blueprint.resultDef |>.rew (Rew.substs ![#0, #3, #1, #2])
 
 lemma substItr_defined : 𝚺₁-Function₃ (substItr : V → V → V → V) via substItrDef :=
-  fun v ↦ by simp [construction.result_defined_iff, substItrDef, substItr]; rfl
+  fun v ↦ by simp [construction.result_defined_iff, substItrDef, substItr]
 
 @[simp] lemma substItr_defined_iff (v) :
     Semiformula.Evalbm V v substItrDef.val ↔ v 0 = substItr (v 1) (v 2) (v 3) := substItr_defined.df.iff v

diff --git a/Arithmetization/ISigmaOne/Metamath/Term/Basic.lean b/Arithmetization/ISigmaOne/Metamath/Term/Basic.lean
@@ -383,7 +383,7 @@ def construction : Fixpoint.Construction V β.blueprint where
         c.func_defined.iff, c.func_defined.graph_delta.proper.iff']
       -/
       simp only [Nat.succ_eq_add_one, Blueprint.blueprint, Nat.reduceAdd, HierarchySymbol.Semiformula.val_sigma,
-        BinderNotation.finSuccItr_one, Nat.add_zero, HierarchySymbol.Semiformula.sigma_mkDelta,
+        Nat.add_zero, HierarchySymbol.Semiformula.sigma_mkDelta,
         HierarchySymbol.Semiformula.val_mkSigma, Semiformula.eval_bexLTSucc', Semiterm.val_bvar,
         Matrix.cons_val_one, Matrix.vecHead, LogicalConnective.HomClass.map_and,
         Semiformula.eval_substs, Matrix.comp_vecCons', Matrix.cons_val_two, Matrix.vecTail,
@@ -408,7 +408,7 @@ def construction : Fixpoint.Construction V β.blueprint where
           c.bvar_defined.iff, c.fvar_defined.iff, c.func_defined.iff]
         using c.phi_iff _ _ _
         -/
-        simpa only [Nat.succ_eq_add_one, BinderNotation.finSuccItr_one, Blueprint.blueprint,
+        simpa only [Nat.succ_eq_add_one, Blueprint.blueprint,
           Nat.reduceAdd, HierarchySymbol.Semiformula.val_sigma,
           HierarchySymbol.Semiformula.val_mkDelta, HierarchySymbol.Semiformula.val_mkSigma,
           Semiformula.eval_bexLTSucc', Semiterm.val_bvar, Matrix.cons_val_one, Matrix.vecHead,

diff --git a/Arithmetization/ISigmaOne/Metamath/Term/Functions.lean b/Arithmetization/ISigmaOne/Metamath/Term/Functions.lean
@@ -25,7 +25,7 @@ def construction : Language.TermRec.Construction V L (blueprint pL) where
   bvar (param z)        := (param 1).[z]
   fvar (_     x)        := ^&x
   func (_     k f _ v') := ^func k f v'
-  bvar_defined := by intro v; simp [blueprint]; rfl
+  bvar_defined := by intro v; simp [blueprint]
   fvar_defined := by intro v; simp [blueprint]
   func_defined := by intro v; simp [blueprint]; rfl
 

diff --git a/Arithmetization/OmegaOne/Nuon.lean b/Arithmetization/OmegaOne/Nuon.lean
@@ -506,7 +506,6 @@ def segmentDef : 𝚺₀.Semisentence 7 := .mkSigma
 
 lemma segmentDef_defined : 𝚺₀.Defined (V := V) (λ v ↦ Segment (v 0) (v 1) (v 2) (v 3) (v 4) (v 5) (v 6)) segmentDef := by
   intro v; simp [Segment, segmentDef, ext_defined.df.iff, isSegmentDef_defined.df.iff, @Eq.comm _ (v 5), @Eq.comm _ (v 6)]
-  rfl
 
 def isSeriesDef : 𝚺₀.Semisentence 6 := .mkSigma
   “U I L A iter T.
@@ -530,7 +529,7 @@ lemma isSerieDef_defined : 𝚺₀.Defined (V := V) (λ v ↦ IsSeries (v 0) (v
   intro v; simp [IsSeries, isSeriesDef, length_defined.df.iff, ext_defined.df.iff, segmentDef_defined.df.iff, lt_succ_iff_le]
   apply forall₂_congr; intro x _
   rw [bex_eq_le_iff, bex_eq_le_iff, bex_eq_le_iff]
-  simp; rfl
+  simp
 
 
 def seriesDef : 𝚺₀.Semisentence 6 := .mkSigma
@@ -557,7 +556,7 @@ lemma seriesSegmentDef_defined : 𝚺₀.Defined (V := V) (λ v ↦ SeriesSegmen
     length_defined.df.iff, div_defined.df.iff, rem_defined.df.iff, seriesDef_defined.df.iff, segmentDef_defined.df.iff, lt_succ_iff_le]
   apply exists_congr; intro nₖ
   apply and_congr_right; intros
-  rw [bex_eq_le_iff, bex_eq_le_iff, bex_eq_le_iff]; simp; rfl
+  rw [bex_eq_le_iff, bex_eq_le_iff, bex_eq_le_iff]; simp
 
 def nuonAuxDef : 𝚺₀.Semisentence 3 := .mkSigma
   “A k n.