diff options
| author | Brian Campbell | 2018-09-03 12:00:16 +0100 |
|---|---|---|
| committer | Brian Campbell | 2018-09-03 12:03:32 +0100 |
| commit | 5a947f5d5f5fd9b83f27bfd4e43170f51d4a27a7 (patch) | |
| tree | a8cc02ddf53de89b476f71b66bdbfbe9c933703c /lib/coq/Sail2_prompt.v | |
| parent | 5ef8cae069e512d3b4ae6793f452d823d34a7af5 (diff) | |
Coq: rework generation of dependent pairs so that they are only
constructed when a function call, cast, or binder demands them, removing
some ambiguous corner cases.
Also
- Don't simplify nexps before printing (note that we usually end up
needing a (8 * x) / 8 lemma as a result)
- More extraction of properties in the goal
- Splitting of conditionals/matches in goals (which can occur more often
because of the new positions of build_ex in definitions)
- Try simple solving first to improve speed / reduce proof sizes / help
fill in metavariables (because manipulating the goal can interfere with
instantiating them)
- Update RISC-V patch
Diffstat (limited to 'lib/coq/Sail2_prompt.v')
| -rw-r--r-- | lib/coq/Sail2_prompt.v | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/lib/coq/Sail2_prompt.v b/lib/coq/Sail2_prompt.v index 0b3a2cd8..0f2c0955 100644 --- a/lib/coq/Sail2_prompt.v +++ b/lib/coq/Sail2_prompt.v @@ -125,3 +125,6 @@ Definition build_ex_m {rv e} {T:Type} (x:monad rv T e) {P:T -> Prop} `{H:forall Definition projT1_m {rv e} {P:Z -> Prop} (x: monad rv {x : Z & P x} e) : monad rv Z e := x >>= fun y => returnm (projT1 y). +Definition derive_m {rv e} {P Q:Z -> Prop} (x : monad rv {x : Z & P x} e) `{forall x, ArithFact (P x) -> ArithFact (Q x)} : monad rv {x : Z & (ArithFact (Q x))} e := + x >>= fun y => returnm (build_ex (projT1 y)). + |