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

<p>You're trying to rewrite</p>

<pre><code>model_p (chop (and (Fnext p) (Fnext q)) r)
</code></pre>

<p>using</p>

<pre><code>model_p (and (Fnext p) (Fnext q)) &lt;-&gt; model_p (Fnext (and p q)).
</code></pre>

<p><code>chop</code> doesn't appear in the equivalence.</p>

CC BY-SA 3.0
2013-07-16T15:48:21.367Z
2013-07-16T15:48:21.367Z
Rui Baptista
<p>I want to embed  PPTL(a kind of logic) in Coq. Because of its complex
semantics, I just embed its systax.  </p>

<pre><code>  Inductive formula :Set:= 
  | For : formula -&gt; formula -&gt; formula 
  | Fneg: formula -&gt; formula  
  | Fnext: formula -&gt; formula  
  | prj : list formula -&gt; formula-&gt;formula.
</code></pre>

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

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

Error: Found no subterm matching "'|-'x ?63 '&amp;&amp; 'x ?
</code></pre>

<p>This is part of the code. </p>

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

Definition derivable : formula -&gt;stream-&gt; 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 '&amp;&amp; q" :=(and p q) (at level 74, left associativity).

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

Definition iff (A B:formula) :formula:= ( (A '==&gt;  B) '&amp;&amp; (B '==&gt; A)) .
Notation "p &lt;'==&gt; 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 '&amp;&amp;  'x q) )&lt;-&gt;('|-('x(p '&amp;&amp; q))).
Theorem tt2 :forall(p q r:formula),('|-('x p '&amp;&amp;  'x q) ; r)-&gt;('|-('x(p '&amp;&amp; q)) ; r).
intros.
rewrite t2 in H.
</code></pre>

CC BY-SA 3.0
2012-08-29T06:19:40.430Z
What is the question? Also, please check the formatting of the post.
Dave Clarke
CC BY-SA 3.0
2012-08-30T01:17:37.517Z
The problem is why the rewirte is worong.
like
CC BY-SA 3.0
2012-08-30T05:44:39.950Z
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
CC BY-SA 3.0
2012-10-08T10:21:08.520Z
`rewrite` works from left to right. `rewrite <- t2` should do the trick.
gallais
<lo.logic><coq><linear-temporal-logic>
Problem in embedding
like
# Problem in embedding

(Asked by: username_0 on 2012-08-29)

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.

**Tags:** lo.logic, coq, linear-temporal-logic

> **Comments:**
> **username_1**: What is the question? Also, please check the formatting of the post.  
> **username_0**: The problem is why the rewirte is worong.  
> **username_1**: 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.  
> **username_2**: `rewrite` works from left to right. `rewrite <- t2` should do the trick.  

---

## 1 answers

### Answer by username_3 on 2013-07-16. Score: 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.


---

