I want to encode a logic into Coq. The semantics of the logic are very complex and I just want to encode the syntax, axioms, inference rules. I use deep embedding, but I can't use notation like:

Axiom nxc:forall (p q:formula),
 chop (next p) q->  (next (chop p q)).(it is wrong) 

They need type prop, but my type is formula. How can I make them unify?

Theorem nxn:forall (p:formula),
derivable (Fnext p)-> derivable(Fneg (Fnext (Fneg p))).

To prove this, I have to give all the axioms. I can't use the axioms of and (in Prop). This would be a very tedious work. Any suggestions?

This is part of the code. 

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

Definition derivable : formula ->stream-> Prop.

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).
rewrite t2 in H.
  • 1
    $\begingroup$ Welcome to cstheory, a Q&A site for research-level questions in theoretical computer science (TCS). Your question does not appear to be a research-level question in TCS. Please see the FAQ for more information on what is meant by this and suggestions for sites that might welcome your question. Finally, if your question is closed for being out of scope, and you believe you can edit the question to make it a research-level question, please feel free to do so. Closing is not permanent and questions can be reopened, check the FAQ for more information. $\endgroup$
    – Kaveh
    Aug 7, 2012 at 1:58
  • 6
    $\begingroup$ This question is relevant: cstheory.stackexchange.com/questions/1370/… $\endgroup$ Aug 10, 2012 at 9:21
  • 1
    $\begingroup$ possible duplicate of problem in embedding $\endgroup$ Jul 16, 2013 at 15:51


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Browse other questions tagged or ask your own question.