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) ,true.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:=  |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.
Encoding a logic in Coq
lo.logic;application of theory;coq