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.
