Commit 5dc3468b authored by Adam Chlipala's avatar Adam Chlipala

Pass through Chapter 6

parent c9ac2de3
...@@ -161,9 +161,9 @@ We rewrite [pred_strong1], using some syntactic sugar for subset types. *) ...@@ -161,9 +161,9 @@ We rewrite [pred_strong1], using some syntactic sugar for subset types. *)
Locate "{ _ : _ | _ }". Locate "{ _ : _ | _ }".
(** %\vspace{-.15in}% [[ (** %\vspace{-.15in}% [[
Notation Notation
"{ x : A | P }" := sig (fun x : A => P) "{ x : A | P }" := sig (fun x : A => P)
]] ]]
*) *)
Definition pred_strong2 (s : {n : nat | n > 0}) : nat := Definition pred_strong2 (s : {n : nat | n > 0}) : nat :=
...@@ -209,6 +209,12 @@ Definition pred_strong3 (s : {n : nat | n > 0}) : {m : nat | proj1_sig s = S m} ...@@ -209,6 +209,12 @@ Definition pred_strong3 (s : {n : nat | n > 0}) : {m : nat | proj1_sig s = S m}
| exist (S n') pf => exist _ n' (eq_refl _) | exist (S n') pf => exist _ n' (eq_refl _)
end. end.
(* begin hide *)
(* begin thide *)
Definition ugh := lt.
(* end thide *)
(* end hide *)
Eval compute in pred_strong3 (exist _ 2 two_gt0). Eval compute in pred_strong3 (exist _ 2 two_gt0).
(** %\vspace{-.15in}% [[ (** %\vspace{-.15in}% [[
= exist (fun m : nat => 2 = S m) 1 (eq_refl 2) = exist (fun m : nat => 2 = S m) 1 (eq_refl 2)
...@@ -370,7 +376,7 @@ Program Definition pred_strong6 (n : nat) (_ : n > 0) : {m : nat | n = S m} := ...@@ -370,7 +376,7 @@ Program Definition pred_strong6 (n : nat) (_ : n > 0) : {m : nat | n = S m} :=
| S n' => n' | S n' => n'
end. end.
(** Printing the resulting definition of [pred_strong6] yields a term very similar to what we built with [refine]. [Program] can save time in writing programs that use subset types. Nonetheless, [refine] is often just as effective, and [refine] gives you more control over the form the final term takes, which can be useful when you want to prove additional theorems about your definition. [Program] will sometimes insert type casts that can complicate theorem proving. *) (** Printing the resulting definition of [pred_strong6] yields a term very similar to what we built with [refine]. [Program] can save time in writing programs that use subset types. Nonetheless, [refine] is often just as effective, and [refine] gives more control over the form the final term takes, which can be useful when you want to prove additional theorems about your definition. [Program] will sometimes insert type casts that can complicate theorem proving. *)
Eval compute in pred_strong6 two_gt0. Eval compute in pred_strong6 two_gt0.
(** %\vspace{-.15in}% [[ (** %\vspace{-.15in}% [[
...@@ -383,7 +389,7 @@ In this case, we see that the new definition yields the same computational behav ...@@ -383,7 +389,7 @@ In this case, we see that the new definition yields the same computational behav
(** * Decidable Proposition Types *) (** * Decidable Proposition Types *)
(** There is another type in the standard library which captures the idea of program values that indicate which of two propositions is true.%\index{Gallina terms!sumbool}% *) (** There is another type in the standard library that captures the idea of program values that indicate which of two propositions is true.%\index{Gallina terms!sumbool}% *)
Print sumbool. Print sumbool.
(** %\vspace{-.15in}% [[ (** %\vspace{-.15in}% [[
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment