diff options
Diffstat (limited to 'src/Util/ForLoop/Tests.v')
-rw-r--r-- | src/Util/ForLoop/Tests.v | 55 |
1 files changed, 0 insertions, 55 deletions
diff --git a/src/Util/ForLoop/Tests.v b/src/Util/ForLoop/Tests.v deleted file mode 100644 index 1061f1958..000000000 --- a/src/Util/ForLoop/Tests.v +++ /dev/null @@ -1,55 +0,0 @@ -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. |