Skip to content

Commit cedfaa7

Browse files
dtumaddtumad
committed
golfing
1 parent fc9a5b8 commit cedfaa7

File tree

1 file changed

+18
-146
lines changed

1 file changed

+18
-146
lines changed

‎AddOperationNew.lean‎

Lines changed: 18 additions & 146 deletions
Original file line numberDiff line numberDiff line change
@@ -1,36 +1,21 @@
11
import Mathlib
22

33
-- random math fact
4-
instance {p : ℕ} [Fact (Nat.Prime p)] : NoZeroDivisors (Fin p) := by
5-
sorry
4+
instance {p : ℕ} [Fact (Nat.Prime p)] : NoZeroDivisors (Fin p) := sorry
65

76
macro "WORD_SIZE" : term => `(2)
87
abbrev p := 2013265921
98

109
@[reducible] def Word (T : Type) := Vector T WORD_SIZE
1110
@[reducible] def AddOperation (T : Type) := Word T
1211

13-
section eliminators
14-
15-
@[elab_as_elim]
12+
@[elab_as_elim] -- induction rule for words
1613
def Word.inductionOn {α : Type} {C : Word α → Prop}
17-
(mk : ∀ x1 x2 : α, C #v[x1, x2]) (w : Word α) : C w := by
18-
refine match w with
19-
| (Vector.mk (Array.mk as) h) => by {
20-
simp at h
21-
sorry
22-
}
23-
24-
@[elab_as_elim]
25-
def AddOperation.inductionOn {α : Type} {C : AddOperation α → Prop}
26-
(mk : ∀ x1 x2 : α, C #v[x1, x2])
27-
(op : AddOperation α) : C op := sorry
28-
29-
end eliminators
14+
(mk : ∀ x1 x2 : α, C #v[x1, x2]) (w : Word α) : C w := sorry
3015

3116
section base
3217

33-
abbrev base : Fin p := 2 ^ 16
18+
abbrev base : Fin p := 65536
3419
abbrev baseInv : Fin p := 2013235201
3520

3621
@[simp] lemma val_base : base.val = 65536 := rfl
@@ -39,7 +24,7 @@ abbrev baseInv : Fin p := 2013235201
3924
@[simp] lemma baseInv_mul_base : baseInv * base = 1 := rfl
4025
@[simp] lemma base_mul_baseInv : base * baseInv = 1 := rfl
4126

42-
@[simp] lemma base_ne_zero : base ≠ 0 := by simp [base]; trivial
27+
@[simp] lemma base_ne_zero : base ≠ 0 := by simp [base]
4328
@[simp] lemma baseInv_ne_zero : baseInv ≠ 0 := by simp [baseInv]
4429

4530
@[simp] lemma mul_baseInv_eq_zero_iff (x : Fin p) :
@@ -49,16 +34,10 @@ abbrev baseInv : Fin p := 2013235201
4934

5035
end base
5136

52-
section isUInt32
53-
5437
-- A word represents a u32 value if both entries are u16 values
5538
def Word.isUInt32 (w : Word (Fin p)) : Prop :=
5639
∀ x ∈ w, x.val < base
5740

58-
end isUInt32
59-
60-
section toNat
61-
6241
-- Convert a word to a natural number in the natural way
6342
def Word.toNat (w : Word (Fin p)) : ℕ :=
6443
w[0].val + base * w[1].val
@@ -67,8 +46,6 @@ lemma toNat_add_toNat (a b : Word (Fin p)) :
6746
a.toNat + b.toNat = (a[0] + b[0]) + base * (a[1] + b[1]) := by
6847
simp [Word.toNat]; omega
6948

70-
end toNat
71-
7249
/-- `AddOperation` should either give the direct sum of the two input values,
7350
or the value plus `2^32` on overflow-/
7451
def AddOperation.spec (cols : AddOperation (Fin p))
@@ -97,128 +74,23 @@ theorem AddOperation.correct [Fact (Nat.Prime p)]
9774
cols.constraints a b → cols.spec a b := by
9875
induction a using Word.inductionOn with | mk a1 a2 =>
9976
induction b using Word.inductionOn with | mk b1 b2 =>
100-
induction cols using AddOperation.inductionOn with | mk v1 v2 =>
77+
induction cols using Word.inductionOn with | mk v1 v2 =>
10178

102-
unfold constraints spec
103-
104-
simp [toNat_add_toNat, Word.isUInt32, mul_eq_zero]
79+
-- Reduce down the basic problem to arithmetic
80+
simp [constraints, spec, toNat_add_toNat, Word.isUInt32, mul_eq_zero]
10581
intros h1 h2 h3 h4 h5 h6 h7 h8
10682

107-
cases a1 with | mk a1 ha1 =>
108-
cases a2 with | mk a2 ha2 =>
109-
cases b1 with | mk b1 hb1 =>
110-
cases b2 with | mk b2 hb2 =>
111-
cases v1 with | mk v1 hv1 =>
112-
cases v2 with | mk v2 hv2 =>
113-
114-
have hinv : (2013235201 : Fin p).val = 2013235201 := rfl
115-
have hbase : (65536 : Fin p).val = 65536 := rfl
116-
have hpow : (2 ^ 16 : Fin p).val = 2 ^ 16 := rfl
83+
-- Case analysis on the two elements of the words
84+
cases a1 with | mk a1 ha1 => cases a2 with | mk a2 ha2 =>
85+
cases b1 with | mk b1 hb1 => cases b2 with | mk b2 hb2 =>
86+
cases v1 with | mk v1 hv1 => cases v2 with | mk v2 hv2 =>
11787

118-
simp only [Fin.val, hpow] at h3 h4 h5 h6 h7 h8
11988
simp only [Fin.isValue, sub_eq_zero, mul_baseInv_eq_zero_iff] at h1 h2
12089

12190
by_cases h_overflow : a1 + b1 + 65536 * (a2 + b2) < 4294967296
122-
·
123-
simp only [h_overflow, if_true, Word.toNat]
124-
simp only [Vector.getElem_mk, List.getElem_toArray, List.getElem_cons_zero, val_base,
125-
List.getElem_cons_succ]
126-
127-
cases h1 with
128-
| inl h1 => cases h2 with
129-
| inl h2 => {
130-
simp [p, Fin.val, base] at *
131-
rw [h1, sub_self, zero_mul, add_zero, sub_eq_zero] at h2
132-
rw [Fin.add_def, Fin.ext_iff] at h1 h2
133-
simp at h1 h2
134-
rw [← h1, ← h2]
135-
136-
omega
137-
}
138-
| inr h2 => {
139-
simp [p, Fin.val, base] at *
140-
rw [h1, sub_self, zero_mul, add_zero] at h2
141-
rw [sub_eq_iff_eq_add] at h2
142-
rw [← sub_eq_iff_eq_add'] at h2
143-
rw [Fin.add_def, Fin.ext_iff] at h1 h2
144-
simp at h1
145-
simp [Fin.sub_def] at h2
146-
rw [← h1, ← h2]
147-
148-
omega
149-
}
150-
| inr h1 => cases h2 with
151-
| inl h2 => {
152-
simp [p] at *
153-
rw [h1] at h2
154-
simp at h2
155-
rw [sub_eq_iff_eq_add, ← sub_eq_iff_eq_add'] at h1
156-
rw [← eq_sub_iff_add_eq, sub_eq_iff_eq_add, ← sub_eq_iff_eq_add'] at h2
157-
simp at h2
158-
simp only [Fin.add_def, Fin.sub_def, Fin.ext_iff] at h1 h2
159-
rw [val_base] at h1
160-
161-
omega
162-
}
163-
| inr h2 => {
164-
rw [h1, base_mul_baseInv] at h2
165-
rw [← eq_sub_iff_add_eq, sub_eq_iff_eq_add, ← sub_eq_iff_eq_add'] at h2
166-
rw [sub_eq_add_neg, neg_sub] at h2
167-
rw [sub_eq_iff_eq_add, ← sub_eq_iff_eq_add'] at h1
168-
simp only [Fin.add_def, Fin.sub_def, Fin.ext_iff] at h1 h2
169-
rw [← h1, ← h2]
170-
simp [mul_add, ← add_assoc]
171-
simp [p] at *
172-
173-
omega
174-
}
175-
· simp only [h_overflow, if_true, Word.toNat,
176-
Vector.getElem_mk, List.getElem_toArray, List.getElem_cons_zero, val_base,
177-
List.getElem_cons_succ]
178-
cases h1 with
179-
| inl h1 => cases h2 with
180-
| inl h2 => {
181-
simp [p, Fin.val, base] at *
182-
rw [h1, sub_self, zero_mul, add_zero, sub_eq_zero] at h2
183-
rw [Fin.add_def, Fin.ext_iff] at h1 h2
184-
simp at h1 h2
185-
rw [← h1, ← h2]
186-
187-
omega
188-
}
189-
| inr h2 => {
190-
simp [p, Fin.val, base] at *
191-
rw [h1, sub_self, zero_mul, add_zero] at h2
192-
rw [sub_eq_iff_eq_add] at h2
193-
rw [← sub_eq_iff_eq_add'] at h2
194-
rw [Fin.add_def, Fin.ext_iff] at h1 h2
195-
simp at h1
196-
simp [Fin.sub_def] at h2
197-
rw [← h1, ← h2]
198-
199-
omega
200-
}
201-
| inr h1 => cases h2 with
202-
| inl h2 => {
203-
simp [p] at *
204-
rw [h1] at h2
205-
simp at h2
206-
rw [sub_eq_iff_eq_add, ← sub_eq_iff_eq_add'] at h1
207-
rw [← eq_sub_iff_add_eq, sub_eq_iff_eq_add, ← sub_eq_iff_eq_add'] at h2
208-
simp at h2
209-
simp only [Fin.add_def, Fin.sub_def, Fin.ext_iff] at h1 h2
210-
rw [val_base] at h1
211-
212-
omega
213-
}
214-
| inr h2 => {
215-
216-
rw [h1, base_mul_baseInv] at h2
217-
rw [← eq_sub_iff_add_eq, sub_eq_iff_eq_add, ← sub_eq_iff_eq_add'] at h2
218-
rw [sub_eq_iff_eq_add, ← sub_eq_iff_eq_add'] at h1
219-
simp only [Fin.add_def, Fin.sub_def, Fin.ext_iff] at h1 h2
220-
rw [← h1, ← h2]
221-
simp [p] at *
222-
223-
omega
224-
}
91+
<;> simp [h_overflow, Word.toNat]
92+
<;> cases h1 with | inl h1 => ?_ | inr h1 => ?_
93+
<;> cases h2 with | inl h2 => ?_ | inr h2 => ?_
94+
<;> { rw [h1] at h2
95+
simp [Fin.add_def, Fin.sub_def, Fin.ext_iff, sub_eq_zero, p] at *
96+
omega }

0 commit comments

Comments
 (0)