Mercurial > cpdt > repo
comparison src/InductiveTypes.v @ 35:6d05ee182b65
Nested Inductive Types
author | Adam Chlipala <adamc@hcoop.net> |
---|---|
date | Wed, 10 Sep 2008 15:47:22 -0400 |
parents | d44274542f8b |
children | 9e46ade5af21 |
comparison
equal
deleted
inserted
replaced
34:d44274542f8b | 35:6d05ee182b65 |
---|---|
324 | NLeaf : nat_btree | 324 | NLeaf : nat_btree |
325 | NNode : nat_btree -> nat -> nat_btree -> nat_btree. | 325 | NNode : nat_btree -> nat -> nat_btree -> nat_btree. |
326 | 326 |
327 Fixpoint nsize (tr : nat_btree) : nat := | 327 Fixpoint nsize (tr : nat_btree) : nat := |
328 match tr with | 328 match tr with |
329 | NLeaf => O | 329 | NLeaf => S O |
330 | NNode tr1 _ tr2 => plus (nsize tr1) (nsize tr2) | 330 | NNode tr1 _ tr2 => plus (nsize tr1) (nsize tr2) |
331 end. | 331 end. |
332 | 332 |
333 Fixpoint nsplice (tr1 tr2 : nat_btree) {struct tr1} : nat_btree := | 333 Fixpoint nsplice (tr1 tr2 : nat_btree) {struct tr1} : nat_btree := |
334 match tr1 with | 334 match tr1 with |
335 | NLeaf => tr2 | 335 | NLeaf => NNode tr2 O NLeaf |
336 | NNode tr1' n tr2' => NNode (nsplice tr1' tr2) n tr2' | 336 | NNode tr1' n tr2' => NNode (nsplice tr1' tr2) n tr2' |
337 end. | 337 end. |
338 | 338 |
339 Theorem plus_assoc : forall n1 n2 n3 : nat, plus (plus n1 n2) n3 = plus n1 (plus n2 n3). | 339 Theorem plus_assoc : forall n1 n2 n3 : nat, plus (plus n1 n2) n3 = plus n1 (plus n2 n3). |
340 induction n1; crush. | 340 induction n1; crush. |
412 Theorem length_app : forall ls1 ls2 : list, length (app ls1 ls2) | 412 Theorem length_app : forall ls1 ls2 : list, length (app ls1 ls2) |
413 = plus (length ls1) (length ls2). | 413 = plus (length ls1) (length ls2). |
414 induction ls1; crush. | 414 induction ls1; crush. |
415 Qed. | 415 Qed. |
416 End list. | 416 End list. |
417 | |
418 (* begin hide *) | |
419 Implicit Arguments Nil [T]. | |
420 (* end hide *) | |
417 | 421 |
418 (** After we end the section, the [Variable]s we used are added as extra function parameters for each defined identifier, as needed. *) | 422 (** After we end the section, the [Variable]s we used are added as extra function parameters for each defined identifier, as needed. *) |
419 | 423 |
420 Check list. | 424 Check list. |
421 (** [[ | 425 (** [[ |
812 | And f1 f2 => And_case (formula_ind' f1) (formula_ind' f2) | 816 | And f1 f2 => And_case (formula_ind' f1) (formula_ind' f2) |
813 | Forall f' => Forall_case f' (fun n => formula_ind' (f' n)) | 817 | Forall f' => Forall_case f' (fun n => formula_ind' (f' n)) |
814 end. | 818 end. |
815 End formula_ind'. | 819 End formula_ind'. |
816 | 820 |
821 | |
822 (** * Nested Inductive Types *) | |
823 | |
824 (** Suppose we want to extend our earlier type of binary trees to trees with arbitrary finite branching. We can use lists to give a simple definition. *) | |
825 | |
826 Inductive nat_tree : Set := | |
827 | NLeaf' : nat_tree | |
828 | NNode' : nat -> list nat_tree -> nat_tree. | |
829 | |
830 (** This is an example of a %\textit{%#<i>#nested#</i>#%}% inductive type definition, because we use the type we are defining as an argument to a parametrized type family. Coq will not allow all such definitions; it effectively pretends that we are defining [nat_tree] mutually with a version of [list] specialized to [nat_tree], checking that the resulting expanded definition satisfies the usual rules. For instance, if we replaced [list] with a type family that used its parameter as a function argument, then the definition would be rejected as violating the positivity restriction. | |
831 | |
832 Like we encountered for mutual inductive types, we find that the automatically-generated induction principle for [nat_tree] is too weak. *) | |
833 | |
834 Check nat_tree_ind. | |
835 (** [[ | |
836 | |
837 nat_tree_ind | |
838 : forall P : nat_tree -> Prop, | |
839 P NLeaf' -> | |
840 (forall (n : nat) (l : list nat_tree), P (NNode' n l)) -> | |
841 forall n : nat_tree, P n | |
842 ]] | |
843 | |
844 There is no command like [Scheme] that will implement an improved principle for us. In general, it takes creativity to figure out how to incorporate nested uses to different type families. Now that we know how to implement induction principles manually, we are in a position to apply just such creativity to this problem. | |
845 | |
846 First, we will need an auxiliary definition, characterizing what it means for a property to hold of every element of a list. *) | |
847 | |
848 Section All. | |
849 Variable T : Set. | |
850 Variable P : T -> Prop. | |
851 | |
852 Fixpoint All (ls : list T) : Prop := | |
853 match ls with | |
854 | Nil => True | |
855 | Cons h t => P h /\ All t | |
856 end. | |
857 End All. | |
858 | |
859 (** It will be useful to look at the definitions of [True] and [/\], since we will want to write manual proofs of them below. *) | |
860 | |
861 Print True. | |
862 (** [[ | |
863 | |
864 Inductive True : Prop := I : True | |
865 ]] | |
866 | |
867 That is, [True] is a proposition with exactly one proof, [I], which we may always supply trivially. | |
868 | |
869 Finding the definition of [/\] takes a little more work. Coq supports user registration of arbitrary parsing rules, and it is such a rule that is letting us write [/\] instead of an application of some inductive type family. We can find the underlying inductive type with the [Locate] command. *) | |
870 | |
871 Locate "/\". | |
872 (** [[ | |
873 | |
874 Notation Scope | |
875 "A /\ B" := and A B : type_scope | |
876 (default interpretation) | |
877 ]] *) | |
878 | |
879 Print and. | |
880 (** [[ | |
881 | |
882 Inductive and (A : Prop) (B : Prop) : Prop := conj : A -> B -> A /\ B | |
883 For conj: Arguments A, B are implicit | |
884 For and: Argument scopes are [type_scope type_scope] | |
885 For conj: Argument scopes are [type_scope type_scope _ _] | |
886 ]] | |
887 | |
888 In addition to the definition of [and] itself, we get information on implicit arguments and parsing rules for [and] and its constructor [conj]. We will ignore the parsing information for now. The implicit argument information tells us that we build a proof of a conjunction by calling the constructor [conj] on proofs of the conjuncts, with no need to include the types of those proofs as explicit arguments. | |
889 | |
890 %\medskip% | |
891 | |
892 Now we create a section for our induction principle, following the same basic plan as in the last section of this chapter. *) | |
893 | |
894 Section nat_tree_ind'. | |
895 Variable P : nat_tree -> Prop. | |
896 | |
897 Variable NLeaf'_case : P NLeaf'. | |
898 Variable NNode'_case : forall (n : nat) (ls : list nat_tree), | |
899 All P ls -> P (NNode' n ls). | |
900 | |
901 (** A first attempt at writing the induction principle itself follows the intuition that nested inductive type definitions are expanded into mutual inductive definitions. | |
902 | |
903 [[ | |
904 | |
905 Fixpoint nat_tree_ind' (tr : nat_tree) : P tr := | |
906 match tr return (P tr) with | |
907 | NLeaf' => NLeaf'_case | |
908 | NNode' n ls => NNode'_case n ls (list_nat_tree_ind ls) | |
909 end | |
910 | |
911 with list_nat_tree_ind (ls : list nat_tree) : All P ls := | |
912 match ls return (All P ls) with | |
913 | Nil => I | |
914 | Cons tr rest => conj (nat_tree_ind' tr) (list_nat_tree_ind rest) | |
915 end. | |
916 | |
917 Coq rejects this definition, saying "Recursive call to nat_tree_ind' has principal argument equal to "tr" instead of rest." The term "nested inductive type" hints at the solution to the problem. Just like true mutually-inductive types require mutually-recursive induction principles, nested types require nested recursion. *) | |
918 | |
919 Fixpoint nat_tree_ind' (tr : nat_tree) : P tr := | |
920 match tr return (P tr) with | |
921 | NLeaf' => NLeaf'_case | |
922 | NNode' n ls => NNode'_case n ls | |
923 ((fix list_nat_tree_ind (ls : list nat_tree) : All P ls := | |
924 match ls return (All P ls) with | |
925 | Nil => I | |
926 | Cons tr rest => conj (nat_tree_ind' tr) (list_nat_tree_ind rest) | |
927 end) ls) | |
928 end. | |
929 | |
930 (** We include an anonymous [fix] version of [list_nat_tree_ind] that is literally %\textit{%#<i>#nested#</i>#%}% inside the definition of the recursive function corresponding to the inductive definition that had the nested use of [list]. *) | |
931 | |
932 End nat_tree_ind'. | |
933 | |
934 (** We can try our induction principle out by defining some recursive functions on [nat_tree]s and proving a theorem about them. First, we define some helper functions that operate on lists. *) | |
935 | |
936 Section map. | |
937 Variables T T' : Set. | |
938 Variable f : T -> T'. | |
939 | |
940 Fixpoint map (ls : list T) : list T' := | |
941 match ls with | |
942 | Nil => Nil | |
943 | Cons h t => Cons (f h) (map t) | |
944 end. | |
945 End map. | |
946 | |
947 Fixpoint sum (ls : list nat) : nat := | |
948 match ls with | |
949 | Nil => O | |
950 | Cons h t => plus h (sum t) | |
951 end. | |
952 | |
953 (** Now we can define a size function over our trees. *) | |
954 | |
955 Fixpoint ntsize (tr : nat_tree) : nat := | |
956 match tr with | |
957 | NLeaf' => S O | |
958 | NNode' _ trs => S (sum (map ntsize trs)) | |
959 end. | |
960 | |
961 (** Notice that Coq was smart enough to expand the definition of [map] to verify that we are using proper nested recursion, even through a use of a higher-order function. *) | |
962 | |
963 Fixpoint ntsplice (tr1 tr2 : nat_tree) {struct tr1} : nat_tree := | |
964 match tr1 with | |
965 | NLeaf' => NNode' O (Cons tr2 Nil) | |
966 | NNode' n Nil => NNode' n (Cons tr2 Nil) | |
967 | NNode' n (Cons tr trs) => NNode' n (Cons (ntsplice tr tr2) trs) | |
968 end. | |
969 | |
970 (** We have defined another arbitrary notion of tree splicing, similar to before, and we can prove an analogous theorem about its relationship with tree size. We start with a useful lemma about addition. *) | |
971 | |
972 Lemma plus_S : forall n1 n2 : nat, | |
973 plus n1 (S n2) = S (plus n1 n2). | |
974 induction n1; crush. | |
975 Qed. | |
976 | |
977 (** Now we begin the proof of the theorem, adding the lemma [plus_S] as a hint. *) | |
978 | |
979 Theorem ntsize_ntsplice : forall tr1 tr2 : nat_tree, ntsize (ntsplice tr1 tr2) | |
980 = plus (ntsize tr2) (ntsize tr1). | |
981 Hint Rewrite plus_S : cpdt. | |
982 | |
983 (** We know that the standard induction principle is insufficient for the task, so we need to provide a [using] clause for the [induction] tactic to specify our alternate principle. *) | |
984 induction tr1 using nat_tree_ind'; crush. | |
985 | |
986 (** One subgoal remains: [[ | |
987 | |
988 n : nat | |
989 ls : list nat_tree | |
990 H : All | |
991 (fun tr1 : nat_tree => | |
992 forall tr2 : nat_tree, | |
993 ntsize (ntsplice tr1 tr2) = plus (ntsize tr2) (ntsize tr1)) ls | |
994 tr2 : nat_tree | |
995 ============================ | |
996 ntsize | |
997 match ls with | |
998 | Nil => NNode' n (Cons tr2 Nil) | |
999 | Cons tr trs => NNode' n (Cons (ntsplice tr tr2) trs) | |
1000 end = S (plus (ntsize tr2) (sum (map ntsize ls))) | |
1001 ]] | |
1002 | |
1003 After a few moments of squinting at this goal, it becomes apparent that we need to do a case analysis on the structure of [ls]. The rest is routine. *) | |
1004 | |
1005 destruct ls; crush. | |
1006 | |
1007 (** We can go further in automating the proof by exploiting the hint mechanism further. *) | |
1008 | |
1009 Restart. | |
1010 Hint Extern 1 (ntsize (match ?LS with Nil => _ | Cons _ _ => _ end) = _) => | |
1011 destruct LS; crush. | |
1012 induction tr1 using nat_tree_ind'; crush. | |
1013 Qed. | |
1014 | |
1015 (** We will go into great detail on hints in a later chapter, but the only important thing to note here is that we register a pattern that describes a conclusion we expect to encounter during the proof. The pattern may contain unification variables, whose names are prefixed with question marks, and we may refer to those bound variables in a tactic that we ask to have run whenever the pattern matches. | |
1016 | |
1017 The advantage of using the hint is not very clear here, because the original proof was so short. However, the hint has fundamentally improved the readability of our proof. Before, the proof refered to the local variable [ls], which has an automatically-generated name. To a human reading the proof script without stepping through it interactively, it was not clear where [ls] came from. The hint explains to the reader the process for choosing which variables to case analyze on, and the hint can continue working even if the rest of the proof structure changes significantly. *) |