The Coq mailing list

[Pierre Casteran <pierre.casteran AT labri.fr>]

Hi,

  It's difficult to answer your question: I think it lacks some
declarations of the operators that occur in t2 and tt2.

Pierre






On 27/08/2012 03:12, like wrote:
> 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 ?