Skip to content

Commit c7fd873

Browse files
hargoniXKha
hargoniX
authored and
Kha
committed
feat: tag lemmas
1 parent a10ce94 commit c7fd873

File tree

3 files changed

+77
-19
lines changed

3 files changed

+77
-19
lines changed

‎src/Init/Data/UInt/Bitwise.lean

Lines changed: 16 additions & 16 deletions
Original file line numberDiff line numberDiff line change
@@ -13,17 +13,17 @@ macro "declare_bitwise_uint_theorems" typeName:ident bits:term:arg : command =>
1313
`(
1414
namespace $typeName
1515

16-
@[simp] protected theorem toBitVec_add {a b : $typeName} : (a + b).toBitVec = a.toBitVec + b.toBitVec := rfl
17-
@[simp] protected theorem toBitVec_sub {a b : $typeName} : (a - b).toBitVec = a.toBitVec - b.toBitVec := rfl
18-
@[simp] protected theorem toBitVec_mul {a b : $typeName} : (a * b).toBitVec = a.toBitVec * b.toBitVec := rfl
19-
@[simp] protected theorem toBitVec_div {a b : $typeName} : (a / b).toBitVec = a.toBitVec / b.toBitVec := rfl
20-
@[simp] protected theorem toBitVec_mod {a b : $typeName} : (a % b).toBitVec = a.toBitVec % b.toBitVec := rfl
21-
@[simp] protected theorem toBitVec_not {a : $typeName} : (~~~a).toBitVec = ~~~a.toBitVec := rfl
22-
@[simp] protected theorem toBitVec_and (a b : $typeName) : (a &&& b).toBitVec = a.toBitVec &&& b.toBitVec := rfl
23-
@[simp] protected theorem toBitVec_or (a b : $typeName) : (a ||| b).toBitVec = a.toBitVec ||| b.toBitVec := rfl
24-
@[simp] protected theorem toBitVec_xor (a b : $typeName) : (a ^^^ b).toBitVec = a.toBitVec ^^^ b.toBitVec := rfl
25-
@[simp] protected theorem toBitVec_shiftLeft (a b : $typeName) : (a <<< b).toBitVec = a.toBitVec <<< (b.toBitVec % $bits) := rfl
26-
@[simp] protected theorem toBitVec_shiftRight (a b : $typeName) : (a >>> b).toBitVec = a.toBitVec >>> (b.toBitVec % $bits) := rfl
16+
@[simp, int_toBitVec] protected theorem toBitVec_add {a b : $typeName} : (a + b).toBitVec = a.toBitVec + b.toBitVec := rfl
17+
@[simp, int_toBitVec] protected theorem toBitVec_sub {a b : $typeName} : (a - b).toBitVec = a.toBitVec - b.toBitVec := rfl
18+
@[simp, int_toBitVec] protected theorem toBitVec_mul {a b : $typeName} : (a * b).toBitVec = a.toBitVec * b.toBitVec := rfl
19+
@[simp, int_toBitVec] protected theorem toBitVec_div {a b : $typeName} : (a / b).toBitVec = a.toBitVec / b.toBitVec := rfl
20+
@[simp, int_toBitVec] protected theorem toBitVec_mod {a b : $typeName} : (a % b).toBitVec = a.toBitVec % b.toBitVec := rfl
21+
@[simp, int_toBitVec] protected theorem toBitVec_not {a : $typeName} : (~~~a).toBitVec = ~~~a.toBitVec := rfl
22+
@[simp, int_toBitVec] protected theorem toBitVec_and (a b : $typeName) : (a &&& b).toBitVec = a.toBitVec &&& b.toBitVec := rfl
23+
@[simp, int_toBitVec] protected theorem toBitVec_or (a b : $typeName) : (a ||| b).toBitVec = a.toBitVec ||| b.toBitVec := rfl
24+
@[simp, int_toBitVec] protected theorem toBitVec_xor (a b : $typeName) : (a ^^^ b).toBitVec = a.toBitVec ^^^ b.toBitVec := rfl
25+
@[simp, int_toBitVec] protected theorem toBitVec_shiftLeft (a b : $typeName) : (a <<< b).toBitVec = a.toBitVec <<< (b.toBitVec % $bits) := rfl
26+
@[simp, int_toBitVec] protected theorem toBitVec_shiftRight (a b : $typeName) : (a >>> b).toBitVec = a.toBitVec >>> (b.toBitVec % $bits) := rfl
2727

2828
@[simp] protected theorem toNat_and (a b : $typeName) : (a &&& b).toNat = a.toNat &&& b.toNat := by simp [toNat]
2929
@[simp] protected theorem toNat_or (a b : $typeName) : (a ||| b).toNat = a.toNat ||| b.toNat := by simp [toNat]
@@ -44,27 +44,27 @@ declare_bitwise_uint_theorems UInt32 32
4444
declare_bitwise_uint_theorems UInt64 64
4545
declare_bitwise_uint_theorems USize System.Platform.numBits
4646

47-
@[simp]
47+
@[simp, int_toBitVec]
4848
theorem Bool.toBitVec_toUInt8 {b : Bool} :
4949
b.toUInt8.toBitVec = (BitVec.ofBool b).setWidth 8 := by
5050
cases b <;> simp [toUInt8]
5151

52-
@[simp]
52+
@[simp, int_toBitVec]
5353
theorem Bool.toBitVec_toUInt16 {b : Bool} :
5454
b.toUInt16.toBitVec = (BitVec.ofBool b).setWidth 16 := by
5555
cases b <;> simp [toUInt16]
5656

57-
@[simp]
57+
@[simp, int_toBitVec]
5858
theorem Bool.toBitVec_toUInt32 {b : Bool} :
5959
b.toUInt32.toBitVec = (BitVec.ofBool b).setWidth 32 := by
6060
cases b <;> simp [toUInt32]
6161

62-
@[simp]
62+
@[simp, int_toBitVec]
6363
theorem Bool.toBitVec_toUInt64 {b : Bool} :
6464
b.toUInt64.toBitVec = (BitVec.ofBool b).setWidth 64 := by
6565
cases b <;> simp [toUInt64]
6666

67-
@[simp]
67+
@[simp, int_toBitVec]
6868
theorem Bool.toBitVec_toUSize {b : Bool} :
6969
b.toUSize.toBitVec = (BitVec.ofBool b).setWidth System.Platform.numBits := by
7070
cases b

‎src/Init/Data/UInt/Lemmas.lean

Lines changed: 17 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -41,9 +41,9 @@ macro "declare_uint_theorems" typeName:ident bits:term:arg : command => do
4141
theorem toNat_ofNat_of_lt {n : Nat} (h : n < size) : (ofNat n).toNat = n := by
4242
rw [toNat, toBitVec_eq_of_lt h]
4343

44-
theorem le_def {a b : $typeName} : a ≤ b ↔ a.toBitVec ≤ b.toBitVec := .rfl
44+
@[int_toBitVec] theorem le_def {a b : $typeName} : a ≤ b ↔ a.toBitVec ≤ b.toBitVec := .rfl
4545

46-
theorem lt_def {a b : $typeName} : a < b ↔ a.toBitVec < b.toBitVec := .rfl
46+
@[int_toBitVec] theorem lt_def {a b : $typeName} : a < b ↔ a.toBitVec < b.toBitVec := .rfl
4747

4848
theorem le_iff_toNat_le {a b : $typeName} : a ≤ b ↔ a.toNat ≤ b.toNat := .rfl
4949

@@ -74,6 +74,11 @@ macro "declare_uint_theorems" typeName:ident bits:term:arg : command => do
7474
protected theorem toBitVec_inj {a b : $typeName} : a.toBitVec = b.toBitVec ↔ a = b :=
7575
Iff.intro eq_of_toBitVec_eq toBitVec_eq_of_eq
7676

77+
open $typeName (eq_of_toBitVec_eq toBitVec_eq_of_eq) in
78+
@[int_toBitVec]
79+
protected theorem eq_iff_toBitVec_eq {a b : $typeName} : a = b ↔ a.toBitVec = b.toBitVec :=
80+
Iff.intro toBitVec_eq_of_eq eq_of_toBitVec_eq
81+
7782
open $typeName (eq_of_toBitVec_eq) in
7883
protected theorem eq_of_val_eq {a b : $typeName} (h : a.val = b.val) : a = b := by
7984
rcases a with ⟨⟨_⟩⟩; rcases b with ⟨⟨_⟩⟩; simp_all [val]
@@ -82,10 +87,19 @@ macro "declare_uint_theorems" typeName:ident bits:term:arg : command => do
8287
protected theorem val_inj {a b : $typeName} : a.val = b.val ↔ a = b :=
8388
Iff.intro eq_of_val_eq (congrArg val)
8489

90+
open $typeName (eq_of_toBitVec_eq) in
91+
protected theorem toBitVec_ne_of_ne {a b : $typeName} (h : a ≠ b) : a.toBitVec ≠ b.toBitVec :=
92+
fun h' => h (eq_of_toBitVec_eq h')
93+
8594
open $typeName (toBitVec_eq_of_eq) in
8695
protected theorem ne_of_toBitVec_ne {a b : $typeName} (h : a.toBitVec ≠ b.toBitVec) : a ≠ b :=
8796
fun h' => absurd (toBitVec_eq_of_eq h') h
8897

98+
open $typeName (ne_of_toBitVec_ne toBitVec_ne_of_ne) in
99+
@[int_toBitVec]
100+
protected theorem ne_iff_toBitVec_ne {a b : $typeName} : a ≠ b ↔ a.toBitVec ≠ b.toBitVec :=
101+
Iff.intro toBitVec_ne_of_ne ne_of_toBitVec_ne
102+
89103
open $typeName (ne_of_toBitVec_ne) in
90104
protected theorem ne_of_lt {a b : $typeName} (h : a < b) : a ≠ b := by
91105
apply ne_of_toBitVec_ne
@@ -159,7 +173,7 @@ macro "declare_uint_theorems" typeName:ident bits:term:arg : command => do
159173
@[simp]
160174
theorem val_ofNat (n : Nat) : val (no_index (OfNat.ofNat n)) = OfNat.ofNat n := rfl
161175

162-
@[simp]
176+
@[simp, int_toBitVec]
163177
theorem toBitVec_ofNat (n : Nat) : toBitVec (no_index (OfNat.ofNat n)) = BitVec.ofNat _ n := rfl
164178

165179
@[simp]

‎tests/lean/run/int_toBitVec.lean

Lines changed: 44 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,44 @@
1+
example (a b c d e : UInt8) : ((a + (b * c)) = (b - d / e)) ↔ (a.toBitVec + b.toBitVec * c.toBitVec = b.toBitVec - d.toBitVec / e.toBitVec) := by
2+
simp only [int_toBitVec]
3+
4+
example (a b c d e : UInt16) : ((a + (b * c)) = (b - d / e)) ↔ (a.toBitVec + b.toBitVec * c.toBitVec = b.toBitVec - d.toBitVec / e.toBitVec) := by
5+
simp only [int_toBitVec]
6+
7+
example (a b c d e : UInt32) : ((a + (b * c)) = (b - d / e)) ↔ (a.toBitVec + b.toBitVec * c.toBitVec = b.toBitVec - d.toBitVec / e.toBitVec) := by
8+
simp only [int_toBitVec]
9+
10+
example (a b c d e : UInt64) : ((a + (b * c)) = (b - d / e)) ↔ (a.toBitVec + b.toBitVec * c.toBitVec = b.toBitVec - d.toBitVec / e.toBitVec) := by
11+
simp only [int_toBitVec]
12+
13+
example (a b c d e : USize) : ((a + (b * c)) = (b - d / e)) ↔ (a.toBitVec + b.toBitVec * c.toBitVec = b.toBitVec - d.toBitVec / e.toBitVec) := by
14+
simp only [int_toBitVec]
15+
16+
example (a b c d e : UInt8) : ((a + (b * c)) < (b - d / e)) ↔ (a.toBitVec + b.toBitVec * c.toBitVec < b.toBitVec - d.toBitVec / e.toBitVec) := by
17+
simp only [int_toBitVec]
18+
19+
example (a b c d e : UInt16) : ((a + (b * c)) < (b - d / e)) ↔ (a.toBitVec + b.toBitVec * c.toBitVec < b.toBitVec - d.toBitVec / e.toBitVec) := by
20+
simp only [int_toBitVec]
21+
22+
example (a b c d e : UInt32) : ((a + (b * c)) < (b - d / e)) ↔ (a.toBitVec + b.toBitVec * c.toBitVec < b.toBitVec - d.toBitVec / e.toBitVec) := by
23+
simp only [int_toBitVec]
24+
25+
example (a b c d e : UInt64) : ((a + (b * c)) < (b - d / e)) ↔ (a.toBitVec + b.toBitVec * c.toBitVec < b.toBitVec - d.toBitVec / e.toBitVec) := by
26+
simp only [int_toBitVec]
27+
28+
example (a b c d e : USize) : ((a + (b * c)) < (b - d / e)) ↔ (a.toBitVec + b.toBitVec * c.toBitVec < b.toBitVec - d.toBitVec / e.toBitVec) := by
29+
simp only [int_toBitVec]
30+
31+
example (a b c d e : UInt8) : ((a + (b * c)) ≤ (b - d / e)) ↔ (a.toBitVec + b.toBitVec * c.toBitVec ≤ b.toBitVec - d.toBitVec / e.toBitVec) := by
32+
simp only [int_toBitVec]
33+
34+
example (a b c d e : UInt16) : ((a + (b * c)) ≤ (b - d / e)) ↔ (a.toBitVec + b.toBitVec * c.toBitVec ≤ b.toBitVec - d.toBitVec / e.toBitVec) := by
35+
simp only [int_toBitVec]
36+
37+
example (a b c d e : UInt32) : ((a + (b * c)) ≤ (b - d / e)) ↔ (a.toBitVec + b.toBitVec * c.toBitVec ≤ b.toBitVec - d.toBitVec / e.toBitVec) := by
38+
simp only [int_toBitVec]
39+
40+
example (a b c d e : UInt64) : ((a + (b * c)) ≤ (b - d / e)) ↔ (a.toBitVec + b.toBitVec * c.toBitVec ≤ b.toBitVec - d.toBitVec / e.toBitVec) := by
41+
simp only [int_toBitVec]
42+
43+
example (a b c d e : USize) : ((a + (b * c)) ≤ (b - d / e)) ↔ (a.toBitVec + b.toBitVec * c.toBitVec ≤ b.toBitVec - d.toBitVec / e.toBitVec) := by
44+
simp only [int_toBitVec]

0 commit comments

Comments
 (0)