如何繼續使用此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證明？

回答

相關問題