The Coq mailing list

[Sylvain Dailler <sylvain.dailler AT ens-lyon.fr>]

Thank you for your help. I think that your tactic solves my problem. And
it helps me to understand what the "inversion" tactic does.

But, the real question behind my problem was :
Why does it work with Set and not with Prop ?

A friend of mine found out that if we put the definitions into a section, the problem is avoided. Actually, this might be a bug (I tested it with 8.2 and 8.3beta0 version of Coq).

2010/7/13 Jean-Francois Monin <jean-francois.monin AT imag.fr>

Hello,

Try using case instead of inversion.

Here there is no link between Hpipo and the conclusion,
hence you have to invent one, e.g. using refl_equal.

example_context <
1 subgoal

 x : A
 Hpipo : example x A0
 ============================
  False

generalize (refl_equal A0); generalize (refl_equal x).
pattern x at -1, A0 at -1.
case Hpipo; intros x0 y eqx eqA.

For more information, the material I just presented at the
2nd Coq Workshop, may be useful, see my webpage.

Hope this helps,
JF

On Tue, Jul 13, 2010 at 11:16:36AM +0100, Sylvain Dailler wrote:
>    Dear Coq users,
>
>    I would like to use the inversion tactic in the sort Prop. But this tactic
>    has not the same behavior as in Set. I don't understand why.
>    My problem can be summarized with this little example :
>
>    Variable A : Set.
>
>    Variable plus : A -> A -> A.
>    Infix "+" := plus.
>    Variable A0 : A.
>    Variable A1 : A.
>
>    Inductive example : A -> A -> Prop :=
>    | example0 : forall x y, example x (y + A1).
>
>    Lemma example_context : forall x, example x A0 -> False.
>    Proof.
>    intros x Hpipo.
>    inversion Hpipo.
>    (*now look at the context with A : Prop*)
>    Admitted.
>
>    Now, if I change "Variable A : Set." into "Variable A : Prop.", the
>    context generated by the inversion tactic is not the same. This hypothesis
>    disappeared :
>    "H1 : y + A1 = A0"
>
>    I would like to know why contexts are different. I don't think I am doing
>    anything wrong with the Prop sort.
>
>    Do you know where I can find the code of the inversion tactic ?

--
Jean-Francois Monin
CNRS-LIAMA, Project FORMES  &  Universite de Grenoble 1

Office 3-605, FIT, Tsinghua University
Haidian District, Beijing 100084, CHINA
Tel: +86 10 62 79 69 79 ext 605
Fax@LIAMA: +86 10 6264 7458