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


---

