Most lemmas that relate several `big_op`

statements only concern themselves with the case when the iteration is performed on the same data. However, at times, even if the structures are actually different, the values combined by `o`

are, in fact, the same.

So, I think that `big_op*_forall`

can be usefully generalized.

Here is my attempt at generalizing `big_opL_forall`

:

```
Theorem big_opL_forall' {M: ofeT} {o: M -> M -> M} {H': Monoid o} {A B: Type}
R f g (l: list A) (l': list B):
Reflexive R ->
Proper (R ==> R ==> R) o ->
length l = length l' ->
(forall k y y', l !! k = Some y -> l' !! k = Some y' -> R (f k y) (g k y')) ->
R ([^o list] k ↦ y ∈ l, f k y) ([^o list] k ↦ y ∈ l', g k y).
Proof.
intros ??. revert l' f g. induction l as [|x l IH]=> l' f g HLen HHyp //=.
all: destruct l'; inversion HLen; eauto.
simpl. f_equiv; eauto.
Qed.
```

A client of this theorem that I actually needed:

```
Lemma big_opL_irrelevant_element (M: ofeT) (o: M -> M -> M) (H': Monoid o)
{A: Type} n (P: nat -> M) (l: list A):
([^o list] i ↦ _ ∈ l, P (n+i)%nat)%I =
([^o list] i ∈ seq n (length l), P i%nat)%I.
Proof.
assert (length l = length (seq n (length l))) as HSeqLen
by (rewrite seq_length; auto).
apply big_opL_forall'; try apply _. done.
intros ? ? ? _ HElem.
assert (k < length l)%nat as HKLt.
{ rewrite HSeqLen. apply lookup_lt_is_Some. by eexists. }
apply nth_lookup_Some with (d:=O) in HElem.
rewrite seq_nth in HElem; subst; done.
Qed.
```

Without `big_forall'`

, I couldn't come up with such a straightforward proof and ended up with this unpleasantness:

```
Lemma big_opL_irrelevant_element (M: ofeT) (o: M -> M -> M) (H': Monoid o)
{A: Type} n (P: nat -> M) (l: list A):
([^o list] i ↦ _ ∈ l, P (n+i)%nat)%I =
([^o list] i ∈ seq n (length l), P i%nat)%I.
Proof.
move: n. induction l; simpl. done.
move=> n. rewrite -plus_n_O.
specialize (IHl (S n)).
rewrite -IHl /= (big_opL_forall _ _ (fun i _ => P (S (n + i))%nat)) //.
intros. by rewrite plus_n_Sm.
Qed.
```

I tried the second approach to see if it brings anything new on the table, but since the task of the proof search is to find an element of `a ∈ l → CoreId a`

, the fact that `a ∈ l`

can be automatically found doesn't help one bit.

This lemma can be improved by automatically constructing the proof of `CoreId l`

from `length l`

proofs of `CoreId x`

. This way, say, `CoreId x → CoreId [x]`

could be automatically found.

For example, like this: strong_list_core_id.v This way, the old `list_core_id`

isn't required at all, it can be found automatically. Maybe `ListForall`

already exists in some form? Or maybe it is useful for other similar cases?

I'm not sure. When I replace the existing `list_core_id`

with the one above in the current `master`

, everything builds. Neither the `examples`

repository nor `lambda-rust`

reference `listUR`

or `listR`

directly, so I couldn't find existing clients to check the change against them. Intuitively, if everything is fine with Coq's search, proving `forall x, x ∈ l -> CoreId x`

isn't harder than proving `forall x, CoreId x`

.

Do I need to do anything else to check that everything is fine?

Hi!

I needed a stronger version of `list_core_id`

that could depend on the structure of a particular list, similarly to `pair_core_id`

. I came up with this:

```
Global Instance list_core_id l : (forall x, x ∈ l -> CoreId x) -> CoreId l.
Proof.
intros Hyp. constructor. apply list_equiv_lookup=> i.
rewrite list_lookup_core.
destruct (l !! i) eqn:E.
2: done.
apply Hyp.
eapply elem_of_list_lookup; by eauto.
Qed.
```

It probably could serve as a drop-in replacement for the old one.

I only tried it on 8.9.1.

Version of Iris: dev.2019-07-01.1.6e79f000

Typeclass search fails when trying to prove that a particular statement is persistent.

In resource algebra

```
authR (prodUR
(prodUR
(optionUR (exclR unitO))
(optionUR (exclR unitO)))
(optionUR (agreeR (boolO))))
```

proof of

`Persistent (own γ (◯((None, None), Some (to_agree true))))`

fails with

`Proof search failed without reaching its limit.`

if performed with `typeclasses eauto 10`

. It similarly doesn't work with `apply _`

.

The statement is actually persistent, as shown by Jonas Kastberg:

```
Proof.
apply own_core_persistent.
apply auth_frag_core_id.
apply pair_core_id; typeclasses eauto.
Qed.
```

Minimal (non-)working example: https://pastebin.com/T7zhm9Zu

Some useful laws I thought of (or actually needed when verifying a counting semaphore):

- General laws of exponentiation for commutative associative structures:
`(P ∗ Q)^n = P^n ∗ Q^n`

,`P^n ∗ P^m = P^(n+m)`

. -
`NonExpansive`

. -
`Persistent`

and`Timeless`

if`P`

is such.

Sometimes it makes sense to have a statement about possessing `n`

copies of the same resource. For example (in pseudocode), `own γ 1%Qp -∗ (own γ (1/n))^n`

. Maybe such an operation should be available in the standard library, along with some useful lemmas about exponentiation?

An example of what exponentiation could be defined as:

```
Fixpoint iPropPow {Σ} (R : iProp Σ) (n : nat) : iProp Σ :=
match n with
| 0 => (True)%I
| S n' => (R ∗ iPropPow R n')%I
end.
```