diff options
| author | Brian Campbell | 2020-01-07 12:01:42 +0000 |
|---|---|---|
| committer | Brian Campbell | 2020-01-07 12:01:42 +0000 |
| commit | 8f5cc175ebe7bb0bbc10ce639461c7db1fa8488e (patch) | |
| tree | 50438cd8c1f22cef4581e538f5204b68a353128f /lib | |
| parent | 0c881d1137ddd3e0f6e7a39629533bb10609a40f (diff) | |
Coq: accelerate wp steps by improving application of existing specs
Diffstat (limited to 'lib')
| -rw-r--r-- | lib/coq/Hoare.v | 16 |
1 files changed, 15 insertions, 1 deletions
diff --git a/lib/coq/Hoare.v b/lib/coq/Hoare.v index af0e8321..f5d764b2 100644 --- a/lib/coq/Hoare.v +++ b/lib/coq/Hoare.v @@ -1111,7 +1111,6 @@ Create HintDb PrePostE_specs. Ltac PrePostE_step := match goal with - | |- _ => solve [ clear; eauto with nocore PrePostE_specs ] | |- PrePostE _ (bindS _ (fun _ => ?f)) _ _ => eapply PrePostE_bindS_ignore | |- PrePostE _ (bindS _ _) _ _ => eapply PrePostE_bindS; intros | |- PrePostE _ (seqS _ _) _ _ => eapply PrePostE_seqS; intros @@ -1166,4 +1165,19 @@ Ltac PrePostE_step := assert (PAIR : x = existT _ (projT1 x) (projT2 x)) by (destruct x; reflexivity); rewrite PAIR at - 1; clear PAIR + (* Applying specifications from the hintdb. For performance, + * don't use hypotheses from the context (if we need to and it's + not good enough, consider using a separate hintdb) + + * use auto rather than eauto - when eauto is applied to a goal + with an evar Coq falls back to trying all of the specs rather + than picking out one which matches (at least, with 8.9). + *) + | |- PrePostE ?pre _ _ _ => + clear; + solve [ tryif is_evar pre then auto with nocore PrePostE_specs + else (eapply PrePostE_strengthen_pre; + [ auto with nocore PrePostE_specs + | exact (fun s p => p) ]) + ] end. |