annotate src/Axioms.v @ 187:71c076dd5f31
Close to automated ccExp_correct
| author |
Adam Chlipala <adamc@hcoop.net> |
| date |
Mon, 17 Nov 2008 10:22:40 -0500 |
| parents |
7fd470d8a788 |
| children |
094bd1e353dd |
| rev |
line source |
|
adamc@125
|
1 (* Copyright (c) 2008, Adam Chlipala
|
|
adamc@125
|
2 *
|
|
adamc@125
|
3 * This work is licensed under a
|
|
adamc@125
|
4 * Creative Commons Attribution-Noncommercial-No Derivative Works 3.0
|
|
adamc@125
|
5 * Unported License.
|
|
adamc@125
|
6 * The license text is available at:
|
|
adamc@125
|
7 * http://creativecommons.org/licenses/by-nc-nd/3.0/
|
|
adamc@125
|
8 *)
|
|
adamc@125
|
9
|
|
adamc@125
|
10 (* Additional axioms not in the Coq standard library *)
|
|
adamc@125
|
11
|
|
adamc@173
|
12 Set Implicit Arguments.
|
|
adamc@173
|
13
|
|
adamc@125
|
14 Axiom ext_eq : forall (A : Type) (B : A -> Type)
|
|
adamc@125
|
15 (f g : forall x, B x),
|
|
adamc@125
|
16 (forall x, f x = g x)
|
|
adamc@125
|
17 -> f = g.
|
|
adamc@125
|
18
|
|
adamc@173
|
19 Theorem ext_eq_Set : forall (A : Set) (B : A -> Set)
|
|
adamc@173
|
20 (f g : forall x, B x),
|
|
adamc@173
|
21 (forall x, f x = g x)
|
|
adamc@173
|
22 -> f = g.
|
|
adamc@173
|
23 intros.
|
|
adamc@173
|
24 rewrite (ext_eq _ _ _ H); reflexivity.
|
|
adamc@173
|
25 Qed.
|
|
adamc@173
|
26
|
|
adamc@173
|
27 Theorem ext_eq_forall : forall (A : Type)
|
|
adamc@173
|
28 (f g : A -> Set),
|
|
adamc@173
|
29 (forall x, f x = g x)
|
|
adamc@173
|
30 -> @eq Type (forall x, f x) (forall x, g x).
|
|
adamc@173
|
31 intros.
|
|
adamc@173
|
32 rewrite (ext_eq _ _ _ H); trivial.
|
|
adamc@173
|
33 Qed.
|
|
adamc@173
|
34
|
|
adamc@173
|
35 Ltac ext_eq := (apply ext_eq || apply ext_eq_Set
|
|
adamc@173
|
36 || apply ext_eq_forall); intro.
|
