The Coq mailing list

[Matthieu Sozeau <Matthieu.Sozeau AT lri.fr>]

> </>
> 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."

Hi Greg,

The induction principle actually does what you want in this case, it's  
just that you have to quantify your goals carefully.
The problem boils down to: do you want to prove
 A (f : A -> A -> A) (a : A) |- forall (xs : list a), folded A f  xs  
(fold A f a xs) or
 A (f : A -> A -> A) |- forall (xs : list a), forall (a : A), folded  
A f  xs (fold A f a xs).

In the first case, you will not get a general enough induction  
hypothesis, as the accumulator changes in the definition of fold.
However, in the second case it could be overkill to quantify on all  
"a : A" if a is actually a parameter of fold like A and f are.
--
Matthieu Sozeau
http://www.lri.fr/~sozeau