update to 4.6.0-rc1

Auto/Embedding/LamBitVec.lean

@@ -52,10 +52,8 @@ namespace BitVec
 
   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⟩⟩
-    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
+    unfold ushiftRight Std.BitVec.toNat
+    dsimp; rw [Nat.shiftRight_eq_div_pow]
 
   theorem toNat_zeroExtend' {a : Std.BitVec n} (le : n ≤ m) : (a.zeroExtend' le).toNat = a.toNat := rfl
 
@@ -95,14 +93,21 @@ namespace BitVec
     rw [poweq, ← Nat.mul_assoc, Nat.mul_comm _ (2^n)]; exact ⟨_, rfl⟩
 
   theorem ushiftRight_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_ushiftRight, toNat_ofNat]; apply (Nat.le_iff_div_eq_zero ?l).mpr ?r
-    case l => apply Nat.pow_two_pos
-    case r => apply Nat.le_trans (toNat_le _) (Nat.pow_le_pow_of_le_right (.step .refl) h)
+    intro h; apply eq_of_val_eq; rw [toNat_ushiftRight, toNat_ofNat]
+    apply (Nat.le_iff_div_eq_zero (Nat.pow_two_pos _)).mpr
+    apply Nat.le_trans (toNat_le _) (Nat.pow_le_pow_of_le_right (.step .refl) h)
+
+  theorem ushiftRight_ge_length_eq_zero' (a : Std.BitVec n) (i : Nat) : i ≥ n → (a.toNat >>> i)#n = 0#n := by
+    intro h; apply congr_arg (@Std.BitVec.ofNat n)
+    rw [Nat.shiftRight_eq_div_pow, Nat.le_iff_div_eq_zero (Nat.pow_two_pos _)]
+    apply Nat.le_trans (toNat_le _) (Nat.pow_le_pow_of_le_right (.step .refl) h)
 
   theorem sshiftRight_ge_length_eq_msb (a : Std.BitVec n) (i : Nat) : i ≥ n → a.sshiftRight i =
     if a.msb then (1#n).neg else 0#n := by
     intro h; cases hmsb : a.msb <;> simp [sshiftRight, Std.BitVec.toInt, hmsb, Int.shiftRight_def]
-    case false => dsimp [Std.BitVec.ofInt]; apply ushiftRight_ge_length_eq_zero _ _ h
+    case false =>
+      dsimp [Std.BitVec.ofInt]
+      apply ushiftRight_ge_length_eq_zero'; exact h
     case true =>
       rw [← Int.subNatNat_eq_coe, Int.subNatNat_of_lt (toNat_le _)]
       simp [Std.BitVec.toInt, Std.BitVec.ofInt]
@@ -120,18 +125,14 @@ namespace BitVec
 
   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⟩⟩;
-    unfold ushiftRight; dsimp [Std.BitVec.toNat]
-    rw [eq_iff_val_eq, toNat_ofNat, toNat_ofNat, Nat.zero_mod, Nat.shiftRight_eq_div_pow]
+    unfold ushiftRight; rw [eq_iff_val_eq]
+    dsimp [Std.BitVec.toNat, Std.BitVec.ofNat]
+    rw [Nat.zero_mod, Nat.shiftRight_eq_div_pow]
     apply Iff.intro <;> intro h
     case mp =>
-      rw [← Nat.dvd_iff_mod_eq_zero] at h; rcases h with ⟨cst, hdvd⟩
-      rw [← Nat.div_add_mod a (2^b)] at isLt; rw [hdvd] at isLt
-      rw [← Nat.mul_assoc, Nat.mul_comm _ (2^n), Nat.mul_assoc] at isLt
-      have isLt' := Nat.eq_zero_of_mul_right_lt (Nat.le_trans (Nat.succ_le_succ (Nat.le_add_right _ _)) isLt)
-      rw [Nat.mul_eq_zero] at isLt'; cases isLt'
-      case inl h => apply False.elim (Nat.ne_zero_of_zero_lt (Nat.pow_two_pos _) h)
-      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
+      rw [← Nat.le_iff_div_eq_zero (Nat.pow_two_pos _)]
+      exact h
+    case mpr => rw [(Nat.le_iff_div_eq_zero (Nat.pow_two_pos _)).mpr h]
 
   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]

Auto/Lib/BinTree.lean

@@ -126,8 +126,8 @@ def get?'WF (bt : BinTree α) (n : Nat) : Option α :=
     match Nat.mod n 2 with
     | 0 => get?'WF bt.left! (Nat.div n 2)
     | _ + 1 => get?'WF bt.right! (Nat.div n 2)
-termination_by get?'WF bt n => n
-decreasing_by apply Bin.wfAux; assumption
+termination_by n
+decreasing_by all_goals { rw [← h]; apply Bin.wfAux; assumption }
 
 theorem get?'WF.succSucc (bt : BinTree α) (n : Nat) :
   get?'WF bt (n + 2) =
@@ -215,8 +215,8 @@ def insert'WF (bt : BinTree α) (n : Nat) (x : α) : BinTree α :=
       match bt with
       | .leaf => .node .leaf .none (insert'WF .leaf (Nat.div n 2) x)
       | .node l v r => .node l v (insert'WF r (Nat.div n 2) x)
-termination_by insert'WF bt n x => n
-decreasing_by rw [← h]; apply Bin.wfAux; assumption
+termination_by n
+decreasing_by all_goals { rw [← h]; apply Bin.wfAux; assumption }
 
 theorem insert'WF.succSucc (bt : BinTree α) (n : Nat) (x : α) :
   insert'WF bt (n + 2) x =
@@ -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
-          simp [Nat.add_mod]; rfl
+          simp [Nat.add_mod]
         have eq₂ : (2 * n + 5) / 2 = n + 2 := by
           rw [Nat.add_comm _ 5];
           rw [Nat.add_mul_div_left];

Auto/Lib/BoolExtra.lean

@@ -37,7 +37,7 @@ noncomputable def Bool.ofProp (c : Prop) : Bool :=
 
 theorem Bool.ofProp_spec (c : Prop) : Bool.ofProp c ↔ c := by
   dsimp [ofProp]
-  cases h : Classical.propDecidable c <;> simp [*]
+  cases Classical.propDecidable c <;> simp [*]
 
 theorem Bool.ofProp_spec' (c : Prop) : Bool.ofProp c = false ↔ ¬ c := by
   conv => enter [2, 1]; rw [← Bool.ofProp_spec c]

Auto/Lib/ListExtra.lean

@@ -54,15 +54,15 @@ theorem List.eq_of_beq_eq_true [BEq α] (H : ∀ (x y : α), (x == y) = true →
 section
 
   variable (l : List α) (x : α) (xs : List α) (d : α)
-  
+
   @[simp]
   theorem List.getD_cons_zero : List.getD (x :: xs) 0 d = x :=
     rfl
-  
+
   @[simp]
   theorem List.getD_cons_succ : List.getD (x :: xs) (n + 1) d = List.getD xs n d :=
     rfl
-  
+
   theorem List.getD_eq_get {n : Nat} (hn : n < l.length) : l.getD n d = l.get ⟨n, hn⟩ := by
     induction l generalizing n
     case nil => cases hn
@@ -107,7 +107,7 @@ def List.merge (r : α → α → Prop) [DecidableRel r] : List α → List α 
   | [], l' => l'
   | l, [] => l
   | a :: l, b :: l' => if r a b then a :: merge r l (b :: l') else b :: merge r (a :: l) l'
-  termination_by merge r l₁ l₂ => List.length l₁ + List.length l₂
+  termination_by l₁ l₂ => List.length l₁ + List.length l₂
 
 def List.mergeSort (r : α → α → Prop) [DecidableRel r]  : List α → List α
   | [] => []
@@ -120,7 +120,7 @@ def List.mergeSort (r : α → α → Prop) [DecidableRel r]  : List α → List
     have := h.1
     have := h.2
     exact merge r (mergeSort r ls.1) (mergeSort r ls.2)
-  termination_by mergeSort r l => List.length l
+  termination_by l => List.length l
 
 theorem List.map_equiv (f₁ f₂ : α → β) (hequiv : ∀ x, f₁ x = f₂ x) : List.map f₁ xs = List.map f₂ xs := by
   induction xs
@@ -134,4 +134,4 @@ theorem List.length_reverseAux (l₁ l₂ : List α) : (l₁.reverseAux l₂).le
 def List.reverse_IsomType : IsomType (List α) (List α) :=
   ⟨List.reverse, List.reverse, List.reverse_reverse, List.reverse_reverse⟩
 
-end Auto
+end Auto

Auto/Lib/Pos.lean

@@ -48,7 +48,7 @@ def ofNat'WF (n : Nat) :=
     match n % 2 with
     | 0 => .xO (ofNat'WF (n / 2))
     | _ => .xI (ofNat'WF (n / 2))
-decreasing_by apply ofNat'WFAux; assumption
+decreasing_by rw [← h]; apply ofNat'WFAux; assumption
 
 theorem ofNat'WF.inductionOn.{u}
   {motive : Nat → Sort u} (x : Nat)
@@ -96,7 +96,7 @@ theorem ofNat'WF.doubleSucc_xI (n : Nat) :
     rw [ofNat'WF.succSucc];
     have heq : (2 * n' + 3 + 2) % 2 = 1 := by
       rw [Nat.add_mod_right]; rw [Nat.add_mod]
-      rw [Nat.mul_mod]; simp; rfl
+      rw [Nat.mul_mod]; simp
     rw [heq]; simp
     have heq' : Nat.succ ((2 * n' + 3) / 2) = n' + 2 := by
       apply congrArg; rw [Nat.add_comm];

lake-manifest.json

@@ -4,7 +4,7 @@
  [{"url": "https://github.com/leanprover/std4.git",
    "type": "git",
    "subDir": null,
-   "rev": "a11bdfc39e95fa5b09e06638a43bd8bd2eddce12",
+   "rev": "276953b13323ca151939eafaaec9129bf7970306",
    "name": "std",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",

lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:v4.5.0-rc1
+leanprover/lean4:v4.6.0-rc1