The Coq mailing list

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

Hi Evgeny,

thanx for answer. It seems like good explanation of this "User error". But
anyway, "Hx is used in hypothesis v" seems like a bug (at least
explanation) because it is not self-explanatory.

Greetings,

Marko Malikoviæ

Evgeny Makarov reèe:
> Hi,
>
>> Coq < Hypothesis Hx : values x.
>>
>> Coq < Goal x<=4.
>
>>> induction Hx.
>>> ^^^^^^^^^^^^
>> User error: Hx is used in hypothesis v
>
> I believe the reason for the error is that the induction tactic erases
> the term which is its argument from the context. Note that when the
> theorem is "values x -> x <= 4" and you say "intro Hx; induction Hx", Hx
> is no longer in the context. If Hx is an axioms then it is not in the
> local context, so apparently this is OK as well. But when Hx is declared
> as a hypothesis, you cannot erase it from the context because your
> theorem is using it. The error message "Hx is used in hypothesis" is
> usually issued by the "clear" tactic. However, I admit that saying "in
> hypothesis v" is cryptic.
>
> You can say "elim Hx" or "case Hx" (but not "destruct Hx", which also
> tries to clear Hx).
>
> Evgeny
>
> --------------------------------------------------------
> 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
>