 08 Dec, 2016 4 commits


Robbert Krebbers authored
Example: Goal ¬False → ¬False → ¬False → ¬False → ¬False → ¬False → ¬False → False. Proof. intros. done. (* takes very long *)

Ralf Jung authored
Add locking to valuescope notation for lambdas This attempts to hide all our locking machinery so that users don't have to care. To this end, `locked` is added to the valuescope notation for lambdas and recursive functions, and the tactics wp_rec and wp_lam are enhanced to unlock properly. The main open question is: How can we figure out automatically what to unfold? The heuristic I cam up with fails in barrier_client because there, we have a value parameterized by something on the Coq level. Maybe a more viable alternative would be to add locking to the coercion that embeds values into expressions? Cc @robbertkrebbers @jjourdan See merge request !34

Robbert Krebbers authored

Ralf Jung authored

 07 Dec, 2016 3 commits
 06 Dec, 2016 23 commits


Robbert Krebbers authored

Robbert Krebbers authored

Ralf Jung authored


Ralf Jung authored

Ralf Jung authored

Ralf Jung authored

Ralf Jung authored

Ralf Jung authored


Ralf Jung authored

Ralf Jung authored

Dan Frumin authored

Ralf Jung authored

Ralf Jung authored


Ralf Jung authored

Robbert Krebbers authored

Robbert Krebbers authored

Robbert Krebbers authored

Ralf Jung authored

Robbert Krebbers authored

 05 Dec, 2016 10 commits


JacquesHenri Jourdan authored

JacquesHenri Jourdan authored

JacquesHenri Jourdan authored

JacquesHenri Jourdan authored

Robbert Krebbers authored
I added the old one in 176a588c but it was never used.

Ralf Jung authored

Robbert Krebbers authored

Robbert authored
New definition of contractive. The current notion of `Contractive` does not allow one to deal with functions with multiple arguments, for example, binary functions that are contractive in both arguments (like `lft_vs` in lambdarust), or binary functions that are contractive in one of their arguments. To that end, I propose I reformulate the notion of `Contractive` so that we can express being contractive using a `Proper`. The new definition is: Definition dist_later {A : ofeT} (n : nat) (x y : A) : Prop := match n with 0 => True  S n => x ≡{n}≡ y end. Notation Contractive f := (∀ n, Proper (dist_later n ==> dist n) f). Also, it turns out that using this definition we can implement a `solve_contractive` tactic in the same way as the `solve_proper` tactic. Unfortunately, the new tactic does not quite work for the weakest precondition connective in Iris because the proof involves induction, and the induction hypothesis does not quite fit into the new `solve_contractive` tactic. See merge request !32

Robbert Krebbers authored
Using this new definition we can express being contractive using a Proper. This has the following advantages:  It makes it easier to state that a function with multiple arguments is contractive (in all or some arguments).  A solve_contractive tactic can be implemented by extending the solve_proper tactic.

Robbert Krebbers authored
This removes Ralf's hack of using later_car, which is not function in the logic. Thanks to Aleš for suggesting this.
