Mercurial > cpdt > repo
comparison src/InductiveTypes.v @ 292:2c88fc1dbe33
A pass of double-quotes and LaTeX operator beautification
author | Adam Chlipala <adam@chlipala.net> |
---|---|
date | Wed, 10 Nov 2010 16:31:04 -0500 |
parents | 4146889930c5 |
children | 7b38729be069 |
comparison
equal
deleted
inserted
replaced
291:da9ccc6bf572 | 292:2c88fc1dbe33 |
---|---|
64 | 64 |
65 destruct x. | 65 destruct x. |
66 | 66 |
67 ]] | 67 ]] |
68 | 68 |
69 %\noindent%...which corresponds to "proof by case analysis" in classical math. For non-recursive inductive types, the two tactics will always have identical behavior. Often case analysis is sufficient, even in proofs about recursive types, and it is nice to avoid introducing unneeded induction hypotheses. | 69 %\noindent%...which corresponds to %``%#"#proof by case analysis#"#%''% in classical math. For non-recursive inductive types, the two tactics will always have identical behavior. Often case analysis is sufficient, even in proofs about recursive types, and it is nice to avoid introducing unneeded induction hypotheses. |
70 | 70 |
71 What exactly %\textit{%#<i>#is#</i>#%}% the induction principle for [unit]? We can ask Coq: *) | 71 What exactly %\textit{%#<i>#is#</i>#%}% the induction principle for [unit]? We can ask Coq: *) |
72 | 72 |
73 Check unit_ind. | 73 Check unit_ind. |
74 (** [unit_ind : forall P : unit -> Prop, P tt -> forall u : unit, P u] *) | 74 (** [unit_ind : forall P : unit -> Prop, P tt -> forall u : unit, P u] *) |
327 forall n : nat_list, P n | 327 forall n : nat_list, P n |
328 ]] | 328 ]] |
329 | 329 |
330 %\medskip% | 330 %\medskip% |
331 | 331 |
332 In general, we can implement any "tree" types as inductive types. For example, here are binary trees of naturals. *) | 332 In general, we can implement any %``%#"#tree#"#%''% types as inductive types. For example, here are binary trees of naturals. *) |
333 | 333 |
334 Inductive nat_btree : Set := | 334 Inductive nat_btree : Set := |
335 | NLeaf : nat_btree | 335 | NLeaf : nat_btree |
336 | NNode : nat_btree -> nat -> nat_btree -> nat_btree. | 336 | NNode : nat_btree -> nat -> nat_btree -> nat_btree. |
337 | 337 |
577 Inductive formula : Set := | 577 Inductive formula : Set := |
578 | Eq : nat -> nat -> formula | 578 | Eq : nat -> nat -> formula |
579 | And : formula -> formula -> formula | 579 | And : formula -> formula -> formula |
580 | Forall : (nat -> formula) -> formula. | 580 | Forall : (nat -> formula) -> formula. |
581 | 581 |
582 (** Our kinds of formulas are equalities between naturals, conjunction, and universal quantification over natural numbers. We avoid needing to include a notion of "variables" in our type, by using Coq functions to encode quantification. For instance, here is the encoding of [forall x : nat, x = x]: *) | 582 (** Our kinds of formulas are equalities between naturals, conjunction, and universal quantification over natural numbers. We avoid needing to include a notion of %``%#"#variables#"#%''% in our type, by using Coq functions to encode quantification. For instance, here is the encoding of [forall x : nat, x = x]: *) |
583 | 583 |
584 Example forall_refl : formula := Forall (fun x => Eq x x). | 584 Example forall_refl : formula := Forall (fun x => Eq x x). |
585 | 585 |
586 (** We can write recursive functions over reflexive types quite naturally. Here is one translating our formulas into native Coq propositions. *) | 586 (** We can write recursive functions over reflexive types quite naturally. Here is one translating our formulas into native Coq propositions. *) |
587 | 587 |
934 | Cons tr rest => conj (nat_tree_ind' tr) (list_nat_tree_ind rest) | 934 | Cons tr rest => conj (nat_tree_ind' tr) (list_nat_tree_ind rest) |
935 end. | 935 end. |
936 | 936 |
937 ]] | 937 ]] |
938 | 938 |
939 Coq rejects this definition, saying "Recursive call to nat_tree_ind' has principal argument equal to "tr" instead of rest." There is no deep theoretical reason why this program should be rejected; Coq applies incomplete termination-checking heuristics, and it is necessary to learn a few of the most important rules. The term "nested inductive type" hints at the solution to this particular problem. Just like true mutually-inductive types require mutually-recursive induction principles, nested types require nested recursion. *) | 939 Coq rejects this definition, saying %``%#"#Recursive call to nat_tree_ind' has principal argument equal to "tr" instead of rest.#"#%''% There is no deep theoretical reason why this program should be rejected; Coq applies incomplete termination-checking heuristics, and it is necessary to learn a few of the most important rules. The term %``%#"#nested inductive type#"#%''% hints at the solution to this particular problem. Just like true mutually-inductive types require mutually-recursive induction principles, nested types require nested recursion. *) |
940 | 940 |
941 Fixpoint nat_tree_ind' (tr : nat_tree) : P tr := | 941 Fixpoint nat_tree_ind' (tr : nat_tree) : P tr := |
942 match tr with | 942 match tr with |
943 | NLeaf' => NLeaf'_case | 943 | NLeaf' => NLeaf'_case |
944 | NNode' n ls => NNode'_case n ls | 944 | NNode' n ls => NNode'_case n ls |
1049 (** It can be useful to understand how tactics like [discriminate] and [injection] work, so it is worth stepping through a manual proof of each kind. We will start with a proof fit for [discriminate]. *) | 1049 (** It can be useful to understand how tactics like [discriminate] and [injection] work, so it is worth stepping through a manual proof of each kind. We will start with a proof fit for [discriminate]. *) |
1050 | 1050 |
1051 Theorem true_neq_false : true <> false. | 1051 Theorem true_neq_false : true <> false. |
1052 | 1052 |
1053 (* begin thide *) | 1053 (* begin thide *) |
1054 (** We begin with the tactic [red], which is short for "one step of reduction," to unfold the definition of logical negation. *) | 1054 (** We begin with the tactic [red], which is short for %``%#"#one step of reduction,#"#%''% to unfold the definition of logical negation. *) |
1055 | 1055 |
1056 red. | 1056 red. |
1057 (** [[ | 1057 (** [[ |
1058 ============================ | 1058 ============================ |
1059 true = false -> False | 1059 true = false -> False |
1126 | 1126 |
1127 (** * Exercises *) | 1127 (** * Exercises *) |
1128 | 1128 |
1129 (** %\begin{enumerate}%#<ol># | 1129 (** %\begin{enumerate}%#<ol># |
1130 | 1130 |
1131 %\item%#<li># Define an inductive type [truth] with three constructors, [Yes], [No], and [Maybe]. [Yes] stands for certain truth, [No] for certain falsehood, and [Maybe] for an unknown situation. Define "not," "and," and "or" for this replacement boolean algebra. Prove that your implementation of "and" is commutative and distributes over your implementation of "or."#</li># | 1131 %\item%#<li># Define an inductive type [truth] with three constructors, [Yes], [No], and [Maybe]. [Yes] stands for certain truth, [No] for certain falsehood, and [Maybe] for an unknown situation. Define %``%#"#not,#"#%''% %``%#"#and,#"#%''% and %``%#"#or#"#%''% for this replacement boolean algebra. Prove that your implementation of %``%#"#and#"#%''% is commutative and distributes over your implementation of %``%#"#or.#"#%''%#</li># |
1132 | 1132 |
1133 %\item%#<li># Modify the first example language of Chapter 2 to include variables, where variables are represented with [nat]. Extend the syntax and semantics of expressions to accommodate the change. Your new [expDenote] function should take as a new extra first argument a value of type [var -> nat], where [var] is a synonym for naturals-as-variables, and the function assigns a value to each variable. Define a constant folding function which does a bottom-up pass over an expression, at each stage replacing every binary operation on constants with an equivalent constant. Prove that constant folding preserves the meanings of expressions.#</li># | 1133 %\item%#<li># Modify the first example language of Chapter 2 to include variables, where variables are represented with [nat]. Extend the syntax and semantics of expressions to accommodate the change. Your new [expDenote] function should take as a new extra first argument a value of type [var -> nat], where [var] is a synonym for naturals-as-variables, and the function assigns a value to each variable. Define a constant folding function which does a bottom-up pass over an expression, at each stage replacing every binary operation on constants with an equivalent constant. Prove that constant folding preserves the meanings of expressions.#</li># |
1134 | 1134 |
1135 %\item%#<li># Reimplement the second example language of Chapter 2 to use mutually-inductive types instead of dependent types. That is, define two separate (non-dependent) inductive types [nat_exp] and [bool_exp] for expressions of the two different types, rather than a single indexed type. To keep things simple, you may consider only the binary operators that take naturals as operands. Add natural number variables to the language, as in the last exercise, and add an "if" expression form taking as arguments one boolean expression and two natural number expressions. Define semantics and constant-folding functions for this new language. Your constant folding should simplify not just binary operations (returning naturals or booleans) with known arguments, but also "if" expressions with known values for their test expressions but possibly undetermined "then" and "else" cases. Prove that constant-folding a natural number expression preserves its meaning.#</li># | 1135 %\item%#<li># Reimplement the second example language of Chapter 2 to use mutually-inductive types instead of dependent types. That is, define two separate (non-dependent) inductive types [nat_exp] and [bool_exp] for expressions of the two different types, rather than a single indexed type. To keep things simple, you may consider only the binary operators that take naturals as operands. Add natural number variables to the language, as in the last exercise, and add an %``%#"#if#"#%''% expression form taking as arguments one boolean expression and two natural number expressions. Define semantics and constant-folding functions for this new language. Your constant folding should simplify not just binary operations (returning naturals or booleans) with known arguments, but also %``%#"#if#"#%''% expressions with known values for their test expressions but possibly undetermined %``%#"#then#"#%''% and %``%#"#else#"#%''% cases. Prove that constant-folding a natural number expression preserves its meaning.#</li># |
1136 | 1136 |
1137 %\item%#<li># Using a reflexive inductive definition, define a type [nat_tree] of infinitary trees, with natural numbers at their leaves and a countable infinity of new trees branching out of each internal node. Define a function [increment] that increments the number in every leaf of a [nat_tree]. Define a function [leapfrog] over a natural [i] and a tree [nt]. [leapfrog] should recurse into the [i]th child of [nt], the [i+1]st child of that node, the [i+2]nd child of the next node, and so on, until reaching a leaf, in which case [leapfrog] should return the number at that leaf. Prove that the result of any call to [leapfrog] is incremented by one by calling [increment] on the tree.#</li># | 1137 %\item%#<li># Using a reflexive inductive definition, define a type [nat_tree] of infinitary trees, with natural numbers at their leaves and a countable infinity of new trees branching out of each internal node. Define a function [increment] that increments the number in every leaf of a [nat_tree]. Define a function [leapfrog] over a natural [i] and a tree [nt]. [leapfrog] should recurse into the [i]th child of [nt], the [i+1]st child of that node, the [i+2]nd child of the next node, and so on, until reaching a leaf, in which case [leapfrog] should return the number at that leaf. Prove that the result of any call to [leapfrog] is incremented by one by calling [increment] on the tree.#</li># |
1138 | 1138 |
1139 %\item%#<li># Define a type of trees of trees of trees of (repeat to infinity). That is, define an inductive type [trexp], whose members are either base cases containing natural numbers or binary trees of [trexp]s. Base your definition on a parameterized binary tree type [btree] that you will also define, so that [trexp] is defined as a nested inductive type. Define a function [total] that sums all of the naturals at the leaves of a [trexp]. Define a function [increment] that increments every leaf of a [trexp] by one. Prove that, for all [tr], [total (increment tr) >= total tr]. On the way to finishing this proof, you will probably want to prove a lemma and add it as a hint using the syntax [Hint Resolve name_of_lemma.].#</li># | 1139 %\item%#<li># Define a type of trees of trees of trees of (repeat to infinity). That is, define an inductive type [trexp], whose members are either base cases containing natural numbers or binary trees of [trexp]s. Base your definition on a parameterized binary tree type [btree] that you will also define, so that [trexp] is defined as a nested inductive type. Define a function [total] that sums all of the naturals at the leaves of a [trexp]. Define a function [increment] that increments every leaf of a [trexp] by one. Prove that, for all [tr], [total (increment tr) >= total tr]. On the way to finishing this proof, you will probably want to prove a lemma and add it as a hint using the syntax [Hint Resolve name_of_lemma.].#</li># |
1140 | 1140 |