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.
  • 1
    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. – Kaveh Aug 7 '12 at 1:58
  • 6
    This question is relevant: cstheory.stackexchange.com/questions/1370/… – Dave Clarke Aug 10 '12 at 9:21
  • 1
    possible duplicate of problem in embedding – Rui Baptista Jul 16 '13 at 15:51

Your Answer

 
discard

By clicking "Post Your Answer", you acknowledge that you have read our updated terms of service, privacy policy and cookie policy, and that your continued use of the website is subject to these policies.

Browse other questions tagged or ask your own question.