diff options
author | Jason Gross <jgross@mit.edu> | 2017-01-21 18:51:47 -0500 |
---|---|---|
committer | Jason Gross <jgross@mit.edu> | 2017-01-21 18:52:02 -0500 |
commit | f178e5ba32761135cf433d7298624ff35ae44f44 (patch) | |
tree | a456963d204417358eadd8e483961f3ac2ce8781 | |
parent | 3c4ff8fe8d2154addcf440690d315c58a529c1f6 (diff) |
Revert "Fix a missing qualification"
This reverts commit 3c4ff8fe8d2154addcf440690d315c58a529c1f6.
Revert "Move weqb_hetero to Bedrock.Word"
This reverts commit c83cb07f1477de33ce9eb43eea6a4f2720a94763.
We probably shouldn't modify Bedrock.Word
-rw-r--r-- | Bedrock/Word.v | 10 | ||||
-rw-r--r-- | src/Util/WordUtil.v | 52 |
2 files changed, 32 insertions, 30 deletions
diff --git a/Bedrock/Word.v b/Bedrock/Word.v index 10bd452bb..2c518807d 100644 --- a/Bedrock/Word.v +++ b/Bedrock/Word.v @@ -300,16 +300,6 @@ Definition weq : forall sz (x y : word sz), {x = y} + {x <> y}. abstract (rewrite (shatter_word y); simpl; intro; injection H; auto). Defined. -Fixpoint weqb_hetero sz1 sz2 (x : word sz1) (y : word sz2) : bool := - match x, y with - | WO, WO => true - | WO, _ => false - | WS b _ x', WS b' _ y' - => eqb b b' && @weqb_hetero _ _ x' y' - | WS _ _ _, _ - => false - end%bool. -Global Arguments weqb_hetero {_ _} _ _. Fixpoint weqb sz (x : word sz) : word sz -> bool := match x in word sz return word sz -> bool with | WO => fun _ => true diff --git a/src/Util/WordUtil.v b/src/Util/WordUtil.v index 0e3f6a168..7f8d7b824 100644 --- a/src/Util/WordUtil.v +++ b/src/Util/WordUtil.v @@ -22,6 +22,38 @@ Create HintDb push_wordToN discriminated. Hint Extern 1 => autorewrite with pull_wordToN in * : pull_wordToN. Hint Extern 1 => autorewrite with push_wordToN in * : push_wordToN. +Module Word. + Fixpoint weqb_hetero sz1 sz2 (x : word sz1) (y : word sz2) : bool := + match x, y with + | WO, WO => true + | WO, _ => false + | WS b _ x', WS b' _ y' + => eqb b b' && @weqb_hetero _ _ x' y' + | WS _ _ _, _ + => false + end%bool. + Global Arguments weqb_hetero {_ _} _ _. + Theorem weqb_hetero_true_iff : forall sz1 x sz2 y, + @weqb_hetero sz1 sz2 x y = true <-> exists pf : sz1 = sz2, eq_rect _ word x _ pf = y. + Proof. + induction x; intros sz2 y; (split; [ destruct y | ]); + repeat first [ progress simpl + | intro + | congruence + | exists eq_refl + | progress destruct_head ex + | progress destruct_head bool + | progress subst + | progress split_andb + | match goal with + | [ IHx : forall sz2 y, weqb_hetero _ y = true <-> _, H : weqb_hetero _ _ = true |- _ ] + => apply IHx in H + | [ IHx : forall sz2 y, weqb_hetero _ y = true <-> _ |- weqb_hetero ?x ?x = true ] + => apply IHx + end ]. + Qed. +End Word. + (* Utility Tactics *) Ltac word_util_arith := omega. @@ -1212,23 +1244,3 @@ Lemma wlast_combine : forall sz a b, @wlast sz (combine a (WS b WO)) = b. Proof. intros; unfold wlast; rewrite split2_combine; cbv; reflexivity. Qed. - -Theorem weqb_hetero_true_iff : forall sz1 x sz2 y, - @weqb_hetero sz1 sz2 x y = true <-> exists pf : sz1 = sz2, eq_rect _ word x _ pf = y. -Proof. - induction x; intros sz2 y; (split; [ destruct y | ]); - repeat first [ progress simpl - | intro - | congruence - | exists Logic.eq_refl - | progress destruct_head ex - | progress destruct_head bool - | progress subst - | progress split_andb - | match goal with - | [ IHx : forall sz2 y, weqb_hetero _ y = true <-> _, H : weqb_hetero _ _ = true |- _ ] - => apply IHx in H - | [ IHx : forall sz2 y, weqb_hetero _ y = true <-> _ |- weqb_hetero ?x ?x = true ] - => apply IHx - end ]. -Qed. |