coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Lemma regarding fold_left

From: mukesh tiwari <mukeshtiwari.iiitm AT gmail.com>
To: coq-club AT inria.fr
Subject: [Coq-Club] Lemma regarding fold_left
Date: Thu, 4 Aug 2016 18:51:31 +1000
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=mukeshtiwari.iiitm AT gmail.com; spf=Pass smtp.mailfrom=mukeshtiwari.iiitm AT gmail.com; spf=None smtp.helo=postmaster AT mail-oi0-f65.google.com
Ironport-phdr: 9a23:VXIa4hMCH1kKHgd7wIMl6mtUPXoX/o7sNwtQ0KIMzox0KP/yrarrMEGX3/hxlliBBdydsKMczbqM+Pi8EUU7or+5+EgYd5JNUxJXwe43pCcHRPC/NEvgMfTxZDY7FskRHHVs/nW8LFQHUJ2mPw6anHS+4HYoFwnlMkItf6KuS9aU3578j7z60qaQSj0AvCC6b7J2IUf+hiTqne5Sv7FfLL0swADCuHpCdrce72ppIVWOg0S0vZ/or9YwuxhX7vkm7otLVbjwV6U+V71RSjo8YE4v48i+sATAQBCPrmcdTWwMk1IcBhXG4Qr6QpbuuzH78Ot82TWfFcLzRLEwHz+l6vE4G1fTlC4bOmthoynsgctqgfcDrQ==

Hello everyone, I am trying to state a property related to fold_left.

Lemma fold_left_true : forall (A : Type) (f : bool -> A -> bool) (l : list A),
fold_left f l true = true -> forall b : A, f true b = true.

fold_left f (h1 :: (h2 :: t)) true = true -> fold_left f (h2 :: t) (f true h1) = true ->

fold_left f t (f (f true h1) h2)

Induction on l is not any helpful because I am stuck with true = true in context, and destruct (f true b) is also not any helpful because of false = true in goal. Any idea how to solve this lemma ?

Best regards,

Mukesh Tiwari

[Coq-Club] Lemma regarding fold_left, mukesh tiwari, 08/04/2016
- RE: [Coq-Club] Lemma regarding fold_left, Soegtrop, Michael, 08/04/2016
- Re: [Coq-Club] Lemma regarding fold_left, Gaetan Gilbert, 08/04/2016
  - Re: [Coq-Club] Lemma regarding fold_left, mukesh tiwari, 08/04/2016