diff options
| author | Brian Campbell | 2019-06-20 18:06:15 +0100 |
|---|---|---|
| committer | Brian Campbell | 2019-06-20 18:26:13 +0100 |
| commit | 1c0c0df14031ba707bd8eb4cbb71c15180de4367 (patch) | |
| tree | d259c0494b42cdd88472e07747c7d598464df88c /lib | |
| parent | 6ad6ce9c1777841e00c1716b55bfcc28c61304a3 (diff) | |
Coq: avoid some unnecessary reduction in the constraint solver
Diffstat (limited to 'lib')
| -rw-r--r-- | lib/coq/Sail2_values.v | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/lib/coq/Sail2_values.v b/lib/coq/Sail2_values.v index e152fb67..1bec7c3b 100644 --- a/lib/coq/Sail2_values.v +++ b/lib/coq/Sail2_values.v @@ -1636,6 +1636,8 @@ Lemma Z_compare_eq_gt : Eq = Gt -> False. congruence. Qed. Lemma Z_compare_gt_lt : Gt = Lt -> False. congruence. Qed. Lemma Z_compare_gt_eq : Gt = Eq -> False. congruence. Qed. Ltac z_comparisons := + (* Don't try terms with variables - reduction may be expensive *) + match goal with |- context[?x] => is_var x; fail 1 | |- _ => idtac end; solve [ exact eq_refl | exact Z_compare_lt_eq @@ -1772,7 +1774,7 @@ Ltac solve_arithfact := (* Attempt a simple proof first to avoid lengthy preparation steps (especially as the large proof terms can upset subsequent proofs). *) intros; (* To solve implications for derive_m *) -try (exact trivial_range); +match goal with |- ArithFact (?x <= ?x <= ?x) => try (exact trivial_range) | _ => idtac end; try fill_in_evar_eq; try match goal with |- context [projT1 ?X] => apply (ArithFact_self_proof X) end; (* Trying reflexivity will fill in more complex metavariable examples than |