diff options
| author | Yann Herklotz <git@yannherklotz.com> | 2020-02-04 14:53:03 +0000 |
|---|---|---|
| committer | Yann Herklotz <git@yannherklotz.com> | 2020-02-04 14:53:03 +0000 |
| commit | b3b21c2d8cb6b89087e30cb901523915b8d71f44 (patch) | |
| tree | fa897bfaa43791bf9745206fcf572f8f610b289d | |
| parent | 4d26fb772d1c685aca6da7e97b5a65da1dd6a833 (diff) | |
| download | vericert-b3b21c2d8cb6b89087e30cb901523915b8d71f44.tar.gz vericert-b3b21c2d8cb6b89087e30cb901523915b8d71f44.zip | |
Add nix file
| -rw-r--r-- | default.nix | 10 | ||||
| -rw-r--r-- | src/CoqUp/Verilog.v | 15 |
2 files changed, 23 insertions, 2 deletions
diff --git a/default.nix b/default.nix new file mode 100644 index 0000000..4e1cfbb --- /dev/null +++ b/default.nix @@ -0,0 +1,10 @@ +with import <nixpkgs> {}; + +stdenv.mkDerivation { + name = "CoqUp"; + src = ./.; + + buildInputs = [ coq_8_10 ]; + + buildPhase = "make"; +} diff --git a/src/CoqUp/Verilog.v b/src/CoqUp/Verilog.v index 0e5c193..de1910c 100644 --- a/src/CoqUp/Verilog.v +++ b/src/CoqUp/Verilog.v @@ -153,8 +153,6 @@ Module Verilog. constructor. apply Forall_forall. intros. inversion H. Qed. - Search "mod" nat. - Lemma check_5_is_101 : value_to_nat (VArray [VBool true; VBool false; VBool true]) = Some 5. Proof. reflexivity. Qed. @@ -165,6 +163,7 @@ Module Verilog. Proof. intros. unfold cons_value. destruct v. - constructor. apply Forall_forall. intros. + inversion H0; subst. constructor. inversion H1; subst. constructor. inversion H2. - intros. inversion H. inversion H1; subst; constructor. @@ -191,6 +190,18 @@ Module Verilog. intros. unfold nat_to_value. apply nat_to_value'_is_flat. Qed. + Lemma nat_to_value_idempotent : + forall (sz n : nat), + sz > 0 -> (value_to_nat' sz (nat_to_value' sz n)) = Some n. + Proof. + induction sz; intros. + - inversion H. + - unfold_rec value_to_nat'. + assert (flat_valueP (nat_to_value' (S sz) n)). + { apply nat_to_value'_is_flat. } + destruct (nat_to_value' (S sz) n) eqn:?. + Admitted. + Module VerilogNotation. Declare Scope verilog_scope. |