# Changeset 2523 for Papers

Ignore:
Timestamp:
Dec 3, 2012, 4:30:39 PM (9 years ago)
Message:

...

File:
1 edited

### Legend:

Unmodified
 r2521 \begin{definition}[Universe encoding] A parametric universe $(\alpha_1,\ldots,\alpha_m) u := K_1:T_1 ~|~ \ldots ~|~ K_n:T_n$ (where $\alpha_1,\ldots, \alpha_m$ are type variables bound in A parametric universe $$(\alpha_1,\ldots,\alpha_m) u := K_1:T_1 ~|~ \ldots ~|~ K_n:T_n$$ (where $\alpha_1,\ldots, \alpha_m$ are type variables bound in $T_1,\ldots,T_n$) is encoded by means of: \begin{itemize} $$inductive~tag\_~ : Type[0] := k_1: tag\_ ~|~ \ldots ~|~ k_n: tag\_$$ \item An equality test $eq\_tag: tag\_ \to tag\_ \to bool$ that returns true iff the two tags are the same. This is boilerplate code that is often iff the two tags are equal. This is boilerplate code that is often automatized by interactive theorem provers. We write $tag$ for the type the $tag\_$ coupled with its decidable equality test $eq\_tag$. This is just a minor technicality of no importance. the $tag\_$ coupled with its decidable equality test $eq\_tag$ and a user provided proof that $\forall x,y:tag. eq\_tag x y = true \iff x=y$. \item A simple function $$tag\_of\_expr: \forall \alpha_1,\ldots,\alpha_m. u \alpha_1 \ldots \alpha_m \to tag$$ This boilerplate code is the bridge from the shallow to the deep encoding of the universe. \item A dual function that is the bridge from the deep to the shallow encoding. We \item A type former $$Q\_holds\_for\_tag: \forall \alpha_1,\ldots,\alpha_m. \forall Q: u~\alpha_1~\ldots~\alpha_n \to Prop. \forall t:tag. Prop$$ that performs pattern matching over the tag and returns the proof obligation for the proof of $Q$ in the case corresponding to the tag. \item A proof of exhaustivity of pattern matching over the tag. This boilerplate proof is the bridge from the deep to the shallow encoding of the universe. The statement is: $$Q\_holds\_for\_tag\_spec: \forall \alpha_1,\ldots,\alpha_m. \forall Q: u~\alpha_1~\ldots~\alpha_m \to Prop. \forall x: u~\alpha_1~\ldots~\alpha_m. Q\_holds\_for\_tag~\ldots~Q~\ldots~(tag\_of\_expr~\ldots~x) \to Q x$$ \end{itemize} \end{definition} \begin{example}[The universe for our running example] \begin{lstlisting} inductive expr (E: Type[0]) : Type[0] ≝ Num : nat -> expr E | Plus : E -> E -> expr E | Mul : E -> E -> expr E. inductive tag_ : Type[0] := num : tag_ | plus : tag_ | mul : tag_. definition eq_tag : tag_ -> tag_ -> bool := λt1,t2. match t1 with [ num => match t2 with [num => true | _ => false] | plus => match t2 with [plus => true | _ => false] | mul => match t2 with [mul => true | _ => false]]. definition tag : DeqSet ≝ mk_DeqSet tag_ eq_tag ?. ** normalize /2/ % #abs destruct qed. definition tag_of_expr : ∀E:Type[0]. expr E -> tag := λE,e. match e with [ Num _ => num | Plus _ _ => plus | Mul _ _ => mul ]. definition Q_holds_for_tag: ∀E:Type[0]. ∀Q: expr E → Prop. ∀t:tag. Prop ≝ λE,Q,t. match t with [ num  ⇒ ∀n.   Q (Num … n) | plus ⇒ ∀x,y. Q (Plus … x y) | mul  ⇒ ∀x,y. Q (Mul … x y) ]. theorem Q_holds_for_tag_spec: ∀E:Type[0]. ∀Q: expr E → Prop. ∀x: expr E. Q_holds_for_tag … Q … (tag_of_expr … x) → Q x. #E #Q * normalize // qed. \end{lstlisting} \end{example} \subsection{Simulation (reduction + type checking)}