CODEWITHSUNDEEP
coq
Lance Pollard
Lance Pollard

Reputation: 79468

What <> is in Coq

It's difficult to search for but wondering what <> means as in here:

Axiom point : Type.
Axiom line  : Type.
Axiom lies_in : point -> line -> Prop.
Axiom ax : forall (p1 p2 : point), p1 <> p2 ->
           exists! l : line, lies_in p1 l /\ lies_in p2 l.

Upvotes: 0

Views: 51

Answers (2)

SCappella
SCappella

Reputation: 10474

x <> y is a notation for ~(x = y) (which itself is a notation for (x = y) -> False). It's possible to search for notations with the Locate vernacular command, which is used like Locate "<>". and gives output like

Notation
"x <> y  :> T" := not (eq x y) : type_scope
(default interpretation)
"x <> y" := not (eq x y) : type_scope
(default interpretation)

Upvotes: 3

Arthur Azevedo De Amorim
Arthur Azevedo De Amorim

Reputation: 23622

The x <> y form is a notation for not (x = y) -- that is, it asserts that it is not the case that x and y are equal. Negation is defined by setting not P := P -> False. In other words, by showing P, we obtain a contradiction.

Upvotes: 2

Related Questions