The Coq mailing list

[AUGER Cedric <Cedric.Auger AT lri.fr>]

Le Sun, 31 Jul 2011 08:22:02 -0400,
Adam Chlipala 
<adam AT chlipala.net>
 a écrit :

> zaman wrote:
> > 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)))
> >    
> 
> The form of this theorem is suspicious.  You have a quantified 
> implication whose conclusion mentions [c] but whose assumption does 
> not.  Thus, in terms of determining the value of [c], the only help
> the assumption [In con (MyConnections x)] may be is if it is
> contradictory, in which case any conclusion follows.
> 
> Your question seems to be more about first-order logic than about Coq
> in particular.  Do you believe you can formulate everything on paper
> in traditional first-order logic?  (I expect the theorem statement
> above is not a desirable part of such a formulation.)

More precisely, assume you have two connections c1 and c2,
with the following hypothesis:
cdiff: client c2 <> client c1
Belongings: In c1 (MyConnections x)

Then now according to your axiom (Ax), you have:
connection_lemma :=
Ax c1 (client c2) Belongings:
  client c2 = client c1 /\
  client c2 <> server c1
\/client c2 <> client c1 /\
  client c2 = server c1

By cdiff, the first case of connection_lemma is inconsistant,
so that you have "client c2 = server c1", which is probably not what
you whish.

Here you gave a universal quantification, where an existential one was
expected.

and by the way, take also care of the place of your hypothesis,

forall con:Connector,
 exists c:Component,
 In con (MyConnections x) ->
 (c = (client con) /\ c<>  (server con)) \/
 (c<>  (client con) /\ c = (server con))

and

forall con:Connector,
 In con (MyConnections x) ->
 exists c:Component,
 (c = (client con) /\ c<>  (server con)) \/
 (c<>  (client con) /\ c = (server con))

are slightly different

(they are equivalent if Component is not empty and if equality on
Connector is decidable; but in this case, even if they are equivalent,
some formulation will probably be easier to use than the other!)

Note also, that you may whish to be able to extract a Component from a
Connector, in which case, consider rather:
forall con:Connector,
 In con (MyConnections x) ->
 { c:Component |
 (c = (client con) /\ c<>  (server con)) \/
 (c<>  (client con) /\ c = (server con)) }


You can also define an inductive type for your purpouse;
it has pros (may be easier to read, shorter to write when in use)
and cons (you have to define it explicitely, and so add a definition;
furthermore, the "contents" are hidden, so at first glance you cannot
tell what is really behind).

Inductive ComponentClass: Connector -> Type :=
| Client:
  forall con, (forall s, client con <> server s) ->
  ComponentClass (client con)
| Server:
  forall con, (forall c, server con <> client c) ->
  ComponentClass (server con)
.

(replacing Type with Prop gives something equivalent
 to the "forall …, exists con, …" version
 where what is proposed is equivalent with the
 "forall …, {con | …}")

and also this version which doesn't involve dependent types in other
places than equalities:

Inductive ComponentClass (C: Connector): Type :=
| Client:
  forall con, C = client con ->
  (forall s, client con <> server s) ->
  ComponentClass C
| Server:
  forall con, C = server con ->
  (forall c, server con <> client c) ->
  ComponentClass C
.

The latter may be heavier to use, but will likely not lead to bad
surprises, where the dependent type one may need some extra care
(but both are equivalent, and proof term the second solution are not
a lot bigger; so the second solution may be a better choice).

If you choose to use inductives, take a look at the following tactics:

* case (the most low level, will do analysis only on the goal,
        so that you may need to revert/generalize some hypothesis)
* destruct (a bit higher level, think of it as a tactic which does
            reverting of all the concerned hypothesis before
            performing a case, and then introduces all the reverted
            hypothesis; if an hypothesis is provided, this hypothesis
            is cleared)
* inversion (even higher, see of it as a destruct introducing
             equalities, but not removing the provided hypothesis)
* inversion_clear (same as above, but with replacing hypothesis in
                   the current goal, NOT in all hypothesis)

"inversion [hyp]; clear [hyp]; subst" is not exactly the same as
"inversion_clear [hyp]"

"inversion" is not at this time very efficient (in fact, not at all!)
in size of the generated proof term, so it is wise to avoid it when
destruct can be simply used
(but it is often not worth to make some complicated things to avoid
use of inversion).