The Coq mailing list

[Pierre Courtieu <pierre.courtieu AT gmail.com>]

Hi Cédric, can you give an example where "induction t" does what you
want (t being a non variable term) and "remember x as t ; induction x"
doesn't?

Actually if you really want to just apply the induction principle,
then "elim" is probably better because "induction" does a lot of other
things anyway (what I propose is just doing a bit more for induction).

P.



2012/11/26 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.
>>
>