diff options
| author | James Pollard <james@pollard.dev> | 2020-06-17 23:19:48 +0100 |
|---|---|---|
| committer | James Pollard <james@pollard.dev> | 2020-06-17 23:19:48 +0100 |
| commit | 9a65ca2731adf234f5ce946503314267ced62a44 (patch) | |
| tree | 507f7fe0c03fca5eea8d2932df301a130bb3b14d /src/verilog | |
| parent | 00c579e603478d452959dde0ec61672d7b5d27a4 (diff) | |
| download | vericert-9a65ca2731adf234f5ce946503314267ced62a44.tar.gz vericert-9a65ca2731adf234f5ce946503314267ced62a44.zip | |
Fix Inop proof to work with new array semantics.
Diffstat (limited to 'src/verilog')
| -rw-r--r-- | src/verilog/Array.v | 8 |
1 files changed, 8 insertions, 0 deletions
diff --git a/src/verilog/Array.v b/src/verilog/Array.v index 0b6e2a9..705dea7 100644 --- a/src/verilog/Array.v +++ b/src/verilog/Array.v @@ -83,6 +83,14 @@ Hint Resolve array_set_spec2 : array. Definition array_get_error {A : Type} (i : nat) (a : Array A) : option A := nth_error a.(arr_contents) i. +Lemma array_get_error_equal {A : Type} : + forall (a b : Array A) i, + a.(arr_contents) = b.(arr_contents) -> + array_get_error i a = array_get_error i b. +Proof. + unfold array_get_error. congruence. +Qed. + Lemma array_get_error_bound {A : Type} : forall (a : Array A) i, i < a.(arr_length) -> exists x, array_get_error i a = Some x. |