The Coq mailing list

[Laurent Thery <Laurent.Thery AT inria.fr>]

Hi,

I think you need to show that you can replace functions under a fold_left

Lemma fold_left_eqf {a : Type} f g  (l : list a) (n : nat) :
  (forall x y, f x y = g x y) ->
fold_left f l n = fold_left g l n.

or rephrase your lemma as:

Lemma fold_left_zero {a : Type}: forall f (l : list a) (n : nat),
(forall n v, f n v = n) -> fold_left f l n = n.


On 08/15/2016 09:20 AM, Durjay Chowdhury wrote:
> Hlw,
>   I am new in Coq. I am stack in a prove related to fold_left.  I
> already proved a lemma:
> Lemma fold_left_zero {a : Type}: forall (l : list a) (n : nat),
> fold_left (fun (n1 : nat) (_ : a) => n1) l n = n.
>
> Now i  try to use this lemma in the following goal but i am not able to
> do it.
>
> fold_left
>   (fun (n : nat) (_ : x) =>
>    fold_left (fun (n0 : nat) (_ : y) => n0) elements n)
>   elements 0 = 0
>
> I need some help.
>
> Regards
> Durjat