The Coq mailing list

[Jean-Marc Notin <notin AT lix.polytechnique.fr>]

Le lundi 10 avril 2006 à 15:03 +0200, Adam Koprowski a écrit :
> 
>    Hello everybody,
> 
>  During my work in Coq I encountered something that looks rather as an
> elementary problem but I got stucked on it nevertheless. Here is the
> relevant snippet:
> 
> Variable A: Set.
> Inductive Test: Set :=
> | Elem: A -> Test
> | Pair: Test -> Test -> Test.
> 
> Fact discr: forall a b, ~a = Pair a b.
> Proof. ?
> 
>   How can one prove discr? I tried all varations of discriminate,
> injection etc. I could think of. Or is this equality not valid
> intuitionistically? Any indications why? Any help appreciated!
> 
There may be simpler ways for this, but you can use the inversion
tactic:

Fact discr: forall a b, ~a = Pair a b.
Proof.
  unfold not; intros a b; induction a as [x|x IHx y IHy]; inversion 1 as
[H'].
  rewrite H0 in H'; contradiction.
Qed.

-- 
Jean-Marc Notin 
<notin AT lix.polytechnique.fr>
LIX

Attachment: signature.asc
Description: This is a digitally signed message part