The Coq mailing list

[Andrew McCreight <andrew.mccreight AT yale.edu>]

You can prove it by induction:

Fact discr: forall a b, ~a = Pair a b.
Proof.
  intros a b.
  induction a.

  discriminate.

  intro Z; injection Z; clear Z; intros H1 H2.
  subst a2.
  apply IHa1.
  assumption.

Qed.


On Mon, 10 Apr 2006, Adam Koprowski wrote:

>   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!
>
>  Adam Koprowski
>
> --
> =====================================================
> Adam.Koprowski AT gmail.com,
>  ICQ: 3204612
> http://www.win.tue.nl/~akoprows
> The difference between impossible and possible
> lies in determination (Tommy Lasorda)
> =====================================================