如何继续使用此Coq证明？

我的Coq证明存在问题，希望得到一些帮助和指导。下面我有我的定义的一部分：如何继续使用此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)

我想说，“组件项必须是一个客户端或连接的服务器，但不能两者兼得。” （基于以上我的定义），我想出了以下作为勒柯克上述的表示：

(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是连接的客户端），但是，因为这不是一组假设，我不能使用像确切的或自动的战术。

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

来源

2011-07-30 zdot

从你已经显示的（部分）定义来看，显然没有什么能够阻止组件成为连接器中的客户端和服务器，所以我不明白你想如何证明它？

我的猜测是你的定义没有正确地捕捉你想要的模型，但是如果没有看到它们（全部定义或它背后的想法），就不可能说更多。

来源

2011-07-30 19:53:03 akoprowski

没有任何东西阻止它，没有。但我想证明事实确实如此。我已经定义了几个关系，并希望证明这个条件适用于他们。 – zdot

好的，但是如果一个组件既可以是连接器的客户端又可以是服务器的一部分，那么显然你可以找到你的引理的反例，所以你不能希望证明它。那有意义吗？ – akoprowski

啊，所以你想证明一个特定的架构呢？我错过了你原来的描述。这应该很容易。但是你展现的目标确实似乎无法证明。所以之前一定有什么问题。我可以尝试提供帮助，但如果您提供工作脚本（可能已简化），则会更容易。 – akoprowski

如何继续使用此Coq证明？

回答

相关问题