 20 Mar, 2017 4 commits


Robbert Krebbers authored

Robbert Krebbers authored
This are useful as proofmode cannot always guess in which direction it should use ⊣⊢.

Ralf Jung authored

Ralf Jung authored

 16 Mar, 2017 10 commits


Robbert Krebbers authored
This fixes issue #81.

Robbert Krebbers authored

Robbert Krebbers authored

Robbert Krebbers authored

Robbert Krebbers authored

Robbert Krebbers authored

Robbert Krebbers authored

Robbert authored
Updating the ProofMode.md docs See merge request !53

Dan Frumin authored

Dan Frumin authored

 15 Mar, 2017 13 commits


Robbert Krebbers authored

Robbert Krebbers authored

Robbert Krebbers authored
The instances frame_big_sepL_cons and frame_big_sepL_app could be applied repeatedly often when framing in [∗ list] k ↦ x ∈ ?e, Φ k x when ?e an evar. This commit fixes this bug.

Robbert Krebbers authored
 Allow framing of persistent hypotheses below the always modality.  Allow framing of persistent hypotheses in just one branch of a disjunction.

Ralf Jung authored

Ralf Jung authored

Ralf Jung authored

Ralf Jung authored

Robbert Krebbers authored

Robbert Krebbers authored

Robbert Krebbers authored

Robbert Krebbers authored

Ralf Jung authored

 14 Mar, 2017 10 commits


Robbert Krebbers authored

Robbert Krebbers authored

Robbert Krebbers authored

Robbert Krebbers authored
This has some advantages:  Evaluation contexts behave like a proper "Huet's zipper", and thus: + We no longer need to reverse the list of evaluation context items in the `reshape_expr` tactic. + The `fill` function becomes tailrecursive.  It gives rise to more definitional equalities in simulation proofs using binary logical relations proofs. In the case of binary logical relations, we simulate an expressions in some ambient context, i.e. `fill K e`. Now, whenever we reshape `e` by turning it into `fill K' e'`, we end up with `fill K (fill K' e')`. In order to use the rules for the expression that is being simulated, we need to turn `fill K (fill K' e')` into `fill K'' e'` for some `K'`. In case of the old `foldr`based approach, we had to rewrite using the lemma `fill_app` to achieve that. However, in case of the old `foldl`based `fill`, we have that `fill K (fill K' e')` is definitionally equal to `fill (K' ++ K) e'` provided that `K'` consists of a bunch of `cons`es (which is always the case, since we obtained `K'` by reshaping `e`). Note that this change hardly affected `heap_lang`. Only the proof of `atomic_correct` broke. I fixed this by proving a more general lemma `ectxi_language_atomic` about `ectxi`languages, which should have been there in the first place.

Robbert Krebbers authored

Robbert Krebbers authored

Robbert Krebbers authored

Robbert Krebbers authored
 Support for a `//` modifier to close the goal using `done`.  Support for framing in the `[#]` specialization pattern for persistent premises, i.e. `[# $H1 $H2]`  Add new "auto framing patterns" `[$]`, `[# $]` and `>[$]` that will try to solve the premise by framing. Hypothesis that are not framed are carried over to the next goal.

Ralf Jung authored

Ralf Jung authored

 12 Mar, 2017 1 commit


Ralf Jung authored

 11 Mar, 2017 2 commits


Robbert Krebbers authored

Robbert Krebbers authored
