1

我的 Coq 证明有问题，希望得到一些帮助和指导。我的部分定义如下：

Inductive Architecture : Set := 
| Create_Architecture (Arch_Name: string)(MyComponents: list Component)
  (MyConnections: list Connector)

with

...

with 

Connector : Set :=
| Create_Connector (Con_Name:string) (client: Component)(server:Component)

我想说“组件术语必须是连接的客户端或服务器；但不能同时是两者。” 我在 Coq 中提出了以下内容作为上述内容的表示（基于我上面的定义）：

(forall con:Connector, forall c:Component, In con (MyConnections x) -> 
(c = (client con) /\ c <> (server con)) \/ (c <> (client con) /\ c = (server con)))

但是，我不确定这是否正确（是吗？），因为当我得到证明时，我陷入了困境

5 subgoals
con : Connector
c : Component
H0 : Connection1 = con
______________________________________(1/5)
c = HotelRes

的类型HotelRes确实是组件（在这种情况下，HotelRes是连接的客户端），但是，由于这不在假设集中，我不能使用确切或自动策略之类的东西。

我怎么能继续这样的证明？

4

1 回答 1

2

从您所展示的（部分）定义来看，显然没有什么可以阻止组件在连接器中既是客户端又是服务器，所以我不明白您想如何证明它？

我的猜测是你的定义没有正确地捕捉到你想要建模的东西，但是如果没有看到（完整的定义和它背后的想法），就不可能说更多。

于 2011-07-30T19:53:03.227 回答