I’m learning to use Coq and I try to prove the theorems of a paper I’m reading. The paper is Having a Part Twice Over of Karen Bennett, published in 2013. The paper propopes a mereological theory composed of two primitives F and Ps and defines the parthood relation P using the two primitives.
I coded it as follows:
Class Entity: Type.
(* Slot Mereology defines the parthood relation
* with the two primitives F and Ps.
* The idea is that wholes have slots
* filled by their parts.
* F x s means that x fills slot s.
* Ps s y means that s is a parthood slot of y.
* P is the parthood relation.
*)
Parameter F : Entity -> Entity -> Prop.
Parameter Ps : Entity -> Entity -> Prop.
Definition P (x y : Entity) :=
exists s, F x s /\ Ps s y.
(* Slot Inheritance *)
Axiom A5 : forall x y z1 z2 : Entity,
(Ps z1 y /\ F x z1) /\ Ps z2 x -> Ps z2 y.
(* Parthood Transitivity *)
Theorem T7 : forall x y z : Entity,
(P x y /\ P y z) -> P x z.
Proof.
intros x y z.
unfold P.
intro h.
destruct h as (EsPxy, EsPyz).
destruct EsPxy as (s1, Pxy).
destruct Pxy as (Fxs1, Pss1y).
destruct EsPyz as (s2, Pyz).
destruct Pyz as (Fys2, Pss2z).
exists s1.
split.
apply Fxs1.
apply A5 with (z1 := s2) (x := y).
split.
split.
assumption.
assumption.
assumption.
Qed.
I succeeded to prove theorem T7. I have two questions:
- is my Coq code ok? (I’m not sure If the way I declared the type, the primitives and the predicate is the right way to do it.)
- is there a shorter proof? (About the length of the proof, I only want to know about the number of tactics.)
>Solution :
Yes, your Coq code is OK. But there are shorter proofs. This theorem is simple enough that it can be solved with Coq’s automation tactics. E.g.,
Parameter Entity: Type.
(* Slot Mereology defines the parthood relation
* with the two primitives F and Ps.
* The idea is that wholes have slots
* filled by their parts.
* F x s means that x fills slot s.
* Ps s y means that s is a parthood slot of y.
* P is the parthood relation.
*)
Parameter F : Entity -> Entity -> Prop.
Parameter Ps : Entity -> Entity -> Prop.
Definition P (x y : Entity) :=
exists s, F x s /\ Ps s y.
(* Slot Inheritance *)
Axiom A5 : forall x y z1 z2 : Entity,
(Ps z1 y /\ F x z1) /\ Ps z2 x -> Ps z2 y.
(* Parthood Transitivity *)
Theorem T7 : forall x y z : Entity,
(P x y /\ P y z) -> P x z.
Proof.
unfold P; firstorder; eauto 10 using A5.
Qed.
(Notice that I replaced "Class Entity" with "Parameter Entity": The first form is actually just defining a type whose elements are records with no fields, whereas the second one is postulating that the type Entity exists without placing any further constraints on it.)