The Coq mailing list

["emmanuel LEDINOT" <emmanuel.ledinot AT dassault-aviation.fr>]

Dear Coq user,

Your problem is likely to be more easily tractable with a BDD-based boolean
computation package, rather than with a theorem prover like Coq.

Your problem looks like a medium size satisfiability problem.

You want to know if the constraints (rules) defining the valid states of
your world are consistent with a set of requirements. You have two sets of
states that can be defined  by two predicates (the first one is the
conjunction of the rules and the second one is the conjunction of the
requirements) and you want to check that the intersection is not empty, in
other words at least one state among the 2^125 satisfies Rules+Requirements.

So take a BDD package, computes the BDD of the unique formula
[(/\Rules)/\(/\Requirements)](A1,........,A125).
If the result is False, your set of requirements is too restrictive.

So computing this BDD incrementally (adding rules and requirements and one
by one) you should solve your problem.

Hoping it will welp you.

--
Emmanuel LEDINOT
Dassault Aviation
DGT/DPR/DESA
78 Quai Marcel Dassault
92552 Saint-Cloud Cedex
Tel: 01.47.11.53.05
Fax: 01.47.11.57.23



Asger Alstrup Nielsen a écrit:

> 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

--
Emmanuel LEDINOT
Dassault Aviation
DGT/DPR/DESA
78 Quai Marcel Dassault
92552 Saint-Cloud Cedex
Tel: 01.47.11.53.05
Fax: 01.47.11.57.23