Certified Programming with Dependent Types: src/Universes.v comparison

comparison src/Universes.v @ 302:7b38729be069

Tweak mark-up to support coqdoc 8.3

author	Adam Chlipala <adam@chlipala.net>
date	Mon, 17 Jan 2011 15:12:30 -0500
parents	be571572c088
children	d5787b70cf48

comparison

equal deleted inserted replaced

-:f4768d5a75eb
+:7b38729be069
 Check nat.
 (** %\vspace{-.15in}% [[
 nat
 : Set
-]] *)
+]]
+*)
 (** printing $ %({}*% #(<a/>*# *)
 (** printing ^ %*{})% #*<a/>)# *)
 Check Set.
 (** %\vspace{-.15in}% [[
 Set
 : Type $ (0)+1 ^
-]] *)
+]]
+*)
 Check Type.
 (** %\vspace{-.15in}% [[
 Type $ Top.3 ^
 : Type $ (Top.3)+1 ^
 Check forall T : nat, fin T.
 (** %\vspace{-.15in}% [[
 forall T : nat, fin T
 : Set
-]] *)
+]]
+*)
 Check forall T : Set, T.
 (** %\vspace{-.15in}% [[
 forall T : Set, T
 : Type $ max(0, (0)+1) ^
-]] *)
+]]
+*)
 Check forall T : Type, T.
 (** %\vspace{-.15in}% [[
 forall T : Type $ Top.9 ^ , T
 : Type $ max(Top.9, (Top.9)+1) ^
 Definition id (T : Type) (x : T) : T := x.
 Check id 0.
 (** %\vspace{-.15in}% [[
 id 0
 : nat
-]] *)
+]]
+*)
 Check id Set.
 (** %\vspace{-.15in}% [[
 id Set
 : Type $ Top.17 ^
-]] *)
+]]
+*)
 Check id Type.
 (** %\vspace{-.15in}% [[
 id Type $ Top.18 ^
 : Type $ Top.19 ^
-]] *)
+]]
+*)
 (** So far so good.  As we apply [id] to different [T] values, the inferred index for [T]'s [Type] occurrence automatically moves higher up the type hierarchy.
 [[
 Check id id.
 Check Const 0.
 (** %\vspace{-.15in}% [[
 Const 0
 : exp nat
-]] *)
+]]
+*)
 Check Pair (Const 0) (Const tt).
 (** %\vspace{-.15in}% [[
 Pair (Const 0) (Const tt)
 : exp (nat * unit)
-]] *)
+]]
+*)
 Check Eq (Const Set) (Const Type).
 (** %\vspace{-.15in}% [[
 Eq (Const Set) (Const Type $ Top.59 ^ )
 : exp bool
 Check foo nat.
 (** %\vspace{-.15in}% [[
 foo nat
 : Set
-]] *)
+]]
+*)
 Check foo Set.
 (** %\vspace{-.15in}% [[
 foo Set
 : Type
-]] *)
+]]
+*)
 Check foo True.
 (** %\vspace{-.15in}% [[
 foo True
 : Prop
 Print sig.
 (** %\vspace{-.15in}% [[
 Inductive sig (A : Type) (P : A -> Prop) : Type :=
 exist : forall x : A, P x -> sig P
-]] *)
+]]
+*)
 Print ex.
 (** %\vspace{-.15in}% [[
 Inductive ex (A : Type) (P : A -> Prop) : Prop :=
 ex_intro : forall x : A, P x -> ex P
 (** val sym_ex : __ **)
 let sym_ex = __
 >>
-In this example, the [ex] type itself is in [Prop], so whole [ex] packages are erased.  Coq extracts every proposition as the (Coq-specific) type %\texttt{%#<tt>#__#</tt>#%}%, whose single constructor is %\texttt{%#<tt>#__#</tt>#%}%.  Not only are proofs replaced by [__], but proof arguments to functions are also removed completely, as we see here.
+In this example, the [ex] type itself is in [Prop], so whole [ex] packages are erased.  Coq extracts every proposition as the (Coq-specific) type %\texttt{\_\_}%#<tt>__</tt>#, whose single constructor is %\texttt{\_\_}%#<tt>__</tt>#.  Not only are proofs replaced by [__], but proof arguments to functions are also removed completely, as we see here.
 Extraction is very helpful as an optimization over programs that contain proofs.  In languages like Haskell, advanced features make it possible to program with proofs, as a way of convincing the type checker to accept particular definitions.  Unfortunately, when proofs are encoded as values in GADTs, these proofs exist at runtime and consume resources.  In contrast, with Coq, as long as you keep all of your proofs within [Prop], extraction is guaranteed to erase them.
 Many fans of the Curry-Howard correspondence support the idea of %\textit{%#<i>#extracting programs from proofs#</i>#%}%.  In reality, few users of Coq and related tools do any such thing.  Instead, extraction is better thought of as an optimization that reduces the runtime costs of expressive typing.
 Check ConstP 0.
 (** %\vspace{-.15in}% [[
 ConstP 0
 : expP nat
-]] *)
+]]
+*)
 Check PairP (ConstP 0) (ConstP tt).
 (** %\vspace{-.15in}% [[
 PairP (ConstP 0) (ConstP tt)
 : expP (nat * unit)
-]] *)
+]]
+*)
 Check EqP (ConstP Set) (ConstP Type).
 (** %\vspace{-.15in}% [[
 EqP (ConstP Set) (ConstP Type)
 : expP bool
-]] *)
+]]
+*)
 Check ConstP (ConstP O).
 (** %\vspace{-.15in}% [[
 ConstP (ConstP 0)
 : expP (expP nat)
 Check (Base 0).
 (** %\vspace{-.15in}% [[
 Base 0
 : eqPlus 0 0
-]] *)
+]]
+*)
 Check (Func (fun n => n) (fun n => 0 + n) (fun n => Base n)).
 (** %\vspace{-.15in}% [[
 Func (fun n : nat => n) (fun n : nat => 0 + n) (fun n : nat => Base n)
 : eqPlus (fun n : nat => n) (fun n : nat => 0 + n)
-]] *)
+]]
+*)
 Check (Base (Base 1)).
 (** %\vspace{-.15in}% [[
 Base (Base 1)
 : eqPlus (Base 1) (Base 1)
-]] *)
+]]
+*)
 (** * Axioms *)
 (** While the specific logic Gallina is hardcoded into Coq's implementation, it is possible to add certain logical rules in a controlled way.  In other words, Coq may be used to reason about many different refinements of Gallina where strictly more theorems are provable.  We achieve this by asserting %\textit{%#<i>#axioms#</i>#%}% without proof.
 Qed.
 Print Assumptions t1.
 (** %\vspace{-.15in}% [[
 Closed under the global context
-]] *)
+]]
+*)
 Theorem t2 : forall P : Prop, ~ ~ P -> P.
 (** [[
 tauto.
 Error: tauto failed.
-]] *)
+]]
+*)
 intro P; destruct (classic P); tauto.
 Qed.
 Print Assumptions t2.
 : forall (A : Set) (f : A -> nat) (g : nat -> A),
 (forall x : A, g (f x) = x) ->
 forall P : A -> Prop,
 (forall x : A, {P x} + {~ P x}) ->
 (exists! x : A, P x) -> {x : A | P x}
-]] *)
+]]
+*)
 Print Assumptions constructive_definite_description.
 (** %\vspace{-.15in}% [[
 Closed under the global context
 Eval compute in (cast (refl_equal (nat -> nat)) (fun n => S n)) 12.
 (** [[
 = 13
 : nat
-]] *)
+]]
+*)
 (** Things do not go as smoothly when we use [cast] with proofs that rely on axioms. *)
 Theorem t3 : (forall n : nat, fin (S n)) = (forall n : nat, fin (n + 1)).
 change ((forall n : nat, (fun n => fin (S n)) n) = (forall n : nat, (fun n => fin (n + 1)) n));
 Eval compute in cast (t4 13) First.
 (** %\vspace{-.15in}% [[
 = First
 : fin (13 + 1)
-]] *)
+]]
+*)

Mercurial > cpdt > repo

comparison src/Universes.v @ 302:7b38729be069