The Coq mailing list

[Frederic Blanqui <Frederic.Blanqui AT lri.fr>]

On Tue, 4 Jul 2000, Asger Alstrup Nielsen wrote:

> 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?

I have the following propositions but I don't know if it will fit well
with the other problems.

------------------------------------------------------------------------------

Require Arith.
Require PolyList.

Parameter A : nat->Prop.

Fixpoint atmost_one [l : (list nat)] : Prop :=
Cases l of
nil => True
| (cons k l') => ((A k) /\ (none l')) \/ (~(A k) /\ (one l'))
end

with none [l : (list nat)] : Prop :=
Cases l of
nil => True
| (cons k l') => ~(A k) /\ (none l')
end.

Definition exactly_one [l : (list nat)] : Prop :=
(atmost_one l) /\ ~(none l).

(* rules *)

Axiom R4 : (one (cons (4) (cons (7) (cons (8) (nil nat))))).

(* you can define a more compact syntax for lists if you want
to write something like:

Axiom R4 : (one [(4),(7),(8)]).

see RM chapter 9 *)

------------------------------------------------------------------------------

You could also try to formalize your worlds as lists of booleans. There is
a module 'Bool' for booleans and a hint base 'bool'.

Require Arith.
Require PolyList.
Require Bool.

Definition world : Set := (list bool).

Definition mynth [n : nat; w : world] : bool :=
(nth n w false).

Definition R1 [w : world] : bool :=
(negb (andb (mynth (2) w) (negb (mynth (1) w)))).

(* xorb is already defined in 'Bool' *)

(* Definition R [w : world] : bool :=
(bigand-to-be-defined (R1 w) ... (Rn w)). *)

(* 'w' is a good world if '(R w) = true' *)

(* then, you can try to check some requirements on good worlds:

Lemma L1 : (w : world) (R w)=true -> (mynth (1) w)=true
-> (mynth (2) w)= true).

*)

------------------------------------------------------------------------------

Frederic Blanqui.

------------------------------------------------------------------------------
Laboratoire de Recherche en Informatique (LRI) - Equipe DEMONS
batiment 490, bureau 153, Universite Paris-Sud 91405 ORSAY (FRANCE)
tel:01 69 15 42 35 - fax:01 69 15 65 86 - web:http://www.lri.fr/~blanqui