diff options
| author | Brian Campbell <Brian.Campbell@ed.ac.uk> | 2022-05-09 09:32:22 +0100 |
|---|---|---|
| committer | Brian Campbell <Brian.Campbell@ed.ac.uk> | 2022-08-09 10:49:56 +0100 |
| commit | 2265a2576fac6d555cfc5f850f78e79c2da56312 (patch) | |
| tree | 3f8808214bb50d47c78d0478b24429f500f659d4 /handwritten_support/riscv_extras.v | |
| parent | 5fce6fbd46cb415e2b857a905cc8b49e4dde203b (diff) | |
| download | sail-riscv-2265a2576fac6d555cfc5f850f78e79c2da56312.zip sail-riscv-2265a2576fac6d555cfc5f850f78e79c2da56312.tar.gz sail-riscv-2265a2576fac6d555cfc5f850f78e79c2da56312.tar.bz2 | |
Minimal updates for Coq proof assistant output
Diffstat (limited to 'handwritten_support/riscv_extras.v')
| -rw-r--r-- | handwritten_support/riscv_extras.v | 6 |
1 files changed, 4 insertions, 2 deletions
diff --git a/handwritten_support/riscv_extras.v b/handwritten_support/riscv_extras.v index 03249f0..bf3e7bc 100644 --- a/handwritten_support/riscv_extras.v +++ b/handwritten_support/riscv_extras.v @@ -69,6 +69,7 @@ Require Import Sail.Base. Require Import String. Require Import List. +Require Import Lia. Import List.ListNotations. Open Scope Z. @@ -190,7 +191,7 @@ unbool_comparisons. unbool_comparisons_goal. assert (Z.abs n = n). { rewrite Z.abs_eq; auto with zarith. } rewrite <- H at 3. -lapply (ZEuclid.mod_always_pos m n); omega. +lapply (ZEuclid.mod_always_pos m n); lia. Qed. (* Override the more general version *) @@ -210,6 +211,7 @@ Axiom sys_enable_writable_misa : unit -> bool. Axiom sys_enable_rvc : unit -> bool. Axiom sys_enable_fdext : unit -> bool. Axiom sys_enable_next : unit -> bool. +Axiom sys_enable_zfinx : unit -> bool. (* The constraint solver can do this itself, but a Coq bug puts anonymous_subproof into the term instead of an actual subproof. *) @@ -217,6 +219,6 @@ Lemma n_leading_spaces_fact {w__0} : w__0 >= 0 -> exists ex17629_ : Z, 1 + w__0 = 1 + ex17629_ /\ 0 <= ex17629_. intro. exists w__0. -omega. +lia. Qed. Hint Resolve n_leading_spaces_fact : sail. |