 24 Mar, 2017 9 commits


Robbert Krebbers committed

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 committed 
Robbert Krebbers committed

Robbert Krebbers committed

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 committed 
Big ops over list with a cons reduce, hence these just follow immediately from conversion.
Robbert Krebbers committed 
Robbert Krebbers committed
 23 Mar, 2017 1 commit

 22 Mar, 2017 2 commits
 21 Mar, 2017 5 commits


Robbert Krebbers committed

This could lead to awkward loops, for example, when having:  As goal `own γ c` with `c` persistent, one could keep on `iSplit`ting the goal. Especially in (semi)automated proof scripts this is annoying as it easily leads to loops.  When having a hypothesis `own γ c` with `c` persistent, one could keep on `iDestruct`ing it. To that end, this commit removes the `IntoOp` and `FromOp` instances for persistent CMRA elements. Instead, we changed the instances for pairs, so that one, for example, can still split `(a ⋅ b, c)` with `c` persistent.
Robbert Krebbers committed 
Robbert Krebbers committed

Ralf Jung committed
 20 Mar, 2017 5 commits


Robbert Krebbers committed

Robbert Krebbers committed

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

Ralf Jung committed

 16 Mar, 2017 10 commits


Robbert Krebbers committed

Robbert Krebbers committed

Robbert Krebbers committed

Robbert Krebbers committed

Robbert Krebbers committed

Robbert Krebbers committed

Dan Frumin committed

Dan Frumin committed
 15 Mar, 2017 8 commits


Robbert Krebbers committed

Robbert Krebbers committed

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 committed 
 Allow framing of persistent hypotheses below the always modality.  Allow framing of persistent hypotheses in just one branch of a disjunction.
Robbert Krebbers committed 
Ralf Jung committed

Ralf Jung committed

Ralf Jung committed

Ralf Jung committed
