Mercurial > cpdt > repo
comparison src/Large.v @ 242:5a32784e30f3
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. *) |