The Coq mailing list

[Julien Forest <forest AT ensiie.fr>]

On Fri, 28 Dec 2007 00:26:23 -0800 (PST)
Michael Day 
<mikeday AT yeslogic.com>
 wrote:

> 
> 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).
> 

You should try the Function construction as follows:


 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).
 

 Function fold (A:Set) (f:A -> A -> A) (a:A) (xs:list A) {struct xs} : list A 
:=
     match xs with
     | nil => nil
     | x::xs0 => (f a x)::(fold A f (f a x) xs0)
     end.



 Theorem foldl_folded : forall (A:Set) (f:A -> A -> A) (a:A) (xs:list A),
     folded A f a xs (fold A f a xs).
 Proof.
   intros A f a xs;
     functional induction (fold A f a xs).
   apply fold_nil.
   apply fold_cons. exact IHl.
Qed.

Julien Forest