The Coq mailing list

[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