The Coq mailing list

[AUGER Cédric <sedrikov AT gmail.com>]

Le Mon, 26 Nov 2012 12:29:25 +0100,
Gert Smolka 
<smolka AT ps.uni-saarland.de>
 a écrit :

> Doing remember and the subsequent inversion automatically
> would certainly spare us a lot of tedium.  I don't like the current
> setting where induction automatically generalizes over 
> non-variables.
> Gert

It is not quite the case. There is no generalization over non variables.
It is just the application of the induction principle.

And what would be the behaviour you would like?
Automatically adding equalities before calling the induction principle?
Rejecting the tactic?

None of these possibilities would satisfy me. For me, the user has to
think of the good generalization himself. In fact there are cases where
you do not wish an automatic generalization over variables, so you have
to select the variables you want to generalize and those you do not
before calling the induction tactic.

Same thing for the 'fix' tactic.

I see no way for Coq to guess what needs to be generalized and what
does not need (beside trying all possible proofs before finding a
correct one, which is not realistic).

> 
> On Nov 26, 2012, at 11:29 , Pierre Courtieu
> <pierre.courtieu AT gmail.com>
>  wrote:
> 
> > Indeed, functional induction is similar to induction (it *is* a call
> > to induction actually): it mostly works on variables. We could
> > modify functional induction (and induction actually) to always do a
> > "remember" when applied to non variable terms. I wonder if this
> > would break some strange usage of induction.
> > 
> > Has anyone ever user successfully "induction X" where X is something
> > else than a variable?
> > 
> > Best regards,
> > Pierre
> > 
> > 2012/11/25 Gert Smolka 
> > <smolka AT ps.uni-saarland.de>:
> >> Thank you so much Jonas and Julien for
> >> opening my eyes.  I shall try to remember
> >> to use remember when doing induction,
> >> see my favorite solution below.  Gert
> >> 
> >> Require Import Recdef Omega.
> >> 
> >> Definition gcd_order (p : nat * nat) : nat := let (x,y) := p in
> >> x+y.
> >> 
> >> Function gcd (p : nat * nat) {measure gcd_order p} : nat :=
> >>  match p with
> >>    | (0,_) => 0
> >>    | (_,0) => 0
> >>    | (x,y) => match gt_eq_gt_dec x y with
> >>                 | inleft (left _) => gcd (x, y-x)
> >>                 | inleft (right _) => x
> >>                 | inright xgty => gcd (x-y, y)
> >>               end
> >>  end.
> >> - unfold gcd_order ; intros ; omega.
> >> - unfold gcd_order ; intros ; omega.
> >> Defined.
> >> 
> >> Lemma gcd_ref x :
> >>  gcd (x,x) = x.
> >> 
> >> Proof.
> >>  remember (x,x) as p.
> >>  functional induction (gcd p) ; inversion Heqp ; omega.
> >> Qed.
>