Question

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?

Answer 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).

友情链接