The Coq mailing list

[Catherine Dubois <dubois AT ensiie.fr>]

Michael Day a écrit :
> Hi,
>
> I'm new to Coq and having trouble proving some properties of this function:
>
> Fixpoint fold (A:Set) (f:A -> A -> A) (a:A) (xs:list A) : list A :=
>     match xs with
>     | nil => nil
>     | x::xs0 => (f a x)::(fold A f (f a x) xs0)
>     end.
>
> The function transforms a list by applying a function to each element. It's
> different from map, as there is an accumulator threaded through the list.
> ("fold" isn't the right name for it, but I'm not sure what is; in Mercury
> there is a function a bit like this called "map_foldl").
>
> I've defined an inductive predicate that represents the results of
> transforming a list with fold:
>
> Inductive folded (A:Set) (f:A -> A -> A) : A -> list A -> list A -> Prop :=
>     | fold_nil : forall (a:A), folded A f a nil nil
>     | fold_cons : forall (a x0:A)(xs0 xs:list A),
>         folded A f (f a x0) xs0 xs -> folded A f a (x0::xs0) ((f a x0)::xs).
>
> But I am utterly unable to prove that the function actually conforms to it:
>
> Theorem foldl_folded : forall (A:Set) (f:A -> A -> A) (a:A) (xs:list A),
>     folded A f a xs (foldl A f a xs).
> Proof.
> induction xs ; simpl.
> ...?
>
> It seems that the induction principle for lists generates the wrong
> hypothesis in this case, which makes it useless for proving the theorem. A
> similar theorem for a "map" function with no accumulator argument is trivial
> to prove.
>
> I tried making up an induction scheme like this:
>
> Theorem foldl_ind : forall (A:Set) (f:A -> A -> A) (P : A -> list A ->
> Prop),
>     (forall (a:A), P a nil) ->
>     (forall (a x:A) (xs:list A), P (f a x) xs -> P a (x::xs)) ->
>     (forall (a:A) (xs:list A), P a xs).
>
> But again was utterly unable to prove it, for similar reasons.
>
> How would I go about proving something like this in Coq? Or am I heading in
> the wrong direction entirely? Any tips would be very much appreciated.
>
> Best regards,
>
> Michael
>
>   
Michael,

Just swap xs and a in your theorem. And thus the induction hypothesis 
will be more general  and usable in the second case of your induction.
Catherine