diff options
| author | Yann Herklotz <git@yannherklotz.com> | 2020-06-23 11:34:16 +0100 |
|---|---|---|
| committer | Yann Herklotz <git@yannherklotz.com> | 2020-06-23 11:34:16 +0100 |
| commit | 8c48e9e1094f037835698c88782772c8b3250a76 (patch) | |
| tree | ba0e97db17b23c5c5887a59daf5eda9de636efe8 /src | |
| parent | 563ee7cf230b85e7ed83c5652392f102974f662c (diff) | |
| download | vericert-8c48e9e1094f037835698c88782772c8b3250a76.tar.gz vericert-8c48e9e1094f037835698c88782772c8b3250a76.zip | |
More to proof
Diffstat (limited to 'src')
| -rw-r--r-- | src/verilog/Value.v | 16 |
1 files changed, 9 insertions, 7 deletions
diff --git a/src/verilog/Value.v b/src/verilog/Value.v index 253595b..bde98b8 100644 --- a/src/verilog/Value.v +++ b/src/verilog/Value.v @@ -374,15 +374,17 @@ Proof. destruct b; unfold valueToBool, boolToValue; simpl; trivial. Qed. Lemma ZToValue_valueToNat : forall x sz, + sz > 0 -> (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.*) - admit. - - admit. -Admitted. + - rewrite posToWord_nat. rewrite wordToNat_natToWord_2. trivial. + unfold Z.of_nat in *. destruct sz eqn:?. omega. simpl in H0. + rewrite <- Pos2Z.inj_pow_pos in H0. Search (Z.pos _ < Z.pos _)%Z. + Search Pos.to_nat (_ < _). (* Pos2Nat.inj_lt *) + Search Pos.to_nat. + (* Pos2Nat.is_succ: forall p : positive, exists n : nat, Pos.to_nat p = S n *) + Search S Pos.to_nat. Search (_ < _ <-> _)%positive. assert (exists p, Pos.to_nat p = S n). + econstructor. Search Pos2Nat.is_succ. Search Pos.of_succ_nat. |