coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Applying Lemma in fold_left

From: Durjay Chowdhury <durjaycsecu AT gmail.com>
To: coq-club AT inria.fr
Subject: [Coq-Club] Applying Lemma in fold_left
Date: Mon, 15 Aug 2016 00:20:18 -0700
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=durjaycsecu AT gmail.com; spf=Pass smtp.mailfrom=durjaycsecu AT gmail.com; spf=None smtp.helo=postmaster AT mail-ua0-f177.google.com
Ironport-phdr: 9a23:LFU3BB08qhitDHjMsmDT+DRfVm0co7zxezQtwd8ZsegQK/ad9pjvdHbS+e9qxAeQG96KsrQd16GP6vioGTRZp83Q6DZaKN0EfiRGoP1epxYnDs+BBB+zB9/RRAt+Iv5/UkR49WqwK0lfFZW2TVTTpnqv8WxaQU2nZkJLL+j4UrTfk96wn7jrvcaCOkMR2HHkOOs6bE3v616A7o9O2coqA51y4yOBmmFPdeVSyDEgDnOotDG42P2N+oV++T9bofMr+p0Ie6z7e6MlUe4QV2x+YChmrPHs4BLEVE6E4mYWemQQiBtBRQbfvz/gWZKknjbgtONskAKaOtL6Ta0uSHz247pxShb5gzwKPCMR/2Tei8g2h6Ve9kHy7ydjypLZNdnGfMF1ebnQKIsX

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