Stream: math-comp users

Topic: ✔ Proof about \big and List.fold_left


view this post on Zulip Mukesh Tiwari (May 25 2022 at 17:30):

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.

view this post on Zulip Li-yao (May 25 2022 at 17:35):

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).

view this post on Zulip Mukesh Tiwari (May 25 2022 at 18:02):

Thanks @Li-yao

view this post on Zulip Notification Bot (May 26 2022 at 08:05):

Mukesh Tiwari has marked this topic as resolved.


Last updated: Jul 15 2024 at 20:02 UTC