Mercurial > cpdt > repo

comparison src/InductiveTypes.v @ 437:8077352044b2

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
A pass over all formatting, after big pile of coqdoc changes
author Adam Chlipala <adam@chlipala.net>
date Fri, 27 Jul 2012 16:47:28 -0400
parents 671a6e7e1f29
children 393b8ed99c2f
comparison
equal deleted inserted replaced
436:5d5e44f905c7 437:8077352044b2
709 709
710 Up to this point, we have seen how to encode in Coq more and more of what is possible with algebraic datatypes in %\index{Haskell}%Haskell and %\index{ML}%ML. This may have given the inaccurate impression that inductive types are a strict extension of algebraic datatypes. In fact, Coq must rule out some types allowed by Haskell and ML, for reasons of soundness. Reflexive types provide our first good example of such a case. 710 Up to this point, we have seen how to encode in Coq more and more of what is possible with algebraic datatypes in %\index{Haskell}%Haskell and %\index{ML}%ML. This may have given the inaccurate impression that inductive types are a strict extension of algebraic datatypes. In fact, Coq must rule out some types allowed by Haskell and ML, for reasons of soundness. Reflexive types provide our first good example of such a case.
711 711
712 Given our last example of an inductive type, many readers are probably eager to try encoding the syntax of %\index{lambda calculus}%lambda calculus. Indeed, the function-based representation technique that we just used, called%\index{higher-order abstract syntax}\index{HOAS|see{higher-order abstract syntax}}% _higher-order abstract syntax_ (HOAS)%~\cite{HOAS}%, is the representation of choice for lambda calculi in %\index{Twelf}%Twelf and in many applications implemented in Haskell and ML. Let us try to import that choice to Coq: *) 712 Given our last example of an inductive type, many readers are probably eager to try encoding the syntax of %\index{lambda calculus}%lambda calculus. Indeed, the function-based representation technique that we just used, called%\index{higher-order abstract syntax}\index{HOAS|see{higher-order abstract syntax}}% _higher-order abstract syntax_ (HOAS)%~\cite{HOAS}%, is the representation of choice for lambda calculi in %\index{Twelf}%Twelf and in many applications implemented in Haskell and ML. Let us try to import that choice to Coq: *)
713 (* begin hide *) 713 (* begin hide *)
714 (* begin thide *)
714 Inductive term : Set := App | Abs. 715 Inductive term : Set := App | Abs.
715 Reset term. 716 Reset term.
716 Definition uhoh := O. 717 Definition uhoh := O.
718 (* end thide *)
717 (* end hide *) 719 (* end hide *)
718 (** [[ 720 (** [[
719 Inductive term : Set := 721 Inductive term : Set :=
720 | App : term -> term -> term 722 | App : term -> term -> term
721 | Abs : (term -> term) -> term. 723 | Abs : (term -> term) -> term.
747 749
748 (** * An Interlude on Induction Principles *) 750 (** * An Interlude on Induction Principles *)
749 751
750 (** As we have emphasized a few times already, Coq proofs are actually programs, written in the same language we have been using in our examples all along. We can get a first sense of what this means by taking a look at the definitions of some of the %\index{induction principles}%induction principles we have used. A close look at the details here will help us construct induction principles manually, which we will see is necessary for some more advanced inductive definitions. *) 752 (** As we have emphasized a few times already, Coq proofs are actually programs, written in the same language we have been using in our examples all along. We can get a first sense of what this means by taking a look at the definitions of some of the %\index{induction principles}%induction principles we have used. A close look at the details here will help us construct induction principles manually, which we will see is necessary for some more advanced inductive definitions. *)
751 753
752 (* begin hide *)
753 Print unit_ind. 754 Print unit_ind.
754 (* end hide *) 755 (** %\vspace{-.15in}%[[
755 (** %\noindent%[Print] [unit_ind.] *)
756 (** [[
757 unit_ind = 756 unit_ind =
758 fun P : unit -> Prop => unit_rect P 757 fun P : unit -> Prop => unit_rect P
759 : forall P : unit -> Prop, P tt -> forall u : unit, P u 758 : forall P : unit -> Prop, P tt -> forall u : unit, P u
760 759
761 ]] 760 ]]
769 768
770 ]] 769 ]]
771 770
772 The principle [unit_rect] gives [P] type [unit -> Type] instead of [unit -> Prop]. [Type] is another universe, like [Set] and [Prop]. In fact, it is a common supertype of both. Later on, we will discuss exactly what the significances of the different universes are. For now, it is just important that we can use [Type] as a sort of meta-universe that may turn out to be either [Set] or [Prop]. We can see the symmetry inherent in the subtyping relationship by printing the definition of another principle that was generated for [unit] automatically: *) 771 The principle [unit_rect] gives [P] type [unit -> Type] instead of [unit -> Prop]. [Type] is another universe, like [Set] and [Prop]. In fact, it is a common supertype of both. Later on, we will discuss exactly what the significances of the different universes are. For now, it is just important that we can use [Type] as a sort of meta-universe that may turn out to be either [Set] or [Prop]. We can see the symmetry inherent in the subtyping relationship by printing the definition of another principle that was generated for [unit] automatically: *)
773 772
774 (* begin hide *)
775 Print unit_rec. 773 Print unit_rec.
776 (* end hide *) 774 (** %\vspace{-.15in}%[[
777 (** %\noindent%[Print] [unit_rec.] *)
778 (** [[
779 unit_rec = 775 unit_rec =
780 fun P : unit -> Set => unit_rect P 776 fun P : unit -> Set => unit_rect P
781 : forall P : unit -> Set, P tt -> forall u : unit, P u 777 : forall P : unit -> Set, P tt -> forall u : unit, P u
782 778
783 ]] 779 ]]
792 Definition always_O' (u : unit) : nat := 788 Definition always_O' (u : unit) : nat :=
793 unit_rec (fun _ : unit => nat) O u. 789 unit_rec (fun _ : unit => nat) O u.
794 790
795 (** Going even further down the rabbit hole, [unit_rect] itself is not even a primitive. It is a functional program that we can write manually. *) 791 (** Going even further down the rabbit hole, [unit_rect] itself is not even a primitive. It is a functional program that we can write manually. *)
796 792
797 (* begin hide *)
798 Print unit_rect. 793 Print unit_rect.
799 (* end hide *) 794 (** %\vspace{-.15in}%[[
800 (** %\noindent%[Print] [unit_rect.] *)
801 (** [[
802 unit_rect = 795 unit_rect =
803 fun (P : unit -> Type) (f : P tt) (u : unit) => 796 fun (P : unit -> Type) (f : P tt) (u : unit) =>
804 match u as u0 return (P u0) with 797 match u as u0 return (P u0) with
805 | tt => f 798 | tt => f
806 end 799 end
818 match u with 811 match u with
819 | tt => f 812 | tt => f
820 end. 813 end.
821 814
822 (* begin hide *) 815 (* begin hide *)
816 (* begin thide *)
823 Definition foo := nat_rect. 817 Definition foo := nat_rect.
818 (* end thide *)
824 (* end hide *) 819 (* end hide *)
825 820
826 (** We rely on Coq's heuristics for inferring [match] annotations, which are not consulted in the pretty-printing of terms. 821 (** We rely on Coq's heuristics for inferring [match] annotations, which are not consulted in the pretty-printing of terms.
827 822
828 We can check the implementation [nat_rect] as well: *) 823 We can check the implementation [nat_rect] as well: *)
1018 Hypothesis NLeaf'_case : P NLeaf'. 1013 Hypothesis NLeaf'_case : P NLeaf'.
1019 Hypothesis NNode'_case : forall (n : nat) (ls : list nat_tree), 1014 Hypothesis NNode'_case : forall (n : nat) (ls : list nat_tree),
1020 All P ls -> P (NNode' n ls). 1015 All P ls -> P (NNode' n ls).
1021 1016
1022 (* begin hide *) 1017 (* begin hide *)
1018 (* begin thide *)
1023 Definition list_nat_tree_ind := O. 1019 Definition list_nat_tree_ind := O.
1020 (* end thide *)
1024 (* end hide *) 1021 (* end hide *)
1025 1022
1026 (** A first attempt at writing the induction principle itself follows the intuition that nested inductive type definitions are expanded into mutual inductive definitions. 1023 (** A first attempt at writing the induction principle itself follows the intuition that nested inductive type definitions are expanded into mutual inductive definitions.
1027 1024
1028 [[ 1025 [[