diff options
author | Yann Herklotz <git@yannherklotz.com> | 2020-06-20 10:18:25 +0100 |
---|---|---|
committer | Yann Herklotz <git@yannherklotz.com> | 2020-06-20 10:18:25 +0100 |
commit | 11ff840afe29c5340582e513613dc70c13879997 (patch) | |
tree | 4c9b3081eab5c969d2f25ce0157295f6eaae0ce6 /src/verilog | |
parent | 2d10f818ff05b028ab2930d3ccfddd5a11bb1ad0 (diff) | |
download | vericert-kvx-11ff840afe29c5340582e513613dc70c13879997.tar.gz vericert-kvx-11ff840afe29c5340582e513613dc70c13879997.zip |
Add proof of nat equiv
Diffstat (limited to 'src/verilog')
-rw-r--r-- | src/verilog/Value.v | 17 |
1 files changed, 15 insertions, 2 deletions
diff --git a/src/verilog/Value.v b/src/verilog/Value.v index b1ee353..18a69ef 100644 --- a/src/verilog/Value.v +++ b/src/verilog/Value.v @@ -19,7 +19,7 @@ (* begin hide *) From bbv Require Import Word. From bbv Require HexNotation WordScope. -From Coq Require Import ZArith.ZArith FSets.FMapPositive. +From Coq Require Import ZArith.ZArith FSets.FMapPositive Lia. From compcert Require Import lib.Integers common.Values. (* end hide *) @@ -335,7 +335,7 @@ Proof. rewrite uvalueToZ_ZToValue. auto. rewrite positive_nat_Z. split. apply Zle_0_pos. - assert (p < 2 ^ (Pos.size p))%positive. apply Pos.size_gt. + assert (p < 2 ^ (Pos.size p))%positive by apply Pos.size_gt. inversion H. rewrite <- Z.compare_lt_iff. rewrite <- H1. simpl. rewrite <- Pos2Z.inj_pow_pos. trivial. Qed. @@ -366,3 +366,16 @@ Lemma boolToValue_ValueToBool : forall b, valueToBool (boolToValue 32 b) = b. Proof. destruct b; unfold valueToBool, boolToValue; simpl; trivial. Qed. + +Lemma ZToValue_valueToNat : + forall x sz, + (x < 2^(Z.of_nat sz))%Z -> + valueToNat (ZToValue sz x) = Z.to_nat x. +Proof. + destruct x; intros; unfold ZToValue, valueToNat; simpl. + - rewrite wzero'_def. apply wordToNat_wzero. + - rewrite posToWord_nat. rewrite wordToNat_natToWord_2. auto. + inversion H. destruct (2 ^ Z.of_nat sz)%Z eqn:?; try discriminate. + Set Printing All. + Search positive Z. + - lia. |