The Coq mailing list

[Hugo Herbelin <herbelin AT pauillac.inria.fr>]

Hi,

> Is it possible to define a tactic that at some point calls 'induction n' for
> some natural number 'n'?

You can do it this way: 

<<<<<
Ltac OnLastHyp tac :=
  match goal with
  [ n:_ |-_  ] => tac n || fail 1 "Application on last hypothesis failed"
  end.

Tactic Notation "my_induction" integer(n) :=
  let ind n := (induction n) in intros until n; OnLastHyp ind.
 
Inductive even : nat -> Prop :=   
  | even_zero : even 0
  | even_succ : forall n, even n -> even (S (S n)).
 
Lemma foo : forall (n:nat), even n -> True.
Proof.
  my_induction 1.
>>>>>

Passing induction arguments referring to quantified (dependent or non
dependent) hypotheses in Ltac functions was actually not
implemented. This will be made available for further releases.

> In nested Ltac calls to "my_induction'" and "n"), last term evaluation
> failed.
> Error: Variable n should be bound to a term.
> 
> BTW There seems to be an extraneous bracket in the error message :)

Oops, not very nice, this will be fixed at once in the bugfix branch.

Hugo Herbelin