The Coq mailing list

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

OK, if I put assumption "Hx : values x" with

Axiom Hx : values x.

in the global context instead in local context (with Hypothesis) then
induction work.

But, tactic "intro Hx" puts "Hx" in local context like "Hypothesis" but
induction work.

Thanx,

Marko Malikoviæ

Marko Malikoviæ reèe:
> 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æ
>
> --------------------------------------------------------
> Bug reports: http://logical.futurs.inria.fr/coq-bugs
> Archives: http://pauillac.inria.fr/pipermail/coq-club
>           http://pauillac.inria.fr/bin/wilma/coq-club
> Info: http://pauillac.inria.fr/mailman/listinfo/coq-club
>