diff options
Diffstat (limited to 'src/Util/FixedWordSizesEquality.v')
| -rw-r--r-- | src/Util/FixedWordSizesEquality.v | 9 |
1 files changed, 7 insertions, 2 deletions
diff --git a/src/Util/FixedWordSizesEquality.v b/src/Util/FixedWordSizesEquality.v index 430684070..56c7debf6 100644 --- a/src/Util/FixedWordSizesEquality.v +++ b/src/Util/FixedWordSizesEquality.v @@ -23,6 +23,7 @@ Lemma pow2_inj_helper x y : 2^x = 2^y -> x = y. Proof. destruct (NatUtil.nat_eq_dec x y) as [pf|pf]; [ intros; assumption | ]. intro H; exfalso. + let pf := pf in abstract (apply pf; eapply NPeano.Nat.pow_inj_r; [ | eassumption ]; omega). Defined. Lemma pow2_inj_helper_refl x p : pow2_inj_helper x x p = eq_refl. @@ -43,6 +44,7 @@ Proof. intros [pf H]; exists (pow2_inj_helper x y pf); subst v'. destruct (NatUtil.nat_eq_dec x y) as [H|H]; [ | exfalso; clear -pf H; + let pf := pf in abstract (apply pow2_inj_helper in pf; omega) ]. subst; rewrite pow2_inj_helper_refl; simpl. pose proof (NatUtil.UIP_nat_transparent _ _ pf eq_refl); subst pf. @@ -99,7 +101,10 @@ Proof. | _, _ => fun x y pf => match _ : False with end end; - try abstract (rewrite wordT_beq_hetero_type_lb_false in pf by omega; clear -pf; congruence). + match goal with + | [ pf : _ = _ |- _ ] + => abstract (rewrite wordT_beq_hetero_type_lb_false in pf by omega; clear -pf; congruence) + end. Defined. Lemma ZToWord_gen_wordToZ_gen : forall {sz} v, ZToWord_gen (@wordToZ_gen sz v) = v. @@ -123,7 +128,7 @@ Qed. Lemma wordToZ_gen_ZToWord_gen_mod : forall {sz} w, (0 <= w)%Z -> wordToZ_gen (@ZToWord_gen sz w) = (w mod (2^Z.of_nat sz))%Z. Proof. unfold ZToWord_gen, wordToZ_gen. - intros. + intros sz w H. rewrite wordToN_NToWord_mod. rewrite N2Z.inj_mod by (destruct sz; simpl; congruence). rewrite Z2N.id, N2Z.inj_pow, nat_N_Z by assumption. |