Changeset 2523


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

...

File:
1 edited

Legend:

Unmodified
Added
Removed
  • Papers/polymorphic-variants-2012/polymorphic-variants.tex

    r2521 r2523  
    501501
    502502\begin{definition}[Universe encoding]
    503 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
     503A parametric universe
     504$$(\alpha_1,\ldots,\alpha_m) u := K_1:T_1 ~|~ \ldots ~|~ K_n:T_n$$
     505(where $\alpha_1,\ldots, \alpha_m$ are type variables bound in
    504506$T_1,\ldots,T_n$) is encoded by means of:
    505507\begin{itemize}
     
    510512  $$inductive~tag\_~ : Type[0] := k_1: tag\_ ~|~ \ldots ~|~ k_n: tag\_$$
    511513 \item An equality test $eq\_tag: tag\_ \to tag\_ \to bool$ that returns true
    512   iff the two tags are the same. This is boilerplate code that is often
     514  iff the two tags are equal. This is boilerplate code that is often
    513515  automatized by interactive theorem provers. We write $tag$ for the type
    514   the $tag\_$ coupled with its decidable equality test $eq\_tag$. This is just
    515   a minor technicality of no importance.
     516  the $tag\_$ coupled with its decidable equality test $eq\_tag$ and
     517  a user provided proof that $\forall x,y:tag. eq\_tag x y = true \iff x=y$.
    516518 \item A simple function $$tag\_of\_expr: \forall \alpha_1,\ldots,\alpha_m.
    517519   u \alpha_1 \ldots \alpha_m \to  tag$$
     
    520522   This boilerplate code is the bridge from the shallow to the deep
    521523   encoding of the universe.
    522  \item A dual function that is the bridge from the deep to the shallow encoding.
    523    We
     524 \item A type former
     525   $$Q\_holds\_for\_tag: \forall \alpha_1,\ldots,\alpha_m.
     526      \forall Q: u~\alpha_1~\ldots~\alpha_n \to Prop.
     527       \forall t:tag. Prop$$
     528   that performs pattern matching over the tag and returns the proof obligation
     529   for the proof of $Q$ in the case corresponding to the tag.
     530 \item A proof of exhaustivity of pattern matching over the tag. This
     531   boilerplate proof is the bridge from the deep to the shallow encoding of the
     532   universe. The statement is:
     533   $$Q\_holds\_for\_tag\_spec:
     534    \forall \alpha_1,\ldots,\alpha_m.
     535     \forall Q: u~\alpha_1~\ldots~\alpha_m \to Prop.
     536      \forall x: u~\alpha_1~\ldots~\alpha_m.
     537       Q\_holds\_for\_tag~\ldots~Q~\ldots~(tag\_of\_expr~\ldots~x) \to Q x$$
    524538\end{itemize}
    525539\end{definition}
     540
     541\begin{example}[The universe for our running example]
     542\begin{lstlisting}
     543inductive expr (E: Type[0]) : Type[0] ≝
     544   Num : nat -> expr E
     545 | Plus : E -> E -> expr E
     546 | Mul : E -> E -> expr E.
     547
     548inductive tag_ : Type[0] := num : tag_ | plus : tag_ | mul : tag_.
     549
     550definition eq_tag : tag_ -> tag_ -> bool :=
     551 λt1,t2.
     552  match t1 with
     553  [ num => match t2 with [num => true | _ => false]
     554  | plus => match t2 with [plus => true | _ => false]
     555  | mul => match t2 with [mul => true | _ => false]].
     556
     557definition tag : DeqSet ≝ mk_DeqSet tag_ eq_tag ?.
     558 ** normalize /2/ % #abs destruct
     559qed.
     560
     561definition tag_of_expr : ∀E:Type[0]. expr E -> tag :=
     562 λE,e.
     563   match e with
     564   [ Num _ => num
     565   | Plus _ _ => plus
     566   | Mul _ _ => mul ].
     567
     568definition Q_holds_for_tag:
     569 ∀E:Type[0]. ∀Q: expr E → Prop. ∀t:tag. Prop ≝
     570 λE,Q,t.
     571  match t with
     572    [ num  ⇒ ∀n.   Q (Num … n)
     573    | plus ⇒ ∀x,y. Q (Plus … x y)
     574    | mul  ⇒ ∀x,y. Q (Mul … x y)
     575    ].
     576
     577theorem Q_holds_for_tag_spec:
     578 ∀E:Type[0]. ∀Q: expr E → Prop.
     579  ∀x: expr E. Q_holds_for_tag … Q … (tag_of_expr … x) → Q x.
     580#E #Q * normalize //
     581qed.
     582\end{lstlisting}
     583\end{example}
    526584
    527585\subsection{Simulation (reduction + type checking)}
Note: See TracChangeset for help on using the changeset viewer.