Skip to content

Generic big operators that are computational for lists

Robbert Krebbers requested to merge gen_big_op into master

This merge request fixes issue #38 (closed).

Monoids

Big operators are no longer tied to CMRAs. Instead, I have introduced a type class Monoid that is used by all 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 uPreds 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.

Big operators

The list big operator is now defined as:

Fixpoint big_opL `{Monoid M o} {A} (f : nat → A → M) (xs : list A) : M :=
  match xs with
  | [] => monoid_unit
  | x :: xs => o (f 0 x) (big_opL (λ n, f (S n)) xs)
  end.

Note that it no longer relies on imap and that we get the desired unfolding of cons definitionally.

The generic notation is [^o list] k ↦ y ∈ l.

On top of the big operator for lists, I have defined big operators for maps, sets, and multisets.

Problems

It works well, and I started porting lambdarust where simpl beautifully unfolds the new big ops. Also, I was able to remove most uses of big_sepL_cons and big_sepL_nil. There are still some problems though:

Problem 1

We still have the ambiguously when one can split the big op and the predicate inside of the big op, see #76 (closed). This merge request does not change the status quo.

Problem 2

Refolding of big operators in the proof mode does not work nicely, e.g.:

Goal forall M (P : nat → uPred M) l,
  ([∗ list] x ∈ 10 :: l, P x) -∗ True.
Proof. iIntros (M P l) "[H1 H2]".

Now we get:

"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 looks for an instance of IntoAnd for [∗ list] x ∈ 10 :: l, P x and then applies the instance for separating conjunction after 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)

I see some solutions:

  • Require one to always run simpl before destructing big ops. If I do iIntros (M P l) "/= [H1 H2]". in the above example, I nicely get:

    "H1" : P 10
"H2" : [∗ list] x ∈ l, P x
--------------------------------------∗
True

  • Add specific IntoAnd and FromSep instances for big operators with cons that have a lower precedence. For the case of Frame, which is not a leaf instance, we have to be careful though, as it could lead to an exponential explosion due to backtracking on both the big operator and the separating conjunction instance.

  • Make big operators type class opaque and handle them solely via instance in proof mode instead of relying on their computational behavior.

Merge request reports