如何进行 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)
我想说“组件术语必须是连接的客户端或服务器；但不能同时是两者。”我在 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 的类型确实是 Component （在本例中，HotelRes 是连接的客户端），因为它不在假设，我不能使用类似的确切或自动战术。
我该如何进行这样的证明呢？
I'm having a problem with my Coq proof and was hoping for some help and guidance. I have part of my definition below:
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)
I wish to say that "A component term must be either a client or server of a connection; but not both." I have come up with the following as a representation of the above in the Coq (based on my definition above):
(forall con:Connector, forall c:Component, In con (MyConnections x) ->
(c = (client con) /\ c <> (server con)) \/ (c <> (client con) /\ c = (server con)))
However, I'm not sure if that is correct (is it?), as when I get to the proof, I get stuck at the point
5 subgoals
con : Connector
c : Component
H0 : Connection1 = con
______________________________________(1/5)
c = HotelRes
The type of HotelRes is indeed Component (in this case, HotelRes is the client of the connection), however, since this is not in the set of assumptions, I can't use something like the exact or auto tactics.
How could I proceed with such a proof?
如果你对这篇内容有疑问，欢迎到本站社区发帖提问 参与讨论，获取更多帮助，或者扫码二维码加入 Web 技术交流群。
绑定邮箱获取回复消息
由于您还没有绑定你的真实邮箱，如果其他用户或者作者回复了您的评论，将不能在第一时间通知您！
发布评论
评论（1）
从您所显示的（部分）定义来看，显然没有什么可以阻止组件既是连接器中的客户端又是服务器，所以我不明白您想如何证明它？
我的猜测是，您的定义没有正确捕获您想要建模的内容，但是如果没有看到（完整的定义及其背后的想法），就不可能说更多。
From the (part of the) definition that you have shown there is clearly nothing preventing a Component to be both a client and a server in a connector, so I don't understand how you want to prove it?
My guess is that your definition does not properly capture what you want to model, but it's impossible to say more without seeing neither (full definition nor the idea behind it).