이 Coq Proof를 진행하는 방법은 무엇입니까?

Question

나는 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))) 

, 잘 모르겠어요 (그것을인가?) 때와 같이 이 세트에없는 때문에 내가 증거로, 내가 HotelRes의 유형이 실제로 구성 요소입니다

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

시점에 박히면서 얻을 그러나 (이 경우, HotelRes는 연결의 클라이언트입니다) 가정, 나는 정확한 또는 자동 전술 같은 것을 사용할 수 없다.

어떻게 증명할 수 있습니까?

Answer 1

당신이 보여준 (일부) 정의에서 분명히 커넥터가 클라이언트와 서버가되는 것을 방해하는 것이 아무것도 없으므로 어떻게 증명할 것인지 이해할 수 없습니까?

내 생각에 당신의 정의는 당신이 모델링하고자하는 것을 제대로 포착하지 못하지만, 둘 다 (완전한 정의 또는 그 뒤에있는 생각)을 보지 않고는 더 이상 말하기가 불가능합니다.