The Coq mailing list

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

Good Day,

Might have been a really silly question, but it might be useful for someone so i'll post the answer, i defined a pair of functions (head and tail) for the list of propositions, and then another one that created a sequence of implications, then added another rule for Deduction:

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.

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 => exists x:D, (evalCons C1)

end.

Fixpoint map (l:list process) : list token :=

 match l with

  nil => nil

| cons a t => cons(evalCons(stores a)) (map t)

end.

Definition insImp (t1 t2 : token) :token := t1->t2. 

Fixpoint hd (l:list token) :=

 match l with

  | nil => False

  | x :: _ => x

 end.

Fixpoint tl (l:list token) :=

 match l with

      | nil => nil

      | a :: m => m

    end.

Fixpoint hyp (l:list token) (t : token) :=

  match l with

   | nil =>  t

   | x::l' => x -> hyp(l') t

  end.

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

 |introAsk : forall (p: list process) (q:process) (c d:constraint),

              Deduction p c  -> Deduction (q::p) d -> Deduction ((ask c then q)::p) d

 |introLoc : forall (p: list process) (q:process) (x:D) (c:constraint),

              Deduction (q::p) c -> Deduction ((local x q)::p) (exist x c)

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

            (hyp (map p) (evalCons c)) -> Deduction p c. 

And this, did the trick.

Thank you

 

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

Mauricio Alejandro Cano

Pontificia Universidad Javeriana 

Facultad de Ingeniería

Ingeniería de Sistemas y Computación

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

Good Day,

I have a question, is it possible, given a list of propositions, for example

[p, r, r->s,q] to define a function that uses the elements of the list to deduce something? the exact problem is this, i have this definitions:

(*Requirements*)

Require Export List.

Require Export Permutation.

Set Implicit Arguments.

(*Global notation for lists*)

Notation "[]" := nil.

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

(*Global definitions and more notation definitions*)

(*Tokens*)

Definition token:=Prop.

(*Variable Domain*)

Definition D:=Set.

(*Definition of constraints*)

Inductive constraint : Type :=

  basic : token->constraint

 |exist : D->constraint->constraint

 |conj : constraint->constraint->constraint

 |impl : constraint->constraint->constraint.

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

(*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*)

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

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 => exists x:D, (evalCons C1)

end.

Fixpoint map (l:list process) : list token :=

 match l with

  nil => nil

| cons a t => cons(evalCons(stores a)) (map t)

end.

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

 |introAsk : forall (p: list process) (q:process) (c d:constraint),

              Deduction p c  -> Deduction (q::p) d -> Deduction ((ask c then q)::p) d

 |introLoc : forall (p: list process) (q:process) (x:D) (c:constraint),

              Deduction (q::p) c -> Deduction ((local x q)::p) (exist x c).

 Hypothesis t1 t2  t3: token.

 Variable u y z:nat.

 Definition c1:= %(u>10).

 Definition c2:= %(y<5).

 Definition c3:= %(z=1).

 Variable x:D.

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

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

 Definition P5: process:= (local x (tell(c1))).

 Definition P1: list token := (map [P4,tell(c1),tell(c2) // tell(c3)]). 

 

  

  (* Some Theorems *)

  Theorem Th1: Deduction [tell(c1)//P4, tell(c2) // tell(c3)] c2.

   apply introPar. (*with (p:=[])(q:=tell(c1))(r:=P4).*)

   apply strPerm with (p:=[P4,tell(c1),tell(c2) // tell(c3)]).

   + apply perm_swap.

   + apply introAsk. (*with (c:=c1)(d:=c2).*)

     apply introTell.

     apply introTell. 

  Qed.

  Theorem Th2: Deduction [P5,P4,P3] (exist x c1).

    apply introLoc. (*with (q:=tell(c1)).*)

    apply introTell.

  Qed. 

As you can see, stores, evalCons and map, translate the list of processes to a list of tokens, that in this case are propositions, the thing is that i'm not sure how i can define a transformation that allows me to use a translated list to proof normally (with usual coq tactics such as intros, assumption, split, etc) a constraint transformed into a proposition.

I was thinking to create a function that generates a variable: A->B->C->D->...->N

where A,B,C,D,...,N are elements of the list, but i'm not sure what is the function for proving or if there is one.

Can anyone recommend me some literature, an explanation of how can i to do this.

Thank you all

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

Mauricio Alejandro Cano

Pontificia Universidad Javeriana 

Facultad de Ingeniería

Ingeniería de Sistemas y Computación