 24 May, 2016 5 commits


Robbert Krebbers authored

Robbert Krebbers authored
To do so, we have introduced the specialization patterns: =>[H1 .. Hn] and =>[H1 .. Hn] That generate a goal in which the view shift is preserved. These specialization patterns can also be used for e.g. iApply. Note that this machinery is not tied to primitive view shifts, and works for various kinds of goal (as captured by the ToAssert type class, which describes how to transform the asserted goal based on the main goal). TODO: change the name of these specialization patterns to reflect this generality.

Robbert Krebbers authored

Robbert Krebbers authored

Robbert Krebbers authored
Changes:  We no longer have a different syntax for specializing a term H : P ★ Q whose range P or domain Q is persistent. There is just one syntax, and the system automatically determines whether either P or Q is persistent.  While specializing a term, always modalities are automatically stripped. This gets rid of the specialization pattern !.  Make the syntax of specialization patterns more consistent. The syntax for generating a goal is [goal_spec] where goal_spec is one of the following: H1 .. Hn : generate a goal using hypotheses H1 .. Hn H1 .. Hn : generate a goal using all hypotheses but H1 .. Hn # : generate a goal for the premise in which all hypotheses can be used. This is only allowed when specializing H : P ★ Q where either P or Q is persistent. % : generate a goal for a pure premise.

 22 May, 2016 7 commits


Robbert Krebbers authored

Robbert Krebbers authored
Initial commit by Amin Timany.

Robbert Krebbers authored

Robbert Krebbers authored

Robbert Krebbers authored

Robbert Krebbers authored

Robbert Krebbers authored

 21 May, 2016 1 commit


Ralf Jung authored

 20 May, 2016 3 commits


Robbert Krebbers authored

Robbert Krebbers authored
I have introduced the following definition to avoid many case analyses where both branches had nearly identical proofs. Definition uPred_always_if {M} (p : bool) (P : uPred M) : uPred M := (if p then □ P else P)%I.

Robbert Krebbers authored

 19 May, 2016 1 commit


Ralf Jung authored

 13 May, 2016 2 commits
 10 May, 2016 10 commits


Robbert Krebbers authored

Robbert Krebbers authored

Robbert Krebbers authored
And make constants P for which we do not want of_val P to reduce Opaque.

Robbert Krebbers authored
through definitions.

Robbert Krebbers authored

Robbert Krebbers authored

Robbert Krebbers authored

Robbert Krebbers authored

Robbert Krebbers authored
This is more consistent with wp_cas_fail.

Robbert Krebbers authored

 09 May, 2016 1 commit


Robbert Krebbers authored

 07 May, 2016 4 commits


Robbert Krebbers authored

Robbert Krebbers authored

Robbert Krebbers authored

Robbert Krebbers authored

 06 May, 2016 6 commits


Robbert Krebbers authored

Robbert Krebbers authored

Robbert Krebbers authored
We may want to do the same for iIntros ? and iDestruct "H" as {?} "H", but that requires more work. However, I do not think I want to rely on names chosen this way.

Robbert Krebbers authored

Robbert Krebbers authored

Robbert Krebbers authored
