diff options
| author | Brian Campbell | 2018-08-14 18:15:24 +0100 |
|---|---|---|
| committer | Brian Campbell | 2018-08-14 21:07:23 +0100 |
| commit | 39fea17bac77535c9cff47cd6657a308e391ac8a (patch) | |
| tree | 05c3bb014d38bfd87b9f09bd43cd80c0f4e1a1a2 /lib | |
| parent | 7adf0f81af82f3d401a9b45f87c1dc92c5062f8e (diff) | |
Coq: attempt a quick proof before an indepth one
Diffstat (limited to 'lib')
| -rw-r--r-- | lib/coq/Sail2_values.v | 8 |
1 files changed, 7 insertions, 1 deletions
diff --git a/lib/coq/Sail2_values.v b/lib/coq/Sail2_values.v index 7766e6af..c63e8453 100644 --- a/lib/coq/Sail2_values.v +++ b/lib/coq/Sail2_values.v @@ -1021,6 +1021,9 @@ Ltac prepare_for_solver := reduce_list_lengths; reduce_pow. Ltac solve_arithfact := +(* Attempt a simple proof first to avoid lengthy preparation steps (especially + as the large proof terms can upset subsequent proofs). *) +try (constructor; omega); prepare_for_solver; (*dump_context;*) solve @@ -1037,7 +1040,10 @@ prepare_for_solver; | constructor; eauto 3 with datatypes zarith sail | constructor; idtac "Unable to solve constraint"; dump_context; fail ]. -Hint Extern 0 (ArithFact _) => solve_arithfact : typeclass_instances. +(* Add an indirection so that you can redefine run_solver to fail to get + slow running constraints into proof mode. *) +Ltac run_solver := solve_arithfact. +Hint Extern 0 (ArithFact _) => run_solver : typeclass_instances. Hint Unfold length_mword : sail. |