Mercurial > cpdt > repo

comparison 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
comparison
equal deleted inserted replaced
234:82eae7bc91ea 235:52b9e43be069
1 (* Copyright (c) 2009, Adam Chlipala
2 *
3 * This work is licensed under a
4 * Creative Commons Attribution-Noncommercial-No Derivative Works 3.0
5 * Unported License.
6 * The license text is available at:
7 * http://creativecommons.org/licenses/by-nc-nd/3.0/
8 *)
9
10 (* begin hide *)
11 Require Import Tactics.
12
13 Set Implicit Arguments.
14 (* end hide *)
15
16
17 (** %\chapter{Proving in the Large}% *)
18
19
20 (** * Modules *)
21
22 Module Type GROUP.
23 Parameter G : Set.
24 Parameter f : G -> G -> G.
25 Parameter e : G.
26 Parameter i : G -> G.
27
28 Axiom assoc : forall a b c, f (f a b) c = f a (f b c).
29 Axiom ident : forall a, f e a = a.
30 Axiom inverse : forall a, f (i a) a = e.
31 End GROUP.
32
33 Module Type GROUP_THEOREMS.
34 Declare Module M : GROUP.
35
36 Axiom ident' : forall a, M.f a M.e = a.
37
38 Axiom inverse' : forall a, M.f a (M.i a) = M.e.
39
40 Axiom unique_ident : forall e', (forall a, M.f e' a = a) -> e' = M.e.
41 End GROUP_THEOREMS.
42
43 Module Group (M : GROUP) : GROUP_THEOREMS.
44 Module M := M.
45
46 Import M.
47
48 Theorem inverse' : forall a, f a (i a) = e.
49 intro.
50 rewrite <- (ident (f a (i a))).
51 rewrite <- (inverse (f a (i a))) at 1.
52 rewrite assoc.
53 rewrite assoc.
54 rewrite <- (assoc (i a) a (i a)).
55 rewrite inverse.
56 rewrite ident.
57 apply inverse.
58 Qed.
59
60 Theorem ident' : forall a, f a e = a.
61 intro.
62 rewrite <- (inverse a).
63 rewrite <- assoc.
64 rewrite inverse'.
65 apply ident.
66 Qed.
67
68 Theorem unique_ident : forall e', (forall a, M.f e' a = a) -> e' = M.e.
69 intros.
70 rewrite <- (H e).
71 symmetry.
72 apply ident'.
73 Qed.
74 End Group.