diff options
| -rw-r--r-- | src/Util/FixedWordSizesEquality.v | 40 | ||||
| -rw-r--r-- | src/Util/WordUtil.v | 48 |
2 files changed, 51 insertions, 37 deletions
diff --git a/src/Util/FixedWordSizesEquality.v b/src/Util/FixedWordSizesEquality.v index 99512f6a1..09b15eb7c 100644 --- a/src/Util/FixedWordSizesEquality.v +++ b/src/Util/FixedWordSizesEquality.v @@ -128,6 +128,14 @@ Proof. reflexivity. Qed. +Lemma wordToZ_gen_ZToWord_gen_wordToZ_gen sz1 sz2 w + : (sz1 <= sz2)%nat -> wordToZ_gen (@ZToWord_gen sz2 (@wordToZ_gen sz1 w)) = wordToZ_gen w. +Proof. + unfold ZToWord_gen, wordToZ_gen; intro H. + rewrite N2Z.id, wordToN_NToWord_wordToN by omega. + reflexivity. +Qed. + Lemma ZToWord_wordToZ : forall {sz} v, ZToWord (@wordToZ sz v) = v. Proof. unfold wordT, word_case in *. @@ -141,20 +149,30 @@ Proof. assumption. Qed. +Local Ltac handle_le := + repeat match goal with + | [ |- (S ?a <= 2^?b)%nat ] + => change (2^(Nat.log2 (S a)) <= 2^b)%nat + | [ |- (2^_ <= 2^_)%nat ] + => apply Nat.pow_le_mono_r + | [ |- _ <> _ ] => intro; omega + | _ => assumption + | [ |- (_ <= S _)%nat ] + => apply Nat.leb_le; vm_compute; reflexivity + | _ => exfalso; omega + end. + Lemma ZToWord_wordToZ_ZToWord : forall {sz1 sz2} v, (sz2 <= sz1)%nat -> @ZToWord sz2 (wordToZ (@ZToWord sz1 v)) = ZToWord v. Proof. unfold wordToZ, ZToWord, word_case_dep. intros sz1 sz2; break_match; intros; apply ZToWord_gen_wordToZ_gen_ZToWord_gen; - repeat match goal with - | [ |- (S ?a <= 2^?b)%nat ] - => change (2^(Nat.log2 (S a)) <= 2^b)%nat - | [ |- (2^_ <= 2^_)%nat ] - => apply Nat.pow_le_mono_r - | [ |- _ <> _ ] => intro; omega - | _ => assumption - | [ |- (_ <= S _)%nat ] - => apply Nat.leb_le; vm_compute; reflexivity - | _ => exfalso; omega - end. + handle_le. +Qed. + +Lemma wordToZ_ZToWord_wordToZ : forall sz1 sz2 w, (sz1 <= sz2)%nat -> wordToZ (@ZToWord sz2 (@wordToZ sz1 w)) = wordToZ w. +Proof. + unfold wordToZ, ZToWord, word_case_dep. + intros sz1 sz2; break_match; intros; apply wordToZ_gen_ZToWord_gen_wordToZ_gen; + handle_le. Qed. diff --git a/src/Util/WordUtil.v b/src/Util/WordUtil.v index 0a33d6e54..3c3b61bc4 100644 --- a/src/Util/WordUtil.v +++ b/src/Util/WordUtil.v @@ -419,6 +419,13 @@ Section WordToN. end end x. + Lemma wbit_large {n} (x: word n) (k: nat) + : n <= k -> wbit x k = false. + Proof. + revert k; induction x, k; intro H; simpl; try reflexivity; try omega. + apply IHx; omega. + Qed. + Lemma wbit_inj_iff {n} (x y : word n) : (forall k, wbit x k = wbit y k) <-> x = y. Proof. @@ -455,32 +462,10 @@ Section WordToN. : (forall k, k < n -> wbit x k = wbit y k) <-> x = y. Proof. rewrite <- wbit_inj_iff. - induction n. - { split; intros H k; specialize (H k); try intro H'; try omega. - refine match x, y with - | WO, WO => eq_refl - | _, _ => I - end. } - { do 2 let n := match goal with n : nat |- _ => n end in - revert dependent n; - let G := match goal with |- forall n x, @?G n x => G end in - intros n x; - refine match x in word n return match n with - | S n' => G n' - | _ => fun _ => True - end x - with - | WO => I - | _ => _ - end; clear n x; - intro y; move y at top. - intro IH. - split; intros H k; pose proof (H k) as Hk; destruct k; - simpl in Hk |- *; - try solve [ intros; try (first [ apply H | apply Hk ]; omega) ]. - clear Hk; revert k. - apply IH; intros k H'. - specialize (H (S k)); apply H; omega. } + split; intros H k; specialize (H k); + destruct (le_lt_dec n k); + rewrite ?wbit_large by assumption; + auto. Qed. Lemma wordToN_testbit: forall {n} (x: word n) k, @@ -566,6 +551,17 @@ Section WordToN. end. Qed. + Lemma wordToN_NToWord_wordToN : forall sz1 sz2 w, (sz1 <= sz2)%nat -> wordToN (NToWord sz2 (@wordToN sz1 w)) = wordToN w. + Proof. + intros sz1 sz2 w H. + apply N.bits_inj; intro k. + rewrite !wordToN_testbit, !wbit_NToWord, wordToN_testbit, N2Nat.id. + destruct (N.to_nat k <? sz2) eqn:H'; try reflexivity. + apply Nat.ltb_ge in H'. + rewrite wbit_large by omega. + reflexivity. + Qed. + Lemma wordToN_split1: forall {n m} x, wordToN (@split1 n m x) = N.land (wordToN x) (wordToN (wones n)). Proof. |