blob: 1061f19582afae5104fd643c30ba925193a02743 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
|
Require Import Coq.ZArith.BinInt.
Require Import Coq.micromega.Psatz.
Require Import Crypto.Util.ForLoop.
Require Import Crypto.Util.ForLoop.InvariantFramework.
Require Import Crypto.Util.ZUtil.
Local Open Scope Z_scope.
Check (for i (:= 0; += 1; < 10) updating (v := 5) {{ v + i }}).
Check (for (int i = 0; i < 5; i++) updating ( '(v1, v2) = (0, 0) ) {{ (v1 + i, v2 + i) }}).
Compute for (int i = 0; i < 5; i++) updating (v = 0) {{ v + i }}.
Compute for (int i = 0; i <= 5; i++) updating (v = 0) {{ v + i }}.
Compute for (int i = 5; i > -1; i--) updating (v = 0) {{ v + i }}.
Compute for (int i = 5; i >= 0; i--) updating (v = 0) {{ v + i }}.
Compute for (int i = 0; i < 5; i += 2) updating (v = 0) {{ v + i }}.
Compute for (int i = 0; i <= 5; i += 2) updating (v = 0) {{ v + i }}.
Compute for (int i = 5; i > -1; i -= 2) updating (v = 0) {{ v + i }}.
Compute for (int i = 5; i >= 0; i -= 2) updating (v = 0) {{ v + i }}.
Compute for (int i = 0; i < 6; i += 2) updating (v = 0) {{ v + i }}.
Compute for (int i = 0; i <= 6; i += 2) updating (v = 0) {{ v + i }}.
Compute for (int i = 6; i > -1; i -= 2) updating (v = 0) {{ v + i }}.
Compute for (int i = 6; i >= 0; i -= 2) updating (v = 0) {{ v + i }}.
Check eq_refl : for (int i = 0; i <= 5; i++) updating (v = 0) {{ v + i }} = 15.
Check eq_refl : for (int i = 0; i < 5; i++) updating (v = 0) {{ v + i }} = 10.
Check eq_refl : for (int i = 5; i >= 0; i--) updating (v = 0) {{ v + i }} = 15.
Check eq_refl : for (int i = 5; i > -1; i--) updating (v = 0) {{ v + i }} = 15.
Check eq_refl : for (int i = 0; i <= 5; i += 2) updating (v = 0) {{ v + i }} = 6.
Check eq_refl : for (int i = 0; i < 5; i += 2) updating (v = 0) {{ v + i }} = 6.
Check eq_refl : for (int i = 5; i > -1; i -= 2) updating (v = 0) {{ v + i }} = 9.
Check eq_refl : for (int i = 5; i >= 0; i -= 2) updating (v = 0) {{ v + i }} = 9.
Check eq_refl : for (int i = 0; i <= 6; i += 2) updating (v = 0) {{ v + i }} = 12.
Check eq_refl : for (int i = 0; i < 6; i += 2) updating (v = 0) {{ v + i }} = 6.
Check eq_refl : for (int i = 6; i > -1; i -= 2) updating (v = 0) {{ v + i }} = 12.
Check eq_refl : for (int i = 6; i >= 0; i -= 2) updating (v = 0) {{ v + i }} = 12.
Local Notation for_sumT n'
:= (let n := Z.pos n' in
(2 *
for (int i = 0; i <= n; i++) updating (v = 0) {{
v + i
}})%Z
= n * (n + 1))
(only parsing).
Check eq_refl : for_sumT 5.
(** Here we show that if we add the numbers from 0 to n, we get [n * (n + 1) / 2] *)
Example for_sum n' : for_sumT n'.
Proof.
intro n.
apply for_loop_ind_le1.
{ compute; reflexivity. }
{ intros; nia. }
Qed.
|
