The Coq mailing list

[mukesh tiwari <mukeshtiwari.iiitm AT gmail.com>]

Dear Micheal, Gaetan,

Thank you very much. Now I can see my mistake.

Best regards,

Mukesh Tiwari

On Thu, Aug 4, 2016 at 7:04 PM, Gaetan Gilbert <gaetan.gilbert AT ens-lyon.fr> wrote:

With

f := fun _ _ => false

l := []

you get forall A, A -> false = true

which isn't true.

Gaëtan Gilbert

On 04/08/2016 10:51, mukesh tiwari wrote:

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