-2

I want to embed PPTL(a kind of logic) in Coq. Because of its complex semantics, I just embed its systax. 

  Inductive formula :Set:= 
  | For : formula -> formula -> formula 
  | Fneg: formula -> formula  
  | Fnext: formula -> formula  
  | prj : list formula -> formula->formula.

And then I define some axioms for it. But I have a problem when proving this, I don't know why.

Axiom t2 :forall(p q:formula),('|-('x p '&&  'x q) )<->('|-('x(p '&& q))).
Theorem tt2 :forall(p q r:formula),('|-('x p '&&  'x q) ; r)->('|-('x(p '&& q)) ; r).
intros.
rewrite t2 in H.

Error: Found no subterm matching "'|-'x ?63 '&& 'x ?

This is part of the code. 

Require Import Setoid.
Variables (state : Set).
CoInductive stream : Set :=
cons_str : state -> stream -> stream.
Inductive formula :Set:=
|ftrue:formula
|ffalse:formula
| For : formula -> formula -> formula
| Fneg: formula -> formula
| Fnext: formula -> formula
| prj : list formula -> formula->formula.

Definition derivable : formula ->stream-> Prop.
Admitted.

Definition model_p (f :formula) := forall pi : stream, derivable f pi .
Notation "'|- f" := (model_p f) (at level 100, no associativity) .

Notation "p '|| q" := (For p q) (at level 76, right associativity) .
Notation "! p" := (Fneg p) (at level 71, right associativity) .
Notation "f 'prj g" := (prj f g) (at level 77, right associativity).
Notation "'x g" := (Fnext g) (at level 73, right associativity).

(************************derived  formulas  ********************)

Definition and(p q: formula) : formula :=!(!p '|| !q).
Notation "p '&& q" :=(and p q) (at level 74, left associativity).

Definition imp(p q: formula) : formula :=!p '|| q.
Notation "p '==> q" := (imp p q) (at level 79, no associativity) .

Definition iff (A B:formula) :formula:= ( (A '==>  B) '&& (B '==> A)) .
Notation "p <'==> q" := (iff p q) (at level 79, no associativity) .

Definition empty := ! 'x ftrue .

Definition chop(p:formula)(q:formula):= (cons p (cons q nil)) 'prj (empty).
Notation "p ; q" := (chop p q) (at level 75, right associativity).

Axiom t2 :forall(p q:formula),('|-('x p '&&  'x q) )<->('|-('x(p '&& q))).
Theorem tt2 :forall(p q r:formula),('|-('x p '&&  'x q) ; r)->('|-('x(p '&& q)) ; r).
intros.
rewrite t2 in H.
Omar Shehab
  • 831
  • 9
  • 21
like
  • 33
  • 3
  • 4
    What is the question? Also, please check the formatting of the post. – Dave Clarke Aug 29 '12 at 06:19
  • The problem is why the rewirte is worong. – like Aug 30 '12 at 01:17
  • 2
    The problem is that you need to put some effort into writing a proper question. Edit the question above, rather than just answer in a comment. If you spent 5 more minutes on your posts, you might increase the chance of getting an answer. – Dave Clarke Aug 30 '12 at 05:44
  • rewrite works from left to right. rewrite <- t2 should do the trick. – gallais Oct 08 '12 at 10:21

1 Answers1

0

The reason you can't rewrite with t2 is because it doesn't have the shape as H. You can see this more clearly with notations turned off.

You're trying to rewrite

model_p (chop (and (Fnext p) (Fnext q)) r)

using

model_p (and (Fnext p) (Fnext q)) <-> model_p (Fnext (and p q)).

chop doesn't appear in the equivalence.

Rui Baptista
  • 101
  • 1