The Coq mailing list

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

Le Mon, 26 Nov 2012 14:50:02 +0100,
Pierre Courtieu 
<pierre.courtieu AT gmail.com>
 a écrit :

> 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?

I guess you mean "remember t as x ; induction x."

Almost everywhere, I never want to have my environments polluted by
needless equalities. Plus the generated proof term will be horrible,
and it has an impact on performances when doing big developpements.

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

A LOT of other things? Well beside generalizing all hypothesis relying
on the pattern on which induction is done, and then reintroducing them
in the environment, I do not see what this 'lot' is. I have never used
elim, since I never understood really what it is used for. 'case' and
'destruct' do all what I need when dealing with non recursive stuff.
With recursion, I either use 'fix' (when I want full control, or when I
use 'Unset Elimination Schemes.') or induction (after having carefuly
selected what I want to be generalized).

I will take a look on elim, but I doubt it will interest me much.

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