<p>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:</p>

<pre><code>Axiom nxc:forall (p q:formula),
 chop (next p) q-&gt;  (next (chop p q)).(it is wrong) 
,true.
</code></pre>

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

<hr>

<pre><code>Theorem nxn:forall (p:formula),
derivable (Fnext p)-&gt; derivable(Fneg (Fnext (Fneg p))).
</code></pre>

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

<pre><code>This is part of the code. 

Require Import Setoid.
Variables (state : Set).
CoInductive stream : Set :=
    cons_str : state -&gt; stream -&gt; stream.
Inductive formula :Set:=
  |ftrue:formula
  |ffalse:formula
  | For : formula -&gt; formula -&gt; formula
  | Fneg: formula -&gt; formula
  | Fnext: formula -&gt; formula
  | prj : list formula -&gt; formula-&gt;formula.

Definition derivable : formula -&gt;stream-&gt; 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 '&amp;&amp; q" :=(and p q) (at level 74, left associativity).

Definition imp(p q: formula) : formula :=!p '|| q.
Notation "p '==&gt; q" := (imp p q) (at level 79, no associativity) .

Definition iff (A B:formula) :formula:= ( (A '==&gt;  B) '&amp;&amp; (B '==&gt; A)) .
Notation "p &lt;'==&gt; 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 '&amp;&amp;  'x q) )&lt;-&gt;('|-('x(p '&amp;&amp; q))).
Theorem tt2 :forall(p q r:formula),('|-('x p '&amp;&amp;  'x q) ; r)-&gt;('|-('x(p '&amp;&amp; q))
; r).
intros.
rewrite t2 in H.
</code></pre>

CC BY-SA 3.0
2012-08-07T01:58:56.083Z
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
CC BY-SA 3.0
2012-08-10T09:21:01.327Z
This question is relevant: http://cstheory.stackexchange.com/questions/1370/shallow-versus-deep-embeddings
Dave Clarke
CC BY-SA 3.0
2013-07-16T15:51:55.150Z
possible duplicate of [problem in embedding](http://cstheory.stackexchange.com/questions/12427/problem-in-embedding)
Rui Baptista
<lo.logic><application-of-theory><coq>
Encoding a logic in Coq
like
# Encoding a logic in Coq

(Asked by: username_0 on 2012-08-06)

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 username_0:
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.

**Tags:** lo.logic, application-of-theory, coq

> **Comments:**
> **username_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.  
> **username_2**: This question is relevant: http://cstheory.stackexchange.com/questions/1370/shallow-versus-deep-embeddings  
> **username_3**: possible duplicate of [problem in embedding](http://cstheory.stackexchange.com/questions/12427/problem-in-embedding)  

---

## 0 answers

