The Coq mailing list

[mauricio cano <mcano.programas AT gmail.com>]

Good Day to everyone,

Beforehand, sorry for the long message, but i needed to express this definitions

I have the following definitions:

Definition token:=Prop.

Definition D:=nat. 

(*Definition of constraints*)

Inductive constraint : Type :=

  This definition will be useful for this pruposes*)

  basic : token->constraint

| exist : D->constraint->constraint

| conj : constraint->constraint->constraint

| impl : constraint->constraint->constraint.

Notation "% c" := (basic c) (at level 30, right associativity).

Inductive process : Type :=

  tell : constraint -> process 

 |parallel : process -> process -> process 

 |ask : constraint -> process ->process 

 |local : D -> process -> process.

Notation "tell( c )" := (tell c) (at level 30, right associativity).

Notation "p // q" := (parallel p q) (at level 30 , right associativity).

Notation "( 'ask' c 'then' p )" := (ask c p) (at level 30, right associativity).

(* Stores reachable from a process *)

Fixpoint stores (P : process): constraint :=

 match P with

   tell(c)=> c

 | P1 // P2 =>  conj (stores P1)  (stores P2)

 | (ask c then P1) => impl c (stores P1)

 | local x P1 => exist x (stores P1)

end.

Print stores.

Fixpoint evalCons (c: constraint) : token :=

 match c with 

  basic C1 => C1

| conj C1 C2 => (evalCons C1) /\ (evalCons C2)

| impl C1 C2 => (evalCons C1) -> (evalCons C2)

| exist x C1 => evalConsEx (exist x C1)

| exist x C1 => exists x, evalCons(C1)

end.

Now, this would be the first approach, but the evaluation of evalCons with exist x c, fails because coq is not able to infer the type of x, that could be solved doing this:

Fixpoint evalCons (c: constraint) : token :=

 match c with 

  basic C1 => C1

| conj C1 C2 => (evalCons C1) /\ (evalCons C2)

| impl C1 C2 => (evalCons C1) -> (evalCons C2)

| exist x C1 => evalConsEx (exist x C1)

| exist x C1 => exists x:D, evalCons(C1)

end.

However this approach is not correct, because when the application is done, it returns the following:

Print evalCons.

evalCons = 

fix evalCons (c : constraint) : token :=

  match c with

  | %C1 => C1

  | exist _ C1 => exists _ : D, evalCons C1

  | conj C1 C2 => evalCons C1 /\ evalCons C2

  | impl C1 C2 => evalCons C1 -> evalCons C2

  end

     : constraint -> token

As you can see, x was not taken in account, which is not what i want, also, i've tried the following approach:

Fixpoint evalCons (c: constraint) : token :=

 match c with 

  basic C1 => C1

| conj C1 C2 => (evalCons C1) /\ (evalCons C2)

| impl C1 C2 => (evalCons C1) -> (evalCons C2)

| exist x C1 => evalConsEx (exist x C1)

 end

with evalConsEx (c:constraint): token:=

  match x c with

      exist x C1 => exists x, evalCons(C1)

However, i'm stucked on what should i do with the x, since i cannot add is as a parameter of the function, because the types do not coincide, i would appreciate if someone could give me a hint about this issue .

On the other hand, is there any way to compute a substitution, let's say i have something like 

Compute(sub P x)  -----I'm assuming sub is the function mentioned earlier and P is an _expression_ with a bounded variable z

and this returns something like

P[z/x]

or should i define it? 

Again, a hint or some literature about it would be appreciated.

Thank You

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

Mauricio Alejandro Cano

Pontificia Universidad Javeriana 

Facultad de Ingeniería

Ingeniería de Sistemas y Computación