The Coq mailing list

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

Le Mon, 27 Aug 2012 01:12:26 +0000 (UTC),
like 
<12like34xiongmao AT 163.com>
 a écrit :

> Hello:
>      I want to embed  PPTL(a kind of logic) in Coq. Because of its
> complex semantic, 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 ?
> 

Isn't it normally "apply" rather than "rewrite" used when dealing with
equivalences ?