Mercurial > cpdt > repo

comparison src/Large.v @ 239:a3f0cdcb09c3

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
More maint & debug code
author Adam Chlipala <adamc@hcoop.net>
date Mon, 07 Dec 2009 16:42:42 -0500
parents 0a2146dafa8e
children b28c6e6eca0c
comparison
equal deleted inserted replaced
238:0a2146dafa8e 239:a3f0cdcb09c3
399 | None => _ end] ] => 399 | None => _ end] ] =>
400 dep_destruct E 400 dep_destruct E
401 end; crush). 401 end; crush).
402 Qed. 402 Qed.
403 403
404 Section slow.
405 Hint Resolve trans_eq.
406
407 Variable A : Set.
408 Variables P Q R S : A -> A -> Prop.
409 Variable f : A -> A.
410
411 Hypothesis H1 : forall x y, P x y -> Q x y -> R x y -> f x = f y.
412 Hypothesis H2 : forall x y, S x y -> R x y.
413
414 Lemma slow : forall x y, P x y -> Q x y -> S x y -> f x = f y.
415 debug eauto.
416 Qed.
417
418 Hypothesis H3 : forall x y, x = y -> f x = f y.
419
420 Lemma slow' : forall x y, P x y -> Q x y -> S x y -> f x = f y.
421 debug eauto.
422 Qed.
423 End slow.
424
404 425
405 (** * Modules *) 426 (** * Modules *)
406 427
407 Module Type GROUP. 428 Module Type GROUP.
408 Parameter G : Set. 429 Parameter G : Set.
423 Axiom inverse' : forall a, M.f a (M.i a) = M.e. 444 Axiom inverse' : forall a, M.f a (M.i a) = M.e.
424 445
425 Axiom unique_ident : forall e', (forall a, M.f e' a = a) -> e' = M.e. 446 Axiom unique_ident : forall e', (forall a, M.f e' a = a) -> e' = M.e.
426 End GROUP_THEOREMS. 447 End GROUP_THEOREMS.
427 448
428 Module Group (M : GROUP) : GROUP_THEOREMS. 449 Module Group (M : GROUP) : GROUP_THEOREMS with Module M := M.
429 Module M := M. 450 Module M := M.
430 451
431 Import M. 452 Import M.
432 453
433 Theorem inverse' : forall a, f a (i a) = e. 454 Theorem inverse' : forall a, f a (i a) = e.
455 rewrite <- (H e). 476 rewrite <- (H e).
456 symmetry. 477 symmetry.
457 apply ident'. 478 apply ident'.
458 Qed. 479 Qed.
459 End Group. 480 End Group.
481
482 Require Import ZArith.
483 Open Scope Z_scope.
484
485 Module Int.
486 Definition G := Z.
487 Definition f x y := x + y.
488 Definition e := 0.
489 Definition i x := -x.
490
491 Theorem assoc : forall a b c, f (f a b) c = f a (f b c).
492 unfold f; crush.
493 Qed.
494 Theorem ident : forall a, f e a = a.
495 unfold f, e; crush.
496 Qed.
497 Theorem inverse : forall a, f (i a) a = e.
498 unfold f, i, e; crush.
499 Qed.
500 End Int.
501
502 Module IntTheorems := Group(Int).
503
504 Check IntTheorems.unique_ident.
505
506 Theorem unique_ident : forall e', (forall a, e' + a = a) -> e' = 0.
507 exact IntTheorems.unique_ident.
508 Qed.