Modifying the duper branch to match the main branch

Auto/Embedding/LamBitVec.lean

@@ -47,23 +47,47 @@ namespace BitVec
 
   theorem toNat_shiftLeft {a : Std.BitVec n} (i : Nat) : (a <<< i).toNat = (a.toNat * (2 ^ i)) % (2 ^ n) := by
     rw [shiftLeft_def]; rcases a with ⟨⟨a, isLt⟩⟩
-    dsimp [Std.BitVec.shiftLeft, Std.BitVec.toNat, Std.BitVec.ofNat, Fin.ofNat']
-    rw [Nat.shiftLeft_eq]
+    unfold Std.BitVec.shiftLeft Std.BitVec.toNat Std.BitVec.ofNat Fin.ofNat'
+    dsimp; rw [Nat.shiftLeft_eq]
 
   theorem toNat_ushiftRight {a : Std.BitVec n} (i : Nat) : (a >>> i).toNat = (a.toNat) / (2 ^ i) := by
     rw [ushiftRight_def]; rcases a with ⟨⟨a, isLt⟩⟩
-    dsimp [ushiftRight, Std.BitVec.toNat, Std.BitVec.ofNat, Fin.ofNat']
-    rw [Nat.mod_eq_of_lt, Nat.shiftRight_eq_div_pow]
+    unfold ushiftRight Std.BitVec.toNat Std.BitVec.ofNat Fin.ofNat'
+    dsimp; rw [Nat.mod_eq_of_lt, Nat.shiftRight_eq_div_pow]
     apply Nat.le_trans (Nat.succ_le_succ _) isLt
     rw [Nat.shiftRight_eq_div_pow]; apply Nat.div_le_self
 
-  theorem toNat_zeroExtend {a : Std.BitVec n} (i : Nat) : (a.zeroExtend i).toNat = a.toNat % (2 ^ i) := rfl
+  theorem toNat_zeroExtend' {a : Std.BitVec n} (le : n ≤ m) : (a.zeroExtend' le).toNat = a.toNat := rfl
+
+  theorem toNat_zeroExtend {a : Std.BitVec n} (i : Nat) : (a.zeroExtend i).toNat = a.toNat % (2 ^ i) := by
+    unfold zeroExtend; cases hdec : decide (n ≤ i)
+    case false =>
+      have hnle := of_decide_eq_false hdec
+      rw [Bool.dite_eq_false (proof:=hnle)]; rfl
+    case true =>
+      have hle := of_decide_eq_true hdec
+      rw [Bool.dite_eq_true (proof:=hle), toNat_zeroExtend']
+      rw [Nat.mod_eq_of_lt]; rcases a with ⟨⟨a, isLt⟩⟩;
+      apply Nat.le_trans isLt; apply Nat.pow_le_pow_of_le_right (Nat.le_step .refl) hle
 
   theorem toNat_sub (a b : Std.BitVec n) : (a - b).toNat = (a.toNat + (2 ^ n - b.toNat)) % (2 ^ n) := rfl
 
   theorem toNat_neg (a : Std.BitVec n) : (-a).toNat = (2^n - a.toNat) % (2^n) := by
-    rw [neg_def]; dsimp [Std.BitVec.neg]
-    rw [← sub_def, toNat_sub, toNat_ofNat, Nat.zero_mod, Nat.zero_add]
+    rw [neg_def]; unfold Std.BitVec.neg;
+    rw [← sub_def, toNat_sub]; dsimp
+    rw [toNat_ofNat, Nat.zero_mod, Nat.zero_add]
+
+  theorem toNat_and (a b : Std.BitVec n) : (a &&& b).toNat = a.toNat &&& b.toNat := rfl
+
+  theorem toNat_or (a b : Std.BitVec n) : (a ||| b).toNat = a.toNat ||| b.toNat := rfl
+
+  theorem toNat_xor (a b : Std.BitVec n) : (a ^^^ b).toNat = a.toNat ^^^ b.toNat := rfl
+
+  theorem toNat_not_aux (a : Std.BitVec n) : (~~~a).toNat = (1 <<< n).pred ^^^ a.toNat := rfl
+
+  theorem toNat_not (a : Std.BitVec n) : (~~~a).toNat = 2 ^ n - 1 - a.toNat := by
+    rw [toNat_not_aux]; rw [Nat.shiftLeft_eq, Nat.one_mul, ← Nat.sub_one, Nat.ones_xor]
+    rcases a with ⟨⟨_, isLt⟩⟩; exact isLt
 
   theorem shiftLeft_ge_length_eq_zero (a : Std.BitVec n) (i : Nat) : i ≥ n → a <<< i = 0#n := by
     intro h; apply eq_of_val_eq; rw [toNat_shiftLeft, toNat_ofNat]; apply Nat.mod_eq_zero_of_dvd
@@ -86,15 +110,17 @@ namespace BitVec
         rw [Nat.shiftRight_eq_div_pow]; apply (Nat.le_iff_div_eq_zero (Nat.pow_two_pos _)).mpr
         rw [Nat.pred_lt_iff_le (Nat.pow_two_pos _)]
         apply Nat.le_trans (Nat.sub_le _ _) (Nat.pow_le_pow_of_le_right (.step .refl) h)
-      rw [hzero, Nat.zero_mod, Nat.sub_zero]; apply eq_of_val_eq
-      rw [toNat_ofNat, ← neg_def, toNat_neg, toNat_ofNat]
+      rw [hzero]; apply eq_of_val_eq; rw [toNat_not]
+      rw [toNat_ofNat, toNat_neg, toNat_ofNat, Nat.zero_mod, Nat.sub_zero]
       cases n <;> try rfl
-      case succ =>
-        rw [Nat.mod_eq_of_lt (a:=1)]
-        apply @Nat.pow_le_pow_of_le_right 2 (.step .refl) 1 _ (Nat.succ_le_succ (Nat.zero_le _))
+      case succ n =>
+        have hlt : 2 ≤ 2 ^ Nat.succ n := @Nat.pow_le_pow_of_le_right 2 (.step .refl) 1 (.succ n) (Nat.succ_le_succ (Nat.zero_le _))
+        rw [Nat.mod_eq_of_lt (a:=1) hlt]
+        rw [Nat.mod_eq_of_lt]; apply Nat.sub_lt (Nat.le_trans (.step .refl) hlt) .refl
 
   theorem shiftRight_eq_zero_iff (a : Std.BitVec n) (b : Nat) : a >>> b = 0#n ↔ a.toNat < 2 ^ b := by
-    rw [ushiftRight_def]; rcases a with ⟨⟨a, isLt⟩⟩; dsimp [ushiftRight, Std.BitVec.toNat]
+    rw [ushiftRight_def]; rcases a with ⟨⟨a, isLt⟩⟩;
+    unfold ushiftRight; dsimp [Std.BitVec.toNat]
     rw [eq_iff_val_eq, toNat_ofNat, toNat_ofNat, Nat.zero_mod, Nat.shiftRight_eq_div_pow]
     apply Iff.intro <;> intro h
     case mp =>
@@ -107,6 +133,9 @@ namespace BitVec
       case inr h => cases h; rw [Nat.mul_zero] at hdvd; apply (Nat.le_iff_div_eq_zero (Nat.pow_two_pos _)).mp hdvd
     case mpr => rw [(Nat.le_iff_div_eq_zero (Nat.pow_two_pos _)).mpr h]; rfl
 
+  theorem ofNat_toNat (a : Std.BitVec n) : .ofNat m a.toNat = a.zeroExtend m := by
+    apply eq_of_val_eq; rw [toNat_ofNat, toNat_zeroExtend]
+
   theorem ofNat_add (n a b : Nat) : (a + b)#n = a#n + b#n := by
     apply congrArg (f:=Std.BitVec.ofFin); apply Fin.eq_of_val_eq
     dsimp [Fin.ofNat']; rw [Nat.add_mod]; rfl
@@ -286,7 +315,8 @@ theorem LamEquiv.bvofNat_bvtoNat
     (.mkBvofNat m (.mkBvUOp n (.bvtoNat n) t))
     (.app (.base (.bv n)) (.base (.bvzeroExtend n m)) t) :=
   ⟨.mkBvofNat (.mkBvUOp (.ofBvtoNat n) wft),
-   .ofApp _ (.ofBase (.ofBvzeroExtend n m)) wft, fun lctxTerm => rfl⟩
+   .ofApp _ (.ofBase (.ofBvzeroExtend n m)) wft, fun lctxTerm => by
+    apply GLift.down.inj; apply BitVec.ofNat_toNat⟩
 
 theorem LamEquiv.bvofNat_nadd
   (wfa : LamWF lval.toLamTyVal ⟨lctx, a, .base .nat⟩)

Auto/Embedding/LamChecker.lean

@@ -3,8 +3,7 @@ import Auto.Embedding.LamConv
 import Auto.Embedding.LamInference
 import Auto.Embedding.LamLCtx
 import Auto.Embedding.LamPrep
--- Temporarily removing this input until I can get this file to build on Lean v4.4.0-rc1
--- import Auto.Embedding.BitVec
+import Auto.Embedding.LamBitVec
 import Auto.Embedding.LamInductive
 import Auto.Lib.BinTree
 open Lean
@@ -602,10 +601,8 @@ inductive PrepConvStep where
   | validOfPropEq : PrepConvStep
   /-- (a = b) ↔ (a ∨ b) ∧ (¬ a ∨ ¬ b) -/
   | validOfPropNe : PrepConvStep
-  /- Temporarily removing this operation until I can get Auto.Embedding.BitVec to build on Lean v4.4.0-rc1
   /-- Basic BitVec simplification operations -/
   | validOfPushBVCast : PrepConvStep
-  -/
   deriving Inhabited, Hashable, BEq, Lean.ToExpr
 
 inductive WFStep where
@@ -706,9 +703,7 @@ def PrepConvStep.toString : PrepConvStep → String
 | .validOfNotImpEquivAndNot => s!"validOfNotImpEquivAndNot"
 | .validOfPropEq => s!"validOfPropEq"
 | .validOfPropNe => s!"validOfPropNe"
-/- Temporarily removing this operation until I can get Auto.Embedding.BitVec to build on Lean v4.4.0-rc1
 | .validOfPushBVCast => s!"validOfPushBVCast"
--/
 
 def WFStep.toString : WFStep → String
 | .wfOfCheck lctx t => s!"wfOfCheck {lctx} {t}"
@@ -1150,9 +1145,7 @@ def InferenceStep.evalValidOfBVarLowers (r : RTable) (lctx : List LamSort) (pns
 | .validOfNotImpEquivAndNot => LamTerm.not_imp_equiv_and_not?
 | .validOfPropEq => LamTerm.propeq?
 | .validOfPropNe => LamTerm.propne?
-/- Temporarily removing this operation until I can get Auto.Embedding.BitVec to build on Lean v4.4.0-rc1
 | .validOfPushBVCast => fun t => LamTerm.pushBVCast .none t
--/
 
 @[reducible] def WFStep.eval (lvt lit : Nat → LamSort) (r : RTable) : (cs : WFStep) → EvalResult
 | .wfOfCheck lctx t =>
@@ -2117,11 +2110,9 @@ theorem PrepConvStep.eval_correct (lval : LamValuation) :
 | .validOfPropNe => And.intro
   LamGenConv.propne?
   (LamTerm.evarBounded_of_evarEquiv @LamTerm.maxEVarSucc_propne?)
-/- Temporarily removing this operation until I can get Auto.Embedding.BitVec to build on Lean v4.4.0-rc1
 | .validOfPushBVCast => And.intro
   LamGenConv.pushBVCast
   (LamTerm.evarBounded_of_evarEquiv LamTerm.evarEquiv_pushBVCast)
--/
 
 theorem WFStep.eval_correct
   (r : RTable) (cv : CVal.{u} r.lamEVarTy) (inv : r.inv cv) :
@@ -2339,7 +2330,7 @@ theorem Checker.getValidExport_indirectReduceAux
     apply congrFun; apply congrArg; rw [hlit, BinTree.get?_mapOpt]
     apply Eq.symm; apply Option.map_eq_bind
   rw [lvtEq, litEq] at runEq; cases runEq; apply ChkSteps.run_correct
-  dsimp [RTable.inv, BinTree.get?]
+  unfold RTable.inv BinTree.get?
   exists fun _ => BinTree.get?'_leaf _ ▸ GLift.up False
   cases hImport; apply ImportTable.importFacts_correct
 

Auto/Embedding/Lift.lean

@@ -185,6 +185,18 @@ def bvsltLift.{u} (n : Nat) (x y : GLift.{1, u} (Std.BitVec n)) : GLift.{1, u} B
 def bvsleLift.{u} (n : Nat) (x y : GLift.{1, u} (Std.BitVec n)) : GLift.{1, u} Bool :=
   GLift.up (Std.BitVec.sle x.down y.down)
 
+def bvpropultLift.{u} (n : Nat) (x y : GLift.{1, u} (Std.BitVec n)) : GLift.{1, u} Prop :=
+  GLift.up (x.down.toFin < y.down.toFin)
+
+def bvpropuleLift.{u} (n : Nat) (x y : GLift.{1, u} (Std.BitVec n)) : GLift.{1, u} Prop :=
+  GLift.up (x.down.toFin <= y.down.toFin)
+
+def bvpropsltLift.{u} (n : Nat) (x y : GLift.{1, u} (Std.BitVec n)) : GLift.{1, u} Prop :=
+  GLift.up (x.down.toInt < y.down.toInt)
+
+def bvpropsleLift.{u} (n : Nat) (x y : GLift.{1, u} (Std.BitVec n)) : GLift.{1, u} Prop :=
+  GLift.up (x.down.toInt <= y.down.toInt)
+
 def bvandLift.{u} (n : Nat) (x y : GLift.{1, u} (Std.BitVec n)) : GLift.{1, u} (Std.BitVec n) :=
   GLift.up (Std.BitVec.and x.down y.down)
 

Auto/Lib/BinTree.lean

@@ -432,7 +432,7 @@ theorem allp'_node (p : α → Prop) :
         have h' := h (2 * n + 5)
         rw [get?'_succSucc] at h'
         have eq₁ : (2 * n + 5) % 2 = 1 := by
-          rw [Nat.add_mod]; simp; rfl
+          simp [Nat.add_mod]; rfl
         have eq₂ : (2 * n + 5) / 2 = n + 2 := by
           rw [Nat.add_comm _ 5];
           rw [Nat.add_mul_div_left];

Auto/Lib/BoolExtra.lean

@@ -15,7 +15,7 @@ theorem Bool.eq_false_of_ne_true {a : Bool} : a ≠ true → a = false := by
 theorem Bool.ne_true_of_eq_false {a : Bool} : a = false → a ≠ true := by
   cases a <;> decide
 
-theorem Bool.eq_false_eq_not_eq_true {a : Bool} : (a ≠ true) = (a = false) := by
+theorem Bool.eq_false_eq_not_eq_true {a : Bool} : (a = false) = (a ≠ true) := by
   cases a <;> decide
 
 theorem Bool.and_eq_false (a b : Bool) : ((a && b) = false) = ((a = false) ∨ (b = false)) := by
@@ -53,6 +53,16 @@ theorem Bool.ite_eq_false (p : Prop) [inst : Decidable p] (a b : α) : ¬ p →
   case isFalse _ => rfl
   case isTrue hp => apply False.elim (hnp hp)
 
+theorem Bool.dite_eq_true (p : Prop) [inst : Decidable p] (a : p → α) (b : ¬ p → α) (proof : p) : dite p a b = a proof := by
+  dsimp [dite]; cases inst
+  case isFalse hnp => apply False.elim (hnp proof)
+  case isTrue _ => rfl
+
+theorem Bool.dite_eq_false (p : Prop) [inst : Decidable p] (a : p → α) (b : ¬ p → α) (proof : ¬ p) : dite p a b = b proof := by
+  dsimp [dite]; cases inst
+  case isFalse _ => rfl
+  case isTrue hp => apply False.elim (proof hp)
+
 /--
   Similar to `ite`, but does not have complicated dependent types
 -/

Auto/Lib/NatExtra.lean

@@ -1,4 +1,6 @@
 import Std.Data.Nat.Lemmas
+import Std.Data.Nat.Bitwise
+import Auto.Lib.BoolExtra
 
 namespace Auto
 
@@ -86,6 +88,8 @@ theorem Nat.le_max_iff (m n k : Nat) : k ≤ max m n ↔ k ≤ m ∨ k ≤ n :=
     case inl h => exact Nat.le_trans h (Nat.le_max_left _ _)
     case inr h => exact Nat.le_trans h (Nat.le_max_right _ _)
 
+theorem Nat.lt_eq_succ_le {m n : Nat} : n < m ↔ .succ n ≤ m := by rfl
+
 theorem Nat.gt_eq_succ_le {m n : Nat} : m > n ↔ .succ n ≤ m := by rfl
 
 theorem Nat.le_pred_of_succ_le {n m : Nat} : m > 0 → Nat.succ n ≤ m → n ≤ Nat.pred m :=
@@ -109,8 +113,8 @@ theorem Nat.max_add {a b c : Nat} : max a b + c = max (a + c) (b + c) := by
     simp [h, naleb]
 
 theorem Nat.max_lt {a b c : Nat} : max a b < c ↔ a < c ∧ b < c := by
-  rw [← Nat.lt_eq, Nat.lt]; dsimp only [Nat.le_eq]; rw [← Nat.add_one];
-  rw [Nat.max_add]; rw [Nat.max_le]; apply Iff.intro id id
+  rw [show (max a b < c ↔ max a b + 1 ≤ c) by rfl, Nat.max_add, Nat.max_le]
+  apply Iff.intro id id
 
 theorem Nat.max_zero_left {a : Nat} : max 0 a = a := by
   rw [Nat.max_def]; simp
@@ -176,4 +180,122 @@ theorem Nat.le_pow (h : b ≥ 2) : a < b ^ a := by
     rw [Nat.mul_two, Nat.succ_add]
     apply Nat.succ_le_succ; apply Nat.succ_le_succ; apply Nat.le_add_left
 
+  theorem Nat.mod_par {a b c : Nat} (h : a % b = c) : ∃ d, a = b * d + c := by
+    exists (a / b); rw [← h, Nat.div_add_mod]
+
+  theorem Nat.div_par {a b c : Nat} (h : a / b = c) (hnz : b > 0) : ∃ d, a = b * c + d ∧ d < b := by
+    exists (a % b); rw [← h, Nat.div_add_mod]; apply And.intro rfl; apply Nat.mod_lt _ hnz
+
+  theorem Nat.le_par {a b : Nat} (h : a ≤ b) : ∃ c, b = a + c := by
+    exists (b - a); rw [Nat.add_comm, Nat.sub_add_cancel h]
+
+  theorem Nat.lt_par {a b : Nat} (h : a < b) : ∃ c, b = (a + 1) + c := Nat.le_par h
+
+  theorem Nat.sub_mod (a b n : Nat) (h : a ≥ b) : (a - b) % n = (a - b % n) % n := by
+    have ⟨k, hk⟩ := Nat.le_par h
+    generalize hl : b % n = l; have ⟨d, hd⟩ := Nat.mod_par hl
+    have llb : l ≤ b := by rw [← hl]; apply Nat.mod_le
+    have lla : l ≤ a := Nat.le_trans llb h
+    cases hd; rw [Nat.add_comm, Nat.sub_add_eq, Nat.sub_mul_mod]
+    rw [Nat.le_sub_iff_add_le lla]; apply h
+
+  theorem Nat.testBit_true_iff (a i : Nat) : a.testBit i ↔ 2 ^ i ≤ a % 2 ^ (i + 1) := by
+    rw [Nat.testBit_to_div_mod, decide_eq_true_iff]; apply Iff.intro <;> intro h
+    case mp =>
+      have ⟨k, hk⟩ := Nat.mod_par h; clear h
+      have ⟨r, ⟨er, lr⟩⟩ := Nat.div_par hk (Nat.pow_two_pos _); clear hk; cases er
+      have eqi : 2 ^ i * (2 * k + 1) + r = 2 ^ (i + 1) * k + (2 ^ i + r) := by
+        rw [Nat.mul_add _ _ 1, ← Nat.mul_assoc, Nat.pow_add, Nat.add_assoc]; simp
+      rw [eqi, Nat.mul_add_mod]
+      have elt : 2 ^ i + r < 2 ^ (i + 1) := by
+        rw [Nat.pow_add, show (2 ^ 1 = 2) by rfl, Nat.mul_two]
+        rw [Nat.add_lt_add_iff_left]; apply lr
+      rw [Nat.mod_eq_of_lt elt]; apply Nat.le_add_right
+    case mpr =>
+      generalize ek : a % 2 ^ (i + 1) = k at h
+      have lk : k < 2 ^ (i + 1) := by cases ek; apply Nat.mod_lt; apply Nat.pow_two_pos
+      have ⟨l, hl⟩ := Nat.mod_par ek; clear ek; cases hl
+      have eqi : 2 ^ (i + 1) * l + k = 2 ^ i * (2 * l) + k := by
+        rw [Nat.pow_add, Nat.mul_assoc]; simp
+      rw [eqi, Nat.mul_add_div (Nat.pow_two_pos _), Nat.mul_add_mod]
+      have kdge : k / (2 ^ i) > 0 := (Nat.le_div_iff_mul_le (Nat.pow_two_pos _)).mpr (by simp [h])
+      have kdle : k / (2 ^ i) < 2 := (Nat.div_lt_iff_lt_mul (Nat.pow_two_pos _)).mpr (by rw [Nat.pow_add, Nat.mul_comm] at lk; apply lk)
+      have kone : k / (2 ^ i) = 1 := Nat.eq_iff_le_and_ge.mpr (And.intro (Nat.le_of_succ_le_succ kdle) kdge)
+      rw [kone]; rfl
+
+  theorem Nat.testBit_false_iff (a i : Nat) : a.testBit i = false ↔ a % 2 ^ (i + 1) < 2 ^ i := by
+    rw [Bool.eq_false_eq_not_eq_true, ne_eq, Nat.testBit_true_iff, Nat.not_le]
+
+  theorem Nat.ones_testBit_true_of_lt (n i : Nat) (h : i < n) : (2 ^ n - 1).testBit i := by
+    rw [Nat.testBit_true_iff]; have ⟨k, ek⟩ := Nat.lt_par h; clear h; cases ek
+    have eqi : 2 ^ (i + 1 + k) - 1 = 2 ^ (i + 1) * (2 ^ k - 1) + (2 ^ (i + 1) - 1) := calc
+      _ = 2 ^ (i + 1) * 2 ^ k - 1 := by rw [Nat.pow_add]
+      _ = 2 ^ (i + 1) * (2 ^ k - 1 + 1) - 1 := by rw [Nat.sub_add_cancel]; apply Nat.pow_two_pos
+      _ = _ := by
+        have hle : 1 ≤ 2 ^ (i + 1) * 1 := by rw [Nat.mul_one]; apply Nat.pow_two_pos
+        rw [Nat.mul_add]; rw [Nat.add_sub_assoc hle]; simp
+    rw [eqi, Nat.mul_add_mod, Nat.mod_eq_of_lt (Nat.sub_lt (Nat.pow_two_pos _) .refl)]
+    rw [Nat.pow_add, show (2 ^ 1 = 2) by rfl, Nat.mul_two, show (Nat.succ 0 = 1) by rfl]
+    rw [Nat.add_sub_assoc (Nat.pow_two_pos _)]; apply Nat.le_add_right
+
+  theorem Nat.ones_testBit_false_of_ge (n i : Nat) (h : i ≥ n) : (2 ^ n - 1).testBit i = false := by
+    have hl : 2 ^ n - 1 < 2 ^ i := by
+      rw [Nat.lt_eq_succ_le, Nat.succ_eq_add_one, Nat.sub_add_cancel (Nat.pow_two_pos _)]
+      apply Nat.pow_le_pow_of_le_right (Nat.le_step .refl) h
+    have hls : 2 ^ i ≤ 2 ^ (i + 1) := Nat.pow_le_pow_of_le_right (Nat.le_step .refl) (Nat.le_add_right _ _)
+    rw [Nat.testBit_false_iff]; rw [Nat.mod_eq_of_lt (Nat.le_trans hl hls)]; apply hl
+
+  theorem Nat.xor_def (a b : Nat) : a ^^^ b = a.xor b := rfl
+
+  theorem Nat.ones_xor (n a : Nat) (h : a < 2 ^ n) : (2 ^ n - 1) ^^^ a = 2 ^ n - 1 - a := by
+    apply Nat.eq_of_testBit_eq; intro i
+    rw [xor_def, Nat.xor, Nat.testBit_bitwise (f:=bne) rfl]
+    have texp : 2 ^ (i + 1) = 2 ^ i + 2 ^ i := by rw [Nat.pow_add, show (2 ^ 1 = 2) by rfl, Nat.mul_two]
+    cases @Nat.dichotomy n i
+    case inl hl =>
+      rw [Nat.ones_testBit_false_of_ge _ _ hl]
+      rw [show (∀ b, (false != b) = b) by (intro b; simp)]
+      have ple : 2 ^ n ≤ 2 ^ i := Nat.pow_le_pow_of_le_right (Nat.le_step .refl) hl
+      have lf : Nat.testBit a i = false := by
+        rw [Nat.testBit_false_iff]
+        apply Nat.le_trans _ (Nat.le_trans h ple); apply Nat.succ_le_succ
+        apply Nat.mod_le
+      have rf : Nat.testBit (2 ^ n - 1 - a) i = false := by
+        rw [Nat.testBit_false_iff]
+        have li : 2 ^ n - 1 - a < 2 ^ i := by
+          rw [← Nat.sub_add_eq, Nat.lt_eq_succ_le, Nat.succ_eq_add_one]
+          rw [← Nat.sub_add_comm (show 1 + a ≤ 2 ^ n by rw [Nat.add_comm]; exact h)]
+          rw [Nat.sub_add_eq, Nat.add_sub_cancel]; rw [Nat.sub_le_iff_le_add]
+          apply Nat.le_trans ple (Nat.le_add_right _ _)
+        rw [Nat.mod_eq_of_lt (Nat.le_trans li (by rw [texp]; apply Nat.le_add_right))]
+        apply li
+      rw [lf, rf]
+    case inr hl =>
+      rw [Nat.ones_testBit_true_of_lt _ _ hl]
+      rw [show (∀ b, (true != b) = !b) by (intro b; simp)]
+      generalize hk : a % 2 ^ (i + 1) = k
+      have kl : k < 2 ^ (i + 1) := by rw [← hk]; apply Nat.mod_lt; apply Nat.pow_two_pos
+      have tr : (2 ^ n - 1 - a) % 2 ^ (i + 1) = 2 ^ (i + 1) - (k + 1) := by
+        rw [Nat.sub_mod _ _ _ (show a ≤ 2 ^ n - 1 by exact (Nat.le_sub_iff_add_le (Nat.pow_two_pos _)).mpr h)]
+        rw [hk]; have ⟨dn, hdn⟩ := Nat.lt_par hl; cases hdn
+        rw [Nat.pow_add _ _ dn, show (2 ^ dn = 2 ^ dn - 1 + 1) by rw[Nat.sub_add_cancel (Nat.pow_two_pos _)]]
+        rw [Nat.mul_add, Nat.mul_one, ← Nat.sub_add_eq]
+        rw [Nat.add_sub_assoc (by rw [Nat.add_comm]; exact kl)]
+        rw [Nat.mul_add_mod, Nat.mod_eq_of_lt, Nat.add_comm 1 k]
+        apply Nat.sub_lt (Nat.pow_two_pos _)
+        rw [Nat.add_comm]; apply Nat.zero_lt_succ
+      cases hai : Nat.testBit a i
+      case false =>
+        rw [Nat.testBit_false_iff] at hai
+        apply Eq.symm; rw [show ((!false) = true) by rfl, Nat.testBit_true_iff]
+        rw [hk] at hai; rw [tr, Nat.le_sub_iff_add_le kl, Nat.succ_eq_add_one]
+        rw [texp]; apply Nat.add_le_add_left; exact hai
+      case true =>
+        rw [Nat.testBit_true_iff] at hai
+        apply Eq.symm; rw [show ((!true) = false) by rfl, Nat.testBit_false_iff]
+        rw [hk] at hai; rw [tr, Nat.lt_eq_succ_le, Nat.succ_eq_add_one]
+        rw [← Nat.sub_add_comm kl, Nat.succ_eq_add_one]
+        rw [Nat.add_comm k 1, Nat.sub_add_eq, Nat.add_sub_cancel]
+        rw [Nat.sub_le_iff_le_add, texp]; apply Nat.add_le_add_left; exact hai
+
 end Auto

Auto/Lib/Pos.lean

@@ -118,7 +118,7 @@ theorem ofNat'WF_toNat' (p : Pos) : ofNat'WF (toNat' p) = p := by
 theorem toNat'_ofNat'WF (n : Nat) : n ≠ 0 → toNat' (ofNat'WF n) = n := by
   revert n; apply ofNat'WF.induction
   case base₀ => intro H; contradiction
-  case base₁ => intro H; rfl
+  case base₁ => intro _; rfl
   case ind =>
     intro x IH _
     have hne : (x + 2) / 2 ≠ 0 := by