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

 1 edited
Legend:
 Unmodified
 Added
 Removed

Papers/polymorphicvariants2012/polymorphicvariants.tex
r2521 r2523 501 501 502 502 \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 503 A 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 504 506 $T_1,\ldots,T_n$) is encoded by means of: 505 507 \begin{itemize} … … 510 512 $$inductive~tag\_~ : Type[0] := k_1: tag\_ ~~ \ldots ~~ k_n: tag\_$$ 511 513 \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 often514 iff the two tags are equal. This is boilerplate code that is often 513 515 automatized by interactive theorem provers. We write $tag$ for the type 514 the $tag\_$ coupled with its decidable equality test $eq\_tag$ . This is just515 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$. 516 518 \item A simple function $$tag\_of\_expr: \forall \alpha_1,\ldots,\alpha_m. 517 519 u \alpha_1 \ldots \alpha_m \to tag$$ … … 520 522 This boilerplate code is the bridge from the shallow to the deep 521 523 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$$ 524 538 \end{itemize} 525 539 \end{definition} 540 541 \begin{example}[The universe for our running example] 542 \begin{lstlisting} 543 inductive expr (E: Type[0]) : Type[0] ≝ 544 Num : nat > expr E 545  Plus : E > E > expr E 546  Mul : E > E > expr E. 547 548 inductive tag_ : Type[0] := num : tag_  plus : tag_  mul : tag_. 549 550 definition 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 557 definition tag : DeqSet ≝ mk_DeqSet tag_ eq_tag ?. 558 ** normalize /2/ % #abs destruct 559 qed. 560 561 definition 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 568 definition 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 577 theorem 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 // 581 qed. 582 \end{lstlisting} 583 \end{example} 526 584 527 585 \subsection{Simulation (reduction + type checking)}
Note: See TracChangeset
for help on using the changeset viewer.