Hi everyone, I am trying to prove that these two definitions are same. It is very simple but the challenge is that finding a right lemma to show that `seq.foldr and List.fold_right`

are same (`F`

is a type with `Field`

axioms, `Fadd : F -> F -> F`

, and `0 : F`

(additive identity of plus (`Fadd`

)).

```
Lemma bigop_to_list : forall n (f : ordinal n -> F),
\big[Fadd/0]_(j <- Finite.enum (ordinal_finType n)) (f j)
= List.fold_left Fadd (List.map f (Finite.enum (ordinal_finType n))) 0.
Proof.
intros *.
rewrite List.fold_symmetric.
rewrite unlock /=.
unfold reducebig.
Search (seq.foldr).
Search (fold_right).
n : nat
f : 'I_n -> F
============================
seq.foldr (applybig \o (fun j : 'I_n => BigBody j Fadd true (f j))) 0 (Finite.enum (ordinal_finType n)) =
List.fold_right Fadd 0 (List.map f (Finite.enum (ordinal_finType n)))
goal 2 (ID 963) is:
forall x y z : F, x + (y + z) = x + y + z
goal 3 (ID 964) is:
forall y : F, 0 + y = y + 0
```

Edit: Complete proof.

```
Lemma fold_right_map {n : nat} :
forall (l : list 'I_n) (f : 'I_n -> F),
List.fold_right
(applybig \o (fun j : 'I_n => BigBody j Fadd true (f j))) 0
l =
List.fold_right Fadd 0
(List.map f l).
Proof.
induction l.
+ intros; simpl.
reflexivity.
+ intros; simpl.
rewrite IHl.
reflexivity.
Qed.
Lemma bigop_to_list : forall n (f : ordinal n -> F),
\big[Fadd/0]_(j <- Finite.enum (ordinal_finType n)) (f j)
= List.fold_left Fadd (List.map f (Finite.enum (ordinal_finType n))) 0.
Proof.
intros *.
rewrite unlock /=.
unfold reducebig.
change (@seq.foldr ?A ?B) with (@List.fold_right B A).
rewrite List.fold_symmetric.
rewrite fold_right_map.
reflexivity.
all: intros; field.
Qed.
```

math-comp does not talk about `fold_right`

at all so that's why `Search`

gives no relevant result. However the two functions have almost the same definition, so you can try `change (@seq.foldr ?A ?B) with (@List.fold_right B A).`

Thanks @Li-yao

Mukesh Tiwari has marked this topic as resolved.

Last updated: Jul 15 2024 at 20:02 UTC