The Coq mailing list

[Marko Malikovi� <marko AT ffri.hr>]

Hi,

I'm searching for reason way this cases have different epilogue but I
can't find one:

FIRST:

Coq < Section Proba.
Coq < Inductive values : nat -> Prop :=
Coq < | value1 : values 1
Coq < | value2 : values 2
Coq < | value3 : values 3
Coq < | value4 : values 4.
values is defined
values_ind is defined

Coq < Parameter x : nat.
x is assumed

Coq < Hypothesis Hx : values x.
Hx is assumed

Coq <
Coq < Goal x<=4.
1 subgoal

  Hx : values x
  ============================
   x <= 4

Unnamed_thm < induction Hx.
Toplevel input, characters 0-12
> induction Hx.
> ^^^^^^^^^^^^
User error: Hx is used in hypothesis v

SECOND:

Coq < Section Proba.

Coq < Inductive values : nat -> Prop :=
Coq < | value1 : values 1
Coq < | value2 : values 2
Coq < | value3 : values 3
Coq < | value4 : values 4.
values is defined
values_ind is defined

Coq < Parameter x : nat.
x is assumed

Coq < Goal values x -> x<=4.
1 subgoal

  ============================
   values x -> x <= 4

Unnamed_thm < intro Hx.
1 subgoal

  Hx : values x
  ============================
   x <= 4

Unnamed_thm < induction Hx.
4 subgoals

  ============================
   1 <= 4

subgoal 2 is:
 2 <= 4
subgoal 3 is:
 3 <= 4
subgoal 4 is:
 4 <= 4

Is it reason in rule implemented with intro tactis or what?

Thank you very much,

Marko Malikoviæ