The Coq mailing list

[AUGER Cédric <sedrikov AT gmail.com>]

Le Fri, 5 Apr 2013 00:29:38 -0500,
mauricio cano 
<mcano.programas AT gmail.com>
 a écrit :

> 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.
> 
In fact you cannot prove your theorem (assuming consistency of the
theory of course)

  Theorem Th1: ~(Deduction [P1 // P2]  c1).
  Proof.
   intros Habs.
   remember [P1//P2].
   revert Heql.
   generalize P1 P2.
   induction Habs.
   + intros.
     apply (IHHabs p0 p1).
     revert Heql; generalize (p0 // p1); clear - H.
     induction H; intros r Hr; inversion Hr; clear Hr; subst; auto.
     f_equal.
     remember (@nil process) as l'.
     revert Heql'; clear - H.
     induction H; intros K; inversion K; clear K; subst; auto.
     assert (P := IHPermutation2 (eq_refl _)); subst; clear -
  IHPermutation1. auto.
   + simpl; intros.
     inversion Heql.
   + simpl; intros.
     inversion Heql.
  Qed.

Since you claim to be a beginner, you could try to run this proof
interactively and consult the documentation for each tactic you do not
know of. And if the documentation is not clear enough, contact us on
the list.

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

In fact, it would be the other way around:

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

Maybe, you misstyped the definition of Deduction, and wanted

>  |introPar : forall (p: list process) (q r : process) (c:constraint),
>             Deduction ([q,r]++p) c -> Deduction ([q//r]++p) c.

instead of

>  |introPar : forall (p: list process) (q r : process) (c:constraint),
>             Deduction ([q//r]++p) c -> Deduction ([q,r]++p) c.