max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore: debug.byAsSorry on broken proofs

Browse source
This commit is contained in:
Kim Morrison 2024-09-10 16:56:04 +10:00
parent cb4a73a487
commit 5bc199ea1c
1 changed files with 2 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/Init/Data/BitVec/Lemmas.lean
View file

@ -570,6 +570,7 @@ theorem msb_zeroExtend (x : BitVec w) : (x.zeroExtend v).msb = (decide (0 < v) &
theorem msb_zeroExtend' (x : BitVec w) (h : w ≤ v) : (x.zeroExtend' h).msb = (decide (0 < v) && x.getLsbD (v - 1)) := by
rw [zeroExtend'_eq, msb_zeroExtend]
set_option debug.byAsSorry true in
/-- zero extending a bitvector to width 1 equals the boolean of the lsb. -/
theorem zeroExtend_one_eq_ofBool_getLsb_zero (x : BitVec w) :
x.zeroExtend 1 = BitVec.ofBool (x.getLsbD 0) := by
@ -586,6 +587,7 @@ theorem zeroExtend_ofNat_one_eq_ofNat_one_of_lt {v w : Nat} (hv : 0 < v) :
have hv := Nat.testBit_one_eq_true_iff_self_eq_zero.mp hi₁
omega
set_option debug.byAsSorry true in
/-- Truncating to width 1 produces a bitvector equal to the least significant bit. -/
theorem truncate_one {x : BitVec w} :
x.truncate 1 = ofBool (x.getLsbD 0) := by