The Coq mailing list

[gbush <gbush AT mysck.com>]

Hi Michael:

I know that you can do the induction "manually" with the fix tactic like
this...

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.
fix 4.
intros.
destruct xs.
simpl.
apply fold_nil.
simpl.
apply fold_cons.
apply foldl_folded.
Qed.

The fix tactic essentially corresponds with Fixpoint functions in Coq, where
the numeric argument is the index of the argument that will be structurally
decreasing.  It can be tricky to use, since you must guarantee yourself that
the primary argument is structurally decreasing, and you will not get
confirmation that it is or isn’t until Qed.

I am also relatively new to Coq, so there may be a more elegant way to
approach this, but if I get stuck with an induction principle that doesn't
seem to do what I want, I usually go to "fix."

Greg

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