Mercurial > cpdt > repo

comparison src/Large.v @ 242:5a32784e30f3

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Prose for Modules section
author Adam Chlipala <adamc@hcoop.net>
date Wed, 09 Dec 2009 13:07:31 -0500
parents cb3f3ef9d5bb
children b2c72c77ad47
comparison
equal deleted inserted replaced
241:cb3f3ef9d5bb 242:5a32784e30f3
626 The [abstract] tactical helps us force thunks by proving some subgoals as their own lemmas. For instance, a proof [induction x; crush] can in many cases be made to use significantly less peak memory by changing it to [induction x; abstract crush]. The main limitation of [abstract] is that it can only be applied to subgoals that are proved completely, with no undetermined unification variables remaining. Still, many large automated proofs can realize vast memory savings via [abstract]. *) 626 The [abstract] tactical helps us force thunks by proving some subgoals as their own lemmas. For instance, a proof [induction x; crush] can in many cases be made to use significantly less peak memory by changing it to [induction x; abstract crush]. The main limitation of [abstract] is that it can only be applied to subgoals that are proved completely, with no undetermined unification variables remaining. Still, many large automated proofs can realize vast memory savings via [abstract]. *)
627 627
628 628
629 (** * Modules *) 629 (** * Modules *)
630 630
631 (** Last chapter's examples of proof by reflection demonstrate opportunities for implementing abstract proof strategies with stronger formal guarantees than can be had with Ltac scripting. Coq's %\textit{%#<i>#module system#</i>#%}% provides another tool for more rigorous development of generic theorems. This feature is inspired by the module systems found in Standard ML and Objective Caml, and the discussion that follows assumes familiarity with the basics of one of those systems.
632
633 ML modules facilitate the grouping of abstract types with operations over those types. Moreover, there is support for %\textit{%#<i>#functors#</i>#%}%, which are functions from modules to modules. A canonical example of a functor is one that builds a data structure implementation from a module that describes a domain of keys and its associated comparison operations.
634
635 When we add modules to a base language with dependent types, it becomes possible to use modules and functors to formalize kinds of reasoning that are common in algebra. For instance, this module signature captures the essence of the algebraic structure known as a group. A group consists of a carrier set [G], an associative binary operation [f], a left identity element [e] for [f], and an operation [i] that is a left inverse for [f]. *)
636
631 Module Type GROUP. 637 Module Type GROUP.
632 Parameter G : Set. 638 Parameter G : Set.
633 Parameter f : G -> G -> G. 639 Parameter f : G -> G -> G.
634 Parameter e : G. 640 Parameter e : G.
635 Parameter i : G -> G. 641 Parameter i : G -> G.
637 Axiom assoc : forall a b c, f (f a b) c = f a (f b c). 643 Axiom assoc : forall a b c, f (f a b) c = f a (f b c).
638 Axiom ident : forall a, f e a = a. 644 Axiom ident : forall a, f e a = a.
639 Axiom inverse : forall a, f (i a) a = e. 645 Axiom inverse : forall a, f (i a) a = e.
640 End GROUP. 646 End GROUP.
641 647
648 (** Many useful theorems hold of arbitrary groups. We capture some such theorem statements in another module signature. *)
649
642 Module Type GROUP_THEOREMS. 650 Module Type GROUP_THEOREMS.
643 Declare Module M : GROUP. 651 Declare Module M : GROUP.
644 652
645 Axiom ident' : forall a, M.f a M.e = a. 653 Axiom ident' : forall a, M.f a M.e = a.
646 654
647 Axiom inverse' : forall a, M.f a (M.i a) = M.e. 655 Axiom inverse' : forall a, M.f a (M.i a) = M.e.
648 656
649 Axiom unique_ident : forall e', (forall a, M.f e' a = a) -> e' = M.e. 657 Axiom unique_ident : forall e', (forall a, M.f e' a = a) -> e' = M.e.
650 End GROUP_THEOREMS. 658 End GROUP_THEOREMS.
659
660 (** We implement generic proofs of these theorems with a functor, whose input is an arbitrary group [M]. The proofs are completely manual, since it would take some effort to build suitable generic automation; rather, these theorems can serve as a basis for an automated procedure for simplifying group expressions, along the lines of the procedure for monoids from the last chapter. We take the proofs from the Wikipedia page on elementary group theory. *)
651 661
652 Module Group (M : GROUP) : GROUP_THEOREMS with Module M := M. 662 Module Group (M : GROUP) : GROUP_THEOREMS with Module M := M.
653 Module M := M. 663 Module M := M.
654 664
655 Import M. 665 Import M.
680 symmetry. 690 symmetry.
681 apply ident'. 691 apply ident'.
682 Qed. 692 Qed.
683 End Group. 693 End Group.
684 694
695 (** We can show that the integers with [+] form a group. *)
696
685 Require Import ZArith. 697 Require Import ZArith.
686 Open Scope Z_scope. 698 Open Scope Z_scope.
687 699
688 Module Int. 700 Module Int.
689 Definition G := Z. 701 Definition G := Z.
700 Theorem inverse : forall a, f (i a) a = e. 712 Theorem inverse : forall a, f (i a) a = e.
701 unfold f, i, e; crush. 713 unfold f, i, e; crush.
702 Qed. 714 Qed.
703 End Int. 715 End Int.
704 716
717 (** Next, we can produce integer-specific versions of the generic group theorems. *)
718
705 Module IntTheorems := Group(Int). 719 Module IntTheorems := Group(Int).
706 720
707 Check IntTheorems.unique_ident. 721 Check IntTheorems.unique_ident.
722 (** %\vspace{-.15in}% [[
723 IntTheorems.unique_ident
724 : forall e' : Int.G, (forall a : Int.G, Int.f e' a = a) -> e' = Int.e
725 ]] *)
708 726
709 Theorem unique_ident : forall e', (forall a, e' + a = a) -> e' = 0. 727 Theorem unique_ident : forall e', (forall a, e' + a = a) -> e' = 0.
710 exact IntTheorems.unique_ident. 728 exact IntTheorems.unique_ident.
711 Qed. 729 Qed.
730
731 (** As in ML, the module system provides an effective way to structure large developments. Unlike in ML, Coq modules add no expressiveness; we can implement any module as an inhabitant of a dependent record type. It is the second-class nature of modules that makes them easier to use than dependent records in many case. Because modules may only be used in quite restricted ways, it is easier to support convenient module coding through special commands and editing modes, as the above example demonstrates. An isomorphic implementation with records would have suffered from lack of such conveniences as module subtyping and importation of the fields of a module. *)