coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- 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
- [Coq-Club] Simple question about tactic notation, Edsko de Vries
- Re: [Coq-Club] Simple question about tactic notation,
Thomas Braibant
- Re: [Coq-Club] Simple question about tactic notation,
Samuel E. Moelius III
- Re: [Coq-Club] Simple question about tactic notation,
Edsko de Vries
- Re: [Coq-Club] Simple question about tactic notation,
Samuel E. Moelius III
- Re: [Coq-Club] Simple question about tactic notation,
Samuel E. Moelius III
- Re: [Coq-Club] Simple question about tactic notation, Edsko de Vries
- Re: [Coq-Club] Simple question about tactic notation,
Samuel E. Moelius III
- Re: [Coq-Club] Simple question about tactic notation,
Samuel E. Moelius III
- Re: [Coq-Club] Simple question about tactic notation,
Edsko de Vries
- Re: [Coq-Club] Simple question about tactic notation,
Edsko de Vries
- Re: [Coq-Club] Simple question about tactic notation, Edsko de Vries
- Re: [Coq-Club] Simple question about tactic notation,
Samuel E. Moelius III
- Re: [Coq-Club] Simple question about tactic notation, Hugo Herbelin
- Re: [Coq-Club] Simple question about tactic notation,
Thomas Braibant
Archive powered by MhonArc 2.6.16.