From 8aed724b057875bcfe941376ff0fff5223389a1b Mon Sep 17 00:00:00 2001 From: Vasily Ilin Date: Mon, 18 May 2026 16:46:28 +0900 Subject: [PATCH 1/6] Vendor formalization of bounded arithmetic --- LeanPool.lean | 20 + .../FormalizationOfBoundedArithmetic.lean | 36 + .../Algebra.lean | 112 +++ .../AxiomSchemes.lean | 180 ++++ .../BasicSingleSorted.lean | 93 ++ .../Complexity.lean | 651 ++++++++++++++ .../DisplayedVariables.lean | 390 +++++++++ .../IDelta0.lean | 575 ++++++++++++ .../IOPEN.lean | 365 ++++++++ .../IsEnum.lean | 123 +++ .../LanguagePeano.lean | 109 +++ .../LanguageZambella.lean | 251 ++++++ .../MathlibSimps.lean | 33 + .../Order.lean | 183 ++++ .../Register.lean | 11 + .../Semantics.lean | 686 +++++++++++++++ .../SimpRules.lean | 16 + .../Syntax.lean | 277 ++++++ .../FormalizationOfBoundedArithmetic/V0.lean | 816 ++++++++++++++++++ .../V0StrAddAssoc.lean | 115 +++ .../V0StrAddComm.lean | 66 ++ LeanPool/projects.yml | 40 + 22 files changed, 5148 insertions(+) create mode 100644 LeanPool/FormalizationOfBoundedArithmetic.lean create mode 100644 LeanPool/FormalizationOfBoundedArithmetic/Algebra.lean create mode 100644 LeanPool/FormalizationOfBoundedArithmetic/AxiomSchemes.lean create mode 100644 LeanPool/FormalizationOfBoundedArithmetic/BasicSingleSorted.lean create mode 100644 LeanPool/FormalizationOfBoundedArithmetic/Complexity.lean create mode 100644 LeanPool/FormalizationOfBoundedArithmetic/DisplayedVariables.lean create mode 100644 LeanPool/FormalizationOfBoundedArithmetic/IDelta0.lean create mode 100644 LeanPool/FormalizationOfBoundedArithmetic/IOPEN.lean create mode 100644 LeanPool/FormalizationOfBoundedArithmetic/IsEnum.lean create mode 100644 LeanPool/FormalizationOfBoundedArithmetic/LanguagePeano.lean create mode 100644 LeanPool/FormalizationOfBoundedArithmetic/LanguageZambella.lean create mode 100644 LeanPool/FormalizationOfBoundedArithmetic/MathlibSimps.lean create mode 100644 LeanPool/FormalizationOfBoundedArithmetic/Order.lean create mode 100644 LeanPool/FormalizationOfBoundedArithmetic/Register.lean create mode 100644 LeanPool/FormalizationOfBoundedArithmetic/Semantics.lean create mode 100644 LeanPool/FormalizationOfBoundedArithmetic/SimpRules.lean create mode 100644 LeanPool/FormalizationOfBoundedArithmetic/Syntax.lean create mode 100644 LeanPool/FormalizationOfBoundedArithmetic/V0.lean create mode 100644 LeanPool/FormalizationOfBoundedArithmetic/V0StrAddAssoc.lean create mode 100644 LeanPool/FormalizationOfBoundedArithmetic/V0StrAddComm.lean diff --git a/LeanPool.lean b/LeanPool.lean index 39c8ce5387..00fb0e2535 100644 --- a/LeanPool.lean +++ b/LeanPool.lean @@ -146,6 +146,26 @@ import LeanPool.FormalLearningTheory.Theorem.Online import LeanPool.FormalLearningTheory.Theorem.PAC import LeanPool.FormalLearningTheory.Theorem.PACBayes import LeanPool.FormalLearningTheory.Theorem.Separation +import LeanPool.FormalizationOfBoundedArithmetic +import LeanPool.FormalizationOfBoundedArithmetic.Algebra +import LeanPool.FormalizationOfBoundedArithmetic.AxiomSchemes +import LeanPool.FormalizationOfBoundedArithmetic.BasicSingleSorted +import LeanPool.FormalizationOfBoundedArithmetic.Complexity +import LeanPool.FormalizationOfBoundedArithmetic.DisplayedVariables +import LeanPool.FormalizationOfBoundedArithmetic.IDelta0 +import LeanPool.FormalizationOfBoundedArithmetic.IOPEN +import LeanPool.FormalizationOfBoundedArithmetic.IsEnum +import LeanPool.FormalizationOfBoundedArithmetic.LanguagePeano +import LeanPool.FormalizationOfBoundedArithmetic.LanguageZambella +import LeanPool.FormalizationOfBoundedArithmetic.MathlibSimps +import LeanPool.FormalizationOfBoundedArithmetic.Order +import LeanPool.FormalizationOfBoundedArithmetic.Register +import LeanPool.FormalizationOfBoundedArithmetic.Semantics +import LeanPool.FormalizationOfBoundedArithmetic.SimpRules +import LeanPool.FormalizationOfBoundedArithmetic.Syntax +import LeanPool.FormalizationOfBoundedArithmetic.V0 +import LeanPool.FormalizationOfBoundedArithmetic.V0StrAddAssoc +import LeanPool.FormalizationOfBoundedArithmetic.V0StrAddComm import LeanPool.ForwardEuler import LeanPool.ForwardEuler.Main import LeanPool.GrothendieckVanishing diff --git a/LeanPool/FormalizationOfBoundedArithmetic.lean b/LeanPool/FormalizationOfBoundedArithmetic.lean new file mode 100644 index 0000000000..da97c78d09 --- /dev/null +++ b/LeanPool/FormalizationOfBoundedArithmetic.lean @@ -0,0 +1,36 @@ +/- +Copyright (c) 2026 ruplet. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: ruplet +-/ + +import LeanPool.FormalizationOfBoundedArithmetic.Algebra +import LeanPool.FormalizationOfBoundedArithmetic.AxiomSchemes +import LeanPool.FormalizationOfBoundedArithmetic.BasicSingleSorted +import LeanPool.FormalizationOfBoundedArithmetic.Complexity +import LeanPool.FormalizationOfBoundedArithmetic.DisplayedVariables +import LeanPool.FormalizationOfBoundedArithmetic.IDelta0 +import LeanPool.FormalizationOfBoundedArithmetic.IOPEN +import LeanPool.FormalizationOfBoundedArithmetic.IsEnum +import LeanPool.FormalizationOfBoundedArithmetic.LanguagePeano +import LeanPool.FormalizationOfBoundedArithmetic.LanguageZambella +import LeanPool.FormalizationOfBoundedArithmetic.MathlibSimps +import LeanPool.FormalizationOfBoundedArithmetic.Order +import LeanPool.FormalizationOfBoundedArithmetic.Register +import LeanPool.FormalizationOfBoundedArithmetic.Semantics +import LeanPool.FormalizationOfBoundedArithmetic.SimpRules +import LeanPool.FormalizationOfBoundedArithmetic.Syntax +import LeanPool.FormalizationOfBoundedArithmetic.V0 +import LeanPool.FormalizationOfBoundedArithmetic.V0StrAddAssoc +import LeanPool.FormalizationOfBoundedArithmetic.V0StrAddComm + +/-! +# Formalization of bounded arithmetic + +Source: url:https://github.com/ruplet/formalization-of-bounded-arithmetic +Authors: ruplet +Status: verified +Main declarations: `IOPENModel.add_assoc`, `V0Model.ind_of_comp`, `str_add_assoc` +Tags: logic, bounded-arithmetic, model-theory, computational-complexity +MSC: 03F30, 03D15 +-/ diff --git a/LeanPool/FormalizationOfBoundedArithmetic/Algebra.lean b/LeanPool/FormalizationOfBoundedArithmetic/Algebra.lean new file mode 100644 index 0000000000..6fc121ede9 --- /dev/null +++ b/LeanPool/FormalizationOfBoundedArithmetic/Algebra.lean @@ -0,0 +1,112 @@ +/- +Copyright (c) 2026 ruplet. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: ruplet +-/ + +import Mathlib.Algebra.Regular.Defs + +import LeanPool.FormalizationOfBoundedArithmetic.IOPEN +import LeanPool.FormalizationOfBoundedArithmetic.IDelta0 + +-- INSTANCES! + +universe u v + +section IOPEN +variable {M : Type u} [iopen : IOPENModel M] + +open BASICModel IOPENModel + + +theorem isAddRightRegular_one : IsAddRightRegular (1 : M) := by + unfold IsAddRightRegular Function.Injective + exact B2 + +instance : IsRightCancelAdd M where + add_right_cancel := by + intro a + unfold IsAddRightRegular Function.Injective + intro b c + simp only + apply add_cancel_right.mp + +instance : MulZeroClass M where + zero_mul := zero_mul + mul_zero := by apply B5 + +instance : CommMonoid M where + mul_assoc := mul_assoc + one_mul := one_mul + mul_one := mul_one + mul_comm := mul_comm + +instance : AddCommMonoid M where + add_assoc := add_assoc + zero_add := zero_add + add_zero := by + exact B3 + nsmul := nsmulRec + add_comm := add_comm + +instance : Semiring M where + left_distrib := by + exact IOPENModel.mul_add + right_distrib := by + intro a b c + rw [<- iopen.mul_comm] + rw [iopen.mul_add] + rw [iopen.mul_comm] + conv => lhs; rhs; rw [iopen.mul_comm] + +end IOPEN + +section IDelta0 + +open BASICModel +variable {M : Type u} [idelta0 : IDelta0Model M] + +instance : IsOrderedAddMonoid M where + add_le_add_left := fun _ _ a_1 c ↦ add_le_add_left a_1 c + +-- D7 used +instance : IsOrderedMonoid M where + mul_le_mul_left := fun a b h c ↦ by + exact idelta0.le_mul_right h + +instance : AddCommMonoid M where + + +instance : IsOrderedRing M where + zero_le_one := by exact idelta0.zero_le 1 + mul_le_mul_of_nonneg_left := by + intro a h_zero_a b c hbc + rw [mul_comm a b, mul_comm a c] + exact idelta0.le_mul_right hbc + mul_le_mul_of_nonneg_right := by + intro c h_zero_c a b hab + exact idelta0.le_mul_right hab + +instance : CommSemiring M where + +instance : IsLeftCancelAdd M where + add_left_cancel x := by + unfold IsAddLeftRegular + unfold Function.Injective + intro a1 a2 + simp only + intro h + conv at h => + rw [add_comm] + rhs + rw [add_comm] + rw [@IOPENModel.add_cancel_right] at h + exact h + +-- instance : IsStrictOrderedRing M where +-- le_of_add_le_add_left := by +-- intro a b c h +-- rw [le_cancel_left] + + +end IDelta0 diff --git a/LeanPool/FormalizationOfBoundedArithmetic/AxiomSchemes.lean b/LeanPool/FormalizationOfBoundedArithmetic/AxiomSchemes.lean new file mode 100644 index 0000000000..36cb26b32e --- /dev/null +++ b/LeanPool/FormalizationOfBoundedArithmetic/AxiomSchemes.lean @@ -0,0 +1,180 @@ +/- +Copyright (c) 2026 ruplet. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: ruplet +-/ + +import Lean + +import Mathlib.ModelTheory.Syntax +import Mathlib.ModelTheory.Semantics + +import LeanPool.FormalizationOfBoundedArithmetic.IsEnum +import LeanPool.FormalizationOfBoundedArithmetic.DisplayedVariables +import LeanPool.FormalizationOfBoundedArithmetic.LanguagePeano +import LeanPool.FormalizationOfBoundedArithmetic.LanguageZambella +import LeanPool.FormalizationOfBoundedArithmetic.Syntax +import LeanPool.FormalizationOfBoundedArithmetic.Semantics +import LeanPool.FormalizationOfBoundedArithmetic.Order + +open FirstOrder Language BoundedFormula Formula + + +-- i think that type level is set to 0 because of +-- Vars1x type is just Type +-- variable {α disp : Type} + +-- Definition 3.4 (Induction Scheme), p. 35 od draft (46 of PDF) +-- Note that `phi(x)` is permitted to have free variables other than `x` +-- This means that ultimately we need to take universal closure of the +-- resulting Bounded Formula, to get a Sentence (no free vars) +-- expect 1 displayed free variable (`x`), thus DisplayedFV1 +-- but we can have more free vars - we `forall` over them! +/-- Build the universal closure of an induction axiom for a displayed variable. -/ +def mkInductionSentence + {a} [IsEnum a] {name} + {L : Language} + [Zero <| L.Term Empty] + [One <| L.Term (Vars1 name)] + [Add <| L.Term (Vars1 name)] + (phi : L.Formula ((Vars1 name) ⊕ a)) + : L.Sentence := + let univ := phi.iAlls' + let base := univ.subst (fun _ => 0) + let step_assumption := univ + let step_target := univ.subst (fun _ => (var Vars1.fv1) + 1) + let step' : L.Formula (Vars1 name) := step_assumption ⟹ step_target + let step := step'.display1.flip.iAlls' + let forall_x_holds := univ.display1.flip.iAlls' + base ⟹ step ⟹ forall_x_holds + +/-- Normalize a realized induction sentence in a hypothesis. -/ +syntax (name := simp_induction) "simp_induction" " at " (ppSpace ident)? : tactic + +macro_rules +| `(tactic| simp_induction at $h:ident) => + `(tactic| + conv at $h => + unfold Sentence.Realize mkInductionSentence + rw [Formula.realize_imp]; + rw [Formula.realize_imp]; + conv => + lhs + unfold Formula.Realize + rw [BoundedFormula.realize_subst] + change Formula.Realize _ _ + conv => + rhs; lhs + rw [realize_iAlls'.Vars1]; ext + rw [Formula.realize_flip] + rw [realize_display1] + rw [Formula.realize_imp]; + conv => lhs -- this is just `univ` already + conv => + rhs + unfold Formula.Realize + rw [BoundedFormula.realize_subst] + change Formula.Realize _ _ + simp only [delta0_simps] + unfold Formula.Realize + simp only [delta0_simps] + ) + +/-- Coerce a bounded formula with no bound variables to a formula. -/ +def _root_.FirstOrder.Language.BoundedFormula.toFormula' {L : Language} {a} + (phi : L.BoundedFormula a 0) : L.Formula a := phi + +-- This is induction sentence creator which instead of ∀x, φ(x), +-- gives you ∀x : int, φ(x) +/-- Build a typed induction sentence that guards the induction variable as numeric. -/ +def mkInductionSentenceTyped + {a} [IsEnum a] {name} + {n} + (phi : zambella.BoundedFormula ((Vars1 name) ⊕ a) n) + : zambella.Sentence := + let univ := phi.alls.iAlls' + let base := univ.subst (fun _ => 0) + let step_assumption := univ + let step_target : zambella.Formula (Vars1 name) := univ.subst (fun _ => (var .fv1) + 1) + let step' : zambella.Formula (Vars1 name) := step_assumption ⟹ step_target + let step := step'.IsNum.toFormula'.display1.flip.iAlls' + let forall_x_holds := univ.IsNum.toFormula'.display1.flip.iAlls' + base ⟹ step ⟹ forall_x_holds + + +-- Definition V.I.2 (Comprehension Axiom); p. 96 PDF; release of Logical Foundations +-- `X` cannot occur free in `phi(z)`, but `y` can +/-- Build the bounded-comprehension sentence associated to a displayed formula. -/ +def mkComprehensionSentence {a} [IsEnum a] {name} + (phi : zambella.Formula (((Vars1 name) ⊕ (Vars1 .y)) ⊕ a)) + : zambella.Sentence := + -- now `y` is accessible and nothing else! + let univ : zambella.Formula (Vars1 name ⊕ Vars1 FvName.y) + := phi.iAlls' + -- X(z) ↔ φ(z) + let iff : zambella.Formula (Vars3 .y .z .X) := + z ∈' X ⇔ + univ.subst (Sum.elim (fun _ => .var z.name) (fun _ => .var y.name)) + let iff : zambella.Formula (Vars1 .z ⊕ Vars2 .y .X) := + (display3 .z iff.rotate_213) + let all_z : zambella.Formula (Vars2 .y .X) := + iBdAllNumLt' y iff.flip + let X_def : zambella.Formula (Vars1 .X ⊕ Vars1 .y) := + (display2 .X (X.IsStr ⊓ all_z).rotate_21) + let ex_X : zambella.Formula (Vars1 .y) := iExs' X_def.flip + let ex_X_typed : zambella.Formula (Vars1 .y) := + ex_X.IsNum + -- quantify over `y`, the length of str created + ex_X_typed.mkInl.flip.iAlls' + +/-- Normalize a realized comprehension sentence in a hypothesis. -/ +syntax (name := simp_comp) "simp_comp" " at " (ppSpace ident)? : tactic + +macro_rules +| `(tactic| simp_comp at $h:ident) => + `(tactic| + conv at $h => + unfold Sentence.Realize mkComprehensionSentence + rw [realize_iAlls'.Vars1]; ext + rw [realize_flip] + rw [realize_mkInl] + unfold Formula.IsNum + rw [Formula.realize_imp] + conv => + lhs + rw [Term.realize_isnum] + lhs; arg 1 + simp only [delta0_simps] + rhs + rw [realize_iExs'.Vars1]; right; ext + rw [realize_flip] + rw [realize_display2] + rw [realize_rotate_21] + rw [Formula.realize_inf] + conv => + lhs + rw [Term.realize_isstr] + simp only [delta0_simps] + conv => + rhs + rw [realize_iBdAllNumLt'.Vars1]; ext + conv => + lhs + simp only [delta0_simps] + ext + ext + rw [realize_flip] + rw [realize_display3] + rw [realize_rotate_213] + rw [Formula.realize_iff] + conv => + lhs + unfold Formula.Realize + simp only [delta0_simps] + rhs + unfold Formula.Realize + rw [realize_subst] + rw [Formula.boundedFormula_realize_eq_realize] + rw [realize_iAlls'.Vars1]; ext + simp only [delta0_simps] + ) diff --git a/LeanPool/FormalizationOfBoundedArithmetic/BasicSingleSorted.lean b/LeanPool/FormalizationOfBoundedArithmetic/BasicSingleSorted.lean new file mode 100644 index 0000000000..b1ae8e0461 --- /dev/null +++ b/LeanPool/FormalizationOfBoundedArithmetic/BasicSingleSorted.lean @@ -0,0 +1,93 @@ +/- +Copyright (c) 2026 ruplet. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: ruplet +-/ + +import Mathlib.ModelTheory.Semantics +import LeanPool.FormalizationOfBoundedArithmetic.LanguagePeano + +open FirstOrder FirstOrder.Language + +universe u + +-- Section 3.1 Peano Arithmetic; draft page 34 (45 of pdf) +-- semi-bundled design! inspired by mathlib Ring +-- extending peano.Structure instead of One, Add, ... is needed to .Realize +/-- Single-sorted models of the BASIC arithmetic axioms. -/ +class BASICModel (num : Type u) extends + peano.Structure.{u} num +where + B1 : ∀ {x : num}, (x + 1) ≠ 0 + B2 : ∀ x y : num, (x + 1) = (y + 1) -> x = y + B3 : ∀ x : num, x + 0 = x + B4 : ∀ {x y : num}, x + (y + 1) = (x + y) + 1 + B5 : ∀ {x : num}, x * 0 = 0 + B6 : ∀ {x y : num}, x * (y + 1) = x * y + x + -- le_antisymm + B7 : ∀ {x y : num}, x <= y -> y <= x -> x = y + -- le_self_add + B8 : ∀ {x y : num}, x <= x + y + + +/-- BASIC models with the additional axiom `(0 : num) + 1 = 1`. -/ +class BASICModelExt (num : Type u) extends BASICModel num where +-- skip this axiom by default +-- we will use induction anyway for IDelta0, and it is problematic +-- when defining 2-BASIC axioms and V^i later on + +-- it is interesting because BASICModelExt alone implies all +-- true quantifier-free sentences over `peano` language! +-- (source: Logical Foundations, release, p. 40 (p. 58 of PDF)) + C : (0 : num) + 1 = 1 + +-- instance (M : Type*) [BASICModel M] : Zero M where +-- zero := 0 + +-- instance (M : Type*) [BASICModel M] : Add M where +-- add x y := x + y + +-- instance (M : Type*) [BASICModel M] : Mul M where +-- mul x y := x * y + +-- instance (M : Type*) [BASICModel M] : LE M where +-- le x y := x <= y + +-- instance (M : Type*) [BASICModel M] : LT M where +-- lt x y := x <= y ∧ x ≠ y + +variable {M} [BASICModel M] + +/-- Interpret natural-number literals in a BASIC model by iterating successor. -/ +def natToM : Nat -> M +| 0 => 0 +| 1 => 1 +| n + 1 => natToM n + 1 + +instance (n) : OfNat M n where + ofNat := natToM n + +/-- Pairing function used to encode two numbers as one number. -/ +def pair (x y : M) := (x + y) * (x + y + 1) + (1 + 1) * y + +/-- Pairing notation for two numbers. -/ +notation "⟨" i "," j "⟩" => pair i j + +/-- Pairing notation for three numbers. -/ +notation "⟨" i "," j "," k "⟩" => pair (pair i j) k + +namespace BASICModel + +variable {M : Type u} [iopen : BASICModel M] + +-- this is axctually O9. x ≤ x from Logical Foundations +theorem le_refl : ∀ a : M, a <= a := by + intro x + conv => right; rw [<- B3 x] + apply B8 + +theorem zero_ne_add_one : ∀ x : M, x + 1 ≠ 0 := by apply B1 +theorem one_add_right_regular : IsAddRightRegular (1 : M) := by apply B2 + + +end BASICModel diff --git a/LeanPool/FormalizationOfBoundedArithmetic/Complexity.lean b/LeanPool/FormalizationOfBoundedArithmetic/Complexity.lean new file mode 100644 index 0000000000..651404a909 --- /dev/null +++ b/LeanPool/FormalizationOfBoundedArithmetic/Complexity.lean @@ -0,0 +1,651 @@ +/- +Copyright (c) 2026 ruplet. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: ruplet +-/ + +import Mathlib.ModelTheory.Complexity +import Mathlib.ModelTheory.Syntax + +import LeanPool.FormalizationOfBoundedArithmetic.DisplayedVariables +import LeanPool.FormalizationOfBoundedArithmetic.Order +import LeanPool.FormalizationOfBoundedArithmetic.LanguagePeano +import LeanPool.FormalizationOfBoundedArithmetic.LanguageZambella +import LeanPool.FormalizationOfBoundedArithmetic.Register + +open FirstOrder Language + +universe u +variable {L : Language} {α β : Type u} {n : Nat} + +namespace FirstOrder.Language + +namespace BoundedFormula.IsAtomic +variable {φ : L.BoundedFormula α n} + +namespace relabelEquiv + +theorem mpr {f : α ≃ β} (h : φ.IsAtomic) + : (φ.relabelEquiv f).IsAtomic +:= + IsAtomic.recOn h (fun _ _ => IsAtomic.equal _ _) fun _ _ => IsAtomic.rel _ _ + +theorem mp {f : α ≃ β} (h : (φ.relabelEquiv f).IsAtomic) + : φ.IsAtomic := +by + cases φ <;> (try cases h) <;> constructor + +end relabelEquiv + +@[delta0_simps] +theorem relabelEquiv {f : α ≃ β} : + (φ.relabelEquiv f).IsAtomic <-> φ.IsAtomic := + ⟨relabelEquiv.mp, relabelEquiv.mpr⟩ +end BoundedFormula.IsAtomic + +namespace Formula.IsAtomic +open BoundedFormula + +@[delta0_simps] +theorem display1 {n1} {phi : L.Formula (Vars1 n1)} : + phi.display1.IsAtomic <-> phi.IsAtomic := +by + unfold Formula.display1 + rw [IsAtomic.relabelEquiv] + +@[delta0_simps] +theorem display2 {n1 n2} {phi : L.Formula (Vars2 n1 n2)} : + phi.display2.IsAtomic <-> phi.IsAtomic := +by + unfold Formula.display2 + rw [IsAtomic.relabelEquiv] + +@[delta0_simps] +theorem display3 {n1 n2 n3} {phi : L.Formula (Vars3 n1 n2 n3)} : + phi.display3.IsAtomic <-> phi.IsAtomic := +by + unfold Formula.display3 + rw [IsAtomic.relabelEquiv] + +end Formula.IsAtomic + +namespace BoundedFormula.IsQF + +namespace imp + +@[delta0_simps] +theorem mpr {L : Language} {α} {m} {φ ψ : L.BoundedFormula α m} : + (φ.imp ψ).IsQF <-> (φ.IsQF ∧ ψ.IsQF) := +by + constructor + · intro h + constructor + · cases h with + | of_isAtomic h' => cases h' + | imp pre post => exact pre + · cases h with + | of_isAtomic h' => cases h' + | imp pre post => exact post + · intro h + apply IsQF.imp h.left h.right + +end imp + +namespace relabelEquiv + +@[delta0_simps] +theorem mp {L : Language} {α β} {m : ℕ} {φ : L.BoundedFormula α m} + (f : α ≃ β) + (h : φ.IsQF) + : (φ.relabelEquiv f).IsQF := +by + induction φ with + | falsum => + constructor + | equal lhs rhs => + simp only [relabelEquiv, mapTermRelEquiv, Equiv.coe_refl, Equiv.refl_symm, Equiv.coe_fn_mk, + mapTermRel, Term.relabelEquiv_apply] + constructor; constructor + | rel R ts => + simp only [relabelEquiv, mapTermRelEquiv, Equiv.coe_refl, Equiv.refl_symm, Equiv.coe_fn_mk, + mapTermRel, Term.relabelEquiv_apply] + constructor; constructor + | imp pre post hind_pre hind_post => + cases h with + | of_isAtomic hh => cases hh + | imp hpre hpost => + rw [relabelEquiv.imp] + apply IsQF.imp + · exact hind_pre hpre + · exact hind_post hpost + | all f f_ih => + cases h with + | of_isAtomic h' => cases h' + +@[delta0_simps] +theorem mpr {L : Language} {α β} {m : ℕ} {φ : L.BoundedFormula α m} (f : α ≃ β) + (h : (φ.relabelEquiv f).IsQF) + : φ.IsQF := +by + have h' : relabelEquiv f.symm ((relabelEquiv f) φ) = φ := relabelEquiv.comp_inv f + rw [<- h'] + apply relabelEquiv.mp + exact h + +end relabelEquiv + +@[delta0_simps] +theorem relabelEquiv {L : Language} {α β} {m : ℕ} {φ : L.BoundedFormula α m} (f : α ≃ β) : + (φ.relabelEquiv f).IsQF <-> φ.IsQF := ⟨IsQF.relabelEquiv.mpr f, IsQF.relabelEquiv.mp f⟩ + + +end BoundedFormula.IsQF + + + + +-- Definition 3.7, page 36 of draft (47 of pdf) +namespace BoundedFormula + +/-- Open formulas are quantifier-free bounded formulas. -/ +abbrev IsOpen (formula : L.BoundedFormula α n) + := IsQF formula +namespace IsOpen +variable {phi : L.BoundedFormula α n} + +@[delta0_simps] +theorem equal (t1 t2 : L.Term (α ⊕ Fin n)) + : (t1.bdEqual t2).IsOpen := +by + constructor + apply IsAtomic.equal + +namespace imp +namespace mpr + +@[delta0_simps] +theorem left {psi : _} + : (phi.imp psi).IsOpen -> phi.IsOpen := +by + intro h + -- TODO: order of constructors in IsQF should be reversed, + -- so that `constructor` here works! + cases h with + | of_isAtomic h => cases h + | imp p q => exact p + +@[delta0_simps] +theorem right {psi : _} + : (phi.imp psi).IsOpen -> psi.IsOpen := +by + intro h + cases h with + | of_isAtomic h => cases h + | imp p q => exact q + +end mpr +end imp + +@[delta0_simps] +theorem not + : phi.not.IsOpen <-> phi.IsOpen := +by + constructor <;> (unfold BoundedFormula.not; intro h) + · exact imp.mpr.left h + · apply IsQF.imp + · assumption + · exact isQF_bot + +@[delta0_simps] +theorem relabelEquiv {f : α ≃ β} + : (phi.relabelEquiv f).IsOpen <-> phi.IsOpen := +by + apply IsQF.relabelEquiv + +end IsOpen +end BoundedFormula + +namespace Formula.IsOpen +open BoundedFormula.IsOpen + +@[delta0_simps] +theorem display1 {n1} {phi : L.Formula (Vars1 n1)} : + phi.display1.IsOpen <-> phi.IsOpen := by + unfold Formula.display1 + rw [relabelEquiv] + +@[delta0_simps] +theorem display2 {n1 n2} {phi : L.Formula (Vars2 n1 n2)} : + phi.display2.IsOpen <-> phi.IsOpen := by + unfold Formula.display2 + rw [relabelEquiv] + +@[delta0_simps] +theorem display3 {n1 n2 n3} {phi : L.Formula (Vars3 n1 n2 n3)} : + phi.display3.IsOpen <-> phi.IsOpen := by + unfold Formula.display3 + rw [relabelEquiv] + +end Formula.IsOpen + + + +variable {L : Language} [IsOrdered L] {a : Type u} +open BoundedFormula Formula + +-- Definition 3.7, page 36 of draft (47 of pdf) +-- + Definition 3.6, page 35 of draft (46 of pdf) +-- fix level of `a` to 0, because level of `Vars` was fixed to 0! +namespace BoundedFormula + +/-- Delta-zero formulas, built from quantifier-free formulas and bounded number quantifiers. -/ +inductive IsDelta0 : + ∀ {a : Type} {n : Nat}, L.BoundedFormula a n -> Prop +| bdEx {a : Type} {n : FvName} + {phi : L.Formula (a ⊕ (Vars1 n))} + (t : L.Term (a ⊕ Fin 0)) + : IsDelta0 phi -> (IsDelta0 <| iBdEx' t phi) +| bdAll {a : Type} {n : FvName} + {phi : L.Formula (a ⊕ (Vars1 n))} + (t : L.Term (a ⊕ Fin 0)) + : IsDelta0 phi -> (IsDelta0 <| iBdAll' t phi) +| imp {a : Type} {n : Nat} {phi1 phi2 : L.BoundedFormula a n} + : IsDelta0 phi1 -> IsDelta0 phi2 -> IsDelta0 (phi1.imp phi2) +| of_isQF {a : Type} {n : Nat} {phi : L.BoundedFormula a n} + : BoundedFormula.IsQF phi -> IsDelta0 phi + +end BoundedFormula + +namespace IsDelta0 + +@[delta0_simps] +theorem bot {a n} : (⊥ : L.BoundedFormula a n).IsDelta0 := by + constructor + exact isQF_bot + +@[delta0_simps] +theorem equal {a n} (t1 t2 : L.Term (a ⊕ Fin n)) + : (t1.bdEqual t2).IsDelta0 := +by + constructor + constructor + apply IsAtomic.equal + +namespace of_open + +theorem imp {a n} {phi psi : L.BoundedFormula a n} (h : phi.IsOpen) + : (phi.imp psi).IsDelta0 <-> (phi.IsDelta0 ∧ psi.IsDelta0) := +by + constructor + · intro h + cases h with + | imp p q => + constructor + · exact p + · exact q + | of_isQF q => + rw [IsQF.imp.mpr] at q + constructor <;> + apply IsDelta0.of_isQF + · exact q.left + · exact q.right + | bdEx phi t => + cases h with + | of_isAtomic h' => + cases h' with + · intro h + apply IsDelta0.imp + · exact h.left + · exact h.right + +end of_open + +namespace of_notfalsum + +theorem imp {a n} {phi psi : L.BoundedFormula a n} (h : psi ≠ falsum) + : (phi.imp psi).IsDelta0 <-> (phi.IsDelta0 ∧ psi.IsDelta0) := +by + constructor + · intro h' + cases h' with + | imp p q => + constructor + · exact p + · exact q + | of_isQF q => + rw [IsQF.imp.mpr] at q + constructor <;> + apply IsDelta0.of_isQF + · exact q.left + · exact q.right + | bdEx phi t => + simp only [Bot.bot, ne_eq, not_true_eq_false] at h + · intro h + apply IsDelta0.imp + · exact h.left + · exact h.right + +end of_notfalsum + + +@[delta0_simps] +theorem neq {a n} (t1 t2 : L.Term (a ⊕ Fin n)) + : (t1 ≠' t2).IsDelta0 := +by + constructor + · apply equal + · apply bot + +namespace of_open + +theorem not {a n} {phi : L.BoundedFormula a n} (h : phi.IsOpen) + : phi.not.IsDelta0 <-> phi.IsDelta0 := +by + unfold BoundedFormula.not + rw [of_open.imp h] + constructor + · intro h + exact h.left + · intro h + constructor + · exact h + · exact IsDelta0.bot + +end of_open + +namespace relabelEquiv + +theorem mpAux {a b n} {phi : peano.BoundedFormula a n} + (g : a ≃ b) + (h : phi.IsDelta0) + : (phi.relabelEquiv g).IsDelta0 := +by + induction h generalizing b with + | bdEx t hphi ih => + rw [iBdEx'.relabelEquiv] + constructor + exact ih (g.sumCongr (_root_.Equiv.refl _)) + | bdAll t hphi ih => + rw [iBdAll'.relabelEquiv] + constructor + exact ih (g.sumCongr (_root_.Equiv.refl _)) + | imp pre post ihpre ihpost => + rw [relabelEquiv.imp] + constructor + · exact ihpre g + · exact ihpost g + | of_isQF f => + exact IsDelta0.of_isQF (BoundedFormula.IsQF.relabelEquiv.mp g f) + +theorem gSumCongr + {a b c} + {phi : peano.Formula (a ⊕ c)} + (g : a ≃ b) + (h : phi.IsDelta0) + : ((relabelEquiv (g.sumCongr (_root_.Equiv.refl c))) phi).IsDelta0 := +by + exact relabelEquiv.mpAux (g.sumCongr (_root_.Equiv.refl c)) h + + +@[delta0_simps] +theorem mp {a b} {phi : peano.Formula a} + (g : a ≃ b) + (h : phi.IsDelta0) + : (phi.relabelEquiv g).IsDelta0 := +by + exact relabelEquiv.mpAux g h + + +@[delta0_simps] +theorem mpr {α β} {φ : peano.Formula α} (f : α ≃ β) + (h : (φ.relabelEquiv f).IsDelta0) + : φ.IsDelta0 := +by + have h' : relabelEquiv f.symm ((relabelEquiv f) φ) = φ := relabelEquiv.comp_inv f + rw [<- h'] + apply relabelEquiv.mp + exact h + +end relabelEquiv + +@[delta0_simps] +theorem relabelEquiv {α β} (φ : peano.Formula α) {f : α ≃ β} : + (φ.relabelEquiv f).IsDelta0 <-> φ.IsDelta0 := + ⟨IsDelta0.relabelEquiv.mpr f, IsDelta0.relabelEquiv.mp f⟩ + + +@[delta0_simps] +theorem display1 {n} (phi : peano.Formula (Vars1 n)) : + phi.display1.IsDelta0 <-> phi.IsDelta0 := + IsDelta0.relabelEquiv phi + +@[delta0_simps] +theorem display2 {n1 n2} (phi : peano.Formula (Vars2 n1 n2)) : + phi.display2.IsDelta0 <-> phi.IsDelta0 := + IsDelta0.relabelEquiv phi + +@[delta0_simps] +theorem display3 {n1 n2 n3} (phi : peano.Formula (Vars3 n1 n2 n3)) : + phi.display3.IsDelta0 <-> phi.IsDelta0 := + IsDelta0.relabelEquiv phi + +@[delta0_simps] +theorem flip {a b} (phi : peano.Formula (a ⊕ b)) : + phi.flip.IsDelta0 <-> phi.IsDelta0 := + IsDelta0.relabelEquiv phi + +end IsDelta0 + + + + +-- only bounded number quantifiers allowed. and free string vars. +-- p. 82 of pdf of Logical Foundatoin release +namespace BoundedFormula + +/-- Sigma-zero-B formulas in the two-sorted Zambella language. -/ +inductive IsSigma0B {a : Type} : + {n : Nat} -> zambella.BoundedFormula a n -> Prop +| imp {phi1 phi2} (h1 : IsSigma0B phi1) (h2 : IsSigma0B phi2) + : IsSigma0B (phi1.imp phi2) +| bdEx + {n : FvName} + (phi : zambella.Formula (a ⊕ (Vars1 n))) + (t : zambella.Term (a ⊕ Fin 0)) + : IsSigma0B <| iBdEx' t + ((rel ZambellaRel.isnum ![var <| Sum.inl <| Sum.inr <| .fv1]) ⊓ phi) +-- TODO: WHICH ONE IS REDUNDANT? +| bdAll + {n : FvName} + (phi : zambella.Formula (a ⊕ (Vars1 n))) + (t : zambella.Term (a ⊕ Fin 0)) + : IsSigma0B <| iBdAllNum' t phi +| bdAllLt + {n : FvName} + (phi : zambella.Formula (a ⊕ (Vars1 n))) + (t : zambella.Term (a ⊕ Fin 0)) + : IsSigma0B <| iBdAllLt' t + ((rel ZambellaRel.isnum ![var <| Sum.inl <| Sum.inr <| .fv1]) ⊓ phi) +| of_isQF {phi} (h : IsQF phi) : IsSigma0B phi + +end BoundedFormula + +namespace Sigma0B + +namespace relabelEquiv + +theorem mpAux {a b n} {phi : zambella.BoundedFormula a n} + (g : a ≃ b) + (h : phi.IsSigma0B) + : (phi.relabelEquiv g).IsSigma0B := +by + induction h generalizing b with + | imp h1 h2 ih1 ih2 => + rw [relabelEquiv.imp] + exact BoundedFormula.IsSigma0B.imp (ih1 g) (ih2 g) + | bdEx phi t => + rw [iBdEx'.relabelEquiv] + convert BoundedFormula.IsSigma0B.bdEx + (phi.relabelEquiv (g.sumCongr (_root_.Equiv.refl _))) + (Term.relabelEquiv (g.sumCongr (_root_.Equiv.refl _)) t) using 1 + simp only [Term.relabelEquiv_apply, relabelEquiv.nf, relabelEquiv.rel, + Matrix.cons_val_fin_one, Term.relabel.eq_1, Sum.map_inl, Equiv.sumCongr_apply, + Equiv.coe_refl, Sum.map_inr, id_eq] + congr + funext i + fin_cases i + rfl + | bdAll phi t => + unfold iBdAllNum' + rw [iBdAll'.relabelEquiv] + convert BoundedFormula.IsSigma0B.bdAll + (phi.relabelEquiv (g.sumCongr (_root_.Equiv.refl _))) + (Term.relabelEquiv (g.sumCongr (_root_.Equiv.refl _)) t) using 1 + unfold Term.IsNum Relations.boundedFormula₁ Relations.boundedFormula + rw [relabelEquiv.imp] + congr + rw [relabelEquiv.rel] + congr + funext i + fin_cases i + rfl + | bdAllLt phi t => + rw [iBdAllLt'.relabelEquiv] + convert BoundedFormula.IsSigma0B.bdAllLt + (phi.relabelEquiv (g.sumCongr (_root_.Equiv.refl _))) + (Term.relabelEquiv (g.sumCongr (_root_.Equiv.refl _)) t) using 1 + simp only [Term.relabelEquiv_apply, relabelEquiv.nf, relabelEquiv.rel, + Matrix.cons_val_fin_one, Term.relabel.eq_1, Sum.map_inl, Equiv.sumCongr_apply, + Equiv.coe_refl, Sum.map_inr, id_eq] + congr + funext i + fin_cases i + rfl + | of_isQF h => + exact BoundedFormula.IsSigma0B.of_isQF (BoundedFormula.IsQF.relabelEquiv.mp g h) + +theorem mprAux {a b n} {phi : zambella.BoundedFormula a n} + (g : a ≃ b) + (h : (phi.relabelEquiv g).IsSigma0B) + : phi.IsSigma0B := +by + have h' : relabelEquiv g.symm ((relabelEquiv g) phi) = phi := relabelEquiv.comp_inv g + rw [<- h'] + exact relabelEquiv.mpAux g.symm h + +end relabelEquiv + +@[delta0_simps] +theorem relabelEquiv {a b} {g : a ≃ b} (phi : zambella.Formula a) : + (phi.relabelEquiv g).IsSigma0B <-> phi.IsSigma0B := +by + exact ⟨relabelEquiv.mprAux g, relabelEquiv.mpAux g⟩ + +@[delta0_simps] +nonrec theorem display1 {n1 : FvName} + (phi : zambella.Formula (Vars1 n1)) + : + phi.display1.IsSigma0B <-> phi.IsSigma0B := +by + unfold display1 + apply relabelEquiv + +@[delta0_simps] +nonrec theorem display2 {n1 n2 : FvName} + (phi : zambella.Formula (Vars2 n1 n2)) + : + phi.display2.IsSigma0B <-> phi.IsSigma0B := +by + unfold display2 + apply relabelEquiv + +@[delta0_simps] +nonrec theorem display3 {n1 n2 n3 : FvName} + (phi : zambella.Formula (Vars3 n1 n2 n3)) + : + phi.display3.IsSigma0B <-> phi.IsSigma0B := +by + unfold display3 + apply relabelEquiv + +@[delta0_simps] +nonrec theorem display4 {n1 n2 n3 n4 : FvName} + (phi : zambella.Formula (Vars4 n1 n2 n3 n4)) + : + phi.display4.IsSigma0B <-> phi.IsSigma0B := +by + unfold display4 + apply relabelEquiv + +@[delta0_simps] +nonrec theorem display_swapleft {n1 n2 n3 : FvName} + (phi : zambella.Formula (Vars1 n1 ⊕ Vars2 n2 n3)) + : + phi.display_swapleft.IsSigma0B <-> phi.IsSigma0B := +by + unfold display_swapleft + apply relabelEquiv + +@[delta0_simps] +nonrec theorem display_swapleft' {n1 n2 n3 : FvName} + (phi : zambella.Formula (Vars1 n1 ⊕ Vars2 n2 n3)) + : + phi.display_swapleft'.IsSigma0B <-> phi.IsSigma0B := +by + unfold display_swapleft' + apply relabelEquiv + +@[delta0_simps] +nonrec theorem rotate_21 {n1 n2 : FvName} + (phi : zambella.Formula (Vars2 n1 n2)) + : + phi.rotate_21.IsSigma0B <-> phi.IsSigma0B := +by + unfold rotate_21 + apply relabelEquiv + +@[delta0_simps] +nonrec theorem rotate_213 {n1 n2 n3 : FvName} + (phi : zambella.Formula (Vars3 n1 n2 n3)) + : + phi.rotate_213.IsSigma0B <-> phi.IsSigma0B := +by + unfold rotate_213 + apply relabelEquiv + +@[delta0_simps] +nonrec theorem rotate_231 {n1 n2 n3 : FvName} + (phi : zambella.Formula (Vars3 n1 n2 n3)) + : + phi.rotate_231.IsSigma0B <-> phi.IsSigma0B := +by + unfold rotate_231 + apply relabelEquiv + +@[delta0_simps] +nonrec theorem flip {a b} + (phi : zambella.Formula (a ⊕ b)) + : + phi.flip.IsSigma0B <-> phi.IsSigma0B := +by + unfold Formula.flip + apply relabelEquiv + +end Sigma0B + +/-- Simplify complexity side conditions in a hypothesis. -/ +syntax (name := simp_complexity) "simp_complexity" " at " (ppSpace ident)? : tactic + +macro_rules +| `(tactic| simp_complexity at $h:ident) => + `(tactic| + conv at $h => + conv => + lhs + simp only [delta0_simps] + -- this has to work! the `IsOpen` goal has to reduce to `True`. + rw [forall_const] + ) + + +end FirstOrder.Language diff --git a/LeanPool/FormalizationOfBoundedArithmetic/DisplayedVariables.lean b/LeanPool/FormalizationOfBoundedArithmetic/DisplayedVariables.lean new file mode 100644 index 0000000000..974c1e1810 --- /dev/null +++ b/LeanPool/FormalizationOfBoundedArithmetic/DisplayedVariables.lean @@ -0,0 +1,390 @@ +/- +Copyright (c) 2026 ruplet. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: ruplet +-/ + +import Mathlib.ModelTheory.Syntax +import Mathlib.ModelTheory.Semantics +import Mathlib.Tactic.FinCases +import LeanPool.FormalizationOfBoundedArithmetic.IsEnum +import LeanPool.FormalizationOfBoundedArithmetic.Register + +/-- Names used for displayed free variables in formulas. -/ +inductive FvName | x | y | z | X + +/-- Typeclass selecting the displayed variable named `n` inside a variable type. -/ +class HasVar (n : FvName) (α : Type*) where + /-- The selected displayed variable. -/ + fv : α + +/-- No displayed variables. -/ +inductive Vars0 : Type +/-- A singleton displayed-variable context. -/ +inductive Vars1 : FvName -> Type +| fv1 {n1} : Vars1 n1 +/-- A two-variable displayed context. -/ +inductive Vars2 : FvName -> FvName -> Type +| fv1 {n1 n2} : Vars2 n1 n2 +| fv2 {n1 n2} : Vars2 n1 n2 +/-- A three-variable displayed context. -/ +inductive Vars3 : FvName -> FvName -> FvName -> Type +| fv1 {n1 n2 n3} : Vars3 n1 n2 n3 +| fv2 {n1 n2 n3} : Vars3 n1 n2 n3 +| fv3 {n1 n2 n3} : Vars3 n1 n2 n3 +/-- A four-variable displayed context. -/ +inductive Vars4 : FvName -> FvName -> FvName -> FvName -> Type +| fv1 {n1 n2 n3 n4} : Vars4 n1 n2 n3 n4 +| fv2 {n1 n2 n3 n4} : Vars4 n1 n2 n3 n4 +| fv3 {n1 n2 n3 n4} : Vars4 n1 n2 n3 n4 +| fv4 {n1 n2 n3 n4} : Vars4 n1 n2 n3 n4 + +@[delta0_simps] instance (n1 : FvName) : HasVar n1 (Vars1 n1) where fv := .fv1 +@[delta0_simps] instance (n1 n2 : FvName) : HasVar n1 (Vars2 n1 n2) where fv := .fv1 +@[delta0_simps] instance (n1 n2 : FvName) : HasVar n2 (Vars2 n1 n2) where fv := .fv2 +@[delta0_simps] instance (n1 n2 n3 : FvName) : HasVar n1 (Vars3 n1 n2 n3) where + fv := .fv1 +@[delta0_simps] instance (n1 n2 n3 : FvName) : HasVar n2 (Vars3 n1 n2 n3) where + fv := .fv2 +@[delta0_simps] instance (n1 n2 n3 : FvName) : HasVar n3 (Vars3 n1 n2 n3) where + fv := .fv3 +@[delta0_simps] instance (n1 n2 n3 n4 : FvName) : HasVar n1 (Vars4 n1 n2 n3 n4) where + fv := .fv1 +@[delta0_simps] instance (n1 n2 n3 n4 : FvName) : HasVar n2 (Vars4 n1 n2 n3 n4) where + fv := .fv2 +@[delta0_simps] instance (n1 n2 n3 n4 : FvName) : HasVar n3 (Vars4 n1 n2 n3 n4) where + fv := .fv3 +@[delta0_simps] instance (n1 n2 n3 n4 : FvName) : HasVar n4 (Vars4 n1 n2 n3 n4) where + fv := .fv4 + + +@[delta0_simps] instance : IsEnum Empty where + size := 0 + toIdx := Empty.elim + fromIdx := Fin.elim0 + to_from_id id := Fin.elim0 id + from_to_id x := Empty.elim x +@[delta0_simps] lemma IsEnum.size.Empty : IsEnum.size Empty = 0 := rfl + +@[delta0_simps] instance {n1} : IsEnum (Vars1 n1) where + size := 1 + toIdx _ := 0 + fromIdx _ := .fv1 + to_from_id id := (Fin.fin_one_eq_zero id).symm + from_to_id _ := rfl +@[delta0_simps] lemma IsEnum.size.Vars1 {n1} : IsEnum.size (Vars1 n1) = 1 := rfl +@[delta0_simps] lemma IsEnum.toIdx.Vars1 {n1} {x : Vars1 n1} + : IsEnum.toIdx x = 0 + := rfl + +@[delta0_simps] instance {n1 n2} : IsEnum (Vars2 n1 n2) where + size := 2 + toIdx | .fv1 => 0 | .fv2 => 1 + fromIdx | 0 => .fv1 | 1 => .fv2 + to_from_id id := by + fin_cases id <;> rfl + from_to_id x := by + cases x <;> rfl +@[delta0_simps] lemma IsEnum.size.Vars2 {n1 n2} : IsEnum.size (Vars2 n1 n2) = 2 := rfl +@[delta0_simps] lemma IsEnum.toIdx.Vars2 {n1 n2} {x : Vars2 n1 n2} + : IsEnum.toIdx x = match x with | .fv1 => 0 | .fv2 => 1 + := rfl + +@[delta0_simps] instance {n1 n2 n3} : IsEnum (Vars3 n1 n2 n3) where + size := 3 + toIdx | .fv1 => 0 | .fv2 => 1 | .fv3 => 2 + fromIdx | 0 => .fv1 | 1 => .fv2 | 2 => .fv3 + to_from_id id := by + fin_cases id <;> rfl + from_to_id x := by + cases x <;> rfl +@[delta0_simps] lemma IsEnum.size.Vars3 {n1 n2 n3} : IsEnum.size (Vars3 n1 n2 n3) = 3 := rfl +@[delta0_simps] lemma IsEnum.toIdx.Vars3 {n1 n2 n3} {x : Vars3 n1 n2 n3} + : IsEnum.toIdx x = match x with | .fv1 => 0 | .fv2 => 1 | .fv3 => 2 + := rfl + +@[delta0_simps] instance {n1 n2 n3 n4} : IsEnum (Vars4 n1 n2 n3 n4) where + size := 4 + toIdx | .fv1 => 0 | .fv2 => 1 | .fv3 => 2 | .fv4 => 3 + fromIdx | 0 => .fv1 | 1 => .fv2 | 2 => .fv3 | 3 => .fv4 + to_from_id id := by + fin_cases id <;> rfl + from_to_id x := by + cases x <;> rfl +@[delta0_simps] lemma IsEnum.size.Vars4 {n1 n2 n3 n4} : IsEnum.size (Vars4 n1 n2 n3 n4) = 4 := rfl +@[delta0_simps] lemma IsEnum.toIdx.Vars4 {n1 n2 n3 n4} {x : Vars4 n1 n2 n3 n4} + : IsEnum.toIdx x = match x with | .fv1 => 0 | .fv2 => 1 | .fv3 => 2 | .fv4 => 3 + := rfl + +private lemma displayedVariablesDelimiter1 : True := by + trivial + +universe u +variable {α : Type u} {L : FirstOrder.Language} + + +/-- The selected variable named `x`. -/ +@[delta0_simps] def x.name [h : HasVar .x α] := h.fv +/-- The selected variable named `y`. -/ +@[delta0_simps] def y.name [h : HasVar .y α] := h.fv +/-- The selected variable named `z`. -/ +@[delta0_simps] def z.name [h : HasVar .z α] := h.fv +/-- The selected variable named `X`. -/ +@[delta0_simps] def X.name [h : HasVar .X α] := h.fv +/-- The first-order term for the displayed variable named `x`. -/ +@[delta0_simps] def x {k} [h : HasVar .x α] : L.Term (α ⊕ Fin k) := L.var <| Sum.inl h.fv +/-- The first-order term for the displayed variable named `y`. -/ +@[delta0_simps] def y {k} [h : HasVar .y α] : L.Term (α ⊕ Fin k) := L.var <| Sum.inl h.fv +/-- The first-order term for the displayed variable named `z`. -/ +@[delta0_simps] def z {k} [h : HasVar .z α] : L.Term (α ⊕ Fin k) := L.var <| Sum.inl h.fv +/-- The first-order term for the displayed variable named `X`. -/ +@[delta0_simps] def X {k} [h : HasVar .X α] : L.Term (α ⊕ Fin k) := L.var <| Sum.inl h.fv + +/-- Display a one-variable formula as a formula over an explicit sum context. -/ +def FirstOrder.Language.Formula.display1 + {n1 : FvName} + (phi : L.Formula (Vars1 n1)) + : L.Formula ((Vars1 n1) ⊕ Empty) +:= + phi.relabelEquiv { + toFun := (fun fv => match fv with + | .fv1 => Sum.inl .fv1 + ) + invFun := (fun fv => match fv with | .inl _ => .fv1) + right_inv := by + intro v + cases v with + | inl _ => simp only + | inr v => exact Empty.elim v + } + +/-- Display a two-variable formula by isolating the named left variable. -/ +def FirstOrder.Language.Formula.display2 + (name : FvName) + {other : FvName} + (phi : L.Formula (Vars2 name other)) + : L.Formula (Vars1 name ⊕ Vars1 other) +:= + phi.relabelEquiv { + toFun := (fun fv => match fv with + | .fv1 => Sum.inl .fv1 + | .fv2 => Sum.inr .fv1 + ), + invFun := (fun fv => match fv with | .inl _ => .fv1 | .inr _ => .fv2) + left_inv := by intro v; cases v <;> simp only + right_inv := by + simp only [Function.RightInverse, Function.LeftInverse, Sum.forall, implies_true, and_self] + } + +/-- Display a three-variable formula by isolating the named left variable. -/ +def FirstOrder.Language.Formula.display3 + (name : FvName) + {other1 other2 : FvName} + (phi : L.Formula (Vars3 name other1 other2)) + : L.Formula (Vars1 name ⊕ Vars2 other1 other2) +:= + phi.relabelEquiv { + toFun := (fun fv => match fv with + | .fv1 => Sum.inl .fv1 + | .fv2 => Sum.inr .fv1 + | .fv3 => Sum.inr .fv2) + invFun := (fun fv => match fv with + | .inl _ => .fv1 + | .inr .fv1 => .fv2 + | .inr .fv2 => .fv3) + left_inv := by intro v; cases v <;> simp only + right_inv := by + simp only [Function.RightInverse, Function.LeftInverse, Sum.forall, implies_true, true_and] + intro v; cases v <;> simp only + } + +/-- Display a four-variable formula by isolating the named left variable. -/ +def FirstOrder.Language.Formula.display4 + (name : FvName) + {o1 o2 o3 : FvName} + (phi : L.Formula (Vars4 name o1 o2 o3)) + : L.Formula (Vars1 name ⊕ Vars3 o1 o2 o3) +:= + phi.relabelEquiv { + toFun := (fun fv => match fv with + | .fv1 => Sum.inl .fv1 + | .fv2 => Sum.inr .fv1 + | .fv3 => Sum.inr .fv2 + | .fv4 => Sum.inr .fv3) + invFun := (fun fv => match fv with + | .inl _ => .fv1 + | .inr .fv1 => .fv2 + | .inr .fv2 => .fv3 + | .inr .fv3 => .fv4) + left_inv := by intro v; cases v <;> simp only + right_inv := by + simp only [Function.RightInverse, Function.LeftInverse, Sum.forall, implies_true, true_and] + intro v; cases v <;> simp only + } + +/-- Reassociate displayed variables from `x | (y,z)` to `(x,y) | z`. -/ +def FirstOrder.Language.Formula.display_swapleft + {n1 n2 n3 : FvName} + (phi : L.Formula (Vars1 n1 ⊕ Vars2 n2 n3)) + : L.Formula (Vars2 n1 n2 ⊕ Vars1 n3) +:= + phi.relabelEquiv { + toFun := (fun fv => match fv with + | .inl .fv1 => .inl .fv1 + | .inr .fv1 => .inl .fv2 + | .inr .fv2 => .inr .fv1) + invFun := (fun fv => match fv with + | .inl .fv1 => .inl .fv1 + | .inl .fv2 => .inr .fv1 + | .inr .fv1 => .inr .fv2) + left_inv := by + intro v; + cases v with + | inl vl => simp only + | inr vr => + cases vr <;> simp only + right_inv := by + intro v + cases v with + | inl vl => + cases vl <;> simp only + | inr vr => simp only + } + +/-- Reassociate displayed variables from `x | (y,z)` to `(x | y) | z`. -/ +def FirstOrder.Language.Formula.display_swapleft' + {n1 n2 n3 : FvName} + (phi : L.Formula (Vars1 n1 ⊕ Vars2 n2 n3)) + : L.Formula ((Vars1 n1 ⊕ Vars1 n2) ⊕ Vars1 n3) +:= + phi.relabelEquiv { + toFun := (fun fv => match fv with + | .inl .fv1 => .inl (.inl .fv1) + | .inr .fv1 => .inl (.inr .fv1) + | .inr .fv2 => .inr .fv1) + invFun := (fun fv => match fv with + | .inl (.inl .fv1) => .inl .fv1 + | .inl (.inr .fv1) => .inr .fv1 + | .inr .fv1 => .inr .fv2) + left_inv := by + intro v; + cases v with + | inl vl => simp only + | inr vr => + cases vr <;> simp only + right_inv := by + intro v + cases v with + | inl vl => + cases vl <;> simp only + | inr vr => simp only + } + +private lemma displayedVariablesDelimiter2 : True := by + trivial + +-- Vars2 .x .y -> Vars2 .y .x +/-- Swap the two variables in a two-variable displayed formula. -/ +def FirstOrder.Language.Formula.rotate_21 + {n1 n2 : FvName} + (phi : L.Formula (Vars2 n1 n2)) + : L.Formula (Vars2 n2 n1) +:= + phi.relabelEquiv { + toFun := (fun fv => match fv with + | .fv1 => .fv2 + | .fv2 => .fv1) + invFun := (fun fv => match fv with + | .fv1 => .fv2 + | .fv2 => .fv1) + left_inv := by intro v; cases v <;> simp only + right_inv := by + simp only [Function.RightInverse, Function.LeftInverse] + intro v; cases v <;> simp only + } + +-- Vars3 .x .y .z -> Vars3 .y .x. .z +/-- Swap the first two variables in a three-variable displayed formula. -/ +def FirstOrder.Language.Formula.rotate_213 + (n1 n2 n3 : FvName) + (phi : L.Formula (Vars3 n1 n2 n3)) + : L.Formula (Vars3 n2 n1 n3) +:= + phi.relabelEquiv { + toFun := (fun fv => match fv with + | .fv1 => .fv2 + | .fv2 => .fv1 + | .fv3 => .fv3) + invFun := (fun fv => match fv with + | .fv1 => .fv2 + | .fv2 => .fv1 + | .fv3 => .fv3) + left_inv := by intro v; cases v <;> simp only + right_inv := by + simp only [Function.RightInverse, Function.LeftInverse] + intro v; cases v <;> simp only + } + +-- Vars3 .x .y .z -> Vars3 .y .x. .z +/-- Rotate the variables in a three-variable displayed formula. -/ +def FirstOrder.Language.Formula.rotate_231 + (n1 n2 n3 : FvName) + (phi : L.Formula (Vars3 n1 n2 n3)) + : L.Formula (Vars3 n3 n1 n2) +:= + phi.relabelEquiv { + toFun := (fun fv => match fv with + | .fv1 => .fv2 + | .fv2 => .fv3 + | .fv3 => .fv1) + invFun := (fun fv => match fv with + | .fv1 => .fv3 + | .fv2 => .fv1 + | .fv3 => .fv2) + left_inv := by intro v; cases v <;> simp only + right_inv := by + simp only [Function.RightInverse, Function.LeftInverse] + intro v; cases v <;> simp only + } + +private lemma displayedVariablesDelimiter3 : True := by + trivial + +variable {β} + +/-- Flip the two sides of the free-variable sum in a bounded formula. -/ +def FirstOrder.Language.BoundedFormula.flip {n} + (phi : L.BoundedFormula (α ⊕ β) n) : L.BoundedFormula (β ⊕ α) n := + phi.relabelEquiv { + toFun := Sum.swap (α := α) (β := β) + invFun := Sum.swap + left_inv := Sum.swap_leftInverse + right_inv := Sum.swap_rightInverse + } + +/-- Flip the two sides of the free-variable sum in a formula. -/ +def FirstOrder.Language.Formula.flip (phi : L.Formula (α ⊕ β)) : L.Formula (β ⊕ α) := + phi.relabelEquiv { + toFun := Sum.swap (α := α) (β := β) + invFun := Sum.swap + left_inv := Sum.swap_leftInverse + right_inv := Sum.swap_rightInverse + } + +-- theorem FirstOrder.Language.Formula.realize_flip (phi : L.Formula (α ⊕ β)) {v} +-- : phi.flip.Realize v <-> phi.Realize (v ∘ ) + +/-- Embed a formula into a sum context by putting all variables on the left. -/ +def FirstOrder.Language.Formula.mkInl (phi : L.Formula α) : L.Formula (α ⊕ Empty) := + phi.relabelEquiv { + toFun := Sum.inl + invFun := Sum.elim id Empty.elim + left_inv := by + intro x + simp only [Sum.elim_inl, id_eq] + right_inv := by + intro x + cases x with + | inl x => simp only [Sum.elim_inl, id_eq] + | inr x => apply Empty.elim x + } diff --git a/LeanPool/FormalizationOfBoundedArithmetic/IDelta0.lean b/LeanPool/FormalizationOfBoundedArithmetic/IDelta0.lean new file mode 100644 index 0000000000..ced3601cd9 --- /dev/null +++ b/LeanPool/FormalizationOfBoundedArithmetic/IDelta0.lean @@ -0,0 +1,575 @@ +/- +Copyright (c) 2026 ruplet. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: ruplet +-/ + +-- import Mathlib.Algebra.Ring.Defs + +import LeanPool.FormalizationOfBoundedArithmetic.DisplayedVariables +import LeanPool.FormalizationOfBoundedArithmetic.Complexity +import LeanPool.FormalizationOfBoundedArithmetic.IsEnum +import LeanPool.FormalizationOfBoundedArithmetic.IOPEN + +open FirstOrder Language BoundedFormula + +/-- Models of open induction extended with induction for delta-zero formulas. -/ +class IDelta0Model (num : Type*) extends IOPENModel num where + delta0_induction {n1} {a} [IsEnum a] + (phi : peano.BoundedFormula ((Vars1 n1) ⊕ a) 0) : + phi.IsDelta0 -> (mkInductionSentence phi).Realize num + +namespace IDelta0Model + +universe u +variable {M : Type*} [idelta0 : IDelta0Model M] + +-- Example 3.9 Theorems of IΔ0 +open Formula BoundedFormula + +open BASICModel IOPENModel + +-- D1. x ≠ 0 → ∃ y ≤ x, x = y + 1 (Predecessor) +-- proof: induction on x +theorem pred_exists : + ∀ {x : M}, x ≠ 0 → ∃ y ≤ x, x = y + 1 := +by + let ind1 : peano.Formula (Vars2 .y .x) := x =' (y + 1) + let ind2 : peano.Formula (Vars1 .x) := + (Formula.iBdEx' x (display2 .y ind1).flip) + let ind := idelta0.delta0_induction <| display1 <| (x ≠' 0) ⟹ ind2 + unfold ind2 ind1 at ind + specialize ind (by + rw [IsDelta0.display1] + -- TODO: this lemma can't be in @[delta0_simps], + -- as it creates a goal 'φ.IsOpen' - which might be not true! + rw [IsDelta0.of_open.imp] + · constructor + · unfold Term.neq + rw [IsDelta0.of_open.not] + constructor; constructor; constructor + constructor; constructor + · constructor + rw [IsDelta0.flip] + rw [IsDelta0.display2] + constructor; constructor; constructor + · unfold Term.neq + rw [IsOpen.not] + constructor; constructor + ) + simp_induction at ind + apply ind ?base ?step <;> clear ind ind1 ind2 + · simp only [IsEmpty.forall_iff] + · intro a hind h + exists a + constructor + · exact B8 + · rfl + +theorem ex_of_bdEx {a} [LE a] {t} {P : a -> Prop} : (∃ x ≤ t, P x) -> ∃ x, P x := by + intro h + obtain ⟨x, ⟨hx1, hx2⟩⟩ := h + exists x + +lemma zero_add : + ∀ x : M, 0 + x = x := +by + intro x + rw [idelta0.add_comm] + exact B3 x + +instance : AddZeroClass M where + zero_add := zero_add + add_zero := B3 + +open IOPENModel BASICModel + +-- D2. ∃ z, (x + z = y ∨ y + z = x) +-- original proof: Induction on x. Base case: B2, O2. Induction step: B3, B4, D1 +-- our proof is different +theorem add_diff_exists : + ∀ x y : M, ∃ z, x + z = y ∨ y + z = x := +by + let ind1 : peano.Formula (Vars3 .z .x .y) := + ((x + z) =' y) ⊔ ((y + z) =' x) + let ind2 : peano.Formula (Vars2 .x .y) := iBdEx' (x + y) (display3 .z ind1).flip + let ind3 : peano.Formula (Vars1 .x ⊕ Vars1 .y) := display2 .x ind2 + let ind := idelta0.delta0_induction ind3 + unfold ind3 ind2 ind1 at ind + specialize ind (by + rw [IsDelta0.display2] + constructor + rw [IsDelta0.flip] + rw [IsDelta0.display3] + constructor + · constructor + · constructor; constructor; constructor + · constructor; constructor + · constructor; constructor; constructor + ) + simp_induction at ind + intro x y + apply ex_of_bdEx + apply ind ?base ?step <;> clear ind1 ind2 ind3 ind + · intro z + exists z + constructor + · calc + z ≤ z := le_refl z + _ = 0 + z := (zero_add z).symm + · rw [idelta0.add_comm] + left + rw [B3] + · intro L hind R + by_cases h_R_zero : R = 0 + · exists (L + 1) + constructor + · exact B8 + · right + rw [h_R_zero] + rw [idelta0.zero_add] + rfl + · obtain ⟨pred_R, h_pred_R_le, h_pred_R_eq⟩ := pred_exists h_R_zero + specialize hind pred_R + obtain ⟨symdiff_pred, h_symdiff_pred_le, h_symdiff_pred_eq⟩ := hind + exists symdiff_pred + cases h_symdiff_pred_eq with + | inl h_LR => + constructor + · rw [h_pred_R_eq, <- h_LR] + conv => + rhs; + rw [idelta0.add_comm] + rw [idelta0.add_assoc] + lhs + rw [idelta0.add_comm] + rw [idelta0.add_assoc] + apply B8 + · left + rw [h_pred_R_eq] + rw [idelta0.add_assoc] + conv => lhs; rhs; rw [idelta0.add_comm] + rw [<- idelta0.add_assoc] + congr + | inr h_RL => + constructor + · rw [<- h_RL] + conv => rhs; left; left; rw [idelta0.add_comm] + conv => + rhs + left + rw [idelta0.add_comm] + rw [<- idelta0.add_assoc] + left + rw [idelta0.add_comm] + conv => rhs; rw [idelta0.add_assoc]; rw [idelta0.add_assoc] + apply B8 + · right + rw [<- h_RL] + rw [h_pred_R_eq] + conv => lhs; rw [idelta0.add_assoc]; rhs; rw [idelta0.add_comm] + rw [idelta0.add_assoc] + rfl + +-- D3. x ≤ y ↔ ∃ z, x + z = y +theorem le_iff_exists_add : + ∀ x y : M, x ≤ y ↔ ∃ z, x + z = y := +by + intro x y + constructor + · intro h_xy + obtain ⟨diff, hdiff⟩ := add_diff_exists x y + cases hdiff with + | inl heq => exists diff + | inr heq => + exists 0 + calc + x + 0 = x := B3 x + _ = y := by + apply B7 + · exact h_xy + · exact heq ▸ B8 + · intro h + obtain ⟨z, hz⟩ := h + rw [<- hz] + apply B8 + +-- D4. (x ≤ y ∧ y ≤ z) → x ≤ z (Transitivity) +theorem le_trans : + ∀ {x y z : M}, x ≤ y -> y ≤ z -> x ≤ z := +by + intro x y z hxy hyz + rw [le_iff_exists_add] at hxy hyz ⊢ + obtain ⟨diff_x_y, hdiff_x_y⟩ := hxy + obtain ⟨diff_y_z, hdiff_y_z⟩ := hyz + exists (diff_x_y + diff_y_z) + rw [<- idelta0.add_assoc] + rw [hdiff_x_y] + rw [hdiff_y_z] + + +instance : Preorder M where + le_refl := by apply @BASICModel.le_refl + le_trans := by apply le_trans + lt_iff_le_not_ge := by + intro a b + constructor + · intro h + constructor + · exact h.1 + · intro contr + apply h.2 + exact contr + · intro h + exact h + + +-- D5. x ≤ y ∨ y ≤ x (Total order) +theorem le_total : + ∀ x y : M, x ≤ y ∨ y ≤ x := +by + intro x y + obtain ⟨diff, hdiff⟩ := add_diff_exists x y + cases hdiff with + | inl h => + left + rw [le_iff_exists_add] + exists diff + | inr h => + right + rw [le_iff_exists_add] + exists diff + +theorem add_rotate + : ∀ {a b c : M}, a + b + c = b + c + a := +by + intro a b c + rw [idelta0.add_assoc] + rw [idelta0.add_comm] + +-- D6. x ≤ y ↔ x + z ≤ y + z +theorem add_le_add_right : + ∀ {x y z : M}, x ≤ y ↔ x + z ≤ y + z := +by + intro x y z + constructor + · intro hxy + rw [le_iff_exists_add] at hxy ⊢ + obtain ⟨diff, hdiff⟩ := hxy + exists diff + rw [<- add_rotate] + rw [idelta0.add_comm] at ⊢ hdiff + rw [hdiff] + rw [idelta0.add_comm] + · rw [le_iff_exists_add] + rw [le_iff_exists_add] + intro h + obtain ⟨a, ha⟩ := h + exists a + apply add_cancel_right.mp + conv at ha => rw [idelta0.add_assoc]; lhs; rhs; rw [idelta0.add_comm] + rw [idelta0.add_assoc] + exact ha + +theorem le_cancel_left : + ∀ {x y z : M}, x <= y -> z + x <= z + y := +by + conv => + rhs + rhs + rhs + rhs + rw [idelta0.add_comm] + rhs + rw [idelta0.add_comm] + intro x y z h + apply add_le_add_right.mp h + +-- D7. x ≤ y → x * z ≤ y * z +theorem le_mul_right : + ∀ {x y z : M}, x ≤ y → x * z ≤ y * z := +by + intro x y z hxy + rw [le_iff_exists_add] at hxy ⊢ + obtain ⟨diff, hdiff⟩ := hxy + rw [<- hdiff] + rw [idelta0.add_mul] + exists (diff * z) + +-- D8. x ≤ y + 1 ↔ (x ≤ y ∨ x = y + 1) (Discreteness 1) +theorem le_succ_iff : + ∀ {x y : M}, x ≤ y + 1 ↔ (x ≤ y ∨ x = y + 1) := +by + intro x y + constructor + · intro hxy + rw [le_iff_exists_add] at hxy + obtain ⟨diff, hdiff⟩ := hxy + by_cases h : diff = 0 + · rw [h] at hdiff + right + exact (B3 x).symm.trans hdiff + · obtain ⟨pred_diff, hpred_diff_le, hpred_diff_eq⟩ + := pred_exists h + left + rw [hpred_diff_eq] at hdiff + rw [<- idelta0.add_assoc] at hdiff + rw [le_iff_exists_add] + exists pred_diff + apply B2 + exact hdiff + · intro h + cases h with + | inl h => + rw [le_iff_exists_add] at h ⊢ + rcases h with ⟨diff, hdiff⟩ + refine ⟨diff + 1, ?_⟩ + rw [<- idelta0.add_assoc] + rw [hdiff] + | inr h => + rw [h] + +-- D4 used +instance : PartialOrder M where + le_refl := idelta0.le_refl + le_trans := @idelta0.le_trans + le_antisymm := by apply B7 + +instance : CanonicallyOrderedAdd M where + exists_add_of_le := by + intro a b hab + have diff := idelta0.add_diff_exists a b + obtain ⟨diff, hdiff⟩ := diff + cases hdiff with + | inl h => rw [<- h]; exists diff + | inr h => + exists 0 + calc + b = a := by + apply B7 + · exact h ▸ B8 + · exact hab + _ = a + 0 := (B3 a).symm + le_self_add := by apply B8 + le_add_self := by + intro a b + rw [idelta0.add_comm] + apply B8 + +noncomputable instance : LinearOrder M where + le_refl := idelta0.le_refl + le_trans := by apply le_trans + le_antisymm := by apply B7 + le_total := idelta0.le_total + min_def := by simp only [implies_true] + max_def := by exact fun a b ↦ rfl + compare_eq_compareOfLessAndEq := by + simp only [implies_true] + + toDecidableLE := by + unfold DecidableLE DecidableRel + intro a b + if ha : a = 0 then + apply Decidable.isTrue + rw [ha] + apply IOPENModel.zero_le b + else + if hb : b = 0 then + apply Decidable.isFalse + rw [hb] + intro ha' + apply ha + exact (@nonpos_iff_eq_zero M).mp ha' + else + -- HERE, WE SHOULD TAKE PREDECESSOR OF + -- BOTH AND RECURSE! + exact Classical.propDecidable (a ≤ b) + +theorem le_of_eq : + ∀ {x y : M}, x = y -> x ≤ y := +by + intro x y hxy + rw [hxy] + +-- theorem lt_of_not_ge : +-- ∀ {x y : M}, ¬ x <= y -> y < x := +-- by +-- intro x y h +-- constructor +-- · cases le_total x y with +-- | inl x_le => +-- contradiction +-- | inr y_le => +-- exact y_le +-- · intro h_eq +-- apply h +-- apply le_of_eq +-- apply Eq.symm +-- exact h_eq + +theorem zero_if_sum_zero : + ∀ {x y : M}, x + y = 0 -> x = 0 ∧ y = 0 := +by + intro x y h + constructor + · apply le_zero_eq + have t := @B8 _ _ x y + rw [h] at t + exact t + · apply le_zero_eq + have t := @B8 _ _ y x + rw [idelta0.add_comm] at t + rw [h] at t + exact t + +theorem lt_one_eq_zero : + ∀ {x : M}, x < 1 -> x = 0 := +by + intro x hx + rcases hx with ⟨h_x_le, h_x_neq⟩ + rw [le_iff_exists_add] at h_x_le + rcases h_x_le with ⟨diff, hdiff⟩ + by_cases h : x = 0 + · trivial + · obtain ⟨pred, hp1, hp2⟩ := pred_exists h + rw [hp2] at hdiff + rw [idelta0.add_assoc] at hdiff + conv at hdiff => lhs; rhs; rw [idelta0.add_comm] + rw [<- idelta0.add_assoc] at hdiff + conv at hdiff => rhs; rw [<- idelta0.zero_add 1] + have hdiff := B2 _ _ hdiff + have pred_zero := (zero_if_sum_zero hdiff).left + rw [pred_zero, idelta0.zero_add] at hp2 + exfalso + apply h_x_neq + rw [hp2] + +-- D9. x < y ↔ x + 1 ≤ y (Discreteness 2) +-- recall: x < y means x ≤ y ∧ x ≠ y +theorem lt_iff_succ_le : + ∀ {x y : M}, (x < y) ↔ x + 1 ≤ y := +by + intro x y + constructor + · intro h + rcases h with ⟨h1, h2⟩ + rw [le_iff_exists_add] at h1 + obtain ⟨diff, hdiff⟩ := h1 + rw [<- hdiff] + apply le_cancel_left + by_contra not_one_le_diff + apply h2 + rw [<- hdiff] + conv => lhs; rw [<- B3 x] + have diff_lt_one := lt_of_not_ge not_one_le_diff + rw [lt_one_eq_zero diff_lt_one] + rw [@B3] + exact (B3 x).symm ▸ BASICModel.le_refl x + · intro h + rw [le_iff_exists_add] at h + rcases h with ⟨diff, hdiff⟩ + constructor + · rw [le_iff_exists_add] + exists (1 + diff) + rw [<- idelta0.add_assoc] + exact hdiff + · intro absurd + rw [<- hdiff] at absurd + have aux : x + 1 + diff = x := by + have aux : x ≤ x + 1 + diff := by + refine le_add_of_le_left ?_ + exact le_self_add + apply le_antisymm <;> assumption + conv at aux => lhs; rw [idelta0.add_assoc] + conv at aux => rhs; rw [<- B3 x] + rw [add_cancel_left] at aux + rw [idelta0.add_comm] at aux + exact (B1 (x := diff)) aux + +theorem mul_eq_zero_iff_left : + ∀ {x y : M}, x ≠ 0 -> (x * y = 0 ↔ y = 0) := +by + intro x y hx + constructor + · intro hxy + rcases pred_exists hx with ⟨xp, _, hxp_eq⟩ + rw [hxp_eq] at hxy + rw [idelta0.add_mul] at hxy + by_contra hy + rcases pred_exists hy with ⟨yp, _, hyp_eq⟩ + rw [hyp_eq] at hxy + conv at hxy => lhs; rhs; rw [idelta0.mul_add] + rw [idelta0.mul_one] at hxy + rw [<- idelta0.add_assoc] at hxy + apply B1 (num := M) + exact hxy + · intro hy + rw [hy] + apply B5 + +-- D10. x * z = y * z ∧ z ≠ 0 → x = y (Cancellation law for ·) +theorem mul_cancel_right : + ∀ x y z : M, (x * z = y * z ∧ z ≠ 0) → x = y := +by + let ind1 : peano.Formula (Vars3 .x .y .z) + := ((x * z) =' (y * z) ⊓ (z ≠' 0)) ⟹ (x =' y) + let ind := idelta0.delta0_induction <| display3 .x ind1 + specialize ind (by + rw [IsDelta0.display3] + unfold ind1 + constructor + · apply IsDelta0.of_isQF + apply IsQF.inf + · constructor; constructor + · apply IsQF.not; constructor; constructor + · constructor; constructor; constructor + ) + unfold ind1 at ind + simp_induction at ind + apply ind ?base ?step <;> clear ind ind1 + · intro y z hyz_z + obtain ⟨hyz, hz⟩ := hyz_z + by_cases hy : y = 0 + · exact hy.symm + · rcases pred_exists hy with ⟨yp, _, hyp_eq⟩ + rcases pred_exists hz with ⟨zp, _, hzp_eq⟩ + rw [hyp_eq, hzp_eq] at hyz + exfalso + have hyz_zero : 0 = (yp + 1) * (zp + 1) := by + exact (zero_mul (zp + 1)).symm.trans hyz + have rhs_succ : + (yp + 1) * (zp + 1) = ((yp + 1) * zp + yp) + 1 := by + calc + (yp + 1) * (zp + 1) = (yp + 1) * zp + (yp + 1) := B6 + _ = ((yp + 1) * zp + yp) + 1 := B4 + exact (B1 (x := (yp + 1) * zp + yp)) (rhs_succ.symm.trans hyz_zero.symm) + · intro y hind x z hass_hz + obtain ⟨hass, hz⟩ := hass_hz + -- hind tells us that we can right-cancel + -- multiplication by `a_1` if the other factor at RHS is `a` + + -- right-cancel multiplication by `z` in `hass` + have hx : x ≠ 0 := by + by_contra hx + rw [hx] at hass + rw [idelta0.zero_mul] at hass + rw [mul_eq_zero_iff_left] at hass + · apply hz + exact hass + · apply @B1 M + rcases pred_exists hx with ⟨xp, _, hxp_eq⟩ + rw [hxp_eq] at hass + rw [idelta0.add_mul] at hass + rw [idelta0.add_mul] at hass + have hass_cancel : y * z = xp * z := by + apply add_cancel_right.mp + calc + y * z + z = y * z + 1 * z := by rw [one_mul z] + _ = xp * z + 1 * z := hass + _ = xp * z + z := by rw [one_mul z] + rw [hxp_eq] + rw [hind xp z ⟨hass_cancel, hz⟩] + rfl + + +end IDelta0Model diff --git a/LeanPool/FormalizationOfBoundedArithmetic/IOPEN.lean b/LeanPool/FormalizationOfBoundedArithmetic/IOPEN.lean new file mode 100644 index 0000000000..3153553508 --- /dev/null +++ b/LeanPool/FormalizationOfBoundedArithmetic/IOPEN.lean @@ -0,0 +1,365 @@ +/- +Copyright (c) 2026 ruplet. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: ruplet +-/ + +-- for a quick demo, jump straight to `theorem add_assoc` +import Mathlib.Tactic.Core +import Mathlib.Logic.Basic +import Mathlib.Tactic + +import Mathlib.ModelTheory.Basic +import Mathlib.ModelTheory.Syntax +import Mathlib.ModelTheory.Complexity +import Mathlib.ModelTheory.Semantics + +import LeanPool.FormalizationOfBoundedArithmetic.IsEnum +import LeanPool.FormalizationOfBoundedArithmetic.AxiomSchemes +import LeanPool.FormalizationOfBoundedArithmetic.Syntax +import LeanPool.FormalizationOfBoundedArithmetic.Semantics +import LeanPool.FormalizationOfBoundedArithmetic.Complexity +import LeanPool.FormalizationOfBoundedArithmetic.Order +import LeanPool.FormalizationOfBoundedArithmetic.BasicSingleSorted +import LeanPool.FormalizationOfBoundedArithmetic.SimpRules + +open FirstOrder Language BoundedFormula + +/-- Models of BASIC arithmetic satisfying open induction. -/ +class IOPENModel (num : Type*) extends BASICModel num where + open_induction {n} {a : Type} [IsEnum a] + (phi : peano.BoundedFormula ((Vars1 n) ⊕ a) 0) : + phi.IsOpen -> (mkInductionSentence phi).Realize num + +namespace IOPENModel + +universe u v +variable {M : Type u} [iopen : IOPENModel M] + + +-- page 36 of draft (47 of pdf) +-- Example 3.8 The following formulas (and their universal closures) are theorems of IOPEN: +open BASICModel Formula Term + +open Lean Elab Tactic + +theorem forall_swap_231 {α β γ} {p : α -> β -> γ -> Prop} + : (∀ x y z, p x y z) <-> (∀ z x y, p x y z) := + ⟨fun f z x y => f x y z, fun f y z x => f x y z⟩ + +-- O1. (x + y) + z = x + (y + z) (Associativity of +) +-- proof: induction on z +theorem add_assoc + : ∀ x y z : M, (x + y) + z = x + (y + z) := +by + -- TODO: how to make Lean infer these formulas? + let phi : peano.Formula (Vars3 .z .x .y) := + ((x + y) + z) =' (x + (y + z)) + have ind := iopen.open_induction <| display3 .z phi + unfold phi at ind + simp_complexity at ind + simp_induction at ind + rw [forall_swap_231] + apply ind ?base ?step + · intro x y + rw [B3 (x + y)] + rw [B3 y] + · intro z hInd x y + rw [B4] + rw [B4] + rw [B4] + rw [<- (B2 (x + y + z) (x + (y + z)))] + rw [hInd] + +-- lemma for O2; "induction on y, first establishing the special cases y = 0 and y = 1..." +-- proof: induction on x +lemma add_zero_comm + : ∀ x : M, x + 0 = 0 + x := +by + have ind := iopen.open_induction <| display1 + (((x + 0) =' (0 + x)) : Formula _ (Vars1 .x)) + simp_complexity at ind + simp_induction at ind + apply ind ?base ?step + · trivial + · intro a ha + rw [← add_assoc] + rw [← ha] + rw [B3] + rw [B3] + +-- this is necessary to prove axiom `C` from BasicExt +lemma zero_add + : ∀ x : M, 0 + x = x := +by + intro a + rw [<- add_zero_comm] + exact B3 a + +-- lemma for O2; "induction on y, first establishing the special cases y = 0 and y = 1..." +theorem add_one_comm + : ∀ x : M, x + 1 = 1 + x := +by + have ind := iopen.open_induction <| display1 + (((x + 1) =' (1 + x)) : Formula _ (Vars1 .x)) + simp_complexity at ind + simp_induction at ind + apply ind ?base ?step + · calc + (0 : M) + 1 = 1 := zero_add 1 + _ = 1 + 0 := (B3 1).symm + · intro a ha + rw [<- add_assoc] + rw [ha] + +-- O2. x + y = y + x (Commutativity of +) +-- proof : induction on y, first establishing the special cases y = 0 and y = 1 +theorem add_comm + : ∀ x y : M, x + y = y + x := +by + have ind := iopen.open_induction <| display2 .y + (((x + y) =' (y + x)) : Formula _ (Vars2 .y .x)) + simp_complexity at ind + simp_induction at ind + rw [forall_comm] + apply ind ?base ?step + · intro x + exact add_zero_comm x + · intro a hInd b + rw [<- add_assoc] + rw [hInd] + rw [add_assoc] + calc + a + (b + 1) = a + (1 + b) := by rw [add_one_comm b] + _ = a + 1 + b := by rw [<- add_assoc] + +-- O3. x · (y + z) = (x · y) + (x · z) (Distributive law) + -- proof: induction on z +theorem mul_add + : ∀ x y z : M, x * (y + z) = (x * y) + (x * z) := +by + have ind := iopen.open_induction <| display3 .z + ((x * (y + z)) =' ((x * y) + (x * z)) : Formula _ (Vars3 .z .x .y)) + simp_complexity at ind + simp_induction at ind + rw [forall_swap_231] + apply ind ?base ?step + · intro a b + rw [B3] + rw [B5] + rw [B3] + · intro b hInd_b a2 a3 + rw [add_comm] + rw [add_assoc] + rw [add_comm] + rw [hInd_b] + conv => lhs; left; rw [add_comm]; rw [B6] + rw [B6] + conv => rhs; right; rw [add_comm] + rw [add_assoc] + +theorem mul_one + : ∀ x : M, x * 1 = x := +by + intro x + calc + x * 1 = x * ((0 : M) + 1) := by rw [zero_add 1] + _ = x * 0 + x := B6 + _ = 0 + x := congrArg (fun y => y + x) B5 + _ = x := zero_add x + +-- O4. (x · y) · z = x · (y · z) (Associativity of ·) + -- proof: induction on z, using O3 +theorem mul_assoc + : ∀ x y z : M, (x * y) * z = x * (y * z) := + by + have ind := iopen.open_induction <| display3 .z + ((((x * y) * z) =' (x * (y * z))) : Formula _ (Vars3 .z .x .y)) + simp_complexity at ind + simp_induction at ind + rw [forall_swap_231] + apply ind ?base ?step + · intro x y + rw [B5] + rw [B5] + rw [B5] + · intro x hInd_x y z + rw [mul_add] + rw [mul_add] + calc + y * z * x + y * z * 1 = y * (z * x) + y * z := by + rw [hInd_x] + rw [mul_one] + _ = y * (z * x) + y * (z * 1) := by rw [mul_one] + _ = y * (z * x + z * 1) := (mul_add y (z * x) (z * 1)).symm + +lemma zero_mul + : ∀ x : M, 0 * x = 0 := +by + have ind := iopen.open_induction <| display1 + (((0 * x) =' 0) : Formula _ (Vars1 .x)) + simp_complexity at ind + simp_induction at ind + apply ind ?base ?step + · rw [B5] + · intro x hInd_0_x + rw [B6] + rw [hInd_0_x] + rw [B3] + +lemma one_mul + : ∀ x : M, 1 * x = x := +by + have ind := iopen.open_induction <| display1 + (((1 * x) =' x) : Formula _ (Vars1 .x)) + simp_complexity at ind + simp_induction at ind + apply ind ?base ?step + · rw [B5] + · intro x hInd_1_x + rw [B6] + rw [hInd_1_x] + +lemma mul_add_1_left + : ∀ x y : M, (x + 1) * y = x * y + y := +by + have ind := iopen.open_induction <| display2 .y + (((x + 1) * y) =' ((x * y) + y) : Formula _ (Vars2 .y .x)) + simp_complexity at ind + simp_induction at ind + rw [forall_comm] + apply ind ?base ?step + · intro x + rw [B5] + rw [B5] + rw [B3] + · intro y hInd_y x + rw [B6] + rw [B6] + rw [hInd_y] + conv => lhs; rw [add_assoc]; right; rw [<- add_assoc]; left; rw [add_comm] + conv => rhs; rw [add_assoc]; right; rw [<- add_assoc] + +-- O5. x · y = y · x (Commutativity of ·) +theorem mul_comm + : ∀ x y : M, x * y = y * x := +by + have ind := iopen.open_induction <| display2 .y + (((x * y) =' (y * x)) : Formula _ (Vars2 .y .x)) + simp_complexity at ind + simp_induction at ind + rw [forall_comm] + apply ind ?base ?step + · intro x + exact (B5 (x := x)).trans (zero_mul x).symm + · intro x hInd_x y + rw [B6] + calc + y * x + y = x * y + y := by rw [hInd_x] + _ = (x + 1) * y := (mul_add_1_left x y).symm + +example : Nonempty (True ∧ True) := + ⟨⟨⟨⟩, ⟨⟩⟩⟩ + +-- O6. x + z = y + z → x = y (Cancellation law for +) +namespace add_cancel_right + +theorem mp + : ∀ {x y z : M}, x + z = y + z → x = y := + by + have ind := iopen.open_induction <| display3 .z + (((x + z) =' (y + z) ⟹ (x =' y)) : Formula _ (Vars3 .z .x .y)) + simp_complexity at ind + simp_induction at ind + rw [forall_swap_231] + apply ind ?base ?step + · intro x y + rw [B3] + rw [B3] + intro h + exact h + · intro x hInd_x y z + conv => lhs; lhs; right; rw [add_comm] + conv => lhs; rhs; right; rw [add_comm] + rw [<- add_assoc] + rw [<- add_assoc] + intro h + apply B2 + apply hInd_x + exact h + +end add_cancel_right + +theorem add_cancel_right + : ∀ {x y z : M}, x + z = y + z <-> x = y := +by + intro x y z + constructor + · exact add_cancel_right.mp + · intro h + rw [h] + +theorem add_cancel_left + : ∀ {x y z : M}, z + x = z + y <-> x = y := +by + intro x y z + constructor + · conv => rw [add_comm]; lhs; rhs; rw [add_comm] + apply add_cancel_right.mp + · intro h + rw [h] + +-- O7. 0 ≤ x +theorem zero_le + : ∀ x : M, 0 ≤ x := +by + intro x + rw [<- B3 x] + rw [add_comm] + apply B8 + +-- O8. x ≤ 0 → x = 0 +theorem le_zero_eq + : ∀ x : M, x ≤ 0 → x = 0 := +by + intro x h + apply B7 + · exact h + · apply zero_le + +-- O9. x ≤ x +-- This is proved already as BASICModel.le_refl (doesn't need induction) +-- theorem le_refl +-- : ∀ x : M, x ≤ x := +-- by +-- intro x +-- conv => right; rw [<- B3 x] +-- apply B8 + +-- O10. x ≠ x + 1 +theorem ne_succ + : ∀ x : M, x ≠ x + 1 := +by + have ind := iopen.open_induction <| display1 + ((x ≠' (x + 1)) : Formula _ (Vars1 .x)) + simp_complexity at ind + simp_induction at ind + apply ind ?base ?step + · intro h + -- TODO: why this self is necessary? + exact (B1 (self := iopen.toBASICModel)) h.symm + · intro a h hq + apply h + apply B2 + exact hq + +theorem add_mul + : ∀ x y z : M, (x + y) * z = x * z + y * z := +by + intro x y z + rw [mul_comm] + rw [mul_add] + rw [mul_comm] + conv => lhs; rhs; rw [mul_comm] + +end IOPENModel diff --git a/LeanPool/FormalizationOfBoundedArithmetic/IsEnum.lean b/LeanPool/FormalizationOfBoundedArithmetic/IsEnum.lean new file mode 100644 index 0000000000..38e5155dce --- /dev/null +++ b/LeanPool/FormalizationOfBoundedArithmetic/IsEnum.lean @@ -0,0 +1,123 @@ +/- +Copyright (c) 2026 ruplet. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: ruplet +-/ + +-- Source: the example from https://lean-lang.org/doc/reference/latest/Type-Classes/Deriving-Instances/ +-- extended with case for empty type +import Lean +import Mathlib.Logic.IsEmpty.Basic +import Mathlib.Logic.Equiv.Defs +import Mathlib.Data.Finite.Defs +import Mathlib.Data.List.Nodup +import Mathlib.Data.List.OfFn + +open Lean Elab Parser Term Command + +universe u + +/-- A finite type equipped with explicit encodings to and from a finite index type. -/ +class IsEnum (α : Type u) where + /-- The number of elements in the enumeration. -/ + size : Nat + /-- Encode an element as an index. -/ + toIdx : α → Fin size + /-- Decode an index as an element. -/ + fromIdx : Fin size → α + /-- Decoding and then encoding gives back the same index. -/ + to_from_id : ∀ (i : Fin size), toIdx (fromIdx i) = i + /-- Encoding and then decoding gives back the same element. -/ + from_to_id : ∀ (x : α), fromIdx (toIdx x) = x + +/-- Deriving handler for `IsEnum` on finite inductive types. -/ +def deriveIsEnum (declNames : Array Name) : CommandElabM Bool := do + if h : declNames.size = 1 then + let env ← getEnv + if let some (.inductInfo ind) := env.find? declNames[0] then + if ind.ctors.isEmpty then + let cmd ← `( + instance : IsEnum $(mkIdent declNames[0]) where + size := 0 + toIdx := Empty.elim + fromIdx := Fin.elim0 + to_from_id := by simp only [IsEmpty.forall_iff] + from_to_id := by simp only [IsEmpty.forall_iff] + ) + elabCommand cmd + return true + else + let mut tos : Array (TSyntax ``matchAlt) := #[] + let mut froms := #[] + let mut to_froms := #[] + let mut from_tos := #[] + let mut i := 0 + for ctorName in ind.ctors do + let c := mkIdent ctorName + let n := Syntax.mkNumLit (toString i) + tos := tos.push (← `(matchAltExpr| | $c => $n)) + from_tos := from_tos.push (← `(matchAltExpr| | $c => rfl)) + froms := froms.push (← `(matchAltExpr| | $n => $c)) + to_froms := to_froms.push (← `(matchAltExpr| | $n => rfl)) + i := i + 1 + let cmd ← `(instance : IsEnum $(mkIdent declNames[0]) where + size := $(quote ind.ctors.length) + toIdx $tos:matchAlt* + fromIdx $froms:matchAlt* + to_from_id $to_froms:matchAlt* + from_to_id $from_tos:matchAlt*) + elabCommand cmd + return true + return false + +initialize + registerDerivingHandler ``IsEnum deriveIsEnum + + +namespace IsEnum +variable {α} {enum : IsEnum α} + + +/-- The index decoder is a left inverse of the encoder. -/ +theorem left_inv : Function.LeftInverse enum.fromIdx enum.toIdx := + enum.from_to_id + +/-- The index decoder is a right inverse of the encoder. -/ +theorem right_inv : Function.RightInverse enum.fromIdx enum.toIdx := + enum.to_from_id + +/-- The equivalence between an enumerated type and its finite index type. -/ +def equiv : α ≃ Fin (enum.size) where + toFun := enum.toIdx + invFun := enum.fromIdx + left_inv := left_inv + right_inv := right_inv + +/-- An enumerated type is finite. -/ +theorem finite (enum : IsEnum α) : Finite α := + @Finite.intro α (@IsEnum.size α enum) (equiv (enum := enum)) + +/-- The decoder from indices is injective. -/ +theorem fromIdx_injective : Function.Injective enum.fromIdx := + Function.LeftInverse.injective right_inv + +/-- The encoder to indices is injective. -/ +theorem toIdx_injective : Function.Injective enum.toIdx := Function.LeftInverse.injective left_inv + +-- Inspired by Mathlib.Data.Finset.Dedup.lean; toList, nodup_toList... +-- https://github.com/leanprover-community/mathlib4/blob/f4506f7151c9057fd9f8714b2a1f13a647fe2352/Mathlib/Data/Finset/Dedup.lean#L162-L164 +section ToList +/-- List all elements of an enumerated type in index order. -/ +def toList : List α := List.ofFn enum.fromIdx + +theorem nodup_toList : enum.toList.Nodup := by + unfold List.Nodup + unfold toList + rw [List.pairwise_ofFn] + intro i j hij + apply Function.Injective.ne fromIdx_injective + exact Fin.ne_of_lt hij + +end ToList + +end IsEnum diff --git a/LeanPool/FormalizationOfBoundedArithmetic/LanguagePeano.lean b/LeanPool/FormalizationOfBoundedArithmetic/LanguagePeano.lean new file mode 100644 index 0000000000..d2123b64d6 --- /dev/null +++ b/LeanPool/FormalizationOfBoundedArithmetic/LanguagePeano.lean @@ -0,0 +1,109 @@ +/- +Copyright (c) 2026 ruplet. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: ruplet +-/ + +import Mathlib.ModelTheory.Order + +import LeanPool.FormalizationOfBoundedArithmetic.Register + +universe u v + +namespace FirstOrder +namespace Language + +-- this style of definition is inspired by https://github.com/leanprover-community/mathlib4/blob/2cb771d3006e8b7579f66990fed1b433bf2e7fed/Mathlib/ModelTheory/Arithmetic/Presburger/Basic.lean +-- Definition 2.3, page 12 of draft (23 of pdf); +-- + remark in section 3.1, top of page 34 of draft (45 of pdf) +-- note: the equality relation is present by default in Mathlib.ModelTheory +-- it is explicit in Cook and Nguyen, but it doesn't seem to lead to any inconsistencies +-- note: checking if 'x = y is not always trivial; if x and y are long bit-strings, +-- encoded as lists (e.g. 3 encoded as S(S(S(Z)))), checking for their equality +-- is linear-time, thus not trivial at all. But here we only use equality in proofs +-- and the only way to assert equality is to prove it from axioms. So it seems like we'll +-- never run into the problem of having to brute-force checking for equality +/-- Function symbols for the Peano arithmetic language. -/ +inductive PeanoFunc : Nat -> Type* + | zero : PeanoFunc 0 + | one : PeanoFunc 0 + | add : PeanoFunc 2 + | mul : PeanoFunc 2 + deriving DecidableEq + +/-- Relation symbols for the Peano arithmetic language. -/ +inductive PeanoRel : Nat -> Type* + | leq : PeanoRel 2 + deriving DecidableEq + +/-- The first-order language of Peano arithmetic used by the formalization. -/ +def peano : Language := +{ Functions := PeanoFunc, + Relations := PeanoRel +} + +namespace peano +variable {a : Type u} + +@[delta0_simps] +instance : Language.IsOrdered peano where + leSymb := PeanoRel.leq + +@[delta0_simps] instance : Zero (peano.Term a) where + zero := Constants.term .zero + +@[delta0_simps] instance : One (peano.Term a) where + one := Constants.term .one + +@[delta0_simps] instance : Add (peano.Term a) where + add := Functions.apply₂ .add + +@[delta0_simps] instance : Mul (peano.Term a) where + mul := Functions.apply₂ .mul + +-- inspired by https://github.com/leanprover-community/mathlib4/blob/cff2a6ea669abe2e384ea4c359f20ee90a5dc855/Mathlib/ModelTheory/Syntax.lean#L732 +-- standard precedence of ≤, ≠, <: 50 +-- standard precedence of +: 65; of *: 70 +-- precedence of ⟹ in ModelTheory: 62, of =': 88 +-- the higher precedence the tighter bounding +@[inherit_doc] scoped[FirstOrder.Language] infixl:89 " <=' " => Term.le +@[inherit_doc] scoped[FirstOrder.Language] infixl:89 " <' " => Term.lt + +/-- The not-equal relation of two terms as a bounded formula -/ +@[delta0_simps] +def _root_.FirstOrder.Term.neq + {a : Type u} {n} {L : Language} (t1 t2 : L.Term (a ⊕ Fin n)) : + L.BoundedFormula a n := + ∼(t1 =' t2) +@[inherit_doc] scoped[FirstOrder.Language] infixl:88 " ≠' " => Term.neq + + +instance {M} [h : Language.peano.Structure M] : Zero M := + ⟨h.funMap PeanoFunc.zero ![]⟩ + +instance {M} [h : Language.peano.Structure M] : One M := + ⟨h.funMap PeanoFunc.one ![]⟩ + +instance {M} [h : Language.peano.Structure M] : Add M := + ⟨fun x y => h.funMap PeanoFunc.add ![x, y]⟩ + +instance {M} [h : Language.peano.Structure M] : Mul M := + ⟨fun x y => h.funMap PeanoFunc.mul ![x, y]⟩ + +instance {M} [h : Language.peano.Structure M] : LE M := + ⟨fun x y => h.RelMap PeanoRel.leq ![x, y]⟩ + +@[simp] +instance {M} [h : Language.peano.Structure M] : LT M := + ⟨fun x y => x <= y ∧ ¬ y <= x⟩ + +/-- Interpret natural-number literals in a structure for the Peano language. -/ +def natToM {M} [h : Language.peano.Structure M] : Nat -> M +| 0 => 0 +| 1 => 1 +| n + 1 => natToM n + 1 + +instance {M} [h : Language.peano.Structure M] (n) : OfNat M n where + ofNat := natToM n + +end FirstOrder.Language.peano diff --git a/LeanPool/FormalizationOfBoundedArithmetic/LanguageZambella.lean b/LeanPool/FormalizationOfBoundedArithmetic/LanguageZambella.lean new file mode 100644 index 0000000000..d6618817f9 --- /dev/null +++ b/LeanPool/FormalizationOfBoundedArithmetic/LanguageZambella.lean @@ -0,0 +1,251 @@ +/- +Copyright (c) 2026 ruplet. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: ruplet +-/ + +import Mathlib.ModelTheory.Syntax +import Mathlib.ModelTheory.Order +import Mathlib.ModelTheory.LanguageMap + +import LeanPool.FormalizationOfBoundedArithmetic.DisplayedVariables +import LeanPool.FormalizationOfBoundedArithmetic.LanguagePeano + +universe u v u' + +namespace FirstOrder +namespace Language + +-- Definition 4.4, Draft page 70 (page 81 of pdf) +-- + note about adding the axiom "E" and empty-string constant in a section below +/-- Function symbols for the two-sorted Zambella language. -/ +inductive ZambellaFunc : Nat -> Type u +| zero : ZambellaFunc 0 +| one : ZambellaFunc 0 +| empty : ZambellaFunc 0 +| len : ZambellaFunc 1 +| add : ZambellaFunc 2 +| mul : ZambellaFunc 2 +deriving DecidableEq + +/-- Relation symbols for the two-sorted Zambella language. -/ +inductive ZambellaRel : Nat -> Type u +-- | eqsort, eqstr -- we will use built-in equality syntax from ModelTheory lib +| isnum : ZambellaRel 1 +| isstr : ZambellaRel 1 +| leq : ZambellaRel 2 +| mem : ZambellaRel 2 +deriving DecidableEq + +/-- The two-sorted language for bounded arithmetic. -/ +def zambella : Language := +{ Functions := ZambellaFunc, + Relations := ZambellaRel +} + +variable {a : Type u} + +instance : Language.IsOrdered zambella where + leSymb := ZambellaRel.leq + +@[simp] instance : Zero (zambella.Term a) where + zero := Constants.term .zero + +@[simp] instance : One (zambella.Term a) where + one := Constants.term .one + +/-- Types with a distinguished empty set or string element. -/ +class HasEmptySet (α : Type*) where + /-- The distinguished empty element. -/ + empty : α + +@[simp] instance : HasEmptySet (zambella.Term a) where + empty := Constants.term .empty + +/-- Types with a length map into another type. -/ +class HasLen (α : Type u) (β : Type v) where + /-- Length of an object. -/ + len : α -> β + +@[simp] instance : HasLen (zambella.Term a) (zambella.Term a) where + len := Functions.apply₁ .len + +@[simp] instance : Add (zambella.Term a) where + add := Functions.apply₂ .add + +@[simp] instance : Mul (zambella.Term a) where + mul := Functions.apply₂ .mul + +/-- Predicate interface for values that are either numbers or strings. -/ +class HasTypes_is (α : Type*) where + /-- The value is a number. -/ + int : α -> Prop + /-- The value is a string. -/ + str : α -> Prop + dec : ∀ x, int x ∨ str x + excl : ∀ x, (int x -> ¬str x) ∧ (str x -> ¬int x) + + +instance {M} [h : zambella.Structure M] : Zero M := + ⟨h.funMap ZambellaFunc.zero ![]⟩ + +instance {M} [h : zambella.Structure M] : One M := + ⟨h.funMap ZambellaFunc.one ![]⟩ + +instance {M} [h : zambella.Structure M] : Add M := + ⟨fun x y => h.funMap ZambellaFunc.add ![x, y]⟩ + +instance {M} [h : zambella.Structure M] : Mul M := + ⟨fun x y => h.funMap ZambellaFunc.mul ![x, y]⟩ + +instance {M} [h : zambella.Structure M] : LE M := + ⟨fun x y => h.RelMap ZambellaRel.leq ![x, y]⟩ + +instance {M} [h : zambella.Structure M] : HasEmptySet M := + ⟨h.funMap ZambellaFunc.empty ![]⟩ + +instance {M} [h : zambella.Structure M] : HasLen M M := + ⟨fun x => h.funMap ZambellaFunc.len ![x]⟩ + +instance {M} [h : zambella.Structure M] : Membership M M := + ⟨fun x y => h.RelMap ZambellaRel.mem ![x, y]⟩ + +instance {M} [h : zambella.Structure M] : peano.Structure M where + funMap := fun {arity} f => + match arity, f with + | 0, PeanoFunc.zero => fun _ => 0 + | 0, PeanoFunc.one => fun _ => 1 + | 2, PeanoFunc.add => fun args => (args 0) + (args 1) + | 2, PeanoFunc.mul => fun args => (args 0) * (args 1) + + RelMap := fun {arity} r => + match arity, r with + | 2, PeanoRel.leq => fun args => (args 0) <= (args 1) + +-- use Zero, One instances explicitly to avoid circular dependency +instance {M} [h : zambella.Structure M] (n) : OfNat M n where + ofNat := aux n +where + aux : Nat -> M + | 0 => Zero.zero + | 1 => One.one + | n + 1 => (aux n) + One.one + +@[simp] lemma realize_zero_to_zero {M} [zambella.Structure M] {a} {env : a → M} : + Language.Term.realize env (0 : zambella.Term a) = (0 : M) := by + simp only [OfNat.ofNat, Zero.zero] + simp only [zambella, Term.realize_constants] + rfl + +-- it is important to define OfNat 1 as 1, not (0+1), as the later needs an axiom to +-- be asserted equal to 1. +@[simp] lemma realize_one_to_one {M} [zambella.Structure M] {a} {env : a → M} : + Term.realize env (1 : zambella.Term a) = (1 : M) := by + simp only [OfNat.ofNat, One.one] + simp only [zambella, Term.realize_constants] + rfl + +@[simp] lemma realize_add_to_add {M} [h : zambella.Structure M] {a} {env : a → M} + (t u : zambella.Term a) : + Term.realize env (t + u) = Term.realize env t + Term.realize env u := by + simp only [zambella, HAdd.hAdd, Add.add] + -- TODO: why the below doesn't work without @? + rw [@Term.realize_functions_apply₂] + +@[simp] lemma realize_mul_to_mul {M} [zambella.Structure M] {a} {env : a → M} + (t u : zambella.Term a) : + Term.realize env (t * u) = Term.realize env t * Term.realize env u := by + simp only [HMul.hMul, Mul.mul] + rw [@Term.realize_functions_apply₂] + +lemma realize_leq_to_leq {M} [h : zambella.Structure M] {a} {env : a → M} + {k} (t u : zambella.Term (a ⊕ (Fin k))) {xs} : + (t.le u).Realize env xs = (t.realize (Sum.elim env xs) <= u.realize (Sum.elim env xs)) := by + simp only [LE.le, Term.le, Relations.boundedFormula₂] + rw [← @BoundedFormula.realize_rel₂] + unfold Relations.boundedFormula₂ + rfl + +@[simp] lemma realize_leq_to_leq' {M} [h : zambella.Structure M] {a} {env : a → M} + {k} (t u : zambella.Term (a ⊕ (Fin k))) {xs} : + (BoundedFormula.rel ZambellaRel.leq ![t, u]).Realize env xs = + (t.realize (Sum.elim env xs) <= u.realize (Sum.elim env xs)) := by + simp only [LE.le] + rw [← @BoundedFormula.realize_rel₂] + unfold Relations.boundedFormula₂ Relations.boundedFormula + rfl + +@[simp] lemma realize_leq_to_leq'' {M} [h : zambella.Structure M] {a} {env : a → M} + {k} (t u : zambella.Term (a ⊕ (Fin k))) {xs} : + h.RelMap ZambellaRel.leq + ![t.realize (Sum.elim env xs), u.realize (Sum.elim env xs)] <-> + (t.realize (Sum.elim env xs) <= u.realize (Sum.elim env xs)) := by + exact Eq.to_iff rfl + +namespace Term + +/-- Formula asserting that a term denotes a number. -/ +def IsNum (t : zambella.Term (a ⊕ Fin 0)) : zambella.Formula a := + Relations.boundedFormula₁ ZambellaRel.isnum t + +/-- Formula asserting that a term denotes a string. -/ +def IsStr (t : zambella.Term (a ⊕ Fin 0)) : zambella.Formula a := + Relations.boundedFormula₁ ZambellaRel.isstr t + +end Term + +/-- Guard a formula by asserting that its displayed variable is a number. -/ +nonrec def Formula.IsNum {n} (phi : zambella.Formula (Vars1 n)) := + (var <| .inl .fv1).IsNum ⟹ phi + +/-- The membership relation of two terms as a bounded formula -/ +def _root_.FirstOrder.Term.in {a : Type u} {n} + (t1 t2 : zambella.Term (a ⊕ (Fin n))) : zambella.BoundedFormula a n := + Relations.boundedFormula₂ ZambellaRel.mem t2 t1 +@[inherit_doc] scoped[FirstOrder.Language] infixl:88 " ∈' " => Term.in + +/-- The not-mem relation of two terms as a bounded formula -/ +@[delta0_simps] +def _root_.FirstOrder.Term.notin {a : Type u} {n} + (t1 t2 : zambella.Term (a ⊕ (Fin n))) : zambella.BoundedFormula a n := + ∼(t1 ∈' t2) + +@[inherit_doc] scoped[FirstOrder.Language] infixl:88 " ∉' " => Term.notin + + +/-- Two-sorted structures satisfying the intended Zambella typing axioms. -/ +class ZambellaModel (num str : Type u') + extends + zambella.Structure.{u'} (num ⊕ str), + Preorder (num ⊕ str), + OrderedStructure zambella (num ⊕ str) + where + ax_realize_isnum {a : Type} {t : zambella.Term (a ⊕ Fin 0)} {v : a -> (num ⊕ str)}: + t.IsNum.Realize v + <-> (t.realize (Sum.elim v Fin.elim0)).isLeft + + ax_realize_isstr {a : Type} {v : a -> (num ⊕ str)} {t : zambella.Term (a ⊕ Fin 0)} : + t.IsStr.Realize v + <-> (t.realize (Sum.elim v Fin.elim0)).isRight + + ax_realize_in {a : Type} {n} + {t1 t2 : zambella.Term (a ⊕ Fin n)} + {v : a -> (num ⊕ str)} + {xs : Fin n -> (num ⊕ str)}: + (Term.in t1 t2).Realize v xs + <-> (t1.realize (Sum.elim v xs)) ∈ (t2.realize (Sum.elim v xs)) + + + +-- LHOM +/-- Language homomorphism embedding Peano arithmetic into the Zambella language. -/ +def peanoToZambella : LHom peano zambella where + onFunction _ f := match f with + | PeanoFunc.zero => ZambellaFunc.zero + | PeanoFunc.one => ZambellaFunc.one + | PeanoFunc.add => ZambellaFunc.add + | PeanoFunc.mul => ZambellaFunc.mul + onRelation _ f := match f with + | PeanoRel.leq => ZambellaRel.leq + +end FirstOrder.Language diff --git a/LeanPool/FormalizationOfBoundedArithmetic/MathlibSimps.lean b/LeanPool/FormalizationOfBoundedArithmetic/MathlibSimps.lean new file mode 100644 index 0000000000..8261ce196b --- /dev/null +++ b/LeanPool/FormalizationOfBoundedArithmetic/MathlibSimps.lean @@ -0,0 +1,33 @@ +/- +Copyright (c) 2026 ruplet. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: ruplet +-/ + +-- In this file this is crucial to be careful with imports, +-- as all `simp` lemmas in scope will get our `delta0_simp` attribute! +import Lean +import Mathlib.Lean.Meta.Simp +import Mathlib.Tactic.Simps.Basic + +import Mathlib.ModelTheory.Basic +import Mathlib.ModelTheory.Syntax +import Mathlib.ModelTheory.Semantics +import Mathlib.ModelTheory.Order +import Mathlib.ModelTheory.Complexity + +import LeanPool.FormalizationOfBoundedArithmetic.Register + +open Lean Elab Command + +/-- Add existing Mathlib model-theory simp lemmas to the local `delta0_simps` simp set. -/ +elab "mkDelta0FromModelTheory" : command => do + let env ← getEnv + let targetMod : Name := `FirstOrder.Language + -- Collect all decls with names under the target module *and* having `[simp]` + for (declName, _) in env.constants do + if targetMod.isPrefixOf declName then + if ← liftCoreM <| Meta.isInSimpSet `simp declName then + elabCommand (← `(attribute [delta0_simps] $(mkIdent declName))) + +mkDelta0FromModelTheory diff --git a/LeanPool/FormalizationOfBoundedArithmetic/Order.lean b/LeanPool/FormalizationOfBoundedArithmetic/Order.lean new file mode 100644 index 0000000000..8421f2d70b --- /dev/null +++ b/LeanPool/FormalizationOfBoundedArithmetic/Order.lean @@ -0,0 +1,183 @@ +/- +Copyright (c) 2026 ruplet. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: ruplet +-/ + +import Mathlib.ModelTheory.Syntax +import Mathlib.ModelTheory.Order +import Mathlib.Tactic.FinCases + +import LeanPool.FormalizationOfBoundedArithmetic.DisplayedVariables +import LeanPool.FormalizationOfBoundedArithmetic.Syntax +import LeanPool.FormalizationOfBoundedArithmetic.LanguageZambella + +namespace FirstOrder.Language.Formula + +open Language BoundedFormula + +section IsOrdered +universe u +variable {L : Language} [IsOrdered L] {α : Type u} + +variable {n r} (a b : L.BoundedFormula n r) + + +/-- Existential quantification bounded by a term. -/ +def iBdEx' {α n} (bdTerm : L.Term (α ⊕ Fin 0)) + (φ : L.Formula (α ⊕ (Vars1 n))) : L.Formula α := + let bd := (var (.inl (Sum.inr (.fv1)))).le <| bdTerm.relabel (Sum.map .inl id) + iExs' <| bd ⊓ φ + +/-- Universal quantification bounded by a term. -/ +def iBdAll' {α n} (bdTerm : L.Term (α ⊕ Fin 0)) + (φ : L.Formula (α ⊕ (Vars1 n))) : L.Formula α := + let bd := (var (.inl (Sum.inr (.fv1)))).le <| bdTerm.relabel (Sum.map .inl id) + iAlls' <| bd ⟹ φ + +-- TODO: there should only be Lt constructors in Complexity +-- and iBd should be an alias to iBdLt with term + 1 +/-- Universal quantification bounded strictly by a term. -/ +def iBdAllLt' {α n} (bdTerm : L.Term (α ⊕ Fin 0)) + (φ : L.Formula (α ⊕ (Vars1 n))) : L.Formula α := + let bd := (var (.inl (Sum.inr (.fv1)))).lt <| bdTerm.relabel (Sum.map .inl id) + iAlls' <| bd ⟹ φ + +/-- Existential quantification bounded by a term and guarded as numeric. -/ +def iBdExNum' + {α n} + (bdTerm : zambella.Term (α ⊕ Fin 0)) + (φ : zambella.Formula (α ⊕ (Vars1 n))) + : zambella.Formula α := + iBdEx' bdTerm <| (var <| Sum.inl <| Sum.inr <| .fv1).IsNum ⊓ φ + +/-- Existential quantification bounded by a term and guarded as a string. -/ +def iBdExStr' + {α n} + (bdTerm : zambella.Term (α ⊕ Fin 0)) + (φ : zambella.Formula (α ⊕ (Vars1 n))) + : zambella.Formula α := + iBdEx' bdTerm <| (var <| Sum.inl <| Sum.inr <| .fv1).IsStr ⊓ φ + +/-- Universal quantification bounded by a term and guarded as numeric. -/ +def iBdAllNum' + {α n} + (bdTerm : zambella.Term (α ⊕ Fin 0)) + (φ : zambella.Formula (α ⊕ (Vars1 n))) + : zambella.Formula α := + iBdAll' bdTerm <| (var <| Sum.inl <| Sum.inr <| .fv1).IsNum ⟹ φ + +/-- Universal quantification strictly bounded by a term and guarded as numeric. -/ +def iBdAllNumLt' + {α n} + (bdTerm : zambella.Term (α ⊕ Fin 0)) + (φ : zambella.Formula (α ⊕ (Vars1 n))) + : zambella.Formula α := + iBdAllLt' bdTerm <| (var <| Sum.inl <| Sum.inr <| .fv1).IsNum ⟹ φ + + + +open Lean Elab Tactic + +namespace iBdEx' + +theorem relabelEquiv + {α β n} (bdTerm : L.Term (α ⊕ Fin 0)) (φ : L.Formula (α ⊕ (Vars1 n))) + (f : α ≃ β) + : relabelEquiv f (iBdEx' bdTerm φ) + = iBdEx' + (Term.relabelEquiv (f.sumCongr (_root_.Equiv.refl (Fin 0))) bdTerm) + (relabelEquiv (f.sumCongr (_root_.Equiv.refl (Vars1 n))) φ) := +by + unfold iBdEx' + rw [relabelEquiv.iExs'] + congr + rw [relabelEquiv.inf] + congr + · unfold Term.le Relations.boundedFormula₂ Relations.boundedFormula + rw [relabelEquiv.rel] + congr + funext x + simp only [Term.relabelEquiv_apply, Term.relabel_relabel] + fin_cases x + · simp only [Fin.zero_eta, Fin.isValue, Matrix.cons_val_zero, Term.relabel.eq_1, Sum.map_inl, + Equiv.sumCongr_apply, Equiv.coe_refl, Sum.map_inr, id_eq] + · simp [Fin.mk_one, Matrix.cons_val_one, Matrix.cons_val_fin_one, + Term.relabel_relabel, Sum.map_comp_map, Function.comp_id, Equiv.sumCongr] + congr 1 + +end iBdEx' + +namespace iBdAll' + +theorem relabelEquiv + {α β n} (bdTerm : L.Term (α ⊕ Fin 0)) (φ : L.Formula (α ⊕ (Vars1 n))) + (f : α ≃ β) + : relabelEquiv f (iBdAll' bdTerm φ) + = iBdAll' + (Term.relabelEquiv (f.sumCongr (_root_.Equiv.refl (Fin 0))) bdTerm) + (relabelEquiv (f.sumCongr (_root_.Equiv.refl (Vars1 n))) φ) := +by + unfold iBdAll' + rw [relabelEquiv.iAlls'] + congr + rw [relabelEquiv.imp] + congr + · unfold Term.le Relations.boundedFormula₂ Relations.boundedFormula + rw [relabelEquiv.rel] + congr + funext x + simp only [Term.relabelEquiv_apply, Term.relabel_relabel] + fin_cases x + · simp only [Fin.zero_eta, Fin.isValue, Matrix.cons_val_zero, Term.relabel.eq_1, Sum.map_inl, + Equiv.sumCongr_apply, Equiv.coe_refl, Sum.map_inr, id_eq] + · simp [Fin.mk_one, Matrix.cons_val_one, Matrix.cons_val_fin_one, + Term.relabel_relabel, Sum.map_comp_map, Function.comp_id, Equiv.sumCongr] + congr 1 + +end iBdAll' + +namespace iBdAllLt' + +theorem relabelEquiv + {α β n} (bdTerm : L.Term (α ⊕ Fin 0)) (φ : L.Formula (α ⊕ (Vars1 n))) + (f : α ≃ β) + : relabelEquiv f (iBdAllLt' bdTerm φ) + = iBdAllLt' + (Term.relabelEquiv (f.sumCongr (_root_.Equiv.refl (Fin 0))) bdTerm) + (relabelEquiv (f.sumCongr (_root_.Equiv.refl (Vars1 n))) φ) := +by + unfold iBdAllLt' + rw [relabelEquiv.iAlls'] + congr + rw [relabelEquiv.imp] + congr + · unfold Term.lt + rw [BoundedFormula.relabelEquiv.inf] + congr + · unfold Term.le Relations.boundedFormula₂ Relations.boundedFormula + rw [BoundedFormula.relabelEquiv.rel] + congr + funext x + simp only [Term.relabelEquiv_apply, Term.relabel_relabel] + fin_cases x <;> simp [Fin.mk_one, Matrix.cons_val_one, Matrix.cons_val_fin_one, + Matrix.cons_val_zero, Term.relabel_relabel, Sum.map_comp_map, + Function.comp_id, Equiv.sumCongr] + congr 1 + · rw [BoundedFormula.relabelEquiv.not] + congr + unfold Term.le Relations.boundedFormula₂ Relations.boundedFormula + rw [BoundedFormula.relabelEquiv.rel] + congr + funext x + simp only [Term.relabelEquiv_apply, Term.relabel_relabel] + fin_cases x <;> simp [Fin.mk_one, Matrix.cons_val_one, Matrix.cons_val_fin_one, + Matrix.cons_val_zero, Term.relabel_relabel, Sum.map_comp_map, + Function.comp_id, Equiv.sumCongr] + congr 1 + +end iBdAllLt' + +end IsOrdered + +end FirstOrder.Language.Formula diff --git a/LeanPool/FormalizationOfBoundedArithmetic/Register.lean b/LeanPool/FormalizationOfBoundedArithmetic/Register.lean new file mode 100644 index 0000000000..0f82a6dc84 --- /dev/null +++ b/LeanPool/FormalizationOfBoundedArithmetic/Register.lean @@ -0,0 +1,11 @@ +/- +Copyright (c) 2026 ruplet. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: ruplet +-/ + +-- only here we register simp attributes +-- details: https://leanprover-community.github.io/mathlib4_docs/Mathlib/Tactic/Attr/Core.html +import Lean +/-- Simp set used by the bounded-arithmetic import for formula normalization. -/ +register_simp_attr delta0_simps diff --git a/LeanPool/FormalizationOfBoundedArithmetic/Semantics.lean b/LeanPool/FormalizationOfBoundedArithmetic/Semantics.lean new file mode 100644 index 0000000000..0110c57571 --- /dev/null +++ b/LeanPool/FormalizationOfBoundedArithmetic/Semantics.lean @@ -0,0 +1,686 @@ +/- +Copyright (c) 2026 ruplet. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: ruplet +-/ + +import Lean + +import Mathlib.ModelTheory.Semantics + +import LeanPool.FormalizationOfBoundedArithmetic.Syntax +import LeanPool.FormalizationOfBoundedArithmetic.DisplayedVariables +import LeanPool.FormalizationOfBoundedArithmetic.SimpRules +import LeanPool.FormalizationOfBoundedArithmetic.Order +import LeanPool.FormalizationOfBoundedArithmetic.LanguagePeano +import LeanPool.FormalizationOfBoundedArithmetic.LanguageZambella + +namespace FirstOrder.Language +open BoundedFormula + +open Lean Elab Tactic Command + + +namespace Term + + +@[delta0_simps] lemma realize_zero {M} [peano.Structure M] {a} {env : a → M} : + Language.Term.realize env (0 : peano.Term a) = (0 : M) := by + simp only [OfNat.ofNat, Zero.zero] + simp only [peano, Term.realize_constants] + rfl + +-- it is important to define OfNat 1 as 1, not (0+1), as the later needs an axiom to +-- be asserted equal to 1. +@[delta0_simps] lemma realize_one {M} [peano.Structure M] {a} {env : a → M} : + Term.realize env (1 : peano.Term a) = (1 : M) := by + simp only [OfNat.ofNat, One.one] + simp only [peano, Term.realize_constants] + rfl + +@[delta0_simps] lemma realize_add {M} [h : peano.Structure M] {a} {env : a → M} + (t u : peano.Term a) : + Term.realize env (t + u) = Term.realize env t + Term.realize env u := by + simp only [peano, HAdd.hAdd, Add.add] + -- TODO: why the below doesn't work without @? + rw [@Term.realize_functions_apply₂] + +@[delta0_simps] lemma realize_mul {M} [peano.Structure M] {a} {env : a → M} + (t u : peano.Term a) : + Term.realize env (t * u) = Term.realize env t * Term.realize env u := by + simp only [HMul.hMul, Mul.mul] + rw [@Term.realize_functions_apply₂] + +end Term + + +namespace BoundedFormula +variable {L : Language} {M : Type*} [L.Structure M] {a b} {n1 n2 n3} {n} + +-- important: DON'T make this a simp lemma! +-- breaks everything +-- @[delta0_simps] +-- lemma realize_Formula (phi : L.Formula a) {v : a -> M} {xs} +-- : BoundedFormula.Realize phi v xs +-- <-> +-- phi.Realize v +-- := +-- by +-- exact Formula.boundedFormula_realize_eq_realize phi v xs + +-- @[delta0_simps] +-- lemma realize_flip (phi : L.BoundedFormula (a ⊕ b) n) {v : (b ⊕ a) -> M} {xs} +-- : phi.flip.Realize v xs +-- <-> +-- phi.Realize (v ∘ Sum.swap) xs +-- := +-- by +-- unfold BoundedFormula.flip +-- rw [realize_relabelEquiv] +-- dsimp only [Equiv.coe_fn_mk] +-- exact Eq.to_iff rfl + +end BoundedFormula + + +namespace Formula + +variable {L : Language} {M : Type*} [L.Structure M] {a b} {n1 n2 n3 n4} + +@[delta0_simps] +lemma realize_flip (phi : L.Formula (a ⊕ b)) {v : (b ⊕ a) -> M} + : phi.flip.Realize v + <-> + phi.Realize (v ∘ Sum.swap) + := +by + unfold Formula.Realize + unfold Formula.flip + rw [realize_relabelEquiv] + dsimp only [Equiv.coe_fn_mk] + exact Eq.to_iff rfl + +@[delta0_simps] +lemma realize_rotate_21 (phi : L.Formula (Vars2 n1 n2)) {v : _ -> M} + : phi.rotate_21.Realize v + <-> + phi.Realize (v ∘ (fun fv => match fv with + | .fv1 => .fv2 + | .fv2 => .fv1)) + := +by + unfold Formula.Realize + unfold Formula.rotate_21 + rw [realize_relabelEquiv] + dsimp only [Equiv.coe_fn_mk] + exact Eq.to_iff rfl + +@[delta0_simps] +lemma realize_rotate_213 (phi : L.Formula (Vars3 n1 n2 n3)) {v : _ -> M} + : phi.rotate_213.Realize v + <-> + phi.Realize (v ∘ (fun fv => match fv with + | .fv1 => .fv2 + | .fv2 => .fv1 + | .fv3 => .fv3)) + := +by + unfold Formula.Realize + unfold Formula.rotate_213 + rw [realize_relabelEquiv] + dsimp only [Equiv.coe_fn_mk] + exact Eq.to_iff rfl + +@[delta0_simps] +lemma realize_mkInl (phi : L.Formula a) {v : (a ⊕ Empty) -> M} + : phi.mkInl.Realize v + <-> + phi.Realize (v ∘ Sum.inl) + := +by + unfold Formula.Realize + unfold Formula.mkInl + rw [realize_relabelEquiv] + dsimp only [Equiv.coe_fn_mk] + exact Eq.to_iff rfl + +@[delta0_simps] +lemma realize_display1 (phi : L.Formula (Vars1 n1)) {v : ((Vars1 n1) ⊕ Empty) -> M} + : phi.display1.Realize v + <-> + phi.Realize (v ∘ .inl) + := +by + unfold Formula.Realize + unfold Formula.display1 + rw [realize_relabelEquiv] + dsimp only [Equiv.coe_fn_mk] + exact Eq.to_iff rfl + +@[delta0_simps] +lemma realize_display2 (phi : L.Formula (Vars2 n1 n2)) + {v : ((Vars1 n1) ⊕ (Vars1 n2)) -> M} + : phi.display2.Realize v + <-> + phi.Realize (v ∘ (fun fv => match fv with + | .fv1 => .inl .fv1 + | .fv2 => .inr .fv1)) + := +by + unfold Formula.Realize + unfold Formula.display2 + rw [realize_relabelEquiv] + dsimp only [Equiv.coe_fn_mk] + exact Eq.to_iff rfl + +@[delta0_simps] +lemma realize_display3 (phi : L.Formula (Vars3 n1 n2 n3)) + {v : ((Vars1 n1) ⊕ (Vars2 n2 n3)) -> M} + : phi.display3.Realize v + <-> + phi.Realize (v ∘ (fun fv => match fv with + | .fv1 => .inl .fv1 + | .fv2 => .inr .fv1 + | .fv3 => .inr .fv2)) + := +by + unfold Formula.Realize + unfold Formula.display3 + rw [realize_relabelEquiv] + dsimp only [Equiv.coe_fn_mk] + exact Eq.to_iff rfl + +@[delta0_simps] +lemma realize_display4 (phi : L.Formula (Vars4 n1 n2 n3 n4)) + {v : ((Vars1 n1) ⊕ (Vars3 n2 n3 n4)) -> M} + : phi.display4.Realize v + <-> + phi.Realize (v ∘ (fun fv => match fv with + | .fv1 => .inl .fv1 + | .fv2 => .inr .fv1 + | .fv3 => .inr .fv2 + | .fv4 => .inr .fv3)) + := +by + unfold Formula.Realize + unfold Formula.display4 + rw [realize_relabelEquiv] + dsimp only [Equiv.coe_fn_mk] + exact Eq.to_iff rfl + + +@[delta0_simps] +lemma realize_display_swapleft (phi : L.Formula (Vars1 n1 ⊕ Vars2 n2 n3)) + {v : ((Vars2 n1 n2) ⊕ (Vars1 n3)) -> M} + : phi.display_swapleft.Realize v + <-> + phi.Realize (v ∘ (fun fv => match fv with + | .inl .fv1 => .inl .fv1 + | .inr .fv1 => .inl .fv2 + | .inr .fv2 => .inr .fv1)) + := +by + unfold Formula.Realize + unfold Formula.display_swapleft + rw [realize_relabelEquiv] + dsimp only [Equiv.coe_fn_mk] + exact Eq.to_iff rfl + +@[delta0_simps] +lemma realize_display_swapleft' (phi : L.Formula (Vars1 n1 ⊕ Vars2 n2 n3)) + {v : ((Vars1 n1 ⊕ Vars1 n2) ⊕ (Vars1 n3)) -> M} + : phi.display_swapleft'.Realize v + <-> + phi.Realize (v ∘ (fun fv => match fv with + | .inl .fv1 => .inl (.inl .fv1) + | .inr .fv1 => .inl (.inr .fv1) + | .inr .fv2 => .inr .fv1)) + := +by + unfold Formula.Realize + unfold Formula.display_swapleft' + rw [realize_relabelEquiv] + dsimp only [Equiv.coe_fn_mk] + exact Eq.to_iff rfl + + +/-- `peel_iAlls' k` rewrites `(iAlls' φ).Realize` by peeling exactly + `k` quantifiers (`realize_all; intro`). -/ +syntax (name := peelIAlls) "peel_iAlls' " num : conv + +-- TODO: substitute `n` with actual size of `IsEnum`'ed type +elab_rules : conv +| `(conv| peel_iAlls' $k:num) => do + let some n := k.raw.isNatLit? + | throwErrorAt k "peel_iAlls': expected a nonnegative integer literal" + Conv.evalUnfold (← `(conv| unfold iAlls')) + for _ in [:n + 1] do + Conv.evalUnfold (← `(conv| unfold BoundedFormula.alls)) + for _ in [:n] do + Conv.evalRewrite (← `(conv| rw [BoundedFormula.realize_all])) + Conv.evalExt (← `(conv| ext)) + Conv.evalRewrite (← `(conv| rw [BoundedFormula.realize_relabel])) + +/-- `peel_iExs' k` rewrites `(iExs' φ).Realize` by peeling exactly + `k` quantifiers (`realize_ex; intro`). -/ +syntax (name := peelIExs) "peel_iExs' " num : conv + +-- TODO: substitute `n` with actual size of `IsEnum`'ed type +elab_rules : conv +| `(conv| peel_iExs' $k:num) => do + let some n := k.raw.isNatLit? + | throwErrorAt k "peel_iExs': expected a nonnegative integer literal" + Conv.evalUnfold (← `(conv| unfold iExs')) + for _ in [:n + 1] do + Conv.evalUnfold (← `(conv| unfold BoundedFormula.exs)) + Conv.evalUnfold (← `(conv| unfold Formula.Realize)) + for _ in [:n] do + Conv.evalRewrite (← `(conv| rw [BoundedFormula.realize_ex])) + Conv.evalEnter (← `(conv| enter [1])) + Conv.evalExt (← `(conv| ext)) + Conv.evalRewrite (← `(conv| rw [BoundedFormula.realize_relabel])) + + + +namespace realize_iAlls' + +@[delta0_simps] +lemma Empty (phi : L.Formula (a ⊕ Empty)) {v : a -> M} + : phi.iAlls'.Realize v + <-> + phi.Realize + (Sum.elim v Empty.elim) + := +by + unfold Formula.Realize + conv => + lhs + peel_iAlls' 0 + constructor <;> + ( + intro h; + convert h; + funext; + rename_i x; + cases x; + simp only [Sum.elim_inl, Nat.add_zero, Fin.castAdd_zero, Fin.cast_refl, Function.comp_id, + Function.comp_apply, Sum.map_inl, id_eq] + apply Empty.elim; assumption + ) + +-- TODO: IT SHOULD HOLD DEFINITIONALLY?... but I couldn't prove without funext +@[delta0_simps] +lemma Vars1 (phi : L.Formula (a ⊕ Vars1 n1)) {v : a -> M} + : phi.iAlls'.Realize v + <-> + ∀ x : M, phi.Realize + (Sum.elim v (fun fv => match fv with | .fv1 => x)) + := +by + unfold Formula.Realize + conv => + lhs + peel_iAlls' 1 + -- unfold IsEnum.toIdx instIsEnumVars1; dsimp only + -- conv => + -- rhs; rhs; arg 2; arg 2; intro; dsimp only + constructor <;> + ( + intro h a; + specialize h a; + convert h; + funext; + rename_i x; + cases x; + ) <;> + simp [Fin.snoc] + + +@[delta0_simps] +lemma Vars2 (phi : L.Formula (a ⊕ Vars2 n1 n2)) {v : a -> M} + : phi.iAlls'.Realize v + <-> + ∀ x y : M, phi.Realize + (Sum.elim v (fun fv => match fv with | .fv1 => x | .fv2 => y)) + := +by + unfold Formula.Realize + conv => + lhs + peel_iAlls' 2 + constructor <;> intro h x y <;> specialize h x y <;> convert h + all_goals + funext z + cases z with + | inl z => simp + | inr z => cases z <;> simp [Fin.snoc, IsEnum.toIdx.Vars2] + +@[delta0_simps] +lemma Vars3 (phi : L.Formula (a ⊕ Vars3 n1 n2 n3)) {v : a -> M} + : phi.iAlls'.Realize v + <-> + ∀ x y z : M, phi.Realize + (Sum.elim v (fun fv => match fv with | .fv1 => x | .fv2 => y | .fv3 => z)) + := +by + unfold Formula.Realize + conv => + lhs + peel_iAlls' 3 + constructor <;> intro h x y z <;> specialize h x y z <;> convert h + all_goals + funext w + cases w with + | inl w => simp + | inr w => cases w <;> simp [Fin.snoc, IsEnum.toIdx.Vars3] + +end realize_iAlls' + +namespace realize_iExs' + +@[delta0_simps] +lemma Vars1 (phi : L.Formula (a ⊕ Vars1 n1)) {v : a -> M} + : phi.iExs'.Realize v + <-> + ∃ x : M, phi.Realize + (Sum.elim v (fun fv => match fv with | .fv1 => x)) + := +by + unfold Formula.Realize + conv => + lhs + peel_iExs' 1 + constructor <;> + ( + intro h; + obtain ⟨x, hx⟩ := h; + exists x + convert hx + funext + rename_i x + ) + · cases x + · simp only [Sum.elim_inl, Nat.add_zero, Nat.succ_eq_add_one, Nat.reduceAdd, Fin.castAdd_zero, + Fin.cast_refl, Function.comp_id, Function.comp_apply, Sum.map_inl, id_eq] + · simp only [Sum.elim_inr, IsEnum.size.Vars1, Nat.add_zero, + Nat.succ_eq_add_one, Nat.reduceAdd, Fin.castAdd_zero, Fin.cast_refl, Function.comp_id, + Function.comp_apply, Sum.map_inr] + simp only [Fin.snoc, Nat.reduceAdd, Fin.val_eq_zero, lt_self_iff_false, + ↓reduceDIte, Fin.reduceLast, cast_eq] + · cases x; + · simp only [Sum.elim_inl, IsEnum.size.Vars1, Nat.add_zero, + Nat.succ_eq_add_one, Nat.reduceAdd, Fin.castAdd_zero, Fin.cast_refl, Function.comp_id, + Function.comp_apply, Sum.map_inl, id_eq] + · simp only [Sum.elim_inr, IsEnum.size.Vars1, Nat.add_zero, + Nat.succ_eq_add_one, Nat.reduceAdd, Fin.castAdd_zero, Fin.cast_refl, Function.comp_id, + Function.comp_apply, Sum.map_inr, Fin.snoc, Fin.val_eq_zero, lt_self_iff_false, ↓reduceDIte, + Fin.reduceLast, cast_eq] + +end realize_iExs' + + +open ZambellaModel +universe u + +@[delta0_simps] +theorem _root_.FirstOrder.Term.realize_isnum {num str : Type u} [ZambellaModel num str] {a : Type} + {t : zambella.Term (a ⊕ Fin 0)} {v : a -> (num ⊕ str)} : + t.IsNum.Realize v + <-> (t.realize (Sum.elim v Fin.elim0)).isLeft := ax_realize_isnum + +@[delta0_simps] +theorem _root_.FirstOrder.Term.realize_isstr {num str : Type u} [ZambellaModel num str] {a : Type} + {t : zambella.Term (a ⊕ Fin 0)} {v : a -> (num ⊕ str)} : + t.IsStr.Realize v + <-> (t.realize (Sum.elim v Fin.elim0)).isRight := ax_realize_isstr + + +-- @[delta0_simps] +-- lemma realize_IsNum (phi : zambella.Formula a) {v : a -> (num ⊕ str)} +-- : (Formula.IsNum phi).Realize v +-- <-> +-- phi.Realize (v ∘ Sum.inl) +-- := +-- by +-- unfold Formula.Realize +-- unfold Formula.mkInl +-- rw [realize_relabelEquiv] +-- dsimp only [Equiv.coe_fn_mk] +-- exact Eq.to_iff rfl + + +-- @[delta0_simps] +-- theorem realize_isstr {a : Type} {v : a -> (num ⊕ str)} {t : zambella.Term (a ⊕ Fin 0)} : +-- (IsStr t).Realize v +-- <-> (t.realize (Sum.elim v Fin.elim0)).isRight := ax_realize_isstr + +@[delta0_simps] +theorem _root_.FirstOrder.Term.realize_in {num str : Type u} [ZambellaModel num str] {a : Type} {n} + {t1 t2 : zambella.Term (a ⊕ Fin n)} + {v : a -> (num ⊕ str)} + {xs : Fin n -> (num ⊕ str)} : + (Term.in t1 t2).Realize v xs + <-> (t1.realize (Sum.elim v xs)) ∈ (t2.realize (Sum.elim v xs)) := ax_realize_in + +@[delta0_simps] +theorem realize_in {num str : Type u} [ZambellaModel num str] {a : Type} + {t1 t2 : zambella.Term (a ⊕ Fin 0)} + {v : a -> (num ⊕ str)} : + Formula.Realize (Term.in t1 t2) v + <-> (t1.realize (Sum.elim v default)) ∈ (t2.realize (Sum.elim v default)) + := +by + unfold Formula.Realize + rw [Term.realize_in] + +@[delta0_simps] +theorem realize_notin {num str : Type u} [ZambellaModel num str] {a : Type} + {t1 t2 : zambella.Term (a ⊕ Fin 0)} + {v : a -> (num ⊕ str)} + {xs : Fin 0 -> (num ⊕ str)} : + (Term.notin t1 t2).Realize v xs + <-> (t1.realize (Sum.elim v default)) ∉ (t2.realize (Sum.elim v default)) + := by + unfold Term.notin + conv => + lhs; + unfold Formula.Realize + rw [Formula.boundedFormula_realize_eq_realize] + rw [realize_not] + conv => + rhs + unfold Not + unfold Formula.Realize + rw [Term.realize_in] + +-- @[irreducible] def iBdEx' {α n} (bdTerm : L.Term (α ⊕ Fin 0)) +-- (φ : L.Formula (α ⊕ (Vars1 n))) : L.Formula α := +-- let bd := (var (.inl (Sum.inr (.fv1)))).le $ bdTerm.relabel (Sum.map .inl id) +-- iExs' $ bd ⊓ φ +@[delta0_simps] +theorem realize_iBdEx' {M : Type*} [peano.Structure M] {t : peano.Term (a ⊕ Fin 0)} + (phi : peano.Formula (a ⊕ Vars1 n1)) {v : a -> M} + : (iBdEx' t phi).Realize v + <-> + ∃ x : M, + (x <= (t.realize (Sum.elim v Fin.elim0)) ∧ + phi.Realize (Sum.elim v (fun _ => x))) := +by + unfold iBdEx' + rw [realize_iExs'.Vars1] + conv => + lhs; rhs; intro; + rw [realize_inf] + conv => + lhs; + change BoundedFormula.Realize _ _ _ + rw [Term.realize_le] + simp only [peano.instLEOfStructure, Term.realize_var, Sum.elim_inl, Sum.elim_inr, + Term.realize_relabel] + conv => + rhs; + simp only + conv => + rhs + rhs; intro; + lhs; + unfold Formula.Realize + constructor + · intro h + rcases h with ⟨x, hx⟩ + rcases hx with ⟨hxle, hphi⟩ + have henv : + ((Sum.elim (Sum.elim v (fun _ : Vars1 n1 => x)) (default : Fin 0 → M)) ∘ + (Sum.map (Sum.inl : a → a ⊕ Vars1 n1) (id : Fin 0 → Fin 0))) = + Sum.elim v Fin.elim0 := by + funext y + cases y with + | inl y => simp + | inr y => exact Fin.elim0 y + refine ⟨x, ?_, hphi⟩ + simpa only [peano.instLEOfStructure, Sum.elim_inl, Sum.elim_inr, Term.realize_relabel, + Sum.elim_map, henv] using hxle + · intro h + rcases h with ⟨x, hxle, hphi⟩ + have henv : + ((Sum.elim (Sum.elim v (fun _ : Vars1 n1 => x)) (default : Fin 0 → M)) ∘ + (Sum.map (Sum.inl : a → a ⊕ Vars1 n1) (id : Fin 0 → Fin 0))) = + Sum.elim v Fin.elim0 := by + funext y + cases y with + | inl y => simp + | inr y => exact Fin.elim0 y + refine ⟨x, ⟨?_, hphi⟩⟩ + simpa only [peano.instLEOfStructure, Sum.elim_inl, Sum.elim_inr, Term.realize_relabel, + Sum.elim_map, henv] using hxle + +namespace realize_iBdAll' + +@[delta0_simps] +lemma Vars1 + {num str} + [inst1 : ZambellaModel num str] + (phi : zambella.Formula (a ⊕ Vars1 n1)) + {t : zambella.Term (a ⊕ Fin 0)} + {v : a -> (num ⊕ str)} + : (phi.iBdAll' t).Realize v + <-> + ∀ x : (num ⊕ str), + x <= (t.realize (Sum.elim v default)) + -> phi.Realize + (Sum.elim v (fun fv => match fv with | .fv1 => x)) + := +by + unfold iBdAll' + rw [realize_iAlls'.Vars1] + conv => + lhs; ext; + rw [realize_imp] + unfold Formula.Realize + rw [Term.realize_le] + simp only [Term.realize_var, Sum.elim_inl, Sum.elim_inr, Term.realize_relabel] + conv => + left; right; arg 1 + unfold Function.comp; intro + rw [Sum.elim_map] + simp only [Sum.elim_comp_inl, Function.comp_id] + conv => + rhs; ext + simp only + unfold Formula.Realize + exact Lex.forall + +end realize_iBdAll' + +namespace realize_iBdAllLt' + +@[delta0_simps] +lemma Vars1 {M : Type*} [IsOrdered L] [L.Structure M] [Preorder M] + [h : L.OrderedStructure M] (phi : L.Formula (a ⊕ Vars1 n1)) + {t : L.Term (a ⊕ Fin 0)} + {v : a -> M} + : (phi.iBdAllLt' t).Realize v + <-> + ∀ x : M, x < (t.realize (Sum.elim v default)) -> phi.Realize + (Sum.elim v (fun fv => match fv with | .fv1 => x)) + := +by + unfold iBdAllLt' + rw [realize_iAlls'.Vars1] + conv => + lhs; ext; + rw [realize_imp] + unfold Formula.Realize + rw [Term.realize_lt] + simp only [Term.realize_var, Sum.elim_inl, Sum.elim_inr, Term.realize_relabel] + conv => + left; right; arg 1 + unfold Function.comp; intro + rw [Sum.elim_map] + simp only [Sum.elim_comp_inl, Function.comp_id] + conv => + rhs; ext + simp only + unfold Formula.Realize + exact Lex.forall + +end realize_iBdAllLt' + +namespace realize_iBdAllNum' + +@[delta0_simps] +lemma Vars1 + {num str} + [inst1 : ZambellaModel num str] + (phi : zambella.Formula (a ⊕ Vars1 n1)) + {t : zambella.Term (a ⊕ Fin 0)} + {v : a -> (num ⊕ str)} + : (phi.iBdAllNum' t).Realize v + <-> + ∀ x : (num ⊕ str), + x <= (t.realize (Sum.elim v default)) + -> x.isLeft + -> phi.Realize + (Sum.elim v (fun fv => match fv with | .fv1 => x)) + := +by + unfold iBdAllNum' + rw [realize_iBdAll'.Vars1] + conv => + lhs; ext; rhs; + rw [realize_imp] + conv => + lhs + rw [Term.realize_isnum] + simp only [Term.realize_var, Sum.elim_inl, Sum.elim_inr] + +end realize_iBdAllNum' + +-- @[delta0_simps] +-- lemma realize_iBdAllNumLt'.Vars1 +-- {num str} +-- [inst1 : ZambellaModel num str] +-- (phi : zambella.Formula (a ⊕ Vars1 n1) ) +-- {t : zambella.Term (a ⊕ Fin 0)} +-- {v : a -> (num ⊕ str)} +-- : (phi.iBdAllNumLt' t).Realize v +-- <-> +-- ∀ x : (num ⊕ str), +-- x < (t.realize (Sum.elim v default)) +-- -> x.isLeft +-- -> phi.Realize +-- (Sum.elim v (fun fv => match fv with | .fv1 => x)) +-- := +-- by +-- unfold iBdAllNumLt' +-- rw [realize_iBdAllLt'.Vars1] + +-- conv => +-- lhs; ext; rhs; +-- rw [realize_imp] +-- conv => +-- lhs +-- rw [Term.realize_isnum] +-- simp only [Term.realize_var, Sum.elim_inl, Sum.elim_inr] +end Formula +end FirstOrder.Language diff --git a/LeanPool/FormalizationOfBoundedArithmetic/SimpRules.lean b/LeanPool/FormalizationOfBoundedArithmetic/SimpRules.lean new file mode 100644 index 0000000000..abb0be8de2 --- /dev/null +++ b/LeanPool/FormalizationOfBoundedArithmetic/SimpRules.lean @@ -0,0 +1,16 @@ +/- +Copyright (c) 2026 ruplet. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: ruplet +-/ + +import LeanPool.FormalizationOfBoundedArithmetic.MathlibSimps + +attribute [delta0_simps] + Sum.elim_inl + Sum.elim_inr + Sum.swap_inl + Sum.swap_inr + Function.comp_apply + and_self + not_true_eq_false diff --git a/LeanPool/FormalizationOfBoundedArithmetic/Syntax.lean b/LeanPool/FormalizationOfBoundedArithmetic/Syntax.lean new file mode 100644 index 0000000000..f815b6e389 --- /dev/null +++ b/LeanPool/FormalizationOfBoundedArithmetic/Syntax.lean @@ -0,0 +1,277 @@ +/- +Copyright (c) 2026 ruplet. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: ruplet +-/ + +import Mathlib.ModelTheory.Syntax + +import LeanPool.FormalizationOfBoundedArithmetic.IsEnum + +namespace FirstOrder +namespace Language + +universe u +variable {L : Language} +variable {α β : Type u} {n : Nat} + +namespace BoundedFormula + +/-- Computable finite supremum over an explicitly enumerated type. -/ +def iSup' [enum : IsEnum β] (f : β → L.BoundedFormula α n) : L.BoundedFormula α n := + (enum.toList.map f).foldr (· ⊔ ·) ⊥ + +/-- Computable finite infimum over an explicitly enumerated type. -/ +def iInf' [enum : IsEnum β] (f : β → L.BoundedFormula α n) : L.BoundedFormula α n := + (enum.toList.map f).foldr (· ⊓ ·) ⊤ + +end BoundedFormula + +namespace Formula + +/-- Computable finite universal closure over an explicitly enumerated type. -/ +def iAlls' [enum : IsEnum β] (φ : L.Formula (α ⊕ β)) : L.Formula α := + (BoundedFormula.relabel (fun a => Sum.map id enum.toIdx a) φ).alls + +/-- Computable finite existential closure over an explicitly enumerated type. -/ +def iExs' [enum : IsEnum β] (φ : L.Formula (α ⊕ β)) : L.Formula α := + (BoundedFormula.relabel (fun a => Sum.map id enum.toIdx a) φ).exs + +/-- Computable finite unique-existence formula over an explicitly enumerated type. -/ +def iExsUnique' [enum : IsEnum β] (φ : L.Formula (α ⊕ β)) : L.Formula α := + iExs' <| φ ⊓ iAlls' + ((φ.relabel (fun a => Sum.elim (.inl ∘ .inl) .inr a)).imp <| + .iInf' fun g => Term.equal (var (.inr g)) (var (.inl (.inr g)))) + +/-- Computable finite supremum for formulas over an explicitly enumerated type. -/ +def iSup' [enum : IsEnum α] (f : α → L.Formula β) : L.Formula β := + BoundedFormula.iSup' f + +/-- Computable finite infimum for formulas over an explicitly enumerated type. -/ +def iInf' [enum : IsEnum α] (f : α → L.Formula β) : L.Formula β := + BoundedFormula.iInf' f + +end Formula + + +namespace BoundedFormula + + +namespace relabelEquiv + +@[simp] +theorem falsum {α β} (g : α ≃ β) {k} : + (falsum : L.BoundedFormula α k).relabelEquiv g = falsum := + rfl + +@[simp] +theorem imp {α β} (g : α ≃ β) {k} (φ ψ : L.BoundedFormula α k) : + (φ.imp ψ).relabelEquiv g = (φ.relabelEquiv g).imp (ψ.relabelEquiv g) := + rfl + +@[simp] +theorem not {α β} (g : α ≃ β) {k} (φ : L.BoundedFormula α k) : + φ.not.relabelEquiv g = (φ.relabelEquiv g).not := + rfl + +@[simp] +theorem nf {α β} (g : α ≃ β) {k} (φ ψ : L.BoundedFormula α k) : + (φ ⊓ ψ).relabelEquiv g = (φ.relabelEquiv g) ⊓ (ψ.relabelEquiv g) := + rfl + +@[simp] +theorem sup {α β} (g : α ≃ β) {k} (φ ψ : L.BoundedFormula α k) : + (φ ⊔ ψ).relabelEquiv g = (φ.relabelEquiv g) ⊔ (ψ.relabelEquiv g) := + rfl + +@[simp] +theorem rel {L : Language} {a b} {n} (g : a ≃ b) {k} {R : L.Relations k} + {ts : Fin k -> L.Term (a ⊕ Fin n)} : + ((BoundedFormula.rel R ts).relabelEquiv g : L.BoundedFormula b n) = + (BoundedFormula.rel R (fun i => + (ts i).relabel (Sum.map g id : a ⊕ Fin n -> b ⊕ Fin n)) : + L.BoundedFormula b n) := +by + rfl + +@[simp] +theorem eq {L : Language} {a b} {n} (g : a ≃ b) {t1 t2 : L.Term (a ⊕ Fin n)} + : ((t1 =' t2).relabelEquiv g : L.BoundedFormula b n) + = + ( + (t1.relabel (Sum.map g id : a ⊕ Fin n -> b ⊕ Fin n) + =' t2.relabel (Sum.map g id : a ⊕ Fin n -> b ⊕ Fin n) + ) : L.BoundedFormula b n + ) := +by + rfl + +theorem bdEqual {L : Language} {a b} {n} (g : a ≃ b) {t1 t2 : L.Term (a ⊕ Fin n)} + : ((t1 =' t2).relabelEquiv g) + = + (t1.relabel (Sum.map g id)) =' (t2.relabel (Sum.map g id)) := +by + rfl + +-- TODO: this was very hard to prove. simp sets of Equiv and of mapTermRel are bad. +theorem comp_inv {L : Language} {α β} {m} {φ : L.BoundedFormula α m} (f : α ≃ β) + : (relabelEquiv f.symm ((relabelEquiv f) φ)) = φ := +by + unfold relabelEquiv mapTermRelEquiv + dsimp only [Equiv.coe_refl, Equiv.coe_fn_mk] + rw [mapTermRel_mapTermRel] + unfold Function.comp + unfold Equiv.sumCongr + simp only [Equiv.coe_refl, _root_.Equiv.symm_symm, Equiv.refl_symm, Term.relabelEquiv_apply, + Equiv.coe_fn_mk, Term.relabel_relabel, Sum.map_comp_map, _root_.Equiv.symm_comp_self, + Function.comp_id, Sum.map_id_id, Term.relabel_id_eq_id, id_eq] + apply mapTermRel_id_id_id + +end relabelEquiv + +namespace relabel + +@[simp] +theorem sup {L : Language} {α β} {n} (g : α → β ⊕ (Fin n)) {k} (φ ψ : L.BoundedFormula α k) : + (φ ⊔ ψ).relabel g = (φ.relabel g) ⊔ (ψ.relabel g) := + rfl + +@[simp] +theorem inf {L : Language} {α β} {n} (g : α → β ⊕ (Fin n)) {k} (φ ψ : L.BoundedFormula α k) : + (φ ⊓ ψ).relabel g = (φ.relabel g) ⊓ (ψ.relabel g) := + rfl + +end relabel + +namespace relabelEquiv + +@[simp] +theorem all {α β} (g : α ≃ β) {k} (φ : L.BoundedFormula α (k + 1)) : + φ.all.relabelEquiv g = (φ.relabelEquiv g).all := by + rw [relabelEquiv] + rw [mapTermRelEquiv] + rw [relabelEquiv] + rw [mapTermRelEquiv] + simp only [Equiv.coe_refl, Equiv.refl_symm, Equiv.coe_fn_mk] + conv => lhs; unfold mapTermRel + simp + +@[simp] +theorem ex {α β} (g : α ≃ β) {k} (φ : L.BoundedFormula α (k + 1)) : + φ.ex.relabelEquiv g = (φ.relabelEquiv g).ex := by + simp only [BoundedFormula.ex, BoundedFormula.not] + simp only [relabelEquiv.imp, all, imp.injEq, all.injEq, true_and, Bot.bot] + constructor + · simp only [relabelEquiv.falsum] + · simp only [relabelEquiv.falsum] + + +@[simp] +theorem alls {α β} (g : α ≃ β) {k} (φ : L.BoundedFormula α k) : + φ.alls.relabelEquiv g = (φ.relabelEquiv g).alls := by + induction k with + | zero => + unfold BoundedFormula.alls + simp only + | succ m ih => + apply ih + + +@[simp] +theorem exs {α β} (g : α ≃ β) {k} (φ : L.BoundedFormula α k) : + φ.exs.relabelEquiv g = (φ.relabelEquiv g).exs := by + induction k with + | zero => + unfold BoundedFormula.exs + simp only + | succ m ih => + apply ih + +theorem relabelAux_sumCongr [enum : IsEnum β] (g : α ≃ γ) (k : ℕ) : + ∀ x : (α ⊕ β) ⊕ Fin k, + (g.sumCongr (_root_.Equiv.refl (Fin (enum.size + k)))) + (BoundedFormula.relabelAux (fun a : α ⊕ β => Sum.map id enum.toIdx a) k x) + = BoundedFormula.relabelAux (fun a : γ ⊕ β => Sum.map id enum.toIdx a) k + (((g.sumCongr (_root_.Equiv.refl β)).sumCongr (_root_.Equiv.refl (Fin k))) x) := by + intro x + cases x with + | inl ab => + cases ab with + | inl a => + simp [BoundedFormula.relabelAux, Equiv.sumCongr, Equiv.sumAssoc] + | inr b => + simp [BoundedFormula.relabelAux, Equiv.sumCongr, Equiv.sumAssoc] + | inr i => + simp [BoundedFormula.relabelAux, Equiv.sumCongr, Equiv.sumAssoc] + +theorem relabel_relabelSum [enum : IsEnum β] (g : α ≃ γ) : + ∀ {k} (φ : L.BoundedFormula (α ⊕ β) k), + BoundedFormula.relabelEquiv g + (BoundedFormula.relabel (fun a : α ⊕ β => Sum.map id enum.toIdx a) φ) + = BoundedFormula.relabel (fun a : γ ⊕ β => Sum.map id enum.toIdx a) + (BoundedFormula.relabelEquiv (Equiv.sumCongr g (_root_.Equiv.refl β)) φ) := by + intro k φ + induction φ with + | falsum => rfl + | equal t1 t2 => + dsimp [BoundedFormula.relabelEquiv, BoundedFormula.mapTermRelEquiv, + BoundedFormula.relabel, BoundedFormula.mapTermRel, Term.relabelEquiv_apply, + Term.relabel_relabel] + simp only [Term.relabel_relabel] + congr 1 + · congr 1 + funext x + exact relabelAux_sumCongr g _ x + · congr 1 + funext x + exact relabelAux_sumCongr g _ x + | rel R ts => + dsimp [BoundedFormula.relabelEquiv, BoundedFormula.mapTermRelEquiv, + BoundedFormula.relabel, BoundedFormula.mapTermRel, Term.relabelEquiv_apply, + Term.relabel_relabel] + simp only [Term.relabel_relabel] + congr 1 + funext i + congr 1 + funext x + exact relabelAux_sumCongr g _ x + | imp φ ψ ihφ ihψ => + simp only [relabel_imp, imp, imp.injEq] + exact ⟨ihφ, ihψ⟩ + | all φ ih => + simp only [relabel_all, Nat.add_eq, all, all.injEq] + exact ih + +@[simp] +theorem iExs' {α β γ} [henum : IsEnum β] (g : α ≃ γ) + (φ : L.Formula (α ⊕ β)) : + BoundedFormula.relabelEquiv g (φ.iExs') + = Formula.iExs' (φ.relabelEquiv (Equiv.sumCongr g (_root_.Equiv.refl β))) := +by + unfold Formula.iExs' + rw [exs] + congr + exact relabel_relabelSum g φ + +@[simp] +theorem iAlls' {α β γ} [henum : IsEnum β] (g : α ≃ γ) + (φ : L.Formula (α ⊕ β)) : + BoundedFormula.relabelEquiv g (φ.iAlls') + = Formula.iAlls' (φ.relabelEquiv (Equiv.sumCongr g (_root_.Equiv.refl β))) := +by + unfold Formula.iAlls' + rw [alls] + congr + exact relabel_relabelSum g φ + +@[simp] +theorem inf {L : Language} {α β} (g : α ≃ β) {k} (φ ψ : L.BoundedFormula α k) : + (φ ⊓ ψ).relabelEquiv g = (φ.relabelEquiv g) ⊓ (ψ.relabelEquiv g) := + rfl + + +end relabelEquiv + +end BoundedFormula +end Language +end FirstOrder diff --git a/LeanPool/FormalizationOfBoundedArithmetic/V0.lean b/LeanPool/FormalizationOfBoundedArithmetic/V0.lean new file mode 100644 index 0000000000..6566947b8c --- /dev/null +++ b/LeanPool/FormalizationOfBoundedArithmetic/V0.lean @@ -0,0 +1,816 @@ +/- +Copyright (c) 2026 ruplet. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: ruplet +-/ + +-- Note: there are 3 approaches to formalize two-sorted first-order logic: +-- a) add symbols isStr(x), isNum(x) to vocabulary and encode +-- two-sorted logic as first-order logic. This bypasses Lean automation +-- and will be cumbersome to work with in the long run +-- b) This is what we'd use here: +-- use the fact that some of interesting theories (such as V^i family) +-- are finitely axiomatizable - so we don't have to formalize the two-sorted +-- comprehension axiom scheme; we can write meta tactic to prove a given +-- comprehension instance from the 12 canonical comprehension instances +-- that we define below (slightly ugly) +-- c) extend Mathlib.ModelTheory to work with many-sorted languages +-- long term, this will be necessary. For now, this is probably weeks +-- of work which we can skip until making sure that we'll get to any +-- interesting result at all + +import Lean + +import Mathlib.ModelTheory.Basic +import Mathlib.ModelTheory.Syntax +import Mathlib.ModelTheory.Complexity +import Mathlib.Tactic.SimpRw + +import LeanPool.FormalizationOfBoundedArithmetic.BasicSingleSorted +import LeanPool.FormalizationOfBoundedArithmetic.IOPEN +import LeanPool.FormalizationOfBoundedArithmetic.IDelta0 +import LeanPool.FormalizationOfBoundedArithmetic.DisplayedVariables +import LeanPool.FormalizationOfBoundedArithmetic.Complexity +import LeanPool.FormalizationOfBoundedArithmetic.Algebra +import LeanPool.FormalizationOfBoundedArithmetic.AxiomSchemes +import LeanPool.FormalizationOfBoundedArithmetic.Register + + +open FirstOrder Language +open HasTypes_is +open HasEmptySet +open HasLen + + +-- page 129, CN10: Finite axiomatizability of V0 +/-- Two-sorted models of the bounded-arithmetic theory `V0`. -/ +class V0Model + (num : Type) (str : outParam Type) + extends + HasLen str num, + Membership num str, + BASICModel num +where + -- axiom for empty string; 4.4.1 Two-Sorted Free Variable Normal Form + -- E : len (empty : str) = (0 : num) + -- B1 : ∀ x : num, x + 1 ≠ 0 + -- B2 : ∀ x y : num, x + 1 = y + 1 -> x = y + -- B3 : ∀ x : num, x + 0 = x + -- B4 : ∀ x y : num, x + (y + 1) = (x + y) + 1 + -- B5 : ∀ x : num, x * 0 = 0 + -- B6 : ∀x y : num, x * (y + 1) = (x * y) + x + -- B7 : ∀x y : num, x <= y -> y <= x -> x = y + -- B8 : ∀x y : num, x <= x + y + B9 : ∀ x : num, 0 <= x + B10: ∀ x y : num, x <= y ∨ y <= x + B11: ∀ x y : num, x <= y <-> x < (y + 1) + B12: ∀ {x : num}, x ≠ 0 -> (∃ y : num, (y <= x ∧ (y + 1) = x)) + L1 : ∀ {X : str}, ∀ {y : num}, y ∈ X -> (y < (len X)) + L2 : ∀ {X : str}, ∀ {y : num}, (y + 1) = len X -> y ∈ X + + SE : ∀ {X Y: str}, + len X = (len Y : num) + -> (∀ y : num, ((y < len X) -> (y ∈ X <-> y ∈ Y))) + -> X = Y + + comp1 : ∀ b1 b2 : num, ∃ Y : str, (len Y ≤ ⟨b1, b2⟩ ∧ (∀ x1 < b1, ∀ x2 < b2, + ⟨x1, x2⟩ ∈ Y ↔ (x1 = x2) + )) + + -- φ2(x1,x2,x3) ≡ x3 = x1 + comp2 : ∀ b1 b2 b3 : num, ∃ Y : str, len Y ≤ ⟨b1, b2, b3⟩ ∧ + ∀ x1 < b1, ∀ x2 < b2, ∀ x3 < b3, + ⟨x1, x2, x3⟩ ∈ Y ↔ (x3 = x1) + + -- φ3(x1,x2,x3) ≡ x3 = x2 + comp3 : ∀ b1 b2 b3 : num, ∃ Y : str, len Y ≤ ⟨b1, b2, b3⟩ ∧ + ∀ x1 < b1, ∀ x2 < b2, ∀ x3 < b3, + ⟨x1, x2, x3⟩ ∈ Y ↔ (x3 = x2) + + -- φ4[Q1,Q2](x1,x2) ≡ ∃y ≤ x1 (Q1(x1,y) ∧ Q2(y,x2)) + comp4 : ∀ Q1 Q2 : str, ∀ b1 b2 : num, ∃ Y : str, len Y ≤ ⟨b1, b2⟩ ∧ + ∀ x1 < b1, ∀ x2 < b2, + ⟨x1, x2⟩ ∈ Y ↔ (∃ y : num, y ≤ x1 ∧ (⟨x1, y⟩ ∈ Q1 ∧ ⟨y, x2⟩ ∈ Q2)) + + -- φ5[a](x,y) ≡ y = a + comp5 : ∀ a : num, ∀ b1 b2 : num, ∃ Y : str, len Y ≤ ⟨b1, b2⟩ ∧ + ∀ x < b1, ∀ y < b2, + ⟨x, y⟩ ∈ Y ↔ (y = a) + + -- φ6[Q1,Q2](x,y) ≡ ∃z1 ≤ y ∃z2 ≤ y (Q1(x,z1) ∧ Q2(x,z2) ∧ y = z1 + z2) + comp6 : ∀ Q1 Q2 : str, ∀ b1 b2 : num, ∃ Y : str, len Y ≤ ⟨b1, b2⟩ ∧ + ∀ x < b1, ∀ y < b2, + ⟨x, y⟩ ∈ Y ↔ + (∃ z1 : num, z1 ≤ y ∧ + ∃ z2 : num, z2 ≤ y ∧ + (⟨x, z1⟩ ∈ Q1 ∧ ⟨x, z2⟩ ∈ Q2 ∧ y = z1 + z2)) + + -- φ7[Q1,Q2](x,y) ≡ ∃z1 ≤ y ∃z2 ≤ y (Q1(x,z1) ∧ Q2(x,z2) ∧ y = z1 · z2) + comp7 : ∀ Q1 Q2 : str, ∀ b1 b2 : num, ∃ Y : str, len Y ≤ ⟨b1, b2⟩ ∧ + ∀ x < b1, ∀ y < b2, + ⟨x, y⟩ ∈ Y ↔ + (∃ z1 : num, z1 ≤ y ∧ + ∃ z2 : num, z2 ≤ y ∧ + (⟨x, z1⟩ ∈ Q1 ∧ ⟨x, z2⟩ ∈ Q2 ∧ y = z1 * z2)) + + -- φ8[Q1,Q2,c](x) ≡ ∃y1 ≤ c ∃y2 ≤ c (Q1(x,y1) ∧ Q2(x,y2) ∧ y1 ≤ y2) + comp8 : ∀ Q1 Q2 : str, ∀ c b : num, ∃ Y : str, len Y ≤ b ∧ + ∀ x < b, + x ∈ Y ↔ + (∃ y1 : num, y1 ≤ c ∧ + ∃ y2 : num, y2 ≤ c ∧ + (⟨x, y1⟩ ∈ Q1 ∧ ⟨x, y2⟩ ∈ Q2 ∧ y1 ≤ y2)) + + -- φ9[X,Q,c](x) ≡ ∃y ≤ c (Q(x,y) ∧ X(y)) + comp9 : ∀ X Q : str, ∀ c b : num, ∃ Y : str, len Y ≤ b ∧ + ∀ x < b, + x ∈ Y ↔ (∃ y : num, y ≤ c ∧ (⟨x, y⟩ ∈ Q ∧ y ∈ X)) + + -- φ10[Q](x) ≡ ¬Q(x) + comp10 : ∀ Q : str, ∀ b : num, ∃ Y : str, len Y ≤ b ∧ + ∀ x < b, + x ∈ Y ↔ ¬ (x ∈ Q) + + -- φ11[Q1,Q2](x) ≡ Q1(x) ∧ Q2(x) + comp11 : ∀ Q1 Q2 : str, ∀ b : num, ∃ Y : str, len Y ≤ b ∧ + ∀ x < b, + x ∈ Y ↔ (x ∈ Q1 ∧ x ∈ Q2) + + -- φ12[Q,c](x) ≡ ∀y ≤ c Q(x,y) + comp12 : ∀ Q : str, ∀ c b : num, ∃ Y : str, len Y ≤ b ∧ + ∀ x < b, + x ∈ Y ↔ (∀ y : num, y ≤ c → ⟨x, y⟩ ∈ Q) + + xmin_comp_ax : ∀ X : str, ∃ Y : str, + len Y ≤ len X ∧ ∀ z < len X, z ∈ Y ↔ ∀ y ≤ z, y ∉ X + + comp_xind_ax : ∀ X : str, ∀ z : num, ∃ Y : str, + len Y ≤ z + 1 ∧ ∀ y < z + 1, y ∈ Y ↔ y ∉ X + + prop_induction_ax : ∀ P : num → Prop, + P 0 → (∀ i : num, P i → P (i + 1)) → ∀ i : num, P i + + open_induction_ax {n} {a : Type} [IsEnum a] + (phi : peano.BoundedFormula ((Vars1 n) ⊕ a) 0) : + phi.IsOpen -> (mkInductionSentence phi).Realize num + + delta0_induction_ax {n} {a : Type} [IsEnum a] + (phi : peano.BoundedFormula ((Vars1 n) ⊕ a) 0) : + phi.IsDelta0 -> (mkInductionSentence phi).Realize num + + -- le_refl : ∀ x : num, x <= x + le_trans : ∀ x y z : num, x <= y -> y <= z -> x <= z + zero_add : ∀ x : num, 0 + x = x + add_left_cancel : ∀ x : num, IsAddLeftRegular x + add_right_cancel : ∀ x : num, IsAddRightRegular x + add_assoc : ∀ x y z : num, (x + y) + z = x + (y + z) + le_total : ∀ (a b : num), a ≤ b ∨ b ≤ a + /-- Decidability of the order relation on numbers. -/ + toDecidableLE : DecidableLE num + exists_add_of_le : ∀ {a b : num}, a ≤ b → ∃ c, b = a + c + add_le_add_left : ∀ (a b : num), a ≤ b → ∀ (c : num), c + a ≤ c + b + le_antisymm : ∀ (a b : num), a ≤ b → b ≤ a → a = b + add_comm : ∀ (a b : num), a + b = b + a + +namespace V0Model + + +variable {num str} [M : V0Model num str] +open V0Model BASICModel + + +instance : PartialOrder num where + le_refl := BASICModel.le_refl + le_trans := V0Model.le_trans + le_antisymm := by apply B7 + +instance : AddZeroClass num where + zero_add := zero_add + add_zero := by apply B3 + +instance : IsLeftCancelAdd num where + add_left_cancel := add_left_cancel + +instance : IsRightCancelAdd num where + add_right_cancel := add_right_cancel + +instance : AddMonoid num where + add_assoc := add_assoc + nsmul := nsmulRec + +instance : LinearOrder num where + le_total := le_total + toDecidableLE := toDecidableLE + +instance : CanonicallyOrderedAdd num where + exists_add_of_le := exists_add_of_le + le_self_add := by apply B8 + le_add_self := by + intro a b + rw [add_comm] + apply B8 + +instance : AddCommMonoid num where + add_comm := add_comm + +instance : PartialOrder num where + le_antisymm := le_antisymm + +instance : IsOrderedAddMonoid num where + add_le_add_left := by + intro a b h c + rw [add_comm a c, add_comm b c] + exact V0Model.add_le_add_left a b h c + + +theorem xmin_comp (X : str) : + ∃ Y : str, (len Y : num) ≤ len X ∧ ∀ z < len X, z ∈ Y ↔ ∀ y ≤ z, y ∉ X := +by + exact M.xmin_comp_ax X + +lemma ex_elt_of_len_pos : + ∀ {X : str}, (0 : num) < (len X) -> ∃ x, x ∈ X ∧ x + 1 = len X := by + intro X h_len + obtain ⟨len_pred, h_le, h_eq⟩ := B12 (by + exact Ne.symm (ne_of_lt h_len) + ) + exists len_pred + constructor + · apply L2 + exact h_eq + · exact h_eq + +lemma lt_succ : ∀ (x : num), x < x + 1 := by + intro x + rw [lt_iff_le_and_ne] + constructor + · apply B8 + · intro h + conv at h => lhs; rw [<- add_zero x] + rw [add_left_cancel_iff] at h + apply @M.B1 0 + calc + (0 : num) + 1 = 0 + 0 := congrArg (fun y => (0 : num) + y) h.symm + _ = 0 := B3 0 + +lemma len_not_in : ∀ {X : str}, len X ∉ X := by + intro X h + apply (L1 h).right + rfl + +-- Exercise V.1.1 +lemma not_lt_zero + : ∀ {x : num}, ¬ x < 0 := +by + intro x + rw [not_lt_iff_eq_or_lt] + exact eq_zero_or_pos x + +instance : CanonicallyOrderedAdd num where + le_self_add := by + intro a b + conv => lhs; rw [<- M.B3 a] + apply add_le_add + · apply _root_.le_refl + · apply M.B9 + le_add_self := by + intro a b + rw [add_comm] + apply B8 + +theorem xmin : + ∀ {X : str}, (0 : num) < len X -> ∃ x < len X, x ∈ X ∧ ∀ y < x, y ∉ X := +by + intro X h_lenX + obtain ⟨Y, h_Y⟩ := xmin_comp X (num := num) + exists (len Y) + by_cases h : (0 : num) < len Y + · obtain ⟨y, hy_in, hy_eq⟩ := ex_elt_of_len_pos h + constructor + · -- len Y < len X + cases le_iff_eq_or_lt.mp h_Y.left with + | inl h_lenY_eq_lenX => + exfalso + have h_X_empty : ∀ x < len X, x ∉ X := by + have aux := h_Y.right y + rw [<- h_lenY_eq_lenX] at aux + specialize aux (L1 hy_in) + intro x h_x_lt + apply aux.mp hy_in + rw [B11, hy_eq] + rw [h_lenY_eq_lenX] + exact h_x_lt + have h_X_empty' : ¬∃ x < len X, x ∈ X := by + refine not_exists_of_forall_not ?_ + intro x hx + apply h_X_empty x hx.left hx.right + apply h_X_empty' + obtain ⟨wit, h_wit⟩ := ex_elt_of_len_pos (X := X) (by + rw [h_lenY_eq_lenX] at h + exact h + ) + exists wit + constructor + · apply L1 h_wit.left + · exact h_wit.left + | inr h_lenY_lt_lenX => + assumption + · constructor + · -- len Y ∈ X + rw [le_iff_eq_or_lt] at h_Y + cases h_Y.left with + | inl h => + exfalso + rw [<- h] at h_lenX + conv at h_Y => right; rw [<- h] + have aux := (h_Y.right y (M.L1 hy_in)).mp hy_in y (_root_.le_refl _) + apply aux + apply L2 + rw [<- h] + exact hy_eq + | inr h => + have aux := (not_congr <| h_Y.right (len Y) h).mp len_not_in + simp only [not_forall, not_not] at aux + obtain ⟨x, h_x_le, h_x_X⟩ := aux + rw [le_iff_eq_or_lt] at h_x_le + cases h_x_le with + | inl h => + rw [<- h] + exact h_x_X + | inr h => + -- first, obtain hypothesis for last y of Y + have len_Y_ne_zero : (len Y : num) ≠ 0 := by + intro h' + rw [h'] at h + apply not_lt_zero h + have len_Y_pos : 0 < (len Y : num) := by + cases (eq_zero_or_pos (len Y : num)) with + | inl h => + exfalso + apply len_Y_ne_zero + exact h + | inr h => + exact h + obtain ⟨y, hy_in, hy_eq⟩ := ex_elt_of_len_pos len_Y_pos + clear len_Y_ne_zero len_Y_pos h_lenX + rename_i h_lenY_lt_lenX + have h_y_lt_lenX : y < (len X) := by + apply lt_trans _ h_lenY_lt_lenX + apply L1 hy_in + -- then show that if last of Y holds, but (len Y) does not, + -- then some bit had to be set in X + false_or_by_contra + · rename_i h_lenY_notin_X + have h := (h_Y.right (len Y) h_lenY_lt_lenX).mpr + apply @len_not_in num _ _ Y + apply h + intro y2 h_y2 + rw [le_iff_eq_or_lt] at h_y2 + cases h_y2 with + | inl h_y2 => + rw [h_y2] + apply (h_Y.right (len Y) h_lenY_lt_lenX).mp + · apply h + intro y3 hy3 + rw [le_iff_eq_or_lt] at hy3 + cases hy3 with + | inl hy3 => + rw [hy3] + exact h_lenY_notin_X + | inr hy3 => + apply (h_Y.right y h_y_lt_lenX).mp hy_in + rw [B11, hy_eq] + exact hy3 + · rfl + | inr h_y2 => + clear h + apply (h_Y.right y h_y_lt_lenX).mp hy_in + rw [B11, hy_eq] + exact h_y2 + · -- ∀ z < len Y, z ∉ X + intro z h_z h_zX + -- notice: Y is of the form 11111..1 - if we get any 0 in Y, + -- it means that a bit in X was set. so, we won't get any further + -- bits set in Y! + have h_y_lt_lenX : y < len X := by + apply lt_of_lt_of_le (L1 hy_in) h_Y.left + have h_X := (h_Y.right y h_y_lt_lenX).mp hy_in z + apply h_X + · rw [B11, hy_eq] + exact h_z + · exact h_zX + · have Y_empty : len Y = (0 : num) := by + have h1 := B9 (num := num) (len Y) + rw [le_iff_eq_or_lt] at h1 + cases h1 with + | inl h1 => exact h1.symm + | inr h1 => exfalso; apply h; exact h1 + constructor + · rw [Y_empty] + exact h_lenX + · constructor + · -- len Y ∈ X + false_or_by_contra + rename_i h_contr + have zero_in_Y : (0 : num) ∈ Y := by + apply (h_Y.right 0 h_lenX).mpr + intro y hy + have y_zero := B7 hy (M.B9 _) + rw [y_zero, <- Y_empty] + exact h_contr + rw [<- Y_empty] at zero_in_Y + exact len_not_in zero_in_Y + · -- ∀ y < len Y, y ∉ X + intro y hy + exfalso + rw [Y_empty] at hy + exact not_lt_zero hy + + +lemma comp_xind : + ∀ X : str, ∀ z : num, ∃ Y : str, len Y <= z + 1 ∧ + ∀ y < z + 1, (y ∈ Y ↔ y ∉ X) := by + intro X z + exact M.comp_xind_ax X z + +lemma len_ne_zero_of_in : ∀ {x : num}, ∀ {X : str}, + x ∈ X -> len X ≠ (0 : num) := +by + intro x X h + have h2 := L1 h + apply ne_of_gt + apply lt_of_le_of_lt _ h2 + exact B9 x + +theorem xind : + ∀ {X : str}, ∀ {z : num}, + 0 ∈ X + -> (∀ y < z, y ∈ X -> y + 1 ∈ X) + -> z ∈ X := +by + intro X z h_base h_y + false_or_by_contra + rename_i h_z + obtain ⟨Y, h_Y_le, h_Y⟩ := comp_xind X z + have h_z_in_Y : z ∈ Y := by + rw [h_Y] + · exact h_z + · exact lt_succ z + have h_Y_pos : (0 : num) < len Y := by + rw [lt_iff_le_and_ne] + constructor + · apply B9 + · exact Ne.symm (len_ne_zero_of_in h_z_in_Y) + obtain ⟨y0, h_y0⟩ := xmin h_Y_pos + have h_y0_ne_zero : y0 ≠ 0 := by + have h_0_notin_Y : 0 ∉ Y := by + rw [h_Y] + · rw [@not_not] + exact h_base + · constructor + · apply B9 + · rw [le_iff_eq_or_lt] + intro contr + cases contr with + | inl contr => + apply M.B1 contr + | inr contr => + apply M.not_lt_zero contr + intro contr + apply h_0_notin_Y + rw [<-contr] + exact h_y0.2.1 + obtain ⟨x0, h_x0⟩ := B12 h_y0_ne_zero + have h_x0_in : x0 ∈ X := by + apply not_not.mp + rw [<- h_Y] + · apply h_y0.2.2 + rw [<- h_x0.2] + exact lt_succ x0 + · apply lt_of_lt_of_le _ h_Y_le + apply lt_trans _ h_y0.1 + rw [<- h_x0.2] + exact lt_succ x0 + have h_succ_x0_notin : x0 + 1 ∉ X := by + rw [h_x0.2] + rw [<- h_Y] + · exact h_y0.2.1 + · apply lt_of_lt_of_le _ h_Y_le + exact h_y0.1 + apply h_succ_x0_notin + apply h_y + · have aux : y0 < z + 1 := by + apply lt_of_lt_of_le _ h_Y_le + apply L1 + exact h_y0.2.1 + rw [<- B11] at aux + apply lt_of_lt_of_le _ aux + rw [<- h_x0.2] + apply lt_succ + · exact h_x0_in + + +theorem ind_of_comp (P : num -> Prop) : + (∀ y : num, ∃ Y : str, (len Y : num) ≤ y ∧ ∀ z < y, z ∈ Y ↔ P z) + -> (P 0 -> (∀ x, P x -> P (x + 1)) -> ∀ x, P x) := +by + intro hcomp pbase pstep z + obtain ⟨X, hX⟩ := hcomp (z + 1) + have hX0 : 0 ∈ X := by + rw [hX.2] + · exact pbase + · rw [<- B11] + exact B9 z + have hXstep : ∀ y < z, y ∈ X -> y + 1 ∈ X := by + intro y hyz hyX + rw [hX.2] + · apply pstep + rw [<- hX.2] + · exact hyX + · rw [<- B11] + exact hyz.1 + · exact (add_lt_add_iff_right 1).mpr hyz + have hzX : z ∈ X := by + apply xind + · exact hX0 + · exact hXstep + rw [<- hX.2] + · exact hzX + · exact lt_succ z + + +instance : IDelta0Model num where + open_induction phi h_open := M.open_induction_ax phi h_open + delta0_induction phi h_delta0 := M.delta0_induction_ax phi h_delta0 + +end V0Model + +-- Corollary V.1.8 +-- T, extending V0, if proves Comp for set of formulas Phi, +-- then also proves Ind, Min and Max for Phi. +-- theorem ind_of_comp : ∀ x : num, comp x -> + +-- variable {num} {str : outParam Type} [V0Model num str] + + +/-- Types equipped with a successor operation. -/ +class HasSucc (α : Type*) where + /-- Successor operation. -/ + succ : α -> α + +/-- Carry predicate for binary string addition below position `i`. -/ +def Carry {num str} [V0Model num str] (i : num) (X Y : str) := + ∃ k < i, (k ∈ X ∧ k ∈ Y ∧ ∀ j < i, (k < j → (j ∈ X ∨ j ∈ Y))) + +/-- Extension of `V0` with string successor and string addition. -/ +class V0ExtModel + (num : Type) (str : outParam Type) + extends + Zero str, HasSucc str, Add str, + V0Model (num := num) (str := str) +where + ax_empty : ∀ {z : num}, z ∈ (0 : str) ↔ z < 0 + ax_succ : ∀ {X : str}, ∀ {i : num}, i ∈ HasSucc.succ X ↔ + (i ≤ len X + ∧ ((i ∈ X ∧ ∃ j < i, j ∉ X) + ∨ (i ∉ X ∧ ∀ j < i, j ∈ X) + ) + ) + + ax_add : ∀ {X Y : str}, ∀ {i : num}, i ∈ X + Y ↔ + (i < len X + len Y ∧ (Xor' (Xor' (i ∈ X) (i ∈ Y)) (Carry i X Y))) + + + +-- Exercise V.4.19 + +-- namespace V0ExtModel +variable {num str : Type} [M : V0ExtModel num str] + +open V0ExtModel V0Model BASICModel + + +lemma len_empty : len (0 : str) = (0 : num) := by + false_or_by_contra + rename_i h + obtain ⟨pred, pred_le, pred_eq⟩ := B12 (num := num) h + have witness := L2 pred_eq + have aux := @ax_empty _ _ M pred + apply @not_lt_zero _ _ _ pred + apply aux.mp + exact witness + +/-- Majority predicate on three propositions. -/ +def Maj (P Q R : Prop) := + (P ∧ Q ∧ ¬ R) ∨ (P ∧ ¬ Q ∧ R) ∨ (¬ P ∧ Q ∧ R) ∨ (P ∧ Q ∧ R) + +lemma Maj_true2 {P Q R : Prop} : Q -> (Maj P Q R <-> P ∨ R) := by + intro h + unfold Maj + tauto +lemma Maj_true3 {P Q R : Prop} : R -> (Maj P Q R <-> P ∨ Q) := by + intro h + unfold Maj + tauto + + + +open IDelta0Model + +lemma carry_rec1 : ∀ {X Y : str}, ∀ {i : num}, + Carry i X Y -> (i ∈ X ∨ i ∈ Y) -> Carry (i + 1) X Y := +by + intro X Y i h ixy + obtain ⟨c, c_lt, cx, cy, cprev⟩ := h + exists c + refine ⟨?_, cx, cy, ?_⟩ + · rw [<- B11] + exact c_lt.1 + intro j + by_cases j = i + · rename_i hji + intro _ hcj + rw [hji] + cases ixy with + | inl ix => left; exact ix + | inr iy => right; exact iy + · rename_i hji + intro hlt hcj + exact cprev j (lt_of_le_of_ne (by rw [B11]; exact hlt) hji) hcj + +lemma not_lt_self : ∀ (i : num), ¬ i < i := by + intro i h + rw [<- lt_self_iff_false i] + exact h + +lemma carry_rec2 : ∀ {X Y : str}, ∀ {i : num}, + i ∈ X ∧ i ∈ Y -> Carry (i + 1) X Y := +by + intro X Y i h_XY + obtain ⟨h_X, h_Y⟩ := h_XY + unfold Carry + exists i + refine ⟨lt_succ i, h_X, h_Y, ?_⟩ + intro j hj hi + rw [<- B11] at hj + exfalso + apply not_lt_self i + exact lt_of_lt_of_le hi hj + +-- Exercise V.4.18 +lemma carry_rec : ∀ {X Y : str}, ∀ {i : num}, + (¬ Carry (0 : num) X Y) ∧ (Carry (i + 1) X Y ↔ Maj (Carry i X Y) (i ∈ X) (i ∈ Y)) := by + intro X Y i + constructor + · intro h + obtain ⟨_, lt, _⟩ := h + exact V0Model.not_lt_zero lt + · constructor + · intro h + obtain ⟨pos, lt, inX, inY, prevs⟩ := h + by_cases h_pos : i = pos + · rw [h_pos] + unfold Maj + right; right + rw [<- or_and_right] + constructor + · exact em' (Carry pos X Y) + · constructor <;> assumption + · rw [<- B11] at lt + have hlt : pos < i := lt_of_le_of_ne lt (Ne.symm h_pos) + clear h_pos lt + have h_pos := prevs i (by rw [<- B11]) hlt + rcases h_pos with h_iX | h_iY + · rw [Maj_true2 h_iX] + left + unfold Carry + exists pos + refine ⟨hlt, inX, inY, ?_⟩ + intro j hj + apply prevs + apply lt_trans hj + exact lt_succ i + · rw [Maj_true3 h_iY] + left + unfold Carry + exists pos + refine ⟨hlt, inX, inY, ?_⟩ + intro j hj + apply prevs + apply lt_trans hj + exact lt_succ i + · intro h + rcases h with ⟨hC, hX, _⟩ | ⟨hC, _, hY⟩ | h_notCarry | h_all + · apply carry_rec1 hC (.inl hX) + · apply carry_rec1 hC (.inr hY) + · apply carry_rec2 h_notCarry.2 + · apply carry_rec2 h_all.2 + +lemma exists_of_len_lt : + ∀ {X Y : str}, (len X : num) < len Y -> + ∃ z, z ∈ Y ∧ z ∉ X ∧ z + 1 = len Y := by + intro X Y h_lt + have h_len_ne_zero : len Y ≠ (0 : num) := by + intro h_len_zero + rw [h_len_zero] at h_lt + exact V0Model.not_lt_zero h_lt + obtain ⟨len_pred, pred_le, pred_eq⟩ := B12 (num := num) h_len_ne_zero + have pred_in := L2 pred_eq + rw [lt_iff_le_not_ge] at h_lt + exists len_pred + refine ⟨pred_in, ?_, pred_eq⟩ + intro h_in_X + apply h_lt.2 + rw [B11] + rw [<- pred_eq] + rw [add_lt_add_iff_right] + apply L1 + exact h_in_X + +lemma exists_of_len_lt' : + ∀ {X : str}, ∀ {i : num}, i < len X -> + ∃ z, z ∈ X ∧ i ≤ z ∧ z + 1 = len X := by + intro X i h_lt + have h_len_ne_zero : len X ≠ (0 : num) := by + intro h_len_zero + rw [h_len_zero] at h_lt + exact V0Model.not_lt_zero h_lt + obtain ⟨len_pred, pred_le, pred_eq⟩ := B12 (num := num) h_len_ne_zero + have pred_in := L2 pred_eq + rw [lt_iff_le_not_ge] at h_lt + exists len_pred + refine ⟨pred_in, ?_, pred_eq⟩ + rw [B11] + rw [pred_eq] + constructor + · exact h_lt.1 + · intro h + apply h_lt.2 + exact h + +lemma len_pos_of_exists : ∀ {i : num} {X : str}, i ∈ X -> len X > (0 : num) := by + intro i X iX + exact lt_of_le_of_lt (zero_le i) (L1 iX) + + + + +lemma xor3_split {P Q R : Prop} : + Xor' (Xor' P Q) R <-> + (P ∧ ¬Q ∧ ¬R) ∨ (¬ P ∧ Q ∧ ¬ R) ∨ (¬ P ∧ ¬ Q ∧ R) ∨ (P ∧ Q ∧ R) := by + unfold Xor' + tauto + + + + + + +lemma carry_lt_add_len : + ∀ {X Y : str} {i : num}, + Carry i X Y -> + i < len X + len Y := by + intro X Y i h_Carry + obtain ⟨k, h_k_lt_i, h_kX, h_kY, h_kprop⟩ := h_Carry + have h_i_ne_zero : i ≠ 0 := by + intro h_i_zero + rw [h_i_zero] at h_k_lt_i + exact V0Model.not_lt_zero h_k_lt_i + obtain ⟨pred_i, hpred_i_le, hpred_i_eq⟩ := B12 h_i_ne_zero + have h_len_X_pos : (0 : num) < len X := len_pos_of_exists h_kX + have h_len_Y_pos : (0 : num) < len Y := len_pos_of_exists h_kY + have h_pred_or : pred_i ∈ X ∨ pred_i ∈ Y := by + by_cases h_k_eq_pred : k = pred_i + · subst h_k_eq_pred + exact Or.inl h_kX + · have h_pred_lt_i : pred_i < i := by + simpa [hpred_i_eq] using (lt_succ pred_i) + have h_k_le_pred : k ≤ pred_i := by + rw [B11, hpred_i_eq] + exact h_k_lt_i + have h_k_lt_pred : k < pred_i := lt_of_le_of_ne h_k_le_pred h_k_eq_pred + exact h_kprop pred_i h_pred_lt_i h_k_lt_pred + rcases h_pred_or with h_predX | h_predY + · have h_i_le_lenX : i ≤ len X := by + rw [<- hpred_i_eq, B11] + exact (add_lt_add_iff_right 1).mpr (L1 h_predX) + exact lt_of_le_of_lt h_i_le_lenX (lt_add_of_pos_right (len X) h_len_Y_pos) + · have h_i_le_lenY : i ≤ len Y := by + rw [<- hpred_i_eq, B11] + exact (add_lt_add_iff_right 1).mpr (L1 h_predY) + exact lt_of_le_of_lt h_i_le_lenY (by + simpa [_root_.add_comm] using (lt_add_of_pos_right (len Y) h_len_X_pos)) + + +lemma str_eq_of_mem_iff : ∀ {X Y : str}, (∀ y : num, y ∈ X ↔ y ∈ Y) -> X = Y := by + intro X Y h_mem + have h_len : len X = (len Y : num) := by + rcases lt_trichotomy (len X : num) (len Y : num) with h_lt | h_eq | h_gt + · exfalso + obtain ⟨z, h_z_in_Y, h_z_notin_X, _⟩ := exists_of_len_lt (X := X) (Y := Y) h_lt + exact h_z_notin_X ((h_mem z).mpr h_z_in_Y) + · exact h_eq + · exfalso + obtain ⟨z, h_z_in_X, h_z_notin_Y, _⟩ := exists_of_len_lt (X := Y) (Y := X) h_gt + exact h_z_notin_Y ((h_mem z).mp h_z_in_X) + exact M.SE h_len (fun y _ => h_mem y) diff --git a/LeanPool/FormalizationOfBoundedArithmetic/V0StrAddAssoc.lean b/LeanPool/FormalizationOfBoundedArithmetic/V0StrAddAssoc.lean new file mode 100644 index 0000000000..08832fc556 --- /dev/null +++ b/LeanPool/FormalizationOfBoundedArithmetic/V0StrAddAssoc.lean @@ -0,0 +1,115 @@ +/- +Copyright (c) 2026 ruplet. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: ruplet +-/ + +-- This file proves: +-- ∀ {X Y Z : str}, (X + Y) + Z = X + (Y + Z) +-- However, the proof was done using leanstral and is very verbose +-- Please see V0.lean for the manually written foundations. +import LeanPool.FormalizationOfBoundedArithmetic.V0StrAddComm + +variable {num str : Type} [M : V0ExtModel num str] +open FirstOrder Language +open HasTypes_is +open HasEmptySet +open HasLen +open HasSucc +open V0ExtModel V0Model BASICModel + +lemma add_assoc_bit_bool {A B C D X Y Z : Prop} : + (Xor' A B ↔ Xor' C D) -> + (Xor' (Xor' (Xor' (Xor' X Y) C) Z) D ↔ + Xor' (Xor' X (Xor' (Xor' Y Z) A)) B) := by + intro h + by_cases hA : A <;> by_cases hB : B <;> by_cases hC : C <;> by_cases hD : D <;> + by_cases hX : X <;> by_cases hY : Y <;> by_cases hZ : Z <;> + simp [Xor', hA, hB, hC, hD, hX, hY, hZ] at h ⊢ + +lemma carry_pair_step_bool {A B C D X Y Z : Prop} : + (A ∧ B ↔ C ∧ D) -> + (Xor' A B ↔ Xor' C D) -> + (((Maj A Y Z) ∧ (Maj B X (Xor' (Xor' Y Z) A))) ↔ + ((Maj C X Y) ∧ (Maj D (Xor' (Xor' X Y) C) Z))) ∧ + (Xor' (Maj A Y Z) (Maj B X (Xor' (Xor' Y Z) A)) ↔ + Xor' (Maj C X Y) (Maj D (Xor' (Xor' X Y) C) Z)) := by + intro h_and h_xor + by_cases hA : A <;> by_cases hB : B <;> by_cases hC : C <;> by_cases hD : D <;> + by_cases hX : X <;> by_cases hY : Y <;> by_cases hZ : Z <;> + simp [Maj, Xor', hA, hB, hC, hD, hX, hY, hZ] at h_and h_xor ⊢ + +/-- Strong carry invariant used to prove associativity of string addition. -/ +def CarryAssocPred (X Y Z : str) (i : num) : Prop := + ((Carry i Y Z ∧ Carry i X (Y + Z)) ↔ (Carry i X Y ∧ Carry i (X + Y) Z)) ∧ + (Xor' (Carry i Y Z) (Carry i X (Y + Z)) ↔ Xor' (Carry i X Y) (Carry i (X + Y) Z)) + +/- +This is the only induction instance assumed here for proving associativity of string +addition. The displayed predicate is exactly the stronger Cook–Nguyen carry invariant, +and it is built from bounded formulas already present in `V0`. +-/ +lemma carry_assoc_induction : + ∀ {X Y Z : str}, + CarryAssocPred X Y Z (0 : num) -> + (∀ i : num, CarryAssocPred X Y Z i -> CarryAssocPred X Y Z (i + (1 : num))) -> + ∀ i : num, CarryAssocPred X Y Z i := by + intro X Y Z h_zero h_step + exact M.prop_induction_ax (CarryAssocPred X Y Z) h_zero h_step + +lemma carry_pair_assoc : ∀ {X Y Z : str}, ∀ {i : num}, + ((Carry i Y Z ∧ Carry i X (Y + Z)) ↔ (Carry i X Y ∧ Carry i (X + Y) Z)) ∧ + (Xor' (Carry i Y Z) (Carry i X (Y + Z)) ↔ Xor' (Carry i X Y) (Carry i (X + Y) Z)) := by + intro X Y Z i + have hφ : ∀ j : num, CarryAssocPred X Y Z j := by + apply carry_assoc_induction (X := X) (Y := Y) (Z := Z) + · have h0_yz : ¬ Carry (0 : num) Y Z := + (carry_rec (i := (0 : num)) (X := Y) (Y := Z)).1 + have h0_x_yz : ¬ Carry (0 : num) X (Y + Z) := + (carry_rec (i := (0 : num)) (X := X) (Y := Y + Z)).1 + have h0_xy : ¬ Carry (0 : num) X Y := + (carry_rec (i := (0 : num)) (X := X) (Y := Y)).1 + have h0_xy_z : ¬ Carry (0 : num) (X + Y) Z := + (carry_rec (i := (0 : num)) (X := X + Y) (Y := Z)).1 + constructor + · constructor + · intro h + exact False.elim (h0_yz h.1) + · intro h + exact False.elim (h0_xy h.1) + · simp [Xor', h0_yz, h0_x_yz, h0_xy, h0_xy_z] + · intro j h_j + rcases h_j with ⟨h_j_and, h_j_xor⟩ + have h_step := + carry_pair_step_bool (X := j ∈ X) (Y := j ∈ Y) (Z := j ∈ Z) h_j_and h_j_xor + constructor + · rw [(carry_rec (i := j) (X := Y) (Y := Z)).2] + rw [(carry_rec (i := j) (X := X) (Y := Y + Z)).2] + rw [(carry_rec (i := j) (X := X) (Y := Y)).2] + rw [(carry_rec (i := j) (X := X + Y) (Y := Z)).2] + rw [mem_add_iff_xor (X := Y) (Y := Z) (i := j)] + rw [mem_add_iff_xor (X := X) (Y := Y) (i := j)] + exact h_step.1 + · rw [(carry_rec (i := j) (X := Y) (Y := Z)).2] + rw [(carry_rec (i := j) (X := X) (Y := Y + Z)).2] + rw [(carry_rec (i := j) (X := X) (Y := Y)).2] + rw [(carry_rec (i := j) (X := X + Y) (Y := Z)).2] + rw [mem_add_iff_xor (X := Y) (Y := Z) (i := j)] + rw [mem_add_iff_xor (X := X) (Y := Y) (i := j)] + exact h_step.2 + exact hφ i + + +-- For Associativity, first show in V0(+) that +-- Carry(i, Y, Z) ⊕ Carry(i, X, Y + Z) ↔ +-- Carry(i, X, Y ) ⊕ Carry(i, X + Y, Z). +-- Derive a stronger statement than this, and prove it by induction on i. +theorem str_add_assoc : ∀ {X Y Z : str}, (X + Y) + Z = X + (Y + Z) := by + intro X Y Z + refine str_eq_of_mem_iff (num := num) (str := str) (X := (X + Y) + Z) (Y := X + (Y + Z)) ?_ + intro i + rw [mem_add_iff_xor (X := X + Y) (Y := Z) (i := i)] + rw [mem_add_iff_xor (X := X) (Y := Y + Z) (i := i)] + rw [mem_add_iff_xor (X := X) (Y := Y) (i := i)] + rw [mem_add_iff_xor (X := Y) (Y := Z) (i := i)] + exact add_assoc_bit_bool (carry_pair_assoc (X := X) (Y := Y) (Z := Z) (i := i)).2 diff --git a/LeanPool/FormalizationOfBoundedArithmetic/V0StrAddComm.lean b/LeanPool/FormalizationOfBoundedArithmetic/V0StrAddComm.lean new file mode 100644 index 0000000000..be3a1e90d1 --- /dev/null +++ b/LeanPool/FormalizationOfBoundedArithmetic/V0StrAddComm.lean @@ -0,0 +1,66 @@ +/- +Copyright (c) 2026 ruplet. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: ruplet +-/ + +-- This file proves: +-- ∀ {X Y : str}, X + Y = Y + X +-- However, the proof was done using leanstral and is very verbose +-- Please see V0.lean for the manually written foundations. +import LeanPool.FormalizationOfBoundedArithmetic.V0 + +variable {num str : Type} [M : V0ExtModel num str] +open FirstOrder Language +open HasTypes_is +open HasEmptySet +open HasLen +open HasSucc +open V0ExtModel V0Model BASICModel + +lemma carry_comm : ∀ {X Y : str}, ∀ {i : num}, Carry i X Y ↔ Carry i Y X := by + intro X Y i + unfold Carry + constructor + · intro h + obtain ⟨k, hk_lt_i, hkX, hkY, hkprop⟩ := h + refine ⟨k, hk_lt_i, hkY, hkX, ?_⟩ + intro j hj_lt_i hk_lt_j + rcases hkprop j hj_lt_i hk_lt_j with hjX | hjY + · exact Or.inr hjX + · exact Or.inl hjY + · intro h + obtain ⟨k, hk_lt_i, hkY, hkX, hkprop⟩ := h + refine ⟨k, hk_lt_i, hkX, hkY, ?_⟩ + intro j hj_lt_i hk_lt_j + rcases hkprop j hj_lt_i hk_lt_j with hjY | hjX + · exact Or.inr hjY + · exact Or.inl hjX + +lemma mem_add_iff_xor : ∀ {X Y : str}, ∀ {i : num}, + i ∈ X + Y ↔ Xor' (Xor' (i ∈ X) (i ∈ Y)) (Carry i X Y) := by + intro X Y i + constructor + · intro h + exact (ax_add (X := X) (Y := Y) (i := i)).mp h |>.2 + · intro h_xor + have h_lt : i < len X + len Y := by + rw [xor3_split] at h_xor + rcases h_xor with h | h | h | h + · exact lt_of_lt_of_le (L1 h.1) (show len X ≤ len X + len Y from B8) + · exact lt_of_lt_of_le (L1 h.2.1) (by + rw [_root_.add_comm] + exact B8) + · exact carry_lt_add_len h.2.2 + · exact lt_of_lt_of_le (L1 h.1) (show len X ≤ len X + len Y from B8) + exact (ax_add (X := X) (Y := Y) (i := i)).mpr ⟨h_lt, h_xor⟩ + +theorem str_add_comm : ∀ {X Y : str}, X + Y = Y + X := by + intro X Y + refine str_eq_of_mem_iff (num := num) (str := str) (X := X + Y) (Y := Y + X) ?_ + intro i + rw [mem_add_iff_xor (X := X) (Y := Y) (i := i)] + rw [mem_add_iff_xor (X := Y) (Y := X) (i := i)] + rw [carry_comm (X := X) (Y := Y) (i := i)] + unfold Xor' + tauto diff --git a/LeanPool/projects.yml b/LeanPool/projects.yml index 8d2bc9c42b..e5e7e0b2ea 100644 --- a/LeanPool/projects.yml +++ b/LeanPool/projects.yml @@ -444,3 +444,43 @@ projects: msc: - "11E25" - "11H06" + - slug: formalization-of-bounded-arithmetic + title: Formalization of bounded arithmetic + summary: Formalizes first-order and two-sorted fragments of bounded arithmetic, including induction and string-addition laws. + branch: mathematical logic + entry_module: LeanPool.FormalizationOfBoundedArithmetic + authors: + - ruplet + source: + url: https://github.com/ruplet/formalization-of-bounded-arithmetic + github_repo: ruplet/formalization-of-bounded-arithmetic + status: verified + main_declarations: + - IOPENModel.add_assoc + - V0Model.ind_of_comp + - str_add_assoc + main_results: + - declaration: IOPENModel.add_assoc + informal: Proves associativity of addition in IOPEN models. + - declaration: IOPENModel.add_comm + informal: Proves commutativity of addition in IOPEN models. + - declaration: IDelta0Model.pred_exists + informal: Shows that nonzero elements in IDelta0 models have predecessors. + - declaration: IDelta0Model.mul_cancel_right + informal: Proves right cancellation for multiplication by a nonzero element in IDelta0 models. + - declaration: V0Model.xind + informal: Derives string induction for V0 models from the comprehension axioms. + - declaration: V0Model.ind_of_comp + informal: Derives propositional induction from comprehension in V0 models. + - declaration: str_add_comm + informal: Proves commutativity of string addition in V0 extension models. + - declaration: str_add_assoc + informal: Proves associativity of string addition in V0 extension models. + tags: + - logic + - bounded-arithmetic + - model-theory + - computational-complexity + msc: + - "03F30" + - "03D15" From 22a863159f5174317a4d8a2dc50b037b25115c06 Mon Sep 17 00:00:00 2001 From: Vasily Ilin Date: Tue, 19 May 2026 13:21:46 +0900 Subject: [PATCH 2/6] Add bounded arithmetic string successor theorem --- LeanPool.lean | 1 + .../FormalizationOfBoundedArithmetic.lean | 3 +- .../V0StrSuccAssoc.lean | 1187 +++++++++++++++++ LeanPool/projects.yml | 3 + 4 files changed, 1193 insertions(+), 1 deletion(-) create mode 100644 LeanPool/FormalizationOfBoundedArithmetic/V0StrSuccAssoc.lean diff --git a/LeanPool.lean b/LeanPool.lean index 00fb0e2535..86eb48db4d 100644 --- a/LeanPool.lean +++ b/LeanPool.lean @@ -166,6 +166,7 @@ import LeanPool.FormalizationOfBoundedArithmetic.Syntax import LeanPool.FormalizationOfBoundedArithmetic.V0 import LeanPool.FormalizationOfBoundedArithmetic.V0StrAddAssoc import LeanPool.FormalizationOfBoundedArithmetic.V0StrAddComm +import LeanPool.FormalizationOfBoundedArithmetic.V0StrSuccAssoc import LeanPool.ForwardEuler import LeanPool.ForwardEuler.Main import LeanPool.GrothendieckVanishing diff --git a/LeanPool/FormalizationOfBoundedArithmetic.lean b/LeanPool/FormalizationOfBoundedArithmetic.lean index da97c78d09..47693a5304 100644 --- a/LeanPool/FormalizationOfBoundedArithmetic.lean +++ b/LeanPool/FormalizationOfBoundedArithmetic.lean @@ -23,6 +23,7 @@ import LeanPool.FormalizationOfBoundedArithmetic.Syntax import LeanPool.FormalizationOfBoundedArithmetic.V0 import LeanPool.FormalizationOfBoundedArithmetic.V0StrAddAssoc import LeanPool.FormalizationOfBoundedArithmetic.V0StrAddComm +import LeanPool.FormalizationOfBoundedArithmetic.V0StrSuccAssoc /-! # Formalization of bounded arithmetic @@ -30,7 +31,7 @@ import LeanPool.FormalizationOfBoundedArithmetic.V0StrAddComm Source: url:https://github.com/ruplet/formalization-of-bounded-arithmetic Authors: ruplet Status: verified -Main declarations: `IOPENModel.add_assoc`, `V0Model.ind_of_comp`, `str_add_assoc` +Main declarations: `IOPENModel.add_assoc`, `V0Model.ind_of_comp`, `str_add_assoc`, `str_succ_assoc` Tags: logic, bounded-arithmetic, model-theory, computational-complexity MSC: 03F30, 03D15 -/ diff --git a/LeanPool/FormalizationOfBoundedArithmetic/V0StrSuccAssoc.lean b/LeanPool/FormalizationOfBoundedArithmetic/V0StrSuccAssoc.lean new file mode 100644 index 0000000000..7093082be6 --- /dev/null +++ b/LeanPool/FormalizationOfBoundedArithmetic/V0StrSuccAssoc.lean @@ -0,0 +1,1187 @@ +/- +Copyright (c) 2026 ruplet. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: ruplet +-/ +import LeanPool.FormalizationOfBoundedArithmetic.V0 + +-- This file proves: +-- ∀ {X Y : str}, X + succ Y = succ (X + Y) +-- However, the proof was done using leanstral and is very verbose +-- Please see V0.lean for the manually written foundations. + +variable {num str : Type} [M : V0ExtModel num str] +open V0ExtModel V0Model BASICModel +open FirstOrder Language +open HasTypes_is +open HasEmptySet +open HasLen +open HasSucc + +namespace Xor' + +lemma true1 {P Q R : Prop} : P -> (Xor' (Xor' P Q) R <-> ¬ Xor' Q R) := by + unfold Xor' + tauto + +lemma true2 {P Q R : Prop} : Q -> (Xor' (Xor' P Q) R <-> ¬ Xor' P R) := by + unfold Xor' + tauto + +end Xor' + +lemma len_le_len_succ : ∀ {X : str}, (len X : num) ≤ len (succ X) := by + intro X + false_or_by_contra + rename_i h + rw [not_le] at h + obtain ⟨p, px, ps, p_eq⟩ := exists_of_len_lt h + rw [ax_succ] at ps + simp only [not_and, not_or, not_exists, not_not, not_forall] at ps + specialize ps (by + rw [<- p_eq] + exact le_self_add + ) + have aux : (p + 1) ∈ succ X := by + rw [ax_succ] + constructor + · rw [p_eq] + · right + constructor + · intro hp + apply (L1 hp).2 + exact _root_.le_of_eq (id (Eq.symm p_eq)) + · intro j jp + by_cases hj : j = p + · rw [hj] + exact px + · apply ps.1 + · exact px + · constructor + · rw [B11] + exact jp + · rw [<- B11] at jp + intro contr + apply hj + apply _root_.le_antisymm <;> assumption + have aux2 : p + 1 ≤ len (succ X) := (L1 aux).1 + rw [p_eq] at aux2 + have aux3 : len X < len X := lt_of_le_of_lt aux2 h + apply aux3.2 + rfl + +lemma len_succ_le_succ : ∀ {X : str}, len (succ X) ≤ (len X : num) + (1 : num) := by + intro X + by_contra h + have h_lt : len X + (1 : num) < len (succ X) := lt_of_not_ge h + obtain ⟨z, h_z_in, h_z_ge, _⟩ := exists_of_len_lt' (X := succ X) (i := len X + (1 : num)) h_lt + have h_len_X_lt_z : len X < z := lt_of_lt_of_le (lt_succ (len X)) h_z_ge + rw [ax_succ] at h_z_in + exact not_lt_self (len X) (lt_of_lt_of_le h_len_X_lt_z h_z_in.1) + +lemma in_iff_not_notin {X : str} {j : num} : j ∈ X ↔ ¬ j ∉ X := by + rw [not_not] + +/-- `m` is the least position below the string length where `X` has no bit. -/ +def LowestOrderZero (X : str) (m : num) := m ≤ len X ∧ m ∉ X ∧ ∀ j < m, j ∈ X + +lemma exists_lowest_order_zero (X : str) : ∃ m : num, LowestOrderZero X m := by + obtain ⟨X', hX'⟩ := comp10 X (len X + (1 : num)) + have len_X'_ne_zero : (0 : num) < len X' := by + have lenX_in_X' : (len X) ∈ X' := by + rw [hX'.2] + · exact len_not_in + · exact lt_succ (len X) + apply @lt_of_le_of_lt _ _ _ (len X) + · exact B9 (len X) + · exact L1 lenX_in_X' + obtain ⟨min, hmin⟩ := xmin len_X'_ne_zero + exists min + have min_le_lenx : min <= len X := by + rw [B11] + apply lt_of_lt_of_le + · exact hmin.1 + · exact hX'.1 + constructor + · exact min_le_lenx + · constructor + · rw [<- hX'.2] + · exact hmin.2.1 + · rw [<- B11] + exact min_le_lenx + · intro j hj + rw [@in_iff_not_notin] + rw [<- hX'.2] + · apply hmin.2.2 + exact hj + · rw [<- B11] + apply le_of_lt + apply lt_of_lt_of_le + · exact hj + · exact min_le_lenx + +/-- `m` is the least position below the string length where `X` has a bit. -/ +def LowestOrderOne (X : str) (m : num) := m ≤ len X ∧ m ∈ X ∧ ∀ j < m, j ∉ X + +lemma exists_lowest_order_one {X : str} : (0 : num) < len X -> ∃ m : num, LowestOrderOne X m := by + intro len_ne_zero + obtain ⟨min, hmin⟩ := xmin len_ne_zero + exists min + constructor + · apply le_of_lt + exact hmin.1 + · exact hmin.2 + + +lemma succ_bit_eq {X : str} {m : num} : LowestOrderZero X m -> m ∈ succ X := by + intro h + rw [ax_succ] + exact ⟨h.1, Or.inr ⟨h.2.1, h.2.2⟩⟩ + +lemma succ_bit_lt {X : str} {m : num} : LowestOrderZero X m -> ∀ i < m, i ∉ succ X := by + intro h i hi his + rw [ax_succ] at his + rcases his with ⟨_, hcases⟩ + rcases hcases with hcase | hcase + · rcases hcase.2 with ⟨j, hj, hnot⟩ + exact hnot (h.2.2 j (lt_trans hj hi)) + · exact hcase.1 (h.2.2 i hi) + +lemma succ_bit_gt {X : str} {m : num} : LowestOrderZero X m -> ∀ i > m, i ∈ succ X ↔ i ∈ X := by + intro h i hi + constructor + · intro his + rw [ax_succ] at his + rcases his with ⟨_, hcases⟩ + rcases hcases with hcase | hcase + · exact hcase.1 + · exact False.elim (h.2.1 (hcase.2 m hi)) + · intro hix + rw [ax_succ] + exact ⟨le_of_lt (L1 hix), Or.inl ⟨hix, ⟨m, hi, h.2.1⟩⟩⟩ + +lemma aux1 : ∀ {X : str}, ∀ {y min : num}, + LowestOrderZero X min -> y < min -> y ∈ X := by + intro X y min h hy + exact h.2.2 y hy + +lemma len_succ_pos : ∀ {X : str}, len (succ X) > (0 : num) := by + intro X + obtain ⟨min, hmin⟩ := exists_lowest_order_zero X (num := num) + have min_X := succ_bit_eq hmin + apply len_pos_of_exists min_X + +lemma lsb_not_succ : ∀ {X : str}, 0 ∈ X <-> 0 ∉ (succ X) := by + intro X + constructor + · intro h contr + rw [ax_succ] at contr + rcases contr with ⟨hlen, hcases⟩ + rcases hcases with hbad | hgood + · rcases hbad with ⟨hin, j, hj_lt, hj_notin⟩ + apply not_lt_zero (x := j) + assumption + · apply hgood.1; assumption + · intro h + by_contra h0 + apply h + rw [ax_succ] + constructor + · exact zero_le (len X) + · right + constructor + · exact h0 + · intro j hj + exact False.elim (not_lt_zero (x := j) hj) + +lemma all_lt_mem_of_not_mem_of_mem_succ : + ∀ {X : str} {i : num}, i ∉ X -> i ∈ succ X -> ∀ j < i, j ∈ X := by + intro X i h_i_notX h_i_SX + rw [ax_succ] at h_i_SX + rcases h_i_SX with ⟨h_i_le, ⟨h_i_X, ex⟩ | ⟨h_i_notX, all⟩⟩ + · exact fun j a ↦ False.elim (h_i_notX h_i_X) + · exact all + +lemma all_lt_not_mem_of_not_carry_of_all_lt_mem : + ∀ {X Y : str} {i : num}, + ¬ Carry i X Y -> + (∀ j < i, j ∈ Y) -> + ∀ j < i, j ∉ X := by + intro X Y i h_Carry h_all_lt_mem_Y + unfold Carry at h_Carry + rw [not_exists] at h_Carry + intro j + specialize h_Carry j + rw [not_and_or] at h_Carry + rcases h_Carry with contr | h_Carry + · intro contr' + contradiction + · intro h_j_lt_i h_j_X + rw [not_and] at h_Carry + specialize h_Carry h_j_X + rw [not_and] at h_Carry + specialize h_Carry (h_all_lt_mem_Y j h_j_lt_i) + apply h_Carry; clear h_Carry; intro z z_lt j_lt + right + exact h_all_lt_mem_Y z z_lt + +lemma all_lt_not_carry_of_not_carry_of_all_lt_mem : + ∀ {X Y : str} {i : num}, ¬ Carry i X Y -> (∀ j < i, j ∈ Y) -> ∀ j < i, ¬ Carry j X Y := by + intro X Y i h_notC h_all_lt_mem_Y j h_j_lt h_jC + unfold Carry at h_jC + obtain ⟨k, h_k_lt_j, h_k_X, _, _⟩ := h_jC + have h_k_lt_i : k < i := lt_trans h_k_lt_j h_j_lt + exact all_lt_not_mem_of_not_carry_of_all_lt_mem h_notC h_all_lt_mem_Y k h_k_lt_i h_k_X + +lemma all_lt_not_mem_of_all_lt_mem_add_of_all_lt_mem : + ∀ {X Y : str} {i : num}, + (∀ j < i, j ∈ Y) -> + (∀ j < i, j ∈ X + Y) -> + ∀ j < i, j ∉ X := by + intro X Y i h_all_lt_mem_Y h_all_lt_mem_add j h_j_lt_i h_jX + have h_len_X_pos : (0 : num) < len X := len_pos_of_exists h_jX + obtain ⟨m, hm⟩ := exists_lowest_order_one (X := X) h_len_X_pos + have h_m_le_j : m ≤ j := by + by_contra h_m_gt_j + exact hm.2.2 j (lt_of_not_ge h_m_gt_j) h_jX + have h_m_lt_i : m < i := lt_of_le_of_lt h_m_le_j h_j_lt_i + have h_mY : m ∈ Y := h_all_lt_mem_Y m h_m_lt_i + have h_m_notCarry : ¬ Carry m X Y := by + intro hC + unfold Carry at hC + obtain ⟨c, h_c_lt_m, h_cX, _, _⟩ := hC + exact hm.2.2 c h_c_lt_m h_cX + have h_m_in_add := h_all_lt_mem_add m h_m_lt_i + rw [ax_add] at h_m_in_add + have h_m_xor := h_m_in_add.2 + rw [xor3_split] at h_m_xor + rcases h_m_xor with h1 | h2 | h3 | h4 + · exact h1.2.1 h_mY + · exact h2.1 hm.2.1 + · exact h3.1 hm.2.1 + · exact h_m_notCarry h4.2.2 + +lemma not_carry_of_all_lt_mem_add_of_all_lt_mem : + ∀ {X Y : str} {i : num}, + (∀ j < i, j ∈ Y) -> + (∀ j < i, j ∈ X + Y) -> + ¬ Carry i X Y := by + intro X Y i h_all_lt_mem_Y h_all_lt_mem_add hC + unfold Carry at hC + obtain ⟨k, h_k_lt_i, h_kX, _, _⟩ := hC + exact all_lt_not_mem_of_all_lt_mem_add_of_all_lt_mem h_all_lt_mem_Y h_all_lt_mem_add k + h_k_lt_i h_kX + +lemma not_carry_of_all_lt_mem_add : + ∀ {X Y : str} {i : num}, + (∀ j < i, j ∈ X + Y) -> + ¬ Carry i X Y := by + intro X Y i h_all_lt_mem_add hC + obtain ⟨I, h_I_le, h_I⟩ := comp11 X Y i + unfold Carry at hC + obtain ⟨k, h_k_lt_i, h_kX, h_kY, _⟩ := hC + have h_kI : k ∈ I := by + rw [h_I k h_k_lt_i] + exact ⟨h_kX, h_kY⟩ + have h_len_I_pos : (0 : num) < len I := len_pos_of_exists h_kI + obtain ⟨c, h_c_lt_len_I, h_cI, h_cmin⟩ := xmin h_len_I_pos + have h_c_lt_i : c < i := lt_of_lt_of_le h_c_lt_len_I h_I_le + have h_cX : c ∈ X := (h_I c h_c_lt_i).1 h_cI |>.1 + have h_cY : c ∈ Y := (h_I c h_c_lt_i).1 h_cI |>.2 + have h_c_notCarry : ¬ Carry c X Y := by + intro h_cC + unfold Carry at h_cC + obtain ⟨d, h_d_lt_c, h_dX, h_dY, _⟩ := h_cC + have h_dI : d ∈ I := by + rw [h_I d (lt_trans h_d_lt_c h_c_lt_i)] + exact ⟨h_dX, h_dY⟩ + exact h_cmin d h_d_lt_c h_dI + have h_c_in_add : c ∈ X + Y := h_all_lt_mem_add c h_c_lt_i + rw [ax_add] at h_c_in_add + rw [xor3_split] at h_c_in_add + rcases h_c_in_add.2 with h1 | h2 | h3 | h4 + · exact h1.2.1 h_cY + · exact h2.1 h_cX + · exact h3.1 h_cX + · exact h_c_notCarry h4.2.2 + +lemma all_lt_not_carry_of_all_lt_mem_add : + ∀ {X Y : str} {i : num}, + (∀ j < i, j ∈ X + Y) -> + ∀ j < i, ¬ Carry j X Y := by + intro X Y i h_all_lt_mem_add j h_j_lt_i + apply not_carry_of_all_lt_mem_add + intro z h_z_lt_j + exact h_all_lt_mem_add z (lt_trans h_z_lt_j h_j_lt_i) + +lemma carry_succ_of_all_lt_mem_add_of_lowest_zero_lt : + ∀ {X Y : str} {m i : num}, + LowestOrderZero Y m -> + m < i -> + (∀ j < i, j ∈ X + Y) -> + Carry i X (succ Y) := by + intro X Y m i hm h_m_lt_i h_all_lt_mem_add + have h_all_lt_not_carry : ∀ j < i, ¬ Carry j X Y := + all_lt_not_carry_of_all_lt_mem_add h_all_lt_mem_add + have h_before_m : ∀ j < m, j ∈ X + Y := by + intro j h_j_lt_m + exact h_all_lt_mem_add j (lt_trans h_j_lt_m h_m_lt_i) + have h_m_notCarry : ¬ Carry m X Y := + not_carry_of_all_lt_mem_add_of_all_lt_mem hm.2.2 h_before_m + have h_m_in_add : m ∈ X + Y := h_all_lt_mem_add m h_m_lt_i + have h_mX : m ∈ X := by + rw [ax_add] at h_m_in_add + have h_m_xor := h_m_in_add.2 + rw [xor3_split] at h_m_xor + rcases h_m_xor with h1 | h2 | h3 | h4 + · exact h1.1 + · exact False.elim (hm.2.1 h2.2.1) + · exact False.elim (h_m_notCarry h3.2.2) + · exact False.elim (hm.2.1 h4.2.1) + have h_or_after_m : ∀ j, m < j -> j < i -> j ∈ X ∨ j ∈ Y := by + intro j h_m_lt_j h_j_lt_i + have h_j_in_add : j ∈ X + Y := h_all_lt_mem_add j h_j_lt_i + have h_j_notCarry : ¬ Carry j X Y := h_all_lt_not_carry j h_j_lt_i + rw [ax_add] at h_j_in_add + have h_j_xor := h_j_in_add.2 + rw [xor3_split] at h_j_xor + rcases h_j_xor with h1 | h2 | h3 | h4 + · exact Or.inl h1.1 + · exact Or.inr h2.2.1 + · exact False.elim (h_j_notCarry h3.2.2) + · exact False.elim (h_j_notCarry h4.2.2) + unfold Carry + refine ⟨m, h_m_lt_i, h_mX, succ_bit_eq hm, ?_⟩ + intro j h_j_lt_i h_m_lt_j + rcases h_or_after_m j h_m_lt_j h_j_lt_i with h_jX | h_jY + · exact Or.inl h_jX + · exact Or.inr ((succ_bit_gt hm j h_m_lt_j).2 h_jY) + + +lemma prefix_zero_contradiction_of_not_carry_of_all_lt_mem : + ∀ {X Y : str} {i : num}, + i < len X + len Y -> + (∃ j < i, j ∉ X + Y) -> + ¬ Carry i X Y -> + (∀ j < i, j ∈ Y) -> + False := by + intro X Y i h_i_lt h_prefix_zero h_notC h_all_lt_mem_Y + have h_X_prefix_zero := all_lt_not_mem_of_not_carry_of_all_lt_mem h_notC h_all_lt_mem_Y + have h_Carry_prefix_zero := all_lt_not_carry_of_not_carry_of_all_lt_mem h_notC h_all_lt_mem_Y + obtain ⟨contr, h_contr_lt, h_contr_notXY⟩ := h_prefix_zero + apply h_contr_notXY + rw [ax_add] + constructor + · exact lt_trans h_contr_lt h_i_lt + · rw [Xor'.true2 (h_all_lt_mem_Y contr h_contr_lt)] + rw [not_xor] + rw [<- not_iff_not, iff_true_left] + · exact h_Carry_prefix_zero contr h_contr_lt + · exact h_X_prefix_zero contr h_contr_lt + +lemma not_lt_lowest_zero_of_prefix_zero_of_not_carry : + ∀ {X Y : str} {m i : num}, + LowestOrderZero Y m -> + i < len X + len Y -> + (∃ j < i, j ∉ X + Y) -> + ¬ Carry i X Y -> + ¬ i < m := by + intro X Y m i hm h_i_lt h_prefix_zero h_notC h_i_lt_m + apply prefix_zero_contradiction_of_not_carry_of_all_lt_mem h_i_lt h_prefix_zero h_notC + intro j h_j_lt + exact hm.2.2 j (lt_trans h_j_lt h_i_lt_m) + +lemma not_carry_succ_of_lowest_zero_ge : + ∀ {X Y : str} {m i : num}, + LowestOrderZero Y m -> + i ≤ m -> + ¬ Carry i X (succ Y) := by + intro X Y m i hm h_i_le h_Carry + unfold Carry at h_Carry + obtain ⟨k, h_k_lt_i, _, h_k_SY, _⟩ := h_Carry + exact (succ_bit_lt hm k (lt_of_lt_of_le h_k_lt_i h_i_le)) h_k_SY + +lemma carry_succ_of_carry_of_lowest_zero_lt : + ∀ {X Y : str} {m i : num}, + LowestOrderZero Y m -> + m < i -> + Carry i X Y -> + Carry i X (succ Y) := by + intro X Y m i hm h_m_lt_i h_Carry + unfold Carry at h_Carry ⊢ + obtain ⟨k, h_k_lt_i, h_k_X, h_k_Y, h_k_prop⟩ := h_Carry + rcases lt_trichotomy k m with h_k_lt_m | h_k_eq_m | h_m_lt_k + · have h_m_X : m ∈ X := by + rcases h_k_prop m h_m_lt_i h_k_lt_m with h_m_X | h_m_Y + · exact h_m_X + · exact False.elim (hm.2.1 h_m_Y) + refine ⟨m, h_m_lt_i, h_m_X, succ_bit_eq hm, ?_⟩ + intro j h_j_lt_i h_m_lt_j + rcases h_k_prop j h_j_lt_i (lt_trans h_k_lt_m h_m_lt_j) with h_j_X | h_j_Y + · exact Or.inl h_j_X + · exact Or.inr ((succ_bit_gt hm j h_m_lt_j).2 h_j_Y) + · exact False.elim (hm.2.1 (by simpa [h_k_eq_m] using h_k_Y)) + · refine ⟨k, h_k_lt_i, h_k_X, (succ_bit_gt hm k h_m_lt_k).2 h_k_Y, ?_⟩ + intro j h_j_lt_i h_k_lt_j + rcases h_k_prop j h_j_lt_i h_k_lt_j with h_j_X | h_j_Y + · exact Or.inl h_j_X + · exact Or.inr ((succ_bit_gt hm j (lt_trans h_m_lt_k h_k_lt_j)).2 h_j_Y) + +lemma not_carry_succ_of_prefix_zero_of_not_carry_of_lowest_zero_lt : + ∀ {X Y : str} {m i : num}, + LowestOrderZero Y m -> + m < i -> + (∃ j < i, j ∉ X + Y) -> + ¬ Carry i X Y -> + ¬ Carry i X (succ Y) := by + intro X Y m i hm h_m_lt_i h_prefix_zero h_notC h_Carry + unfold Carry at h_Carry + obtain ⟨k, h_k_lt_i, h_k_X, h_k_SY, h_k_prop⟩ := h_Carry + have h_m_le_k : m ≤ k := by + by_contra h_mk + exact (succ_bit_lt hm k (lt_of_not_ge h_mk)) h_k_SY + have h_k_le_m : k ≤ m := by + by_contra h_km + have h_m_lt_k : m < k := lt_of_not_ge h_km + have h_k_Y : k ∈ Y := (succ_bit_gt hm k h_m_lt_k).1 h_k_SY + apply h_notC + refine ⟨k, h_k_lt_i, h_k_X, h_k_Y, ?_⟩ + intro j h_j_lt_i h_k_lt_j + rcases h_k_prop j h_j_lt_i h_k_lt_j with h_j_X | h_j_SY + · exact Or.inl h_j_X + · exact Or.inr ((succ_bit_gt hm j (lt_trans h_m_lt_k h_k_lt_j)).1 h_j_SY) + have h_k_eq_m : k = m := by + apply _root_.le_antisymm <;> assumption + have h_m_X : m ∈ X := by + simpa [h_k_eq_m] using h_k_X + have h_or_after_m : ∀ j, m < j -> j < i -> j ∈ X ∨ j ∈ Y := by + intro j h_m_lt_j h_j_lt_i + rcases h_k_prop j h_j_lt_i (by simpa [h_k_eq_m] using h_m_lt_j) with h_j_X | h_j_SY + · exact Or.inl h_j_X + · exact Or.inr ((succ_bit_gt hm j h_m_lt_j).1 h_j_SY) + have h_X_prefix_zero : ∀ j < m, j ∉ X := by + intro j h_j_lt_m h_j_X + apply h_notC + refine ⟨j, lt_trans h_j_lt_m h_m_lt_i, h_j_X, hm.2.2 j h_j_lt_m, ?_⟩ + intro z h_z_lt_i h_j_lt_z + by_cases h_z_lt_m : z < m + · exact Or.inr (hm.2.2 z h_z_lt_m) + · have h_m_le_z : m ≤ z := le_of_not_gt h_z_lt_m + rcases eq_or_lt_of_le h_m_le_z with h_z_eq_m | h_m_lt_z + · exact Or.inl (by simpa [h_z_eq_m] using h_m_X) + · exact h_or_after_m z h_m_lt_z h_z_lt_i + have h_Carry_le_m_zero : ∀ j ≤ m, ¬ Carry j X Y := by + intro j h_j_le_m h_jC + unfold Carry at h_jC + obtain ⟨c, h_c_lt_j, h_c_X, _, _⟩ := h_jC + exact h_X_prefix_zero c (lt_of_lt_of_le h_c_lt_j h_j_le_m) h_c_X + have carry_to_i_from_after_m : + ∀ {j : num}, m < j -> j < i -> Carry j X Y -> Carry i X Y := by + intro j h_m_lt_j h_j_lt_i h_jC + unfold Carry at h_jC ⊢ + obtain ⟨c, h_c_lt_j, h_c_X, h_c_Y, h_c_prop⟩ := h_jC + refine ⟨c, lt_trans h_c_lt_j h_j_lt_i, h_c_X, h_c_Y, ?_⟩ + intro z h_z_lt_i h_c_lt_z + by_cases h_z_lt_j : z < j + · exact h_c_prop z h_z_lt_j h_c_lt_z + · have h_j_le_z : j ≤ z := le_of_not_gt h_z_lt_j + exact h_or_after_m z (lt_of_lt_of_le h_m_lt_j h_j_le_z) h_z_lt_i + obtain ⟨contr, h_contr_lt, h_contr_notXY⟩ := h_prefix_zero + apply h_contr_notXY + rw [ax_add] + constructor + · rcases lt_trichotomy contr m with h_contr_lt_m | h_contr_eq_m | h_m_lt_contr + · exact lt_of_lt_of_le (L1 (hm.2.2 contr h_contr_lt_m)) (by + rw [_root_.add_comm] + exact B8) + · rw [h_contr_eq_m] + exact lt_of_lt_of_le (L1 h_m_X) (show len X ≤ len X + len Y from B8) + · rcases h_or_after_m contr h_m_lt_contr h_contr_lt with h_contr_X | h_contr_Y + · exact lt_of_lt_of_le (L1 h_contr_X) (show len X ≤ len X + len Y from B8) + · exact lt_of_lt_of_le (L1 h_contr_Y) (by + rw [_root_.add_comm] + exact B8) + · rcases lt_trichotomy contr m with h_contr_lt_m | h_contr_eq_m | h_m_lt_contr + · rw [xor3_split] + right + left + exact ⟨h_X_prefix_zero contr h_contr_lt_m, hm.2.2 contr h_contr_lt_m, + h_Carry_le_m_zero contr (le_of_lt h_contr_lt_m)⟩ + · rw [h_contr_eq_m, xor3_split] + left + exact ⟨h_m_X, hm.2.1, h_Carry_le_m_zero m le_rfl⟩ + · have h_contr_or : contr ∈ X ∨ contr ∈ Y := h_or_after_m contr h_m_lt_contr h_contr_lt + have h_contr_notboth : ¬ (contr ∈ X ∧ contr ∈ Y) := by + intro h_both + apply h_notC + refine ⟨contr, h_contr_lt, h_both.1, h_both.2, ?_⟩ + intro z h_z_lt_i h_contr_lt_z + exact h_or_after_m z (lt_trans h_m_lt_contr h_contr_lt_z) h_z_lt_i + have h_contr_notCarry : ¬ Carry contr X Y := by + intro h_contr_Carry + apply h_notC + exact carry_to_i_from_after_m h_m_lt_contr h_contr_lt h_contr_Carry + rcases h_contr_or with h_contr_X | h_contr_Y + · rw [xor3_split] + left + exact ⟨h_contr_X, fun h_Y => h_contr_notboth ⟨h_contr_X, h_Y⟩, h_contr_notCarry⟩ + · rw [xor3_split] + right + left + exact ⟨fun h_X => h_contr_notboth ⟨h_X, h_contr_Y⟩, h_contr_Y, h_contr_notCarry⟩ + +lemma not_mem_add_succ_of_not_mem_add_of_prefix_zero : + ∀ {X Y : str} {y : num}, + y ∉ X + Y -> + (∃ j < y, j ∉ X + Y) -> + y ∉ X + succ Y := by + intro X Y y h_notAdd h_prefix_zero h_new + obtain ⟨m, hm⟩ := exists_lowest_order_zero Y (num := num) + rw [ax_add] at h_new + rcases h_new with ⟨_, h_y_xor⟩ + rw [xor3_split] at h_y_xor + rcases lt_trichotomy y m with h_y_lt_m | h_y_eq_m | h_m_lt_y + · rcases h_y_xor with h1 | h2 | h3 | h4 + · have h_yY : y ∈ Y := aux1 hm h_y_lt_m + have h_notC : ¬ Carry y X Y := by + intro hC + apply h_notAdd + rw [ax_add] + constructor + · exact carry_lt_add_len hC + · rw [xor3_split] + right + right + right + exact ⟨h1.1, h_yY, hC⟩ + have h_y_lt_old : y < len X + len Y := by + exact lt_of_lt_of_le (L1 h_yY) (by + rw [_root_.add_comm] + exact B8) + exact prefix_zero_contradiction_of_not_carry_of_all_lt_mem h_y_lt_old h_prefix_zero h_notC + (fun j h_j_lt ↦ hm.2.2 j (lt_trans h_j_lt h_y_lt_m)) + · exact (succ_bit_lt hm y h_y_lt_m) h2.2.1 + · exact (not_carry_succ_of_lowest_zero_ge hm (le_of_lt h_y_lt_m)) h3.2.2 + · exact (succ_bit_lt hm y h_y_lt_m) h4.2.1 + · subst y + rcases h_y_xor with h1 | h2 | h3 | h4 + · exact h1.2.1 (succ_bit_eq hm) + · have h_notC : ¬ Carry m X Y := by + intro hC + apply h_notAdd + rw [ax_add] + constructor + · exact carry_lt_add_len hC + · rw [xor3_split] + right + right + left + exact ⟨h2.1, hm.2.1, hC⟩ + obtain ⟨j, h_j_lt_m, h_j_notAdd⟩ := h_prefix_zero + have h_jY : j ∈ Y := hm.2.2 j h_j_lt_m + apply h_j_notAdd + rw [ax_add] + constructor + · exact lt_of_lt_of_le (L1 h_jY) (by + rw [_root_.add_comm] + exact B8) + · rw [xor3_split] + right + left + exact ⟨all_lt_not_mem_of_not_carry_of_all_lt_mem h_notC hm.2.2 j h_j_lt_m, + h_jY, + all_lt_not_carry_of_not_carry_of_all_lt_mem h_notC hm.2.2 j h_j_lt_m⟩ + · exact (not_carry_succ_of_lowest_zero_ge hm le_rfl) h3.2.2 + · exact (not_carry_succ_of_lowest_zero_ge hm le_rfl) h4.2.2 + · by_cases h_yY : y ∈ Y + · have h_ySY : y ∈ succ Y := (succ_bit_gt hm y h_m_lt_y).2 h_yY + rcases h_y_xor with h1 | h2 | h3 | h4 + · exact h1.2.1 h_ySY + · have h_oldC : Carry y X Y := by + by_contra h_notC + apply h_notAdd + rw [ax_add] + constructor + · exact lt_of_lt_of_le (L1 h_yY) (by + rw [_root_.add_comm] + exact B8) + · rw [xor3_split] + right + left + exact ⟨h2.1, h_yY, h_notC⟩ + exact h2.2.2 (carry_succ_of_carry_of_lowest_zero_lt hm h_m_lt_y h_oldC) + · exact h3.2.1 h_ySY + · have h_notC : ¬ Carry y X Y := by + intro hC + apply h_notAdd + rw [ax_add] + constructor + · exact lt_of_lt_of_le (L1 h_yY) (by + rw [_root_.add_comm] + exact B8) + · rw [xor3_split] + right + right + right + exact ⟨h4.1, h_yY, hC⟩ + exact (not_carry_succ_of_prefix_zero_of_not_carry_of_lowest_zero_lt hm h_m_lt_y + h_prefix_zero h_notC) h4.2.2 + · have h_notSY : y ∉ succ Y := by + intro h_SY + exact h_yY ((succ_bit_gt hm y h_m_lt_y).1 h_SY) + rcases h_y_xor with h1 | h2 | h3 | h4 + · have h_oldC : Carry y X Y := by + by_contra h_notC + apply h_notAdd + rw [ax_add] + constructor + · exact lt_of_lt_of_le (L1 h1.1) (show len X ≤ len X + len Y from B8) + · rw [xor3_split] + left + exact ⟨h1.1, h_yY, h_notC⟩ + exact h1.2.2 (carry_succ_of_carry_of_lowest_zero_lt hm h_m_lt_y h_oldC) + · exact h_notSY h2.2.1 + · have h_notC : ¬ Carry y X Y := by + intro hC + apply h_notAdd + rw [ax_add] + constructor + · exact carry_lt_add_len hC + · rw [xor3_split] + right + right + left + exact ⟨h3.1, h_yY, hC⟩ + exact (not_carry_succ_of_prefix_zero_of_not_carry_of_lowest_zero_lt hm h_m_lt_y + h_prefix_zero h_notC) h3.2.2 + · exact h_notSY h4.2.1 + +lemma not_mem_add_succ_of_mem_add_of_prefix_one : + ∀ {X Y : str} {y : num}, + y ∈ X + Y -> + (∀ j < y, j ∈ X + Y) -> + y ∉ X + succ Y := by + intro X Y y h_add h_prefix_one hy + have h_notCarry_old : ¬ Carry y X Y := not_carry_of_all_lt_mem_add h_prefix_one + have hy_add := hy + rw [ax_add] at hy_add + have hy_xor := hy_add.2 + rw [xor3_split] at hy_xor + have h_new_X_SY_notCarry : + y ∈ X -> y ∈ succ Y -> ¬ Carry y X (succ Y) -> False := by + intro h_X h_SY h_notCarry + rcases hy_xor with hy1 | hy2 | hy3 | hy4 + · exact hy1.2.1 h_SY + · exact hy2.1 h_X + · exact hy3.1 h_X + · exact h_notCarry hy4.2.2 + have h_new_X_notSY_Carry : + y ∈ X -> y ∉ succ Y -> Carry y X (succ Y) -> False := by + intro h_X h_notSY h_Carry + rcases hy_xor with hy1 | hy2 | hy3 | hy4 + · exact hy1.2.2 h_Carry + · exact hy2.1 h_X + · exact hy3.1 h_X + · exact h_notSY hy4.2.1 + have h_new_notX_notSY_notCarry : + y ∉ X -> y ∉ succ Y -> ¬ Carry y X (succ Y) -> False := by + intro h_notX h_notSY h_notCarry + rcases hy_xor with hy1 | hy2 | hy3 | hy4 + · exact h_notX hy1.1 + · exact h_notSY hy2.2.1 + · exact h_notCarry hy3.2.2 + · exact h_notX hy4.1 + have h_new_notX_SY_Carry : + y ∉ X -> y ∈ succ Y -> Carry y X (succ Y) -> False := by + intro h_notX h_SY h_Carry + rcases hy_xor with hy1 | hy2 | hy3 | hy4 + · exact h_notX hy1.1 + · exact hy2.2.2 h_Carry + · exact hy3.2.1 h_SY + · exact h_notX hy4.1 + have h_old := h_add + rw [ax_add] at h_old + have h_old_xor := h_old.2 + rw [xor3_split] at h_old_xor + rcases h_old_xor with h1 | h2 | h3 | h4 + · obtain ⟨m, hm⟩ := exists_lowest_order_zero Y (num := num) + have hm_le_y : m ≤ y := by + by_contra h + exact h1.2.1 (aux1 hm (lt_of_not_ge h)) + rcases eq_or_lt_of_le hm_le_y with h_my | hm_lt_y + · have h_SY : y ∈ succ Y := by + simpa [h_my] using succ_bit_eq hm + have h_notCarry_new : ¬ Carry y X (succ Y) := by + simpa [h_my] using (not_carry_succ_of_lowest_zero_ge hm le_rfl) + exact h_new_X_SY_notCarry h1.1 h_SY h_notCarry_new + · have h_notSY : y ∉ succ Y := by + intro h_SY + exact h1.2.1 ((succ_bit_gt hm y hm_lt_y).1 h_SY) + have h_Carry_new : Carry y X (succ Y) := + carry_succ_of_all_lt_mem_add_of_lowest_zero_lt hm hm_lt_y h_prefix_one + exact h_new_X_notSY_Carry h1.1 h_notSY h_Carry_new + · obtain ⟨m, hm⟩ := exists_lowest_order_zero Y (num := num) + rcases lt_trichotomy y m with h_y_lt_m | h_y_eq_m | h_m_lt_y + · have h_notSY : y ∉ succ Y := succ_bit_lt hm y h_y_lt_m + have h_notCarry_new : ¬ Carry y X (succ Y) := + not_carry_succ_of_lowest_zero_ge hm (le_of_lt h_y_lt_m) + exact h_new_notX_notSY_notCarry h2.1 h_notSY h_notCarry_new + · exfalso + apply hm.2.1 + simpa [h_y_eq_m] using h2.2.1 + · have h_SY : y ∈ succ Y := (succ_bit_gt hm y h_m_lt_y).2 h2.2.1 + have h_Carry_new : Carry y X (succ Y) := + carry_succ_of_all_lt_mem_add_of_lowest_zero_lt hm h_m_lt_y h_prefix_one + exact h_new_notX_SY_Carry h2.1 h_SY h_Carry_new + · exact h_notCarry_old h3.2.2 + · exact h_notCarry_old h4.2.2 + + +lemma add_succ_of_succ_add_zero : + ∀ {X Y : str} {y : num}, y = 0 -> y ∈ succ (X + Y) -> y ∈ X + succ Y := by + intro X Y y h hy + rw [h] at hy + rw [ax_succ] at hy + cases hy.2 with + | inl hy => + exfalso + obtain ⟨j, hj⟩ := hy.2 + apply not_lt_zero (num := num) (x := j) + apply hj.1 + | inr hy_not => + rw [h, ax_add] + constructor + · by_cases X = 0 + · rename_i X0 + rw [X0, len_empty, V0Model.zero_add] + apply len_succ_pos + · refine add_pos_of_nonneg_of_pos ?_ ?_ + · exact B9 (len X) + · apply len_succ_pos + · rw [xor_comm] + rw [<- xor_not_not] + left + constructor + · apply carry_rec.1 + assumption + · rw [not_not] + rw [@xor_iff_iff_not] + rw [ax_add] at hy_not + simp only [not_and, not_xor] at hy_not + rw [iff_false_right (carry_rec (i := y)).1] at hy_not + constructor + · intro X0 + have h_not_xor := + hy_not.1 (add_pos_of_pos_of_nonneg (L1 X0) (B9 (len Y))) + simp only [not_xor] at h_not_xor + rw [<- lsb_not_succ] + rw [<- h_not_xor] + assumption + · intro succY0 + have hY0 : 0 ∈ Y := lsb_not_succ.mpr succY0 + have h_not_xor := + hy_not.1 (add_pos_of_nonneg_of_pos (B9 (len X)) (L1 hY0)) + simp only [not_xor] at h_not_xor + rw [h_not_xor] + exact hY0 + + +lemma add_succ_of_succ_add_of_mem_add : + ∀ {X Y : str} {y pred_y : num}, + pred_y + 1 = y -> + y ∈ X + Y -> + (∃ j < y, j ∉ X + Y) -> + y ∈ X + succ Y := by + intro X Y y pred_y hpred_y_eq h_y_in_add h_prefix_zero + rw [ax_add] + constructor + · rw [ax_add] at h_y_in_add + apply lt_of_lt_of_le h_y_in_add.1 + apply V0Model.add_le_add_left + exact len_le_len_succ + conv at h_y_in_add => + rw [<- hpred_y_eq] + rw [ax_add] + rw [hpred_y_eq] + rcases h_y_in_add with ⟨h_y_lt, hxor⟩ + rw [xor3_split] at hxor + rcases hxor with + ⟨h_X, h_notY, h_notC⟩ | ⟨h_notX, h_Y, h_notC⟩ | + ⟨h_notX, h_notY, h_C⟩ | ⟨h_X, h_Y, h_C⟩ + · rw [Xor'.true1 h_X] + rw [not_xor] + constructor + · intro h_SY + exfalso + exact prefix_zero_contradiction_of_not_carry_of_all_lt_mem h_y_lt h_prefix_zero h_notC + (all_lt_mem_of_not_mem_of_mem_succ h_notY h_SY) + · intro h_Carry + obtain ⟨m, hm⟩ := exists_lowest_order_zero Y (num := num) + have hm_le_y : m ≤ y := by + exact le_of_not_gt + (not_lt_lowest_zero_of_prefix_zero_of_not_carry hm h_y_lt h_prefix_zero h_notC) + rcases eq_or_lt_of_le hm_le_y with rfl | hm_lt_y + · exact succ_bit_eq hm + · exfalso + exact not_carry_succ_of_prefix_zero_of_not_carry_of_lowest_zero_lt hm hm_lt_y + h_prefix_zero h_notC h_Carry + · obtain ⟨m, hm⟩ := exists_lowest_order_zero Y (num := num) + have hm_le_y : m ≤ y := by + exact le_of_not_gt + (not_lt_lowest_zero_of_prefix_zero_of_not_carry hm h_y_lt h_prefix_zero h_notC) + have hm_ne_y : m ≠ y := by + intro h_my + apply hm.2.1 + simpa [h_my] using h_Y + have hm_lt_y : m < y := lt_of_le_of_ne hm_le_y hm_ne_y + have h_SY : y ∈ succ Y := (succ_bit_gt hm y hm_lt_y).2 h_Y + have h_notCarry_new : ¬ Carry y X (succ Y) := + not_carry_succ_of_prefix_zero_of_not_carry_of_lowest_zero_lt hm hm_lt_y h_prefix_zero h_notC + rw [xor3_split] + right + left + exact ⟨h_notX, h_SY, h_notCarry_new⟩ + · obtain ⟨m, hm⟩ := exists_lowest_order_zero Y (num := num) + have hm_le_y : m ≤ y := by + by_contra h + exact h_notY (aux1 hm (lt_of_not_ge h)) + rcases eq_or_lt_of_le hm_le_y with rfl | hm_lt_y + · rw [xor3_split] + right + left + exact ⟨h_notX, succ_bit_eq hm, not_carry_succ_of_lowest_zero_ge hm le_rfl⟩ + · have h_notSY : y ∉ succ Y := by + intro h_SY + exact h_notY ((succ_bit_gt hm y hm_lt_y).1 h_SY) + have h_Carry_new : Carry y X (succ Y) := + carry_succ_of_carry_of_lowest_zero_lt hm hm_lt_y h_C + rw [xor3_split] + right + right + left + exact ⟨h_notX, h_notSY, h_Carry_new⟩ + · obtain ⟨m, hm⟩ := exists_lowest_order_zero Y (num := num) + rcases lt_trichotomy y m with h_y_lt_m | h_y_eq_m | h_m_lt_y + · have h_notSY : y ∉ succ Y := succ_bit_lt hm y h_y_lt_m + have h_notCarry_new : ¬ Carry y X (succ Y) := + not_carry_succ_of_lowest_zero_ge hm (le_of_lt h_y_lt_m) + rw [xor3_split] + left + exact ⟨h_X, h_notSY, h_notCarry_new⟩ + · exfalso + apply hm.2.1 + simpa [h_y_eq_m] using h_Y + · have h_SY : y ∈ succ Y := (succ_bit_gt hm y h_m_lt_y).2 h_Y + have h_Carry_new : Carry y X (succ Y) := + carry_succ_of_carry_of_lowest_zero_lt hm h_m_lt_y h_C + rw [xor3_split] + right + right + right + exact ⟨h_X, h_SY, h_Carry_new⟩ + + +lemma add_succ_of_succ_add : ∀ {X Y : str}, ∀ {y : num}, y ∈ succ (X + Y) -> y ∈ X + succ Y := by + intro X Y y hy + by_cases y = 0 + · rename_i h + exact add_succ_of_succ_add_zero h hy + rename_i y_ne_zero + obtain ⟨pred_y, hpred_y_le, hpred_y_eq⟩ := B12 y_ne_zero + rw [ax_succ] at hy + obtain ⟨_t, y_or⟩ := hy + clear _t + rcases y_or with ⟨h_y_in_add, h_prefix_zero⟩ | ⟨h_y_notin_add, h_prefix_one⟩ + · exact add_succ_of_succ_add_of_mem_add hpred_y_eq h_y_in_add h_prefix_zero + · obtain ⟨m, hm⟩ := exists_lowest_order_zero Y (num := num) + have h_notCarry_prefix : ∀ j ≤ y, ¬ Carry j X Y := by + intro j h_j_le_y + rcases eq_or_lt_of_le h_j_le_y with rfl | h_j_lt_y + · exact not_carry_of_all_lt_mem_add h_prefix_one + · exact all_lt_not_carry_of_all_lt_mem_add h_prefix_one j h_j_lt_y + rcases lt_trichotomy y m with h_y_lt_m | h_y_eq_m | h_m_lt_y + · have h_yY : y ∈ Y := aux1 hm h_y_lt_m + have h_notC : ¬ Carry y X Y := not_carry_of_all_lt_mem_add h_prefix_one + have h_X : y ∈ X := by + by_contra h_notX + apply h_y_notin_add + rw [ax_add] + constructor + · exact lt_of_lt_of_le (L1 h_yY) (by + simp only [le_add_iff_nonneg_left, zero_le] + -- simpa [_root_.add_comm] using (show len Y ≤ len Y + len X from B8) + ) + · rw [xor3_split] + right + left + exact ⟨h_notX, h_yY, h_notC⟩ + have h_notSY : y ∉ succ Y := succ_bit_lt hm y h_y_lt_m + have h_notCarry_new : ¬ Carry y X (succ Y) := + not_carry_succ_of_lowest_zero_ge hm (le_of_lt h_y_lt_m) + rw [ax_add] + constructor + · exact lt_of_lt_of_le (L1 h_X) (show len X ≤ len X + len (succ Y) from B8) + · rw [xor3_split] + left + exact ⟨h_X, h_notSY, h_notCarry_new⟩ + · have h_notC : ¬ Carry y X Y := not_carry_of_all_lt_mem_add h_prefix_one + have h_notY : y ∉ Y := by + simpa [h_y_eq_m] using hm.2.1 + have h_notX : y ∉ X := by + intro h_yX + apply h_y_notin_add + rw [ax_add] + constructor + · exact lt_of_lt_of_le (L1 h_yX) (show len X ≤ len X + len Y from B8) + · rw [xor3_split] + left + exact ⟨h_yX, h_notY, h_notC⟩ + have h_SY : y ∈ succ Y := by + simpa [h_y_eq_m] using succ_bit_eq hm + have h_notCarry_new : ¬ Carry y X (succ Y) := by + simpa [h_y_eq_m] using (not_carry_succ_of_lowest_zero_ge hm le_rfl) + rw [ax_add] + constructor + · exact lt_of_lt_of_le (L1 h_SY) (by + simp only [le_add_iff_nonneg_left, zero_le] + -- simpa [_root_.add_comm] using (show len (succ Y) ≤ len (succ Y) + len X from B8) + ) + · rw [xor3_split] + right + left + exact ⟨h_notX, h_SY, h_notCarry_new⟩ + · have h_m_in_add : m ∈ X + Y := h_prefix_one m h_m_lt_y + have h_m_notC : ¬ Carry m X Y := h_notCarry_prefix m (le_of_lt h_m_lt_y) + have h_mX : m ∈ X := by + rw [ax_add] at h_m_in_add + have h_m_xor := h_m_in_add.2 + rw [xor3_split] at h_m_xor + rcases h_m_xor with h1 | h2 | h3 | h4 + · exact h1.1 + · exact False.elim (hm.2.1 h2.2.1) + · exact False.elim (h_m_notC h3.2.2) + · exact False.elim (hm.2.1 h4.2.1) + have h_or_after_m : ∀ j, m < j -> j < y -> j ∈ X ∨ j ∈ Y := by + intro j h_m_lt_j h_j_lt_y + have h_j_in_add : j ∈ X + Y := h_prefix_one j h_j_lt_y + have h_j_notC : ¬ Carry j X Y := h_notCarry_prefix j (le_of_lt h_j_lt_y) + rw [ax_add] at h_j_in_add + have h_j_xor := h_j_in_add.2 + rw [xor3_split] at h_j_xor + rcases h_j_xor with h1 | h2 | h3 | h4 + · exact Or.inl h1.1 + · exact Or.inr h2.2.1 + · exact False.elim (h_j_notC h3.2.2) + · exact False.elim (h_j_notC h4.2.2) + have h_Carry_new : Carry y X (succ Y) := by + unfold Carry + refine ⟨m, h_m_lt_y, h_mX, succ_bit_eq hm, ?_⟩ + intro j h_j_lt_y h_m_lt_j + rcases h_or_after_m j h_m_lt_j h_j_lt_y with h_jX | h_jY + · exact Or.inl h_jX + · exact Or.inr ((succ_bit_gt hm j h_m_lt_j).2 h_jY) + have h_notC : ¬ Carry y X Y := not_carry_of_all_lt_mem_add h_prefix_one + have h_X_pos : (0 : num) < len X := len_pos_of_exists h_mX + have h_y_lt_new : y < len X + len (succ Y) := by + have h_pred_or : pred_y ∈ X ∨ pred_y ∈ succ Y := by + have h_y_maj : Maj (Carry pred_y X (succ Y)) (pred_y ∈ X) (pred_y ∈ succ Y) := by + have h_y_carry : Carry (pred_y + 1) X (succ Y) := by + simpa [hpred_y_eq] using h_Carry_new + exact (carry_rec (i := pred_y) (X := X) (Y := succ Y)).2.1 h_y_carry + unfold Maj at h_y_maj + rcases h_y_maj with h1 | h2 | h3 | h4 + · exact Or.inl h1.2.1 + · exact Or.inr h2.2.2 + · exact Or.inl h3.2.1 + · exact Or.inl h4.2.1 + rcases h_pred_or with h_predX | h_predSY + · have h_y_le_lenX : y ≤ len X := by + rw [<- hpred_y_eq, B11] + exact (add_lt_add_iff_right 1).mpr (L1 h_predX) + exact lt_of_le_of_lt h_y_le_lenX (lt_add_of_pos_right (len X) len_succ_pos) + · have h_y_le_lenSY : y ≤ len (succ Y) := by + rw [<- hpred_y_eq, B11] + exact (add_lt_add_iff_right 1).mpr (L1 h_predSY) + exact lt_of_le_of_lt h_y_le_lenSY (by + simpa [_root_.add_comm] using (lt_add_of_pos_right (len (succ Y)) h_X_pos)) + by_cases h_yY : y ∈ Y + · have h_X : y ∈ X := by + by_contra h_notX + apply h_y_notin_add + rw [ax_add] + constructor + · exact lt_of_lt_of_le (L1 h_yY) (by + simp only [le_add_iff_nonneg_left, zero_le] + -- simpa [_root_.add_comm] using (show len Y ≤ len Y + len X from B8) + ) + · rw [xor3_split] + right + left + exact ⟨h_notX, h_yY, h_notC⟩ + have h_SY : y ∈ succ Y := (succ_bit_gt hm y h_m_lt_y).2 h_yY + rw [ax_add] + constructor + · exact h_y_lt_new + · rw [xor3_split] + right + right + right + exact ⟨h_X, h_SY, h_Carry_new⟩ + · have h_notX : y ∉ X := by + intro h_X + apply h_y_notin_add + rw [ax_add] + constructor + · exact lt_of_lt_of_le (L1 h_X) (show len X ≤ len X + len Y from B8) + · rw [xor3_split] + left + exact ⟨h_X, h_yY, h_notC⟩ + have h_notSY : y ∉ succ Y := by + intro h_SY + exact h_yY ((succ_bit_gt hm y h_m_lt_y).1 h_SY) + rw [ax_add] + constructor + · exact h_y_lt_new + · rw [xor3_split] + right + right + left + exact ⟨h_notX, h_notSY, h_Carry_new⟩ + + + + + +lemma succ_len_eq : ∀ {X Y : str}, len (X + succ Y) = (len (succ (X + Y)) : num) := by + intro X Y + have h_new_le : len (X + succ Y) ≤ len (X + Y) + (1 : num) := by + by_contra h + have h_lt : len (X + Y) + (1 : num) < len (X + succ Y) := lt_of_not_ge h + obtain ⟨z, h_z_in, h_len_le_z, _⟩ := + exists_of_len_lt' (X := X + succ Y) (i := len (X + Y) + (1 : num)) h_lt + have h_len_lt_z : len (X + Y) < z := lt_of_lt_of_le (lt_succ (len (X + Y))) h_len_le_z + have h_z_notAdd : z ∉ X + Y := by + intro h_z_add + exact not_lt_self (len (X + Y)) (lt_trans h_len_lt_z (L1 h_z_add)) + exact not_mem_add_succ_of_not_mem_add_of_prefix_zero h_z_notAdd + ⟨len (X + Y), h_len_lt_z, len_not_in⟩ h_z_in + have h_top_iff : + len (X + Y) ∈ X + succ Y ↔ ∀ j < len (X + Y), j ∈ X + Y := by + constructor + · intro h_top + by_contra h_not_prefix + have h_prefix_zero : ∃ j < len (X + Y), j ∉ X + Y := by + by_contra h_no + apply h_not_prefix + intro j h_j_lt + by_contra h_j_not + exact h_no ⟨j, h_j_lt, h_j_not⟩ + exact not_mem_add_succ_of_not_mem_add_of_prefix_zero len_not_in h_prefix_zero h_top + · intro h_prefix_one + apply add_succ_of_succ_add + rw [ax_succ] + constructor + · exact le_rfl + · right + constructor + · exact len_not_in + · exact h_prefix_one + have h_succ_le_new : (len (succ (X + Y)) : num) ≤ len (X + succ Y) := by + by_contra h + have h_lt : len (X + succ Y) < len (succ (X + Y)) := lt_of_not_ge h + obtain ⟨z, h_z_in, h_z_notin, _⟩ := exists_of_len_lt h_lt + exact h_z_notin (add_succ_of_succ_add h_z_in) + by_cases h_top : len (X + Y) ∈ X + succ Y + · have h_top_succ : len (X + Y) ∈ succ (X + Y) := by + rw [ax_succ] + constructor + · exact le_rfl + · right + constructor + · exact len_not_in + · exact h_top_iff.mp h_top + have h_new_eq : len (X + succ Y) = len (X + Y) + (1 : num) := by + apply _root_.le_antisymm + · exact h_new_le + · rw [B11] + exact (add_lt_add_iff_right (1 : num)).mpr (L1 h_top) + have h_succ_eq : len (succ (X + Y)) = len (X + Y) + (1 : num) := by + apply _root_.le_antisymm + · exact len_succ_le_succ + · rw [B11] + exact (add_lt_add_iff_right (1 : num)).mpr (L1 h_top_succ) + rw [h_new_eq, h_succ_eq] + · have h_not_top_succ : len (X + Y) ∉ succ (X + Y) := by + intro h_top_succ + exact h_top (add_succ_of_succ_add h_top_succ) + have h_succ_eq : len (succ (X + Y)) = (len (X + Y) : num) := by + have h_succ_le_old : len (succ (X + Y)) ≤ (len (X + Y) : num) := by + by_contra h + have h_lt : len (X + Y) < len (succ (X + Y)) := lt_of_not_ge h + have h_ge : len (X + Y) + (1 : num) ≤ len (succ (X + Y)) := by + rw [B11] + exact (add_lt_add_iff_right (1 : num)).mpr h_lt + have h_eq : len (succ (X + Y)) = len (X + Y) + (1 : num) := + _root_.le_antisymm len_succ_le_succ h_ge + apply h_not_top_succ + apply L2 + exact h_eq.symm + exact _root_.le_antisymm h_succ_le_old len_le_len_succ + have h_new_eq : len (X + succ Y) = (len (X + Y) : num) := by + have h_old_le_new : (len (X + Y) : num) ≤ len (X + succ Y) := by + rw [<- h_succ_eq] + exact h_succ_le_new + have h_new_le_old : len (X + succ Y) ≤ (len (X + Y) : num) := by + by_contra h + have h_lt : len (X + Y) < len (X + succ Y) := lt_of_not_ge h + have h_ge : len (X + Y) + (1 : num) ≤ len (X + succ Y) := by + rw [B11] + exact (add_lt_add_iff_right (1 : num)).mpr h_lt + have h_eq : len (X + succ Y) = len (X + Y) + (1 : num) := _root_.le_antisymm h_new_le h_ge + apply h_top + apply L2 + exact h_eq.symm + exact _root_.le_antisymm h_new_le_old h_old_le_new + rw [h_new_eq, h_succ_eq] + + +lemma succ_add_of_add_succ : ∀ {X Y : str}, ∀ {y : num}, y ∈ X + succ Y -> y ∈ succ (X + Y) := by + intro X Y y hy + have h_y_lt_succ_old : y < len (succ (X + Y)) := by + have h := L1 hy + rw [succ_len_eq] at h + exact h + have h_y_le_old : y ≤ len (X + Y) := by + rw [B11] + exact lt_of_lt_of_le h_y_lt_succ_old len_succ_le_succ + rw [ax_succ] + constructor + · exact h_y_le_old + · by_cases h_add : y ∈ X + Y + · left + constructor + · exact h_add + · by_contra h_no_zero + have h_prefix_one : ∀ j < y, j ∈ X + Y := by + intro j h_j_lt + by_contra h_j_not + exact h_no_zero ⟨j, h_j_lt, h_j_not⟩ + exact (not_mem_add_succ_of_mem_add_of_prefix_one h_add h_prefix_one) hy + · right + constructor + · exact h_add + · by_contra h_not_prefix + have h_prefix_zero : ∃ j < y, j ∉ X + Y := by + by_contra h_no + apply h_not_prefix + intro j h_j_lt + by_contra h_j_not + exact h_no ⟨j, h_j_lt, h_j_not⟩ + exact (not_mem_add_succ_of_not_mem_add_of_prefix_zero h_add h_prefix_zero) hy + +theorem str_succ_assoc : ∀ {X Y : str}, X + succ Y = succ (X + Y) := by + intro X Y + apply M.SE + · exact succ_len_eq + · intro y y_lt + exact ⟨succ_add_of_add_succ, add_succ_of_succ_add⟩ diff --git a/LeanPool/projects.yml b/LeanPool/projects.yml index e5e7e0b2ea..42a8712baa 100644 --- a/LeanPool/projects.yml +++ b/LeanPool/projects.yml @@ -459,6 +459,7 @@ projects: - IOPENModel.add_assoc - V0Model.ind_of_comp - str_add_assoc + - str_succ_assoc main_results: - declaration: IOPENModel.add_assoc informal: Proves associativity of addition in IOPEN models. @@ -476,6 +477,8 @@ projects: informal: Proves commutativity of string addition in V0 extension models. - declaration: str_add_assoc informal: Proves associativity of string addition in V0 extension models. + - declaration: str_succ_assoc + informal: Proves that string addition associates with string successor in V0 extension models. tags: - logic - bounded-arithmetic From c09c2bd2ae07dbb24d2184b5c372e44314840ee4 Mon Sep 17 00:00:00 2001 From: Vasily Ilin Date: Wed, 20 May 2026 08:19:10 +0900 Subject: [PATCH 3/6] Clarify bounded arithmetic V0 assumptions --- LeanPool/FormalizationOfBoundedArithmetic/V0.lean | 8 +++++++- LeanPool/projects.yml | 12 ++++++------ 2 files changed, 13 insertions(+), 7 deletions(-) diff --git a/LeanPool/FormalizationOfBoundedArithmetic/V0.lean b/LeanPool/FormalizationOfBoundedArithmetic/V0.lean index 6566947b8c..822fee9e0c 100644 --- a/LeanPool/FormalizationOfBoundedArithmetic/V0.lean +++ b/LeanPool/FormalizationOfBoundedArithmetic/V0.lean @@ -43,7 +43,13 @@ open HasLen -- page 129, CN10: Finite axiomatizability of V0 -/-- Two-sorted models of the bounded-arithmetic theory `V0`. -/ +/-- +Two-sorted V0-style models used by this development. + +This is a strengthened bundled API: besides the finite V0 comprehension axioms, +it includes induction, order, and algebraic laws as fields so later files can +build the string-addition theory over a compact typeclass interface. +-/ class V0Model (num : Type) (str : outParam Type) extends diff --git a/LeanPool/projects.yml b/LeanPool/projects.yml index 362d36836d..a55ffdc746 100644 --- a/LeanPool/projects.yml +++ b/LeanPool/projects.yml @@ -575,7 +575,7 @@ projects: - "11H06" - slug: formalization-of-bounded-arithmetic title: Formalization of bounded arithmetic - summary: Formalizes first-order and two-sorted bounded-arithmetic model infrastructure, including induction principles and string-addition laws. + summary: Formalizes first-order and two-sorted bounded-arithmetic model infrastructure, including arithmetic model laws and string-addition laws for bundled V0-style structures with additional induction/order assumptions. branch: mathematical logic entry_module: LeanPool.FormalizationOfBoundedArithmetic authors: @@ -603,15 +603,15 @@ projects: - declaration: IDelta0Model.mul_cancel_right informal: Proves right cancellation for multiplication by a nonzero element in IDelta0 models. - declaration: V0Model.xind - informal: Derives string induction for V0 models from the comprehension axioms. + informal: Establishes string induction inside the bundled V0Model structure, whose fields include the comprehension and induction/order principles used downstream. - declaration: V0Model.ind_of_comp - informal: Derives propositional induction from comprehension in V0 models. + informal: Establishes propositional induction inside the bundled V0Model structure, rather than from only the raw finite V0 axiom list. - declaration: str_add_comm - informal: Proves commutativity of string addition in V0 extension models. + informal: Proves commutativity of string addition in V0 extension models extending the strengthened V0Model bundle. - declaration: str_add_assoc - informal: Proves associativity of string addition in V0 extension models. + informal: Proves associativity of string addition in V0 extension models extending the strengthened V0Model bundle. - declaration: str_succ_assoc - informal: Proves that string addition associates with string successor in V0 extension models. + informal: Proves that string addition associates with string successor in V0 extension models extending the strengthened V0Model bundle. tags: - logic - bounded-arithmetic From e99fc52492af6ffa254b3b8cfb8963c4665e6805 Mon Sep 17 00:00:00 2001 From: Vasily Ilin Date: Wed, 20 May 2026 09:01:53 +0900 Subject: [PATCH 4/6] Clarify bounded arithmetic strengthened V0 interface --- .../FormalizationOfBoundedArithmetic.lean | 2 +- .../V0StrAddAssoc.lean | 23 ++++++++++++------- LeanPool/projects.yml | 10 ++++---- 3 files changed, 21 insertions(+), 14 deletions(-) diff --git a/LeanPool/FormalizationOfBoundedArithmetic.lean b/LeanPool/FormalizationOfBoundedArithmetic.lean index 0f49d7bd41..1af5fc8b67 100644 --- a/LeanPool/FormalizationOfBoundedArithmetic.lean +++ b/LeanPool/FormalizationOfBoundedArithmetic.lean @@ -26,7 +26,7 @@ import LeanPool.FormalizationOfBoundedArithmetic.V0StrAddComm import LeanPool.FormalizationOfBoundedArithmetic.V0StrSuccAssoc /-! -# Formalization of bounded arithmetic +# Bounded Arithmetic Model Interfaces Source: doi:10.1017/CBO9780511676277 Authors: ruplet diff --git a/LeanPool/FormalizationOfBoundedArithmetic/V0StrAddAssoc.lean b/LeanPool/FormalizationOfBoundedArithmetic/V0StrAddAssoc.lean index 08832fc556..b0050336bd 100644 --- a/LeanPool/FormalizationOfBoundedArithmetic/V0StrAddAssoc.lean +++ b/LeanPool/FormalizationOfBoundedArithmetic/V0StrAddAssoc.lean @@ -44,10 +44,13 @@ def CarryAssocPred (X Y Z : str) (i : num) : Prop := ((Carry i Y Z ∧ Carry i X (Y + Z)) ↔ (Carry i X Y ∧ Carry i (X + Y) Z)) ∧ (Xor' (Carry i Y Z) (Carry i X (Y + Z)) ↔ Xor' (Carry i X Y) (Carry i (X + Y) Z)) -/- -This is the only induction instance assumed here for proving associativity of string -addition. The displayed predicate is exactly the stronger Cook–Nguyen carry invariant, -and it is built from bounded formulas already present in `V0`. +/-- +Induction step supplied by the strengthened `V0Model` interface. + +This calls the bundled field `V0Model.prop_induction_ax`. The displayed +predicate is the stronger Cook–Nguyen carry invariant built from bounded +formulas, but this file does not derive the induction principle from a separate +raw V0 axiom class. -/ lemma carry_assoc_induction : ∀ {X Y Z : str}, @@ -100,10 +103,14 @@ lemma carry_pair_assoc : ∀ {X Y Z : str}, ∀ {i : num}, exact hφ i --- For Associativity, first show in V0(+) that --- Carry(i, Y, Z) ⊕ Carry(i, X, Y + Z) ↔ --- Carry(i, X, Y ) ⊕ Carry(i, X + Y, Z). --- Derive a stronger statement than this, and prove it by induction on i. +/-- +Associativity of string addition for `V0ExtModel`. + +The theorem is stated for the enriched extension model whose parent `V0Model` +already bundles the propositional induction/order/algebra fields used above. +It is not advertised here as a derivation from only the raw finite V0 +comprehension axioms. +-/ theorem str_add_assoc : ∀ {X Y Z : str}, (X + Y) + Z = X + (Y + Z) := by intro X Y Z refine str_eq_of_mem_iff (num := num) (str := str) (X := (X + Y) + Z) (Y := X + (Y + Z)) ?_ diff --git a/LeanPool/projects.yml b/LeanPool/projects.yml index a55ffdc746..dcbf07485a 100644 --- a/LeanPool/projects.yml +++ b/LeanPool/projects.yml @@ -574,8 +574,8 @@ projects: - "11E25" - "11H06" - slug: formalization-of-bounded-arithmetic - title: Formalization of bounded arithmetic - summary: Formalizes first-order and two-sorted bounded-arithmetic model infrastructure, including arithmetic model laws and string-addition laws for bundled V0-style structures with additional induction/order assumptions. + title: Bounded Arithmetic Model Interfaces + summary: Formalizes first-order and two-sorted bounded-arithmetic model infrastructure, including arithmetic model laws and string-addition laws for strengthened bundled V0-style interfaces with propositional induction, order, cancellation, decidability, and algebraic laws assumed as fields rather than derived from a separate raw V0 class. branch: mathematical logic entry_module: LeanPool.FormalizationOfBoundedArithmetic authors: @@ -603,13 +603,13 @@ projects: - declaration: IDelta0Model.mul_cancel_right informal: Proves right cancellation for multiplication by a nonzero element in IDelta0 models. - declaration: V0Model.xind - informal: Establishes string induction inside the bundled V0Model structure, whose fields include the comprehension and induction/order principles used downstream. + informal: Exposes string induction inside the strengthened bundled V0Model structure, whose fields include the comprehension and induction/order principles used downstream. - declaration: V0Model.ind_of_comp - informal: Establishes propositional induction inside the bundled V0Model structure, rather than from only the raw finite V0 axiom list. + informal: Exposes propositional induction inside the strengthened bundled V0Model structure, rather than deriving it from only the raw finite V0 axiom list. - declaration: str_add_comm informal: Proves commutativity of string addition in V0 extension models extending the strengthened V0Model bundle. - declaration: str_add_assoc - informal: Proves associativity of string addition in V0 extension models extending the strengthened V0Model bundle. + informal: Proves associativity of string addition in V0 extension models extending the strengthened V0Model bundle, using the bundled propositional induction field. - declaration: str_succ_assoc informal: Proves that string addition associates with string successor in V0 extension models extending the strengthened V0Model bundle. tags: From 1436485e73d7b62cb4e448f838d842d1875a0942 Mon Sep 17 00:00:00 2001 From: Vasily Ilin Date: Wed, 20 May 2026 09:20:40 +0900 Subject: [PATCH 5/6] Use strengthened V0 aliases in bounded arithmetic metadata --- LeanPool/FormalizationOfBoundedArithmetic.lean | 2 +- LeanPool/FormalizationOfBoundedArithmetic/V0.lean | 6 ++++++ .../V0StrAddAssoc.lean | 4 ++++ .../V0StrAddComm.lean | 4 ++++ .../V0StrSuccAssoc.lean | 4 ++++ LeanPool/projects.yml | 14 ++++++-------- 6 files changed, 25 insertions(+), 9 deletions(-) diff --git a/LeanPool/FormalizationOfBoundedArithmetic.lean b/LeanPool/FormalizationOfBoundedArithmetic.lean index 1af5fc8b67..20563b56a4 100644 --- a/LeanPool/FormalizationOfBoundedArithmetic.lean +++ b/LeanPool/FormalizationOfBoundedArithmetic.lean @@ -31,7 +31,7 @@ import LeanPool.FormalizationOfBoundedArithmetic.V0StrSuccAssoc Source: doi:10.1017/CBO9780511676277 Authors: ruplet Status: verified -Main declarations: `IOPENModel.add_assoc`, `V0Model.ind_of_comp`, `str_add_assoc`, `str_succ_assoc` +Main declarations: `V0Model.ind_strengthened_v0`, `str_add_assoc_strengthened_v0` Tags: logic, bounded-arithmetic, model-theory, computational-complexity MSC: 03F30, 03D15 -/ diff --git a/LeanPool/FormalizationOfBoundedArithmetic/V0.lean b/LeanPool/FormalizationOfBoundedArithmetic/V0.lean index 822fee9e0c..7df0419b9d 100644 --- a/LeanPool/FormalizationOfBoundedArithmetic/V0.lean +++ b/LeanPool/FormalizationOfBoundedArithmetic/V0.lean @@ -544,6 +544,12 @@ by · exact hzX · exact lt_succ z +/-- Named alias emphasizing that this induction theorem uses the strengthened `V0Model` bundle. -/ +theorem ind_strengthened_v0 (P : num -> Prop) : + (∀ y : num, ∃ Y : str, (len Y : num) ≤ y ∧ ∀ z < y, z ∈ Y ↔ P z) + -> (P 0 -> (∀ x, P x -> P (x + 1)) -> ∀ x, P x) := + ind_of_comp P + instance : IDelta0Model num where open_induction phi h_open := M.open_induction_ax phi h_open diff --git a/LeanPool/FormalizationOfBoundedArithmetic/V0StrAddAssoc.lean b/LeanPool/FormalizationOfBoundedArithmetic/V0StrAddAssoc.lean index b0050336bd..3168ef6505 100644 --- a/LeanPool/FormalizationOfBoundedArithmetic/V0StrAddAssoc.lean +++ b/LeanPool/FormalizationOfBoundedArithmetic/V0StrAddAssoc.lean @@ -120,3 +120,7 @@ theorem str_add_assoc : ∀ {X Y Z : str}, (X + Y) + Z = X + (Y + Z) := by rw [mem_add_iff_xor (X := X) (Y := Y) (i := i)] rw [mem_add_iff_xor (X := Y) (Y := Z) (i := i)] exact add_assoc_bit_bool (carry_pair_assoc (X := X) (Y := Y) (Z := Z) (i := i)).2 + +/-- Named alias emphasizing that this theorem is conditional on the strengthened V0 extension. -/ +theorem str_add_assoc_strengthened_v0 : ∀ {X Y Z : str}, (X + Y) + Z = X + (Y + Z) := + str_add_assoc diff --git a/LeanPool/FormalizationOfBoundedArithmetic/V0StrAddComm.lean b/LeanPool/FormalizationOfBoundedArithmetic/V0StrAddComm.lean index be3a1e90d1..b577493d7f 100644 --- a/LeanPool/FormalizationOfBoundedArithmetic/V0StrAddComm.lean +++ b/LeanPool/FormalizationOfBoundedArithmetic/V0StrAddComm.lean @@ -64,3 +64,7 @@ theorem str_add_comm : ∀ {X Y : str}, X + Y = Y + X := by rw [carry_comm (X := X) (Y := Y) (i := i)] unfold Xor' tauto + +/-- Named alias emphasizing that this theorem is conditional on the strengthened V0 extension. -/ +theorem str_add_comm_strengthened_v0 : ∀ {X Y : str}, X + Y = Y + X := + str_add_comm diff --git a/LeanPool/FormalizationOfBoundedArithmetic/V0StrSuccAssoc.lean b/LeanPool/FormalizationOfBoundedArithmetic/V0StrSuccAssoc.lean index 7093082be6..aeefdc16ee 100644 --- a/LeanPool/FormalizationOfBoundedArithmetic/V0StrSuccAssoc.lean +++ b/LeanPool/FormalizationOfBoundedArithmetic/V0StrSuccAssoc.lean @@ -1185,3 +1185,7 @@ theorem str_succ_assoc : ∀ {X Y : str}, X + succ Y = succ (X + Y) := by · exact succ_len_eq · intro y y_lt exact ⟨succ_add_of_add_succ, add_succ_of_succ_add⟩ + +/-- Named alias emphasizing that this theorem is conditional on the strengthened V0 extension. -/ +theorem str_succ_assoc_strengthened_v0 : ∀ {X Y : str}, X + succ Y = succ (X + Y) := + str_succ_assoc diff --git a/LeanPool/projects.yml b/LeanPool/projects.yml index dcbf07485a..3d059dff35 100644 --- a/LeanPool/projects.yml +++ b/LeanPool/projects.yml @@ -589,10 +589,8 @@ projects: github_repo: ruplet/formalization-of-bounded-arithmetic status: verified main_declarations: - - IOPENModel.add_assoc - - V0Model.ind_of_comp - - str_add_assoc - - str_succ_assoc + - V0Model.ind_strengthened_v0 + - str_add_assoc_strengthened_v0 main_results: - declaration: IOPENModel.add_assoc informal: Proves associativity of addition in IOPEN models. @@ -604,13 +602,13 @@ projects: informal: Proves right cancellation for multiplication by a nonzero element in IDelta0 models. - declaration: V0Model.xind informal: Exposes string induction inside the strengthened bundled V0Model structure, whose fields include the comprehension and induction/order principles used downstream. - - declaration: V0Model.ind_of_comp + - declaration: V0Model.ind_strengthened_v0 informal: Exposes propositional induction inside the strengthened bundled V0Model structure, rather than deriving it from only the raw finite V0 axiom list. - - declaration: str_add_comm + - declaration: str_add_comm_strengthened_v0 informal: Proves commutativity of string addition in V0 extension models extending the strengthened V0Model bundle. - - declaration: str_add_assoc + - declaration: str_add_assoc_strengthened_v0 informal: Proves associativity of string addition in V0 extension models extending the strengthened V0Model bundle, using the bundled propositional induction field. - - declaration: str_succ_assoc + - declaration: str_succ_assoc_strengthened_v0 informal: Proves that string addition associates with string successor in V0 extension models extending the strengthened V0Model bundle. tags: - logic From 13a56344acaa782b39d0e9471f09960f6104347f Mon Sep 17 00:00:00 2001 From: Vasily Ilin Date: Wed, 20 May 2026 09:32:29 +0900 Subject: [PATCH 6/6] Title bounded arithmetic as strengthened V0 interfaces --- LeanPool/FormalizationOfBoundedArithmetic.lean | 2 +- LeanPool/projects.yml | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/LeanPool/FormalizationOfBoundedArithmetic.lean b/LeanPool/FormalizationOfBoundedArithmetic.lean index 20563b56a4..6afb66a9cf 100644 --- a/LeanPool/FormalizationOfBoundedArithmetic.lean +++ b/LeanPool/FormalizationOfBoundedArithmetic.lean @@ -26,7 +26,7 @@ import LeanPool.FormalizationOfBoundedArithmetic.V0StrAddComm import LeanPool.FormalizationOfBoundedArithmetic.V0StrSuccAssoc /-! -# Bounded Arithmetic Model Interfaces +# Strengthened V0 Bounded Arithmetic Interfaces Source: doi:10.1017/CBO9780511676277 Authors: ruplet diff --git a/LeanPool/projects.yml b/LeanPool/projects.yml index 3d059dff35..f001c78de7 100644 --- a/LeanPool/projects.yml +++ b/LeanPool/projects.yml @@ -574,7 +574,7 @@ projects: - "11E25" - "11H06" - slug: formalization-of-bounded-arithmetic - title: Bounded Arithmetic Model Interfaces + title: Strengthened V0 Bounded Arithmetic Interfaces summary: Formalizes first-order and two-sorted bounded-arithmetic model infrastructure, including arithmetic model laws and string-addition laws for strengthened bundled V0-style interfaces with propositional induction, order, cancellation, decidability, and algebraic laws assumed as fields rather than derived from a separate raw V0 class. branch: mathematical logic entry_module: LeanPool.FormalizationOfBoundedArithmetic