Mercurial > cpdt > repo

annotate src/Large.v @ 235:52b9e43be069

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Uncommented functor example
author Adam Chlipala <adamc@hcoop.net>
date Fri, 04 Dec 2009 13:44:05 -0500
parents
children c8f49f07cead
rev   line source
adamc@235 1 (* Copyright (c) 2009, Adam Chlipala
adamc@235 2 *
adamc@235 3 * This work is licensed under a
adamc@235 4 * Creative Commons Attribution-Noncommercial-No Derivative Works 3.0
adamc@235 5 * Unported License.
adamc@235 6 * The license text is available at:
adamc@235 7 * http://creativecommons.org/licenses/by-nc-nd/3.0/
adamc@235 8 *)
adamc@235 9
adamc@235 10 (* begin hide *)
adamc@235 11 Require Import Tactics.
adamc@235 12
adamc@235 13 Set Implicit Arguments.
adamc@235 14 (* end hide *)
adamc@235 15
adamc@235 16
adamc@235 17 (** %\chapter{Proving in the Large}% *)
adamc@235 18
adamc@235 19
adamc@235 20 (** * Modules *)
adamc@235 21
adamc@235 22 Module Type GROUP.
adamc@235 23 Parameter G : Set.
adamc@235 24 Parameter f : G -> G -> G.
adamc@235 25 Parameter e : G.
adamc@235 26 Parameter i : G -> G.
adamc@235 27
adamc@235 28 Axiom assoc : forall a b c, f (f a b) c = f a (f b c).
adamc@235 29 Axiom ident : forall a, f e a = a.
adamc@235 30 Axiom inverse : forall a, f (i a) a = e.
adamc@235 31 End GROUP.
adamc@235 32
adamc@235 33 Module Type GROUP_THEOREMS.
adamc@235 34 Declare Module M : GROUP.
adamc@235 35
adamc@235 36 Axiom ident' : forall a, M.f a M.e = a.
adamc@235 37
adamc@235 38 Axiom inverse' : forall a, M.f a (M.i a) = M.e.
adamc@235 39
adamc@235 40 Axiom unique_ident : forall e', (forall a, M.f e' a = a) -> e' = M.e.
adamc@235 41 End GROUP_THEOREMS.
adamc@235 42
adamc@235 43 Module Group (M : GROUP) : GROUP_THEOREMS.
adamc@235 44 Module M := M.
adamc@235 45
adamc@235 46 Import M.
adamc@235 47
adamc@235 48 Theorem inverse' : forall a, f a (i a) = e.
adamc@235 49 intro.
adamc@235 50 rewrite <- (ident (f a (i a))).
adamc@235 51 rewrite <- (inverse (f a (i a))) at 1.
adamc@235 52 rewrite assoc.
adamc@235 53 rewrite assoc.
adamc@235 54 rewrite <- (assoc (i a) a (i a)).
adamc@235 55 rewrite inverse.
adamc@235 56 rewrite ident.
adamc@235 57 apply inverse.
adamc@235 58 Qed.
adamc@235 59
adamc@235 60 Theorem ident' : forall a, f a e = a.
adamc@235 61 intro.
adamc@235 62 rewrite <- (inverse a).
adamc@235 63 rewrite <- assoc.
adamc@235 64 rewrite inverse'.
adamc@235 65 apply ident.
adamc@235 66 Qed.
adamc@235 67
adamc@235 68 Theorem unique_ident : forall e', (forall a, M.f e' a = a) -> e' = M.e.
adamc@235 69 intros.
adamc@235 70 rewrite <- (H e).
adamc@235 71 symmetry.
adamc@235 72 apply ident'.
adamc@235 73 Qed.
adamc@235 74 End Group.