chore(lean) : update lean to version 4.34.0

ExArray/lean/ExArray/Basic.lean

@@ -443,7 +443,12 @@ theorem readRec_succ (w : Nat) (buf : ExArray) (n : UInt64) numBytes h :
 theorem readRec_uset_disjoint {w : Nat} (buf : ExArray) (n: UInt64) numBytes m (x: UInt8)
     (hDisjoint: m.toNat ∉ support n.toNat numBytes) h₁ h₂ :
     (buf.uset m x h₁).readRec n numBytes h₂ = buf.readRec (w := w) n numBytes (by grind) := by
-  induction numBytes generalizing n buf x <;> grind [readRec_succ]
+  induction numBytes generalizing n
+  case zero =>
+    grind
+  case succ numBytes ih =>
+    simp only [readRec_succ]
+    grind
 
 @[simp, grind =]
 theorem readRec_blitRec_self (w : Nat) (buf : ExArray) (n : UInt64) numBytes (x : BitVec w) h h' :

Veir/Data/Float/Basic.lean

@@ -45,7 +45,7 @@ that represents IEEE-style floating point formats.
 @[expose]
 def FloatFormat.toLeanFormat (format : FloatFormat)
     (hm : 0 < format.mantissa := by grind)
-    (he : 0 < format.exponent := by grind) : _root_.Float.Model.Format where
+    (he : 2 ≤ format.exponent := by grind) : _root_.Float.Model.Format where
   exponentBits := format.exponent
   mantissaBitsWithoutImplicit := format.mantissa
   hm := hm
@@ -54,7 +54,7 @@ def FloatFormat.toLeanFormat (format : FloatFormat)
 @[simp]
 theorem FloatFormat.numBits_toLeanFormat_eq_bitwidth
     (format : FloatFormat)
-    (hm : 0 < format.mantissa) (he : 0 < format.exponent) :
+    (hm : 0 < format.mantissa) (he : 2 ≤ format.exponent) :
     (format.toLeanFormat hm he).numBits = format.bitwidth := by
   simp [toLeanFormat, _root_.Float.Model.Format.numBits, bitwidth]
 
@@ -122,7 +122,7 @@ of `UnpackedFloat.pack`.
 -/
 def ofUnpackedFloat (format : FloatFormat) (uf : UnpackedFloat)
     (hm : 0 < format.mantissa := by grind)
-    (he : 0 < format.exponent := by grind) : FloatValue format :=
+    (he : 2 ≤ format.exponent := by grind) : FloatValue format :=
   .ofBits <| match uf with
   | .notANumber =>
     (UnpackedFloat.packedNaN format.toLeanFormat).cast (by simp)
@@ -165,11 +165,11 @@ def ofUnpackedFloat (format : FloatFormat) (uf : UnpackedFloat)
 The value of `(-1)^negative * significand * 10^exponent` in `format`.
 
 Converts a base-10 float to the exact IEEE-754 bit pattern of `format`,
-using round-to-nearest, ties-to-even. 
+using round-to-nearest, ties-to-even.
 -/
 def ofScientific (format : FloatFormat)
     (negative : Bool) (significand : Nat) (exponent : Int) : FloatValue format :=
-  if hty : format.mantissa = 0 ∨ format.exponent = 0 then
+  if hty : format.mantissa = 0 ∨ format.exponent < 2 then
     .ofBits 0#_
   else
     let uf := UnpackedFloat.ofScientific format.toLeanFormat significand exponent

Veir/ForLean.lean

@@ -495,8 +495,8 @@ theorem sdiv_one_shl_of_smod_eq_zero {w₁ w₂ : Nat} (x : BitVec w₁) (k : Bi
     (hk : k.toNat + 1 < w₁) (h : x.smod ((1#w₁) <<< k) = 0#w₁) :
     x.sdiv ((1#w₁) <<< k) = x.sshiftRight' k := by
   have hy : ((1#w₁) <<< k).toInt = ((2 ^ k.toNat : Nat) : Int) := by
-    rw [BitVec.shiftLeft_eq', ← BitVec.twoPow_eq, BitVec.toInt_twoPow, if_neg (by omega),
-      if_neg (by omega)]
+    rw [BitVec.shiftLeft_eq', ← BitVec.twoPow_eq, BitVec.toInt_twoPow, ite_eq_right (by omega),
+      ite_eq_right (by omega)]
     exact (Int.natCast_pow 2 k.toNat).symm
   apply BitVec.eq_of_toInt_eq
   have hsmod : x.toInt.fmod ((1#w₁) <<< k).toInt = 0 := by
@@ -529,7 +529,7 @@ theorem toInt_neg_one_shl {w₁ w₂ : Nat} (k : BitVec w₂) (hk : k.toNat < w
     rw [BitVec.toNat_neg, hy, Nat.mod_eq_of_lt (Nat.sub_lt (Nat.two_pow_pos w₁) (Nat.two_pow_pos k.toNat)),
       hsubval]
   have hcond : ¬ (2 * (-((1#w₁) <<< k)).toNat < 2 ^ w₁) := by rw [hneg]; omega
-  rw [BitVec.toInt_eq_toNat_cond, if_neg hcond, hneg]
+  rw [BitVec.toInt_eq_toNat_cond, ite_eq_right hcond, hneg]
   omega
 
 /-- Negative-divisor analogue of `sdiv_one_shl_of_smod_eq_zero`: an exact `sdiv` by `-2^k` agrees
@@ -560,9 +560,9 @@ theorem Int.tdiv_eq_ediv_add_of_pos {a p : Int} (hp : 0 < p) :
   have hpne : p ≠ 0 := by omega
   rw [Int.tdiv_eq_ediv, Int.sign_eq_one_of_pos hp]
   by_cases ha : a < 0
-  · rw [if_pos ha]
+  · rw [ite_eq_left ha]
     by_cases hdvd : p ∣ a
-    · rw [if_pos (Or.inr hdvd)]
+    · rw [ite_eq_left (Or.inr hdvd)]
       obtain ⟨q, hq⟩ := hdvd
       subst hq
       have hrw : p * q + (p - 1) = (p - 1) + q * p := by
@@ -573,7 +573,7 @@ theorem Int.tdiv_eq_ediv_add_of_pos {a p : Int} (hp : 0 < p) :
       rw [Int.ediv_eq_zero_of_lt h1 h2, Int.mul_ediv_cancel_left q hpne]
       omega
     · have hnotor : ¬ (0 ≤ a ∨ p ∣ a) := fun h => h.elim (fun h0 => absurd h0 (by omega)) hdvd
-      rw [if_neg hnotor]
+      rw [ite_eq_right hnotor]
       have hr : a % p + a / p * p = a := Int.emod_add_ediv_mul a p
       have hr0 : 0 ≤ a % p := Int.emod_nonneg a hpne
       have hrlt : a % p < p := Int.emod_lt_of_pos a hp
@@ -589,7 +589,7 @@ theorem Int.tdiv_eq_ediv_add_of_pos {a p : Int} (hp : 0 < p) :
       rw [Int.ediv_eq_zero_of_lt h1 h2]
       simp
   · have haux : 0 ≤ a ∨ p ∣ a := Or.inl (by omega)
-    rw [if_neg ha, if_pos haux, Int.add_zero, Int.add_zero]
+    rw [ite_eq_right ha, ite_eq_left haux, Int.add_zero, Int.add_zero]
 
 /-- A shifted-in-from-the-left all-ones mask (`(2^w - 1) >>> (w - k)`, i.e. the top `w - k` bits
     of `allOnes w` cleared) is exactly the `k`-bit all-ones mask `2^k - 1`. Used to compute the
@@ -621,14 +621,14 @@ theorem toNat_sign_mask_shift {w₁ : Nat} (x : BitVec w₁) (k : Nat) (hk : k <
     omega
   rw [BitVec.toNat_ushiftRight]
   by_cases hmsb : x.msb = true
-  · rw [if_pos hmsb, BitVec.toNat_sshiftRight_of_msb_true hmsb]
+  · rw [ite_eq_left hmsb, BitVec.toNat_sshiftRight_of_msb_true hmsb]
     have hxge : 2 ^ (w₁ - 1) ≤ x.toNat := BitVec.le_toNat_of_msb_true hmsb
     have hxlt : x.toNat < 2 ^ w₁ := x.isLt
     have hzero : (2 ^ w₁ - 1 - x.toNat) >>> (w₁ - 1) = 0 := by
       rw [Nat.shiftRight_eq_div_pow, Nat.div_eq_of_lt (by omega)]
     rw [hzero, Nat.sub_zero]
     exact Nat.shiftRight_two_pow_sub_one hk
-  · rw [if_neg hmsb]
+  · rw [ite_eq_right hmsb]
     have hmsb' : x.msb = false := by simpa using hmsb
     rw [BitVec.toNat_sshiftRight_of_msb_false hmsb']
     have hxlt : x.toNat < 2 ^ (w₁ - 1) := BitVec.toNat_lt_of_msb_false hmsb'
@@ -648,8 +648,8 @@ theorem sdiv_one_shl_eq_biased_sshiftRight {w₁ w₂ : Nat} (x : BitVec w₁) (
     x.sdiv ((1#w₁) <<< k) =
       (x + (x.sshiftRight (w₁ - 1) >>> (w₁ - k.toNat))).sshiftRight' k := by
   have hy : ((1#w₁) <<< k).toInt = ((2 ^ k.toNat : Nat) : Int) := by
-    rw [BitVec.shiftLeft_eq', ← BitVec.twoPow_eq, BitVec.toInt_twoPow, if_neg (by omega),
-      if_neg (by omega)]
+    rw [BitVec.shiftLeft_eq', ← BitVec.twoPow_eq, BitVec.toInt_twoPow, ite_eq_right (by omega),
+      ite_eq_right (by omega)]
     exact (Int.natCast_pow 2 k.toNat).symm
   generalize hcorr_def : x.sshiftRight (w₁ - 1) >>> (w₁ - k.toNat) = corr
   have hcorrNat : corr.toNat = if x.msb then 2 ^ k.toNat - 1 else 0 := by
@@ -660,17 +660,17 @@ theorem sdiv_one_shl_eq_biased_sshiftRight {w₁ w₂ : Nat} (x : BitVec w₁) (
     rw [BitVec.msb_eq_toInt] at hcorrNat
     simp only [decide_eq_true_eq] at hcorrNat
     by_cases hx : x.toInt < 0
-    · rw [if_pos hx] at hcorrNat
-      rw [if_pos hx]
+    · rw [ite_eq_left hx] at hcorrNat
+      rw [ite_eq_left hx]
       have hlt : 2 * corr.toNat < 2 ^ w₁ := by
         rw [hcorrNat]
         have : 2 ^ (w₁ - 1) * 2 = 2 ^ w₁ := by
           rw [← Nat.pow_succ]; congr 1; omega
         omega
       rw [BitVec.toInt_eq_toNat_of_lt hlt, hcorrNat]
       exact Int.natCast_sub Nat.one_le_two_pow
-    · rw [if_neg hx] at hcorrNat
-      rw [if_neg hx]
+    · rw [ite_eq_right hx] at hcorrNat
+      rw [ite_eq_right hx]
       have hlt : 2 * corr.toNat < 2 ^ w₁ := by
         rw [hcorrNat]
         have := Nat.two_pow_pos w₁
@@ -691,12 +691,12 @@ theorem sdiv_one_shl_eq_biased_sshiftRight {w₁ w₂ : Nat} (x : BitVec w₁) (
     have hdouble : (2:Int) ^ (w₁ - 1) * 2 = ((2 ^ w₁ : Nat) : Int) := by exact_mod_cast hdoubleNat
     rw [hcorrInt]
     by_cases hx : x.toInt < 0
-    · rw [if_pos hx]
+    · rw [ite_eq_left hx]
       have hb1 : (0:Int) ≤ ((2 ^ k.toNat : Nat) : Int) - 1 := by
         have : (1:Int) ≤ ((2 ^ k.toNat : Nat) : Int) := by exact_mod_cast Nat.one_le_two_pow
         omega
       apply Int.bmod_eq_of_le <;> omega
-    · rw [if_neg hx]
+    · rw [ite_eq_right hx]
       simp only [Int.add_zero]
       apply Int.bmod_eq_of_le <;> omega
   have hppos : (0:Int) < ((2 ^ k.toNat : Nat) : Int) := by
@@ -724,17 +724,17 @@ theorem sdiv_neg_one_shl_eq_neg_biased_sshiftRight {w₁ w₂ : Nat} (x : BitVec
     rw [BitVec.msb_eq_toInt] at hcorrNat
     simp only [decide_eq_true_eq] at hcorrNat
     by_cases hx : x.toInt < 0
-    · rw [if_pos hx] at hcorrNat
-      rw [if_pos hx]
+    · rw [ite_eq_left hx] at hcorrNat
+      rw [ite_eq_left hx]
       have hlt : 2 * corr.toNat < 2 ^ w₁ := by
         rw [hcorrNat]
         have : 2 ^ (w₁ - 1) * 2 = 2 ^ w₁ := by
           rw [← Nat.pow_succ]; congr 1; omega
         omega
       rw [BitVec.toInt_eq_toNat_of_lt hlt, hcorrNat]
       exact Int.natCast_sub Nat.one_le_two_pow
-    · rw [if_neg hx] at hcorrNat
-      rw [if_neg hx]
+    · rw [ite_eq_right hx] at hcorrNat
+      rw [ite_eq_right hx]
       have hlt : 2 * corr.toNat < 2 ^ w₁ := by
         rw [hcorrNat]
         have := Nat.two_pow_pos w₁
@@ -756,12 +756,12 @@ theorem sdiv_neg_one_shl_eq_neg_biased_sshiftRight {w₁ w₂ : Nat} (x : BitVec
     have hdouble : (2:Int) ^ (w₁ - 1) * 2 = ((2 ^ w₁ : Nat) : Int) := by exact_mod_cast hdoubleNat
     rw [hcorrInt]
     by_cases hx : x.toInt < 0
-    · rw [if_pos hx]
+    · rw [ite_eq_left hx]
       have hb1 : (0:Int) ≤ ((2 ^ k.toNat : Nat) : Int) - 1 := by
         have : (1:Int) ≤ ((2 ^ k.toNat : Nat) : Int) := by exact_mod_cast Nat.one_le_two_pow
         omega
       apply Int.bmod_eq_of_le <;> omega
-    · rw [if_neg hx]
+    · rw [ite_eq_right hx]
       simp only [Int.add_zero]
       apply Int.bmod_eq_of_le <;> omega
   have hppos : (0:Int) < ((2 ^ k.toNat : Nat) : Int) := by
@@ -827,7 +827,7 @@ theorem sdiv_one_shl_eq_sshiftRight_of_msb_false (x : BitVec 64) (k : BitVec 6)
   by_cases hk : k.toNat + 1 < 64
   · have hcorr0 : x.sshiftRight 63 >>> (64 - k.toNat) = 0#64 := by
       apply BitVec.eq_of_toNat_eq
-      rw [toNat_sign_mask_shift x k.toNat (by omega), if_neg (by simp [hx])]
+      rw [toNat_sign_mask_shift x k.toNat (by omega), ite_eq_right (by simp [hx])]
       rfl
     rw [sdiv_one_shl_eq_biased_sshiftRight x k hk]
     show (x + (x.sshiftRight (63 : Nat) >>> (64 - k.toNat))).sshiftRight k.toNat =
@@ -841,7 +841,7 @@ theorem sdiv_one_shl_eq_sshiftRight_of_msb_false (x : BitVec 64) (k : BitVec 6)
     rw [hy, BitVec.sdiv_intMin]
     have hxne : x ≠ BitVec.intMin 64 := by
       intro h; rw [h] at hx; simp [BitVec.msb_intMin] at hx
-    rw [if_neg hxne]
+    rw [ite_eq_right hxne]
     apply BitVec.eq_of_toNat_eq
     show (0 : BitVec 64).toNat = (x.sshiftRight (-1 : BitVec 6).toNat).toNat
     rw [BitVec.toNat_sshiftRight_of_msb_false hx]
@@ -873,13 +873,13 @@ theorem sdiv_one_shl_eq_ite_sshiftRight (x : BitVec 64) (k : BitVec 6) :
       else
         x.sshiftRight' k := by
   by_cases hx : x.msb
-  · rw [if_pos hx]
+  · rw [ite_eq_left hx]
     by_cases hk0 : k = 0
-    · rw [if_pos hk0, hk0]
+    · rw [ite_eq_left hk0, hk0]
       simp [BitVec.sshiftRight_eq', BitVec.sdiv_one]
-    · rw [if_neg hk0]
+    · rw [ite_eq_right hk0]
       by_cases hk63 : k ≠ (-1 : BitVec 6)
-      · rw [if_pos hk63]
+      · rw [ite_eq_left hk63]
         have hk0' : 0 < k.toNat := by bv_omega
         have hk' : k.toNat + 1 < 64 := by bv_omega
         have h1 : (1 : BitVec 6).toNat = 1 := BitVec.toNat_one (by decide)
@@ -891,11 +891,11 @@ theorem sdiv_one_shl_eq_ite_sshiftRight (x : BitVec 64) (k : BitVec 6) :
           (x + (x.sshiftRight (-1 : BitVec 6).toNat >>> (-k : BitVec 6).toNat)).sshiftRight k.toNat
         rw [heq1, heq2]
         exact sdiv_one_shl_eq_biased_sshiftRight x k hk'
-      · rw [if_neg hk63]
+      · rw [ite_eq_right hk63]
         have hk63' : k = (-1 : BitVec 6) := Decidable.not_not.mp hk63
         have hy : (1#64) <<< k = BitVec.intMin 64 := by rw [hk63']; decide
         rw [hy, BitVec.sdiv_intMin]
-  · rw [if_neg hx]
+  · rw [ite_eq_right hx]
     exact sdiv_one_shl_eq_sshiftRight_of_msb_false x k (by simpa using hx)
 
 /-- Negative-divisor analogue of `sdiv_one_shl_eq_sshiftRight_of_msb_false`: when `x` is
@@ -908,7 +908,7 @@ theorem sdiv_neg_one_shl_eq_neg_sshiftRight_of_msb_false (x : BitVec 64) (k : Bi
   have hk : k.toNat < 64 := k.isLt
   have hcorr0 : x.sshiftRight 63 >>> (64 - k.toNat) = 0#64 := by
     apply BitVec.eq_of_toNat_eq
-    rw [toNat_sign_mask_shift x k.toNat (by omega), if_neg (by simp [hx])]
+    rw [toNat_sign_mask_shift x k.toNat (by omega), ite_eq_right (by simp [hx])]
     rfl
   rw [sdiv_neg_one_shl_eq_neg_biased_sshiftRight x k hk, hcorr0, BitVec.add_zero]
 
@@ -930,13 +930,13 @@ theorem sdiv_neg_one_shl_eq_ite_sshiftRight (x : BitVec 64) (k : BitVec 6) :
       else
         -(x.sshiftRight' k) := by
   by_cases hx : x.msb
-  · rw [if_pos hx]
+  · rw [ite_eq_left hx]
     by_cases hk0 : k = 0
-    · rw [if_pos hk0, hk0]
+    · rw [ite_eq_left hk0, hk0]
       have hy : (-((1#64) <<< (0 : BitVec 6))) = (-1 : BitVec 64) := by simp
       rw [hy, BitVec.sdiv_neg (by decide)]
       simp [BitVec.sdiv_one, BitVec.sshiftRight_eq']
-    · rw [if_neg hk0]
+    · rw [ite_eq_right hk0]
       have hk0' : 0 < k.toNat := by bv_omega
       have hk' : k.toNat < 64 := k.isLt
       have h1 : (1 : BitVec 6).toNat = 1 := BitVec.toNat_one (by decide)
@@ -948,7 +948,7 @@ theorem sdiv_neg_one_shl_eq_ite_sshiftRight (x : BitVec 64) (k : BitVec 6) :
         -((x + (x.sshiftRight (-1 : BitVec 6).toNat >>> (-k : BitVec 6).toNat)).sshiftRight k.toNat)
       rw [heq1, heq2]
       exact sdiv_neg_one_shl_eq_neg_biased_sshiftRight x k hk'
-  · rw [if_neg hx]
+  · rw [ite_eq_right hx]
     exact sdiv_neg_one_shl_eq_neg_sshiftRight_of_msb_false x k (by simpa using hx)
 
 @[veir_bv_normalize]

Veir/IR/Attribute.lean

@@ -73,7 +73,7 @@ that represents IEEE-style floating point formats.
 -/
 abbrev toFormat (type : FloatType)
     (hm : 0 < type.mantissa := by grind)
-    (he : 0 < type.exponent := by grind) : Float.Model.Format :=
+    (he : 2 ≤ type.exponent := by grind) : Float.Model.Format :=
   type.format.toLeanFormat hm he
 
 def f16 : FloatType := { format := .f16 }

Veir/IR/GetSet.lean

@@ -5462,13 +5462,7 @@ theorem BlockPtr.get!_OpOperandPtrPtr_set {block : BlockPtr} :
       else
         block.get! ctx
     | _ => block.get! ctx := by
-  cases ptr'
-  · grind
-  · split
-    · grind
-    · simp only [OpOperandPtrPtr.set_valueFirstUse, get!_ValuePtr_setFirstUse,
-      Array.set!_eq_setIfInBounds]
-      split <;> grind
+  rcases ptr' with operand | ⟨result | arg⟩ <;> grind
 
 @[simp, grind =]
 theorem BlockPtr.firstUse!_OpOperandPtrPtr_set {block : BlockPtr} :

Veir/PatternRewriter/Puddle/Validity.lean

@@ -362,7 +362,7 @@ macro "provePuddleValid" : tactic =>
     constructor
     · provePuddleSupported
     · cbv
-    · cbv
+    · native_decide
   ))
 
 end Veir.Puddle

Veir/Rewriter/GetSet/BlockOperands.lean

@@ -436,7 +436,9 @@ theorem OperationPtr.getSuccessors!_initBlockOperands {operation : OperationPtr}
     else
       operation.getSuccessors! ctx := by
   simp only [OperationPtr.getSuccessors!_def]
-  grind
+  /- We need to remove some grind patterns from the default grind set, as they make the search
+  space explode. See https://github.com/leanprover/lean4/issues/15183 -/
+  grind [-Array.range'_append, -Array.range'_append_1]
 
 @[simp, grind =, simp_getset]
 theorem BlockPtr.getNumArguments!_initBlockOperands {block : BlockPtr} :

lean-ctrees/lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:v4.33.0
+leanprover/lean4:v4.35.0-rc1

lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:v4.33.0
+leanprover/lean4:v4.35.0-rc1