Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] Simple question about tactic notation

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Simple question about tactic notation


chronological Thread 
  • From: Edsko de Vries <devriese AT cs.tcd.ie>
  • To: coq-club AT pauillac.inria.fr
  • Subject: Re: [Coq-Club] Simple question about tactic notation
  • Date: Sun, 15 Mar 2009 20:11:58 +0000
  • List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>

Hi Sam,

The version of the tactic is the one described in the manual as

  "If term is a num, then induction num behaves as intros until num
  followed by induction applied to the last introduced hypothesis.

I had tried to use intros until num, but then I needed a way to figure
out what the 'last introduced hypothesis' was. For a second it seemed
that your work-around worked (induction 0), but alas; extending the
example again (it makes no semantic sense whatsoever..)

Tactic Notation "my_induction" constr(n) :=
  induction n.

Inductive even : nat -> Prop :=
  | even_zero : even 0
  | even_succ : forall n, even n -> even (S (S n)).

Inductive weird : nat -> Prop :=
  | weird_0 : weird 0
  | weird_1 : weird 1
  | weird_2 : weird 2
  | weird_3 : weird 3.

Lemma foo : forall (n:nat), even n -> weird n -> forall (m:nat), even m.
Proof.

Again, "induction 2" will do induction on "weird n"; untros until 2; induction
0 however does induction on "m" for some reason.

Edsko 





Archive powered by MhonArc 2.6.16.

Top of Page