The Coq mailing list

[Gaetan Gilbert <gaetan.gilbert AT ens-lyon.fr>]

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