这个 Coq 定理有更短的证明吗？

Question

我正在学习使用 Coq，并试图证明我正在阅读的论文中的定理。这篇论文是 Karen Bennett 的 Having a Part Twice Over，发表于 2013 年。论文提出了一个由两个原语 F 和 Ps 组成的分体学理论，并使用这两个原语定义了部分关系 P。

我编码如下：

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.

我成功证明了定理T7。我有两个问题：

我的 Coq 代码可以吗？（我不确定我声明类型、基元和谓词的方式是否正确。）
有更短的证明吗？（关于证明的长度，我只想知道战术的数量。）

Answer 1

是的，你的 Coq 代码没问题。但是有更短的证明。这个定理很简单，可以用 Coq 的自动化策略来解决。例如，

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.

（请注意，我将“Class 实体”替换为“参数实体”：第一种形式实际上只是定义了一个类型，其元素是没有字段的记录，而第二种形式假设该类型Entity 存在而没有对其施加任何进一步的限制。）

Answer 2

另一种方法，使用 ssreflect 及其简洁的解构符号，可以用更紧凑的方式重新表述您的显式证明（我使用的是 Arthur 的版本）。

From mathcomp Require Import all_ssreflect.

Parameter Entity: Type.

Parameter F : Entity -> Entity -> Prop.
Parameter Ps : Entity -> Entity -> Prop.
Definition P (x y : Entity) :=
  exists s, F x s /\ Ps s y.

Axiom A5 : forall x y z1 z2 : Entity,
  (Ps z1 y /\ F x z1) /\ Ps z2 x -> Ps z2 y.

Theorem T7 : forall x y z : Entity,
  (P x y /\ P y z) -> P x z.
Proof.
move=> x y z [[s1 [Fxs1 Ps1y]] [s2 [Fys2 Ps2z]]].
by exists s1; split; [|exact: (A5 y z s2 s1)].
Qed.

这个 Coq 定理有更短的证明吗？

Is there a shorter proof to this Coq theorem?

coq