adamc@235: (* Copyright (c) 2009, Adam Chlipala
adamc@235:  * 
adamc@235:  * This work is licensed under a
adamc@235:  * Creative Commons Attribution-Noncommercial-No Derivative Works 3.0
adamc@235:  * Unported License.
adamc@235:  * The license text is available at:
adamc@235:  *   http://creativecommons.org/licenses/by-nc-nd/3.0/
adamc@235:  *)
adamc@235: 
adamc@235: (* begin hide *)
adamc@235: Require Import Tactics.
adamc@235: 
adamc@235: Set Implicit Arguments.
adamc@235: (* end hide *)
adamc@235: 
adamc@235: 
adamc@235: (** %\chapter{Proving in the Large}% *)
adamc@235: 
adamc@235: 
adamc@235: (** * Modules *)
adamc@235: 
adamc@235: Module Type GROUP.
adamc@235:   Parameter G : Set.
adamc@235:   Parameter f : G -> G -> G.
adamc@235:   Parameter e : G.
adamc@235:   Parameter i : G -> G.
adamc@235: 
adamc@235:   Axiom assoc : forall a b c, f (f a b) c = f a (f b c).
adamc@235:   Axiom ident : forall a, f e a = a.
adamc@235:   Axiom inverse : forall a, f (i a) a = e.
adamc@235: End GROUP.
adamc@235: 
adamc@235: Module Type GROUP_THEOREMS.
adamc@235:   Declare Module M : GROUP.
adamc@235: 
adamc@235:   Axiom ident' : forall a, M.f a M.e = a.
adamc@235: 
adamc@235:   Axiom inverse' : forall a, M.f a (M.i a) = M.e.
adamc@235: 
adamc@235:   Axiom unique_ident : forall e', (forall a, M.f e' a = a) -> e' = M.e.
adamc@235: End GROUP_THEOREMS.
adamc@235: 
adamc@235: Module Group (M : GROUP) : GROUP_THEOREMS.
adamc@235:   Module M := M.
adamc@235: 
adamc@235:   Import M.
adamc@235: 
adamc@235:   Theorem inverse' : forall a, f a (i a) = e.
adamc@235:     intro.
adamc@235:     rewrite <- (ident (f a (i a))).
adamc@235:     rewrite <- (inverse (f a (i a))) at 1.
adamc@235:     rewrite assoc.
adamc@235:     rewrite assoc.
adamc@235:     rewrite <- (assoc (i a) a (i a)).
adamc@235:     rewrite inverse.
adamc@235:     rewrite ident.
adamc@235:     apply inverse.
adamc@235:   Qed.
adamc@235: 
adamc@235:   Theorem ident' : forall a, f a e = a.
adamc@235:     intro.
adamc@235:     rewrite <- (inverse a).
adamc@235:     rewrite <- assoc.
adamc@235:     rewrite inverse'.
adamc@235:     apply ident.
adamc@235:   Qed.
adamc@235: 
adamc@235:   Theorem unique_ident : forall e', (forall a, M.f e' a = a) -> e' = M.e.
adamc@235:     intros.
adamc@235:     rewrite <- (H e).
adamc@235:     symmetry.
adamc@235:     apply ident'.
adamc@235:   Qed.
adamc@235: End Group.