Commit 2b96b14d authored by Robbert Krebbers's avatar Robbert Krebbers

Make use of COFE on lists in big ops.

parent 0781afe2
From iris.algebra Require Export cmra.
From iris.algebra Require Export cmra list.
From iris.prelude Require Import gmap.
Fixpoint big_op {A : cmraT} `{Empty A} (xs : list A) : A :=
......@@ -25,8 +25,9 @@ Proof.
- by rewrite !assoc (comm _ x).
- by trans (big_op xs2).
Qed.
Global Instance big_op_proper : Proper (() ==> ()) big_op.
Global Instance big_op_ne n : Proper (dist n ==> dist n) big_op.
Proof. by induction 1; simpl; repeat apply (_ : Proper (_ ==> _ ==> _) op). Qed.
Global Instance big_op_proper : Proper (() ==> ()) big_op := ne_proper _.
Lemma big_op_app xs ys : big_op (xs ++ ys) big_op xs big_op ys.
Proof.
induction xs as [|x xs IH]; simpl; first by rewrite ?left_id.
......
From iris.algebra Require Export upred.
From iris.algebra Require Export upred list.
From iris.prelude Require Import gmap fin_collections.
Import uPred.
......@@ -44,11 +44,9 @@ Proof. by induction 1 as [|P Q Ps Qs HPQ ? IH]; rewrite /= ?HPQ ?IH. Qed.
Global Instance big_sep_proper : Proper (() ==> ()) (@uPred_big_sep M).
Proof. by induction 1 as [|P Q Ps Qs HPQ ? IH]; rewrite /= ?HPQ ?IH. Qed.
Global Instance big_and_ne n :
Proper (Forall2 (dist n) ==> dist n) (@uPred_big_and M).
Global Instance big_and_ne n : Proper (dist n ==> dist n) (@uPred_big_and M).
Proof. by induction 1 as [|P Q Ps Qs HPQ ? IH]; rewrite /= ?HPQ ?IH. Qed.
Global Instance big_sep_ne n :
Proper (Forall2 (dist n) ==> dist n) (@uPred_big_sep M).
Global Instance big_sep_ne n : Proper (dist n ==> dist n) (@uPred_big_sep M).
Proof. by induction 1 as [|P Q Ps Qs HPQ ? IH]; rewrite /= ?HPQ ?IH. Qed.
Global Instance big_and_mono' : Proper (Forall2 () ==> ()) (@uPred_big_and M).
......
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment