Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] Applying Lemma in fold_left

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Applying Lemma in fold_left


Chronological Thread 
  • From: Laurent Thery <Laurent.Thery AT inria.fr>
  • To: coq-club AT inria.fr
  • Subject: Re: [Coq-Club] Applying Lemma in fold_left
  • Date: Sun, 21 Aug 2016 14:51:56 +0200


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



Archive powered by MHonArc 2.6.18.

Top of Page