diff options
| author |  Jason Gross <jgross@mit.edu> | 2016-10-10 14:34:02 -0400 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2016-10-10 14:34:47 -0400 |
| commit | fa38b037a4b9e26a7153938c2c650966297d0d67 (patch) | |
| tree | 505d9a1bc4d0830a591042b98acae3687987bed1 /src/BoundedArithmetic/Double | |
| parent | 6a316e99febd6799db8b32d14de5ab68115e97d1 (diff) | |
Work around bug 5003 (broken omega on projections)
This is https://coq.inria.fr/bugs/show_bug.cgi?id=5003, [xlia] ([lia],
[nia]) constructs ill typed terms when projections from records are
involved.
Diffstat (limited to 'src/BoundedArithmetic/Double')
| -rw-r--r-- | src/BoundedArithmetic/Double/Proofs/ShiftLeft.v | 4 | ||||
| -rw-r--r-- | src/BoundedArithmetic/Double/Proofs/ShiftLeftRightTactic.v | 2 | ||||
| -rw-r--r-- | src/BoundedArithmetic/Double/Proofs/ShiftRight.v | 4 |
3 files changed, 6 insertions, 4 deletions
diff --git a/src/BoundedArithmetic/Double/Proofs/ShiftLeft.v b/src/BoundedArithmetic/Double/Proofs/ShiftLeft.v index 29d6ddde8..c1f9b7968 100644 --- a/src/BoundedArithmetic/Double/Proofs/ShiftLeft.v +++ b/src/BoundedArithmetic/Double/Proofs/ShiftLeft.v @@ -1,4 +1,4 @@ -Require Import Coq.ZArith.ZArith. +Require Import Coq.ZArith.ZArith Coq.micromega.Psatz. Require Import Crypto.BoundedArithmetic.Interface. Require Import Crypto.BoundedArithmetic.Double.Core. Require Import Crypto.BoundedArithmetic.Double.Proofs.Decode. @@ -35,7 +35,7 @@ Section shl. generalize (decode_range r). pose proof (decode_range (fst r)). pose proof (decode_range (snd r)). - assert (forall n', 2^n <= 2^n' -> 0 <= decode (fst r) < 2^n') by auto with zarith. + assert (forall n', 2^n <= 2^n' -> 0 <= decode (fst r) < 2^n') by (simpl in *; auto with zarith). assert (forall n', n <= n' -> 0 <= decode (fst r) < 2^n') by auto with zarith omega. autorewrite with simpl_tuple_decoder; push_decode. shift_left_right_t. diff --git a/src/BoundedArithmetic/Double/Proofs/ShiftLeftRightTactic.v b/src/BoundedArithmetic/Double/Proofs/ShiftLeftRightTactic.v index 81ac0e9f4..44b4eb36d 100644 --- a/src/BoundedArithmetic/Double/Proofs/ShiftLeftRightTactic.v +++ b/src/BoundedArithmetic/Double/Proofs/ShiftLeftRightTactic.v @@ -24,6 +24,8 @@ Ltac shift_left_right_t := | [ |- context[Z.lor (?x >> ?count) (Z.pow2_mod (?y << (?n - ?count)) ?n)] ] => unique assert (0 <= Z.lor (x >> count) (Z.pow2_mod (y << (n - count)) n) < 2 ^ n) by (autorewrite with Zshift_to_pow; auto with zarith nia) | _ => progress push_decode + | [ |- context[Interface.decode (fst ?x)] ] => is_var x; destruct x; simpl in * + | [ |- context[@Interface.decode ?n ?W ?d ?x] ] => is_var x; generalize dependent (@Interface.decode n W d x); intros | _ => progress Z.rewrite_mod_small | _ => progress autorewrite with convert_to_Ztestbit | _ => progress autorewrite with zsimplify_fast diff --git a/src/BoundedArithmetic/Double/Proofs/ShiftRight.v b/src/BoundedArithmetic/Double/Proofs/ShiftRight.v index 6a9fffbb1..aed7093e6 100644 --- a/src/BoundedArithmetic/Double/Proofs/ShiftRight.v +++ b/src/BoundedArithmetic/Double/Proofs/ShiftRight.v @@ -1,4 +1,4 @@ -Require Import Coq.ZArith.ZArith Coq.micromega.Psatz. +Require Import Coq.ZArith.ZArith. Require Import Crypto.BoundedArithmetic.Interface. Require Import Crypto.BoundedArithmetic.Double.Core. Require Import Crypto.BoundedArithmetic.Double.Proofs.Decode. @@ -36,7 +36,7 @@ Section shr. generalize (decode_range r). pose proof (decode_range (fst r)). pose proof (decode_range (snd r)). - assert (forall n', 2^n <= 2^n' -> 0 <= decode (fst r) < 2^n') by auto with zarith. + assert (forall n', 2^n <= 2^n' -> 0 <= decode (fst r) < 2^n') by (simpl in *; auto with zarith). assert (forall n', n <= n' -> 0 <= decode (fst r) < 2^n') by auto with zarith omega. autorewrite with simpl_tuple_decoder; push_decode. shift_left_right_t. |