COQ中的姿势证明

Question

我试图在COQ中证明定理。我当前的上下文是：

1 subgoal
s, x : Entity
Pssx : Ps s x
Fxs : F x s
IPssx : F x s /\ Ps s x
t : Entity
Ctss : C t s s
Pstx : Ps t x
Fxt : F x t
______________________________________(1/1)
C s s s

f，ps和c是理论的关系。我也是Axiom 4：

Axiom A4 : forall x s t,
  Ps s x /\ F x s /\ Ps t x /\ F x t -> s = t.

我想做的是在证明中使用A4，因为这将帮助我说S和T是平等的。因此，我已经测试了：姿势证明（A4 XST）。< /code>添加了一个新的假设：h：ps sx /\ f xs /\ ps tx /\ f xt-＆gt; s = t。我知道我可以破坏假设H，证明前提并使用结论。但是我也知道我可以直接在姿势证明命令中给出前提。我想做姿势证明（A4 XST前提）之类的事情。，但我不知道该放置什么而不是premisses。

我尝试了几种解决方案：

• 用 /组成假设，例如姿势证明（A4 XST（pssx /\ fxs /\ pstx /\ fxt））。 S X”类型，而预计将具有“ PS SX /\ F XS /\ PS TX /\ F X T”。
• PSSX“具有“ PS >姿势证明（A4 XST H1）。：
  • assert（h1：=（ps sx） /\（f xs） /\（ps tx） /\（f xt））。< /code>，但我得到了一词“ h1”具有类型的“ Prop”，而期望具有类型为“ PS SX /\ F XS /\ PS TX /\ F X T”。< /code> < /li>
  • assert（h1：=（pssx） /\（fxs） /\（pstx） /\（fxt））。< /code>但我得到术语“ pssx”具有“ ps” ps' s x“虽然预计将具有“ prop”。

所以我的问题是以下：我应该放置什么而不是premisses让我的代码工作？是否有命令基于其他假设来创建新假设？我知道如何将假设摧毁两个较小的假设，但我不知道如何构成假设以创建较大的假设。

Answer 1

Coq 中的标准是咖喱你的A4，这样接收一个大连词作为前提时，它接收几个不同的前提：

Axiom A4' : forall x s t,
  Ps s x -> F x s -> Ps t x -> F x t -> s = t.

那么你可以这样做：

pose proof (A4' x s t Pssx Fxs Pstx Fxt).

如果你绝对需要 A4 与连词，你可以使用 conj （你可以使用 A4 来连接连词）可以通过 Print "_ 找到/\ _"):

pose proof (A4 x s t (conj Pssx (conj Fxs (conj Pstx Fxt)))).