 07 Apr, 2017 1 commit


JacquesHenri Jourdan authored

 24 Mar, 2017 5 commits


Robbert Krebbers authored

Robbert Krebbers authored
This commit fixes the issues that refolding of big operators did not work nicely in the proof mode, e.g., given: Goal forall M (P : nat → uPred M) l, ([∗ list] x ∈ 10 :: l, P x) ∗ True. Proof. iIntros (M P l) "[H1 H2]". We got: "H1" : P 10 "H2" : (fix big_opL (M0 : ofeT) (o : M0 → M0 → M0) (H : Monoid o) (A : Type) (f : nat → A → M0) (xs : list A) {struct xs} : M0 := match xs with  [] => monoid_unit  x :: xs0 => o (f 0 x) (big_opL M0 o H A (λ n : nat, f (S n)) xs0) end) (uPredC M) uPred_sep uPred.uPred_sep_monoid nat (λ _ x : nat, P x) l ∗ True The problem here is that proof mode looked for an instance of `IntoAnd` for `[∗ list] x ∈ 10 :: l, P x` and then applies the instance for separating conjunction without folding back the fixpoint. This problem is not specific to the Iris proof mode, but more of a general problem of Coq's `apply`, for example: Goal forall x l, Forall (fun _ => True) (map S (x :: l)). Proof. intros x l. constructor. Gives: Forall (λ _ : nat, True) ((fix map (l0 : list nat) : list nat := match l0 with  [] => []  a :: t => S a :: map t end) l) This commit fixes this issue by making the big operators type class opaque and instead handle them solely via corresponding type classes instances for the proof mode tactics. Furthermore, note that we already had instances for persistence and timelessness. Those were really needed; computation did not help to establish persistence when the list in question was not a ground term. In fact, the sitation was worse, to establish persistence of `[∗ list] x ∈ 10 :: l, P x` it could either use the persistence instance of big ops directly, or use the persistency instance for `∗` first. Worst case, this can lead to an exponential blow up because of back tracking.

Robbert Krebbers authored

Robbert Krebbers authored
Instead, I have introduced a type class `Monoid` that is used by the big operators: Class Monoid {M : ofeT} (o : M → M → M) := { monoid_unit : M; monoid_ne : NonExpansive2 o; monoid_assoc : Assoc (≡) o; monoid_comm : Comm (≡) o; monoid_left_id : LeftId (≡) monoid_unit o; monoid_right_id : RightId (≡) monoid_unit o; }. Note that the operation is an argument because we want to have multiple monoids over the same type (for example, on `uPred`s we have monoids for `∗`, `∧`, and `∨`). However, we do bundle the unit because:  If we would not, the unit would appear explicitly in an implicit argument of the big operators, which confuses rewrite. By bundling the unit in the `Monoid` class it is hidden, and hence rewrite won't even see it.  The unit is unique. We could in principle have big ops over setoids instead of OFEs. However, since we do not have a canonical structure for bundled setoids, I did not go that way.

Robbert Krebbers authored

 21 Mar, 2017 1 commit


Ralf Jung authored

 20 Mar, 2017 1 commit


Robbert Krebbers authored

 14 Mar, 2017 1 commit


Ralf Jung authored

 11 Mar, 2017 1 commit


Robbert Krebbers authored

 10 Mar, 2017 2 commits
 09 Mar, 2017 3 commits


Robbert Krebbers authored
Now, we never need to unfold LimitPreserving in LambdaRust, and hence the entails_lim tactic is no longer needed.

Ralf Jung authored

Robbert Krebbers authored

 01 Mar, 2017 1 commit


Ralf Jung authored

 23 Feb, 2017 1 commit


Ralf Jung authored

 22 Feb, 2017 3 commits


Ralf Jung authored

Robbert Krebbers authored

Ralf Jung authored

 21 Feb, 2017 1 commit


Ralf Jung authored

 16 Feb, 2017 1 commit


Robbert Krebbers authored

 11 Feb, 2017 1 commit


Robbert Krebbers authored

 10 Feb, 2017 5 commits


Robbert Krebbers authored

Robbert Krebbers authored

Robbert Krebbers authored

Robbert Krebbers authored

Robbert Krebbers authored

 09 Feb, 2017 3 commits


Robbert Krebbers authored

Robbert Krebbers authored

Robbert Krebbers authored

 06 Feb, 2017 1 commit


Ralf Jung authored

 03 Feb, 2017 1 commit


Robbert Krebbers authored

 01 Feb, 2017 2 commits


Robbert Krebbers authored

JacquesHenri Jourdan authored
Cancelable elements are a new way of proving local updates, by removing some cancellable element of the global state, provided that we own it and we are willing to lose this ownership. Identityfree elements are an auxiliary that is necessary to prove that [Some x] is cancelable. For technical reasons, these two notions are not defined exactly like what one might expect, but also take into account validity. Otherwise, an exclusive element would not be cancelable or idfree, which is rather confusing.

 30 Jan, 2017 2 commits


Robbert Krebbers authored

JacquesHenri Jourdan authored

 27 Jan, 2017 1 commit


Ralf Jung authored

 26 Jan, 2017 1 commit


JacquesHenri Jourdan authored

 25 Jan, 2017 1 commit


Robbert Krebbers authored
Also, give names to hypotheses that we refer to.
