Skip to Content.
Sympa Menu

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

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Applying Lemma in fold_left


Chronological Thread 
  • 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



Archive powered by MHonArc 2.6.18.

Top of Page