coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- 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
- [Coq-Club] Applying Lemma in fold_left, Durjay Chowdhury, 08/15/2016
- Re: [Coq-Club] Applying Lemma in fold_left, Laurent Thery, 08/21/2016
- RE: [Coq-Club] Applying Lemma in fold_left, Soegtrop, Michael, 08/21/2016
- Re: [Coq-Club] Applying Lemma in fold_left, John Wiegley, 08/21/2016
Archive powered by MHonArc 2.6.18.