Mercurial > cpdt > repo
comparison src/DataStruct.v @ 443:97c60ffdb998
Vertical spacing pass for MoreDep and DataStruct
author | Adam Chlipala <adam@chlipala.net> |
---|---|
date | Wed, 01 Aug 2012 16:32:04 -0400 |
parents | 8077352044b2 |
children | df0a45de158a |
comparison
equal
deleted
inserted
replaced
442:89c67796754e | 443:97c60ffdb998 |
---|---|
42 | Next : forall n, fin n -> fin (S n). | 42 | Next : forall n, fin n -> fin (S n). |
43 | 43 |
44 (** An instance of [fin] is essentially a more richly typed copy of the natural numbers. Every element is a [First] iterated through applying [Next] a number of times that indicates which number is being selected. For instance, the three values of type [fin 3] are [First 2], [Next (First 1)], and [Next (Next (First 0))]. | 44 (** An instance of [fin] is essentially a more richly typed copy of the natural numbers. Every element is a [First] iterated through applying [Next] a number of times that indicates which number is being selected. For instance, the three values of type [fin 3] are [First 2], [Next (First 1)], and [Next (Next (First 0))]. |
45 | 45 |
46 Now it is easy to pick a [Prop]-free type for a selection function. As usual, our first implementation attempt will not convince the type checker, and we will attack the deficiencies one at a time. | 46 Now it is easy to pick a [Prop]-free type for a selection function. As usual, our first implementation attempt will not convince the type checker, and we will attack the deficiencies one at a time. |
47 | |
48 [[ | 47 [[ |
49 Fixpoint get n (ls : ilist n) : fin n -> A := | 48 Fixpoint get n (ls : ilist n) : fin n -> A := |
50 match ls with | 49 match ls with |
51 | Nil => fun idx => ? | 50 | Nil => fun idx => ? |
52 | Cons _ x ls' => fun idx => | 51 | Cons _ x ls' => fun idx => |
53 match idx with | 52 match idx with |
54 | First _ => x | 53 | First _ => x |
55 | Next _ idx' => get ls' idx' | 54 | Next _ idx' => get ls' idx' |
56 end | 55 end |
57 end. | 56 end. |
58 | |
59 ]] | 57 ]] |
60 | 58 %\vspace{-.15in}%We apply the usual wisdom of delaying arguments in [Fixpoint]s so that they may be included in [return] clauses. This still leaves us with a quandary in each of the [match] cases. First, we need to figure out how to take advantage of the contradiction in the [Nil] case. Every [fin] has a type of the form [S n], which cannot unify with the [O] value that we learn for [n] in the [Nil] case. The solution we adopt is another case of [match]-within-[return]. |
61 We apply the usual wisdom of delaying arguments in [Fixpoint]s so that they may be included in [return] clauses. This still leaves us with a quandary in each of the [match] cases. First, we need to figure out how to take advantage of the contradiction in the [Nil] case. Every [fin] has a type of the form [S n], which cannot unify with the [O] value that we learn for [n] in the [Nil] case. The solution we adopt is another case of [match]-within-[return]. | |
62 | |
63 [[ | 59 [[ |
64 Fixpoint get n (ls : ilist n) : fin n -> A := | 60 Fixpoint get n (ls : ilist n) : fin n -> A := |
65 match ls with | 61 match ls with |
66 | Nil => fun idx => | 62 | Nil => fun idx => |
67 match idx in fin n' return (match n' with | 63 match idx in fin n' return (match n' with |
75 match idx with | 71 match idx with |
76 | First _ => x | 72 | First _ => x |
77 | Next _ idx' => get ls' idx' | 73 | Next _ idx' => get ls' idx' |
78 end | 74 end |
79 end. | 75 end. |
80 | |
81 ]] | 76 ]] |
82 | 77 %\vspace{-.15in}%Now the first [match] case type-checks, and we see that the problem with the [Cons] case is that the pattern-bound variable [idx'] does not have an apparent type compatible with [ls']. In fact, the error message Coq gives for this exact code can be confusing, thanks to an overenthusiastic type inference heuristic. We are told that the [Nil] case body has type [match X with | 0 => A | S _ => unit end] for a unification variable [X], while it is expected to have type [A]. We can see that setting [X] to [0] resolves the conflict, but Coq is not yet smart enough to do this unification automatically. Repeating the function's type in a [return] annotation, used with an [in] annotation, leads us to a more informative error message, saying that [idx'] has type [fin n1] while it is expected to have type [fin n0], where [n0] is bound by the [Cons] pattern and [n1] by the [Next] pattern. As the code is written above, nothing forces these two natural numbers to be equal, though we know intuitively that they must be. |
83 Now the first [match] case type-checks, and we see that the problem with the [Cons] case is that the pattern-bound variable [idx'] does not have an apparent type compatible with [ls']. In fact, the error message Coq gives for this exact code can be confusing, thanks to an overenthusiastic type inference heuristic. We are told that the [Nil] case body has type [match X with | 0 => A | S _ => unit end] for a unification variable [X], while it is expected to have type [A]. We can see that setting [X] to [0] resolves the conflict, but Coq is not yet smart enough to do this unification automatically. Repeating the function's type in a [return] annotation, used with an [in] annotation, leads us to a more informative error message, saying that [idx'] has type [fin n1] while it is expected to have type [fin n0], where [n0] is bound by the [Cons] pattern and [n1] by the [Next] pattern. As the code is written above, nothing forces these two natural numbers to be equal, though we know intuitively that they must be. | |
84 | 78 |
85 We need to use [match] annotations to make the relationship explicit. Unfortunately, the usual trick of postponing argument binding will not help us here. We need to match on both [ls] and [idx]; one or the other must be matched first. To get around this, we apply the convoy pattern that we met last chapter. This application is a little more clever than those we saw before; we use the natural number predecessor function [pred] to express the relationship between the types of these variables. | 79 We need to use [match] annotations to make the relationship explicit. Unfortunately, the usual trick of postponing argument binding will not help us here. We need to match on both [ls] and [idx]; one or the other must be matched first. To get around this, we apply the convoy pattern that we met last chapter. This application is a little more clever than those we saw before; we use the natural number predecessor function [pred] to express the relationship between the types of these variables. |
86 | |
87 [[ | 80 [[ |
88 Fixpoint get n (ls : ilist n) : fin n -> A := | 81 Fixpoint get n (ls : ilist n) : fin n -> A := |
89 match ls with | 82 match ls with |
90 | Nil => fun idx => | 83 | Nil => fun idx => |
91 match idx in fin n' return (match n' with | 84 match idx in fin n' return (match n' with |
99 match idx in fin n' return ilist (pred n') -> A with | 92 match idx in fin n' return ilist (pred n') -> A with |
100 | First _ => fun _ => x | 93 | First _ => fun _ => x |
101 | Next _ idx' => fun ls' => get ls' idx' | 94 | Next _ idx' => fun ls' => get ls' idx' |
102 end ls' | 95 end ls' |
103 end. | 96 end. |
104 | |
105 ]] | 97 ]] |
106 | 98 %\vspace{-.15in}%There is just one problem left with this implementation. Though we know that the local [ls'] in the [Next] case is equal to the original [ls'], the type-checker is not satisfied that the recursive call to [get] does not introduce non-termination. We solve the problem by convoy-binding the partial application of [get] to [ls'], rather than [ls'] by itself. *) |
107 There is just one problem left with this implementation. Though we know that the local [ls'] in the [Next] case is equal to the original [ls'], the type-checker is not satisfied that the recursive call to [get] does not introduce non-termination. We solve the problem by convoy-binding the partial application of [get] to [ls'], rather than [ls'] by itself. *) | |
108 | 99 |
109 Fixpoint get n (ls : ilist n) : fin n -> A := | 100 Fixpoint get n (ls : ilist n) : fin n -> A := |
110 match ls with | 101 match ls with |
111 | Nil => fun idx => | 102 | Nil => fun idx => |
112 match idx in fin n' return (match n' with | 103 match idx in fin n' return (match n' with |
283 (** We can also build indexed lists of pairs in this way. *) | 274 (** We can also build indexed lists of pairs in this way. *) |
284 | 275 |
285 Example somePairs : hlist (fun T : Set => T * T)%type someTypes := | 276 Example somePairs : hlist (fun T : Set => T * T)%type someTypes := |
286 MCons (1, 2) (MCons (true, false) MNil). | 277 MCons (1, 2) (MCons (true, false) MNil). |
287 | 278 |
279 (** There are many more useful applications of heterogeneous lists, based on different choices of the first argument to [hlist]. *) | |
280 | |
288 (* end thide *) | 281 (* end thide *) |
289 | 282 |
290 | 283 |
291 (** ** A Lambda Calculus Interpreter *) | 284 (** ** A Lambda Calculus Interpreter *) |
292 | 285 |
442 end%type. | 435 end%type. |
443 | 436 |
444 (** The definition of [fmember] follows the definition of [ffin]. Empty lists have no members, and member types for nonempty lists are built by adding one new option to the type of members of the list tail. While for [ffin] we needed no new information associated with the option that we add, here we need to know that the head of the list equals the element we are searching for. We express that with a sum type whose left branch is the appropriate equality proposition. Since we define [fmember] to live in [Type], we can insert [Prop] types as needed, because [Prop] is a subtype of [Type]. | 437 (** The definition of [fmember] follows the definition of [ffin]. Empty lists have no members, and member types for nonempty lists are built by adding one new option to the type of members of the list tail. While for [ffin] we needed no new information associated with the option that we add, here we need to know that the head of the list equals the element we are searching for. We express that with a sum type whose left branch is the appropriate equality proposition. Since we define [fmember] to live in [Type], we can insert [Prop] types as needed, because [Prop] is a subtype of [Type]. |
445 | 438 |
446 We know all of the tricks needed to write a first attempt at a [get] function for [fhlist]s. | 439 We know all of the tricks needed to write a first attempt at a [get] function for [fhlist]s. |
447 | |
448 [[ | 440 [[ |
449 Fixpoint fhget (ls : list A) : fhlist ls -> fmember ls -> B elm := | 441 Fixpoint fhget (ls : list A) : fhlist ls -> fmember ls -> B elm := |
450 match ls with | 442 match ls with |
451 | nil => fun _ idx => match idx with end | 443 | nil => fun _ idx => match idx with end |
452 | _ :: ls' => fun mls idx => | 444 | _ :: ls' => fun mls idx => |
453 match idx with | 445 match idx with |
454 | inl _ => fst mls | 446 | inl _ => fst mls |
455 | inr idx' => fhget ls' (snd mls) idx' | 447 | inr idx' => fhget ls' (snd mls) idx' |
456 end | 448 end |
457 end. | 449 end. |
458 | |
459 ]] | 450 ]] |
460 | 451 %\vspace{-.15in}%Only one problem remains. The expression [fst mls] is not known to have the proper type. To demonstrate that it does, we need to use the proof available in the [inl] case of the inner [match]. *) |
461 Only one problem remains. The expression [fst mls] is not known to have the proper type. To demonstrate that it does, we need to use the proof available in the [inl] case of the inner [match]. *) | |
462 | 452 |
463 Fixpoint fhget (ls : list A) : fhlist ls -> fmember ls -> B elm := | 453 Fixpoint fhget (ls : list A) : fhlist ls -> fmember ls -> B elm := |
464 match ls with | 454 match ls with |
465 | nil => fun _ idx => match idx with end | 455 | nil => fun _ idx => match idx with end |
466 | _ :: ls' => fun mls idx => | 456 | _ :: ls' => fun mls idx => |
481 (* end hide *) | 471 (* end hide *) |
482 | 472 |
483 Print eq. | 473 Print eq. |
484 (** %\vspace{-.15in}% [[ | 474 (** %\vspace{-.15in}% [[ |
485 Inductive eq (A : Type) (x : A) : A -> Prop := eq_refl : x = x | 475 Inductive eq (A : Type) (x : A) : A -> Prop := eq_refl : x = x |
486 | |
487 ]] | 476 ]] |
488 | 477 |
489 In a proposition [x = y], we see that [x] is a parameter and [y] is a regular argument. The type of the constructor [eq_refl] shows that [y] can only ever be instantiated to [x]. Thus, within a pattern-match with [eq_refl], occurrences of [y] can be replaced with occurrences of [x] for typing purposes. *) | 478 In a proposition [x = y], we see that [x] is a parameter and [y] is a regular argument. The type of the constructor [eq_refl] shows that [y] can only ever be instantiated to [x]. Thus, within a pattern-match with [eq_refl], occurrences of [y] can be replaced with occurrences of [x] for typing purposes. *) |
490 (* end thide *) | 479 (* end thide *) |
491 | 480 |
553 tree_ind | 542 tree_ind |
554 : forall (A : Set) (P : tree A -> Prop), | 543 : forall (A : Set) (P : tree A -> Prop), |
555 (forall a : A, P (Leaf a)) -> | 544 (forall a : A, P (Leaf a)) -> |
556 (forall (n : nat) (i : ilist (tree A) n), P (Node i)) -> | 545 (forall (n : nat) (i : ilist (tree A) n), P (Node i)) -> |
557 forall t : tree A, P t | 546 forall t : tree A, P t |
558 | |
559 ]] | 547 ]] |
560 | 548 |
561 The automatically generated induction principle is too weak. For the [Node] case, it gives us no inductive hypothesis. We could write our own induction principle, as we did in Chapter 3, but there is an easier way, if we are willing to alter the definition of [tree]. *) | 549 The automatically generated induction principle is too weak. For the [Node] case, it gives us no inductive hypothesis. We could write our own induction principle, as we did in Chapter 3, but there is an easier way, if we are willing to alter the definition of [tree]. *) |
562 | 550 |
563 Abort. | 551 Abort. |
711 Implicit Arguments cond [A n]. | 699 Implicit Arguments cond [A n]. |
712 (* end thide *) | 700 (* end thide *) |
713 | 701 |
714 (** Now the expression interpreter is straightforward to write. *) | 702 (** Now the expression interpreter is straightforward to write. *) |
715 | 703 |
704 (* begin thide *) | |
716 Fixpoint exp'Denote t (e : exp' t) : type'Denote t := | 705 Fixpoint exp'Denote t (e : exp' t) : type'Denote t := |
717 match e with | 706 match e with |
718 | NConst n => n | 707 | NConst n => n |
719 | Plus e1 e2 => exp'Denote e1 + exp'Denote e2 | 708 | Plus e1 e2 => exp'Denote e1 + exp'Denote e2 |
720 | Eq e1 e2 => | 709 | Eq e1 e2 => |
721 if eq_nat_dec (exp'Denote e1) (exp'Denote e2) then true else false | 710 if eq_nat_dec (exp'Denote e1) (exp'Denote e2) then true else false |
722 | 711 |
723 | BConst b => b | 712 | BConst b => b |
724 | Cond _ _ tests bodies default => | 713 | Cond _ _ tests bodies default => |
725 (* begin thide *) | |
726 cond | 714 cond |
727 (exp'Denote default) | 715 (exp'Denote default) |
728 (fun idx => exp'Denote (tests idx)) | 716 (fun idx => exp'Denote (tests idx)) |
729 (fun idx => exp'Denote (bodies idx)) | 717 (fun idx => exp'Denote (bodies idx)) |
730 (* end thide *) | 718 end. |
731 end. | 719 (* begin hide *) |
720 Reset exp'Denote. | |
721 (* end hide *) | |
722 (* end thide *) | |
723 | |
724 (* begin hide *) | |
725 Fixpoint exp'Denote t (e : exp' t) : type'Denote t := | |
726 match e with | |
727 | NConst n => n | |
728 | Plus e1 e2 => exp'Denote e1 + exp'Denote e2 | |
729 | Eq e1 e2 => | |
730 if eq_nat_dec (exp'Denote e1) (exp'Denote e2) then true else false | |
731 | |
732 | BConst b => b | |
733 | Cond _ _ tests bodies default => | |
734 (* begin thide *) | |
735 cond | |
736 (exp'Denote default) | |
737 (fun idx => exp'Denote (tests idx)) | |
738 (fun idx => exp'Denote (bodies idx)) | |
739 (* end thide *) | |
740 end. | |
741 (* end hide *) | |
732 | 742 |
733 (** We will implement a constant-folding function that optimizes conditionals, removing cases with known-[false] tests and cases that come after known-[true] tests. A function [cfoldCond] implements the heart of this logic. The convoy pattern is used again near the end of the implementation. *) | 743 (** We will implement a constant-folding function that optimizes conditionals, removing cases with known-[false] tests and cases that come after known-[true] tests. A function [cfoldCond] implements the heart of this logic. The convoy pattern is used again near the end of the implementation. *) |
734 | 744 |
735 (* begin thide *) | 745 (* begin thide *) |
736 Section cfoldCond. | 746 Section cfoldCond. |
819 match goal with | 829 match goal with |
820 | [ IHn : forall tests bodies, _, tests : _ -> _, bodies : _ -> _ |- _ ] => | 830 | [ IHn : forall tests bodies, _, tests : _ -> _, bodies : _ -> _ |- _ ] => |
821 specialize (IHn (fun idx => tests (Some idx)) (fun idx => bodies (Some idx))) | 831 specialize (IHn (fun idx => tests (Some idx)) (fun idx => bodies (Some idx))) |
822 end; | 832 end; |
823 repeat (match goal with | 833 repeat (match goal with |
824 | [ |- context[match ?E with NConst _ => _ | _ => _ end] ] => dep_destruct E | 834 | [ |- context[match ?E with NConst _ => _ | _ => _ end] ] => |
835 dep_destruct E | |
825 | [ |- context[if ?B then _ else _] ] => destruct B | 836 | [ |- context[if ?B then _ else _] ] => destruct B |
826 end; crush). | 837 end; crush). |
827 Qed. | 838 Qed. |
828 | 839 |
829 (** It is also useful to know that the result of a call to [cond] is not changed by substituting new tests and bodies functions, so long as the new functions have the same input-output behavior as the old. It turns out that, in Coq, it is not possible to prove in general that functions related in this way are equal. We treat this issue with our discussion of axioms in a later chapter. For now, it suffices to prove that the particular function [cond] is _extensional_; that is, it is unaffected by substitution of functions with input-output equivalents. *) | 840 (** It is also useful to know that the result of a call to [cond] is not changed by substituting new tests and bodies functions, so long as the new functions have the same input-output behavior as the old. It turns out that, in Coq, it is not possible to prove in general that functions related in this way are equal. We treat this issue with our discussion of axioms in a later chapter. For now, it suffices to prove that the particular function [cond] is _extensional_; that is, it is unaffected by substitution of functions with input-output equivalents. *) |