The Coq mailing list

["Soegtrop, Michael" <michael.soegtrop AT intel.com>]

Dear Tiwari,

 

I would think this is not true in general. Imagine an f which returns false for the first element of a list and true for all other elements of the list regardless of the accumulator bool. Then the result of fold_left would be true, but (f true <firstelem>) would be false.

 

Best regards,

 

Michael

 

From: coq-club-request AT inria.fr [mailto:coq-club-request AT inria.fr] On Behalf Of mukesh tiwari
Sent: Thursday, August 04, 2016 10:52 AM
To: coq-club AT inria.fr
Subject: [Coq-Club] Lemma regarding fold_left

 

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

Intel Deutschland GmbH
Registered Address: Am Campeon 10-12, 85579 Neubiberg, Germany
Tel: +49 89 99 8853-0, www.intel.de
Managing Directors: Christin Eisenschmid, Christian Lamprechter
Chairperson of the Supervisory Board: Nicole Lau
Registered Office: Munich
Commercial Register: Amtsgericht Muenchen HRB 186928