The Coq mailing list

[Michael Day <mikeday AT yeslogic.com>]

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

-- 
View this message in context: 
http://www.nabble.com/Induction-principle-for-folding-over-lists-tp14523344p14523344.html
Sent from the Coq mailing list archive at Nabble.com.