diff options
| author | Brian Campbell | 2019-12-06 10:45:19 +0000 |
|---|---|---|
| committer | Brian Campbell | 2019-12-06 10:45:19 +0000 |
| commit | 235a320e94b432c3ccf021d77c6e8303e1d1a19d (patch) | |
| tree | af58f8737d3c8c2aeeabb454d42f3231f0df76fe /lib/coq/Sail2_state_lemmas.v | |
| parent | d3c7951842da31b511709bb2c6655ebb2e285914 (diff) | |
Coq: use proof irrelevance for a few properties
Includes removing an explicit use of a lemma generated by abstract, which
was causing problems with different versions of Coq because the names
change.
Diffstat (limited to 'lib/coq/Sail2_state_lemmas.v')
| -rw-r--r-- | lib/coq/Sail2_state_lemmas.v | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/lib/coq/Sail2_state_lemmas.v b/lib/coq/Sail2_state_lemmas.v index 39406208..5f409e22 100644 --- a/lib/coq/Sail2_state_lemmas.v +++ b/lib/coq/Sail2_state_lemmas.v @@ -730,6 +730,8 @@ induction (S (Z.abs_nat (from - to))); intros. reflexivity. * simpl. rewrite_liftState. + destruct (sumbool_of_bool (from + off <=? to)); auto. + repeat replace_ArithFact_proof. reflexivity. Qed. Hint Rewrite liftState_foreach_ZM_up : liftState. @@ -751,6 +753,8 @@ induction (S (Z.abs_nat (from - to))); intros. reflexivity. * simpl. rewrite_liftState. + destruct (sumbool_of_bool (to <=? from + off)); auto. + repeat replace_ArithFact_proof. reflexivity. Qed. Hint Rewrite liftState_foreach_ZM_down : liftState. |