`big_op*_forall` that relate traversals over different structures
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.