The Coq mailing list

[Sosuke MORIGUCHI <chiguri.s AT gmail.com>]

Good evening,

The problem is that the deduction system you defined is wrong, at least IntroPar.

The rule you want is

[P1,P2]  |- c

---------------------introPar

[P1//P2] |- c

but, the rule you wrote is

[P1//P2] |- c
---------------------introPar

[P1,P2]  |- c

So, you should write IntroPar as

 |introPar : forall (p: list process) (q r : process) (c:constraint),

            Deduction ([q,r]++p) c -> Deduction ([q//r]++p) c.          

In this kind of descriptions, a left side of an arrow (->) means "an assumption of the rule" and

a right side means "a result derived with the rule".

I hope this will help you.

Sosuke Moriguchi.

2013/4/5 mauricio cano <mcano.programas AT gmail.com>

Good night to everyone, i'm trying to implement a simple deduction system in coq, i have the following:

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

(*Requirements*)

Require Export List.

Require Export Permutation.

(*Global notation for lists*)

Notation "[]" := nil.

Notation "[ x , .. , y ]" := (x :: .. (y :: nil) ..) : list_scope. 

(*Global definitions and more notation definitions*)

(*Tokens*)

Variable token:Set.

(*Definition of constraints*)

Inductive constraint : Type :=

 basic : token->constraint.

(*Definition of processes*) (*x : cartesian product*)

Inductive process : Type :=

  tell : constraint -> process (*tell : C |-> P*)

 |parallel : process -> process -> process (*parallel: PxP |-> P*)

 |ask : constraint -> process ->process. (*ask: cxP |-> P*)

(*Operations Notations (Syntactic Sugar!!)*)

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).

Inductive Deduction : list process -> constraint -> Prop :=

  strPerm : forall (p q : list process) (c : constraint),

             Permutation p q -> Deduction p c -> Deduction q c

 |introTell : forall (p : list process) (c : constraint),

              Deduction ([tell(c)]++p) c

 |introPar : forall (p: list process) (q r : process) (c:constraint),

            Deduction ([q//r]++p) c -> Deduction ([q,r]++p) c.               

 (* Definition of some tokens to work with *)

 Hypothesis t1 t2  t3: token.

 Definition c1:= (basic t1).

  Definition c2:= (basic t2).

  Definition c3:= (basic t3).

 (* Definition of a ccp process *)

 Definition P1:process := tell c1.

 Definition P2:process := tell c2.

 Definition P3: process:= (ask c1 then tell (c2)) // tell (c1).  

  (* Some Theorems *)

  Theorem Th1: Deduction [P1 // P2]  c1.

   apply introPar with (p:=[P1 // P2]) (q:=P1) (r:=P2) (c:=c1). (The problem is here)

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

When i do the apply introPar i got the following error:

Error: Impossible to unify "Deduction ([P1, P2] ++ [P1 // P2]) c1" with

 "Deduction [P1 // P2] c1"

I pretty much know the problem is within the definition of Deduction, however, i'm pretty much new with types,functional languages and coq, so i was wondering if someone could point out what am i doing wrong and how to correct it.

what i want is that the proof ask me to prove that with [P1,P2] (given [P1 // P2]) i can prove c1 something like:

[P1,P2]  |- c

---------------------introPar

[P1//P2] |- c 

Thank You,

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

Mauricio Alejandro Cano

Pontificia Universidad Javeriana 

Facultad de Ingeniería

Ingeniería de Sistemas y Computación