diff options
| author |  Jason Gross <jgross@mit.edu> | 2017-04-08 11:13:52 -0400 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2017-04-08 11:13:52 -0400 |
| commit | 6e78f4fe75a01ddbcc724fa2e192b7952f915b10 (patch) | |
| tree | e06195b461716524085ba024be089db5a60859ba | |
| parent | 676d72059269e349bf731968fa15070dad41b9ac (diff) | |
Add cast_const_idempotent_small
| -rw-r--r-- | src/Compilers/Z/Syntax/Util.v | 27 |
1 files changed, 27 insertions, 0 deletions
diff --git a/src/Compilers/Z/Syntax/Util.v b/src/Compilers/Z/Syntax/Util.v index 6cf54a99c..0fd02edf7 100644 --- a/src/Compilers/Z/Syntax/Util.v +++ b/src/Compilers/Z/Syntax/Util.v @@ -1,3 +1,4 @@ +Require Import Coq.ZArith.ZArith. Require Import Crypto.Compilers.Syntax. Require Import Crypto.Compilers.SmartMap. Require Import Crypto.Compilers.Wf. @@ -7,6 +8,7 @@ Require Import Crypto.Compilers.Z.Syntax. Require Import Crypto.Util.FixedWordSizesEquality. Require Import Crypto.Util.NatUtil. Require Import Crypto.Util.HProp. +Require Import Crypto.Util.ZUtil. Require Import Crypto.Util.Tactics.BreakMatch. Require Import Crypto.Util.Tactics.DestructHead. Require Import Crypto.Util.Notations. @@ -68,6 +70,31 @@ Proof. rewrite ZToWord_wordToZ; reflexivity. Qed. +Lemma cast_const_idempotent_small {a b c} v + : match b with + | TZ => True + | TWord bsz => 0 <= interpToZ (@cast_const a c v) < 2^Z.of_nat (2^bsz) + end%Z + -> @cast_const b c (@cast_const a b v) = @cast_const a c v. +Proof. + repeat first [ reflexivity + | congruence + | progress destruct_head' base_type + | progress simpl + | progress break_match + | progress subst + | intro + | match goal with + | [ H : ?leb _ _ = true |- _ ] => apply Compare_dec.leb_complete in H + | [ H : ?leb _ _ = false |- _ ] => apply Compare_dec.leb_iff_conv in H + | [ H : TWord _ = TWord _ |- _ ] => inversion H; clear H + end + | rewrite ZToWord_wordToZ_ZToWord by omega * + | rewrite wordToZ_ZToWord_wordToZ by omega * + | rewrite wordToZ_ZToWord by assumption + | rewrite ZToWord_wordToZ_ZToWord_small by omega ]. +Qed. + Lemma cast_const_idempotent {a b c} v : base_type_min b (base_type_min a c) = base_type_min a c -> @cast_const b c (@cast_const a b v) = @cast_const a c v. |