-- 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 BoundedArithmetic.BasicSingleSorted import BoundedArithmetic.IOPEN import BoundedArithmetic.IDelta0 import BoundedArithmetic.DisplayedVariables import BoundedArithmetic.Complexity import BoundedArithmetic.Algebra import BoundedArithmetic.AxiomSchemes import BoundedArithmetic.Register open FirstOrder Language open HasTypes_is open HasEmptySet open HasLen -- page 129, CN10: Finite axiomatizability of 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) -- 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 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 instance : AddCommMonoid num where add_comm := add_comm instance : PartialOrder num where le_antisymm := le_antisymm instance : IsOrderedAddMonoid num where add_le_add_left := add_le_add_left theorem xmin_comp (X : str) : ∃ Y : str, (len Y : num) ≤ len X ∧ ∀ z < len X, z ∈ Y ↔ ∀ y ≤ z, y ∉ X := by sorry 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 symm rw [<- h] rw [@right_eq_add] 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 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 intro 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 sorry 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 x := sorry delta0_induction phi h_delta0 x := sorry 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] class HasSucc.{u} (α : Type u) where succ : α -> α 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))) 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 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 constructor; rw [<- B11]; exact c_lt.1 constructor; exact cx constructor; exact cy 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 apply cprev apply lt_of_le_of_ne rw [B11]; exact hlt exact hji exact 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 constructor · exact lt_succ i · constructor; assumption constructor; assumption 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 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 constructor; assumption constructor; assumption constructor; assumption intro j hj apply prevs apply lt_trans hj exact lt_succ i · rw [Maj_true3 h_iY] left unfold Carry exists pos constructor; assumption constructor; assumption constructor; assumption 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 := ne_zero_of_lt h_lt (α := num) 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 constructor exact pred_in symm constructor exact 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 := ne_zero_of_lt h_lt (α := num) 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 constructor exact pred_in symm constructor exact 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 apply lt_of_le_of_lt apply zero_le i apply L1 assumption 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 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)