I'm exercising my proving skills with the book “Mereology” of Cotnoir and Varzi (2021). The first definitions given in the book, after accepting the primitive binary relation P, are :
(D1) PPxy := Pxy /\ ~ (x = y)
(D2) Oxy := ∃z (Pzx /\ Pzy)
(D3) Uxy := ∃z (Pxz /\ Pyz)
(D4) Dxy := ~∃z (Pzx /\ Pzy)
(D5) x - y := ιz∀w (Pwz <-> (Pwx /\ Dwy))
So, I coded the primite and the first four definitions like this:
Parameter Entity : Set.
Parameter P : Entity -> Entity -> Prop.
Definition PP x y := P x y /\ x <> y.
Definition O x y := exists z, P z x /\ P z y.
Definition U x y := exists z, P x z /\ P y z.
Definition D x y := ~ exists z, P z x /\ P z y.
However, I don’t know how to code the fifth one. I identified that it should be a function of type Entity -> Entity -> Entity as the iota operator (ι) refers to the one z that satisfies the following formula. Therefore, "x - y" should return the given z.
At it looks like an operator, I first tried with a notation:
Notation "x - y" := (exists z, forall w ,(P w z <-> (P w x /\ D w y))).
However, as I expected, this is not what I wanted. I checked the type of "x - y":
Variables x y: Entity.
Check x - y.
And I got, as expected, the type Prop, and not Entity.
After a search on Google, I find this in the standard library: Library Coq.Logic.ClassicalDescription, and in particular a definition of a iota operator, but I didn’t understand how to use it.
Therefore, I have two questions: is my implementation choices (in particular the Parameters Entity and P) ok? and if so, how can I implement the operation "x - y"?
I am not sure what you are trying to do. But if you want to use the iota in the Classical Description, it may look like
Require Import ClassicalDescription.
Parameter Entity : Set.
Parameter P : Entity -> Entity -> Prop.
Definition PP x y := P x y /\ x <> y.
Definition O x y := exists z, P z x /\ P z y.
Definition U x y := exists z, P x z /\ P y z.
Definition D x y := ~ exists z, P z x /\ P z y.
Definition B x y := iota x (fun z => forall w , (P w z <-> (P w x /\ D w y))).
Notation "x - y" := (B x y).
Lemma B_spec x y w : P w (x - y) <-> (P w x /\ D w y).
Proof.
apply (iota_spec x (fun z => forall w , (P w z <-> (P w x /\ D w y)))).