The Coq mailing list

[Asger Alstrup Nielsen <alstrup AT sophusmedical.dk>]

Dear Coq Club,

I found Coq this morning, and started using it immediate on my Win NT
system. It's great. 

I use it on a problem that I use Coq to solve, but I need some help with
the syntax to progress. I read the tutorial, and the reference manual,
but I'm stuck. I'm not an expert in automated proof systems or Coq, so
maybe you can help me.
My problems seem to be fairly easy to solve, but I just can't find out
how to...

Let me introduce my problem:

I have a set of attributes
  
  A1, ..., An, where n is 125.

Each attribute is a bool - the attribute can either be set or cleared.
These attributes describe the configuration of my world. The world thus
has 2^125 different states.

However, the world is not that big. Some combinations of attributes are
not legal.
So to restrict the world, I have rules. There are around 50 rules, and
the rules look like this:

  R1:  ~(A2 /\ ~A1)
  R2:  ~(A3 /\ ~A1)
  R3:  ~((A4 \/ A5 \/ A6) /\ ~A1)
  R4:  (A4 /\ ~A7 /\ ~A8) \/ (~A4 /\ A7 /\ ~A8) \/ (~A4 /\ ~A7 /\ A8).

and so on. Some of them involve 20-30 attributes.

At this point, I have the first question:

Rule R4 is an explicit formulation of the rule: "At most one of A4, A7,
A8 may be set at a given time.". I'd like to express this as max_one(A4,
A7, A8). 
Similarly, I have a exactly_one(A1, A2, A3) expression, which states
that exactly one of A1, A2 and A3 must be set at a given time.
My first question is: How can I formulate max_one and exactly_one in
Coq? I.e. I'd like to express R4 like this:

  max_one(A4, A7, A8).

How do I define max_one to do this?

Now, let's return to the main problem. 

All of the rules have to be fulfilled at the same time in order to
describe a valid situation. Therefore, my world is restricted by these
rules. 
Obviously, you can consider the rules R1 - R4 as one big rule:

  (~(A2 /\ ~A1)) /\
  (~(A3 /\ ~A1)) /\
  (~((A4 \/ A5 \/ A6) /\ ~A1)) /\
  ((A4 /\ ~A7 /\ ~A8) \/ (~A4 /\ A7 /\ ~A8) \/ (~A4 /\ ~A7 /\ A8)).

Now, besides the rules that define the world, I have some requirements
for the world.
For instance, I demand that A1 can be changed from False to True
regardless of all other attributes.
Another requirement could be "if A1 is True then A2 must be True". All
in all, I have around 30 requirements, which each are pretty simple.
I would like these requirements to be checked automatically, since it is
not obvious whether the rules invalidate the requirements or not.

In theory, these requirements can be checked by trying all combinations,
and thus verifying that the rules are obeyed. However, since the world
is so big, this is obviously not feasible.

Therefore, I use Coq on this problem. For each requirement, I ask Coq to
prove that each requirement is obeyed in the given world.

For instance, to prove that A1 can always be changed from False to True,
I ask Coq to prove this:

  Section proof.
  Require Classical.
  Variables A0, A1, A2, A3, A4, A5, A6, A7, A8 : Prop.

  (* Try to prove that A1 can be changed from False to True *)
  Goal
    (~(A2 /\ ~False)) /\
    (~(A3 /\ ~False)) /\
    (~((A4 \/ A5 \/ A6) /\ ~False)) /\
    ((A4 /\ ~A7 /\ ~A8) \/ (~A4 /\ A7 /\ ~A8) \/ (~A4 /\ ~A7 /\ A8))

    ->

    (~(A2 /\ ~True)) /\
    (~(A3 /\ ~True)) /\
    (~((A4 \/ A5 \/ A6) /\ ~True)) /\
    ((A4 /\ ~A7 /\ ~A8) \/ (~A4 /\ A7 /\ ~A8) \/ (~A4 /\ ~A7 /\ A8)).

  Intuition.

This works fine, and Coq will prove that the requirement is upheld.

The problem is that this program will only check *one* requirement. This
implies that I have to write separate programs for each requirement.

There must surely be an easier way to do this. I just can't figure out
what syntax to use!

Can anybody help me with these two problems?

Besides these two trivial syntax questions, I have an added bonus
question: 

Which tactic is the best to use to solve these problems? So far, my
experimentation shows that Intuition is a good one, but maybe there is
an even better one?

I have to anticipate that some of the requirements are not upheld from
time to time (because the rules change, and I have to detect when the
rules become too restrictive). In these cases, I'd like to know exactly
what rules prohibit the requirements, if possible. Can Coq be used for
this, or do I have to look for some other system which can find
counter-examples that demonstrate why something can't be proven?

Thank you,

Asger Alstrup Nielsen