Mercurial > cpdt > repo
comparison src/Axioms.v @ 173:7fd470d8a788
System F
author | Adam Chlipala <adamc@hcoop.net> |
---|---|
date | Sun, 09 Nov 2008 15:15:41 -0500 |
parents | 8a548a6c7074 |
children | 094bd1e353dd |
comparison
equal
deleted
inserted
replaced
172:653c03f6061e | 173:7fd470d8a788 |
---|---|
7 * http://creativecommons.org/licenses/by-nc-nd/3.0/ | 7 * http://creativecommons.org/licenses/by-nc-nd/3.0/ |
8 *) | 8 *) |
9 | 9 |
10 (* Additional axioms not in the Coq standard library *) | 10 (* Additional axioms not in the Coq standard library *) |
11 | 11 |
12 Set Implicit Arguments. | |
13 | |
12 Axiom ext_eq : forall (A : Type) (B : A -> Type) | 14 Axiom ext_eq : forall (A : Type) (B : A -> Type) |
13 (f g : forall x, B x), | 15 (f g : forall x, B x), |
14 (forall x, f x = g x) | 16 (forall x, f x = g x) |
15 -> f = g. | 17 -> f = g. |
16 | 18 |
17 Ltac ext_eq := apply ext_eq; intro. | 19 Theorem ext_eq_Set : forall (A : Set) (B : A -> Set) |
20 (f g : forall x, B x), | |
21 (forall x, f x = g x) | |
22 -> f = g. | |
23 intros. | |
24 rewrite (ext_eq _ _ _ H); reflexivity. | |
25 Qed. | |
26 | |
27 Theorem ext_eq_forall : forall (A : Type) | |
28 (f g : A -> Set), | |
29 (forall x, f x = g x) | |
30 -> @eq Type (forall x, f x) (forall x, g x). | |
31 intros. | |
32 rewrite (ext_eq _ _ _ H); trivial. | |
33 Qed. | |
34 | |
35 Ltac ext_eq := (apply ext_eq || apply ext_eq_Set | |
36 || apply ext_eq_forall); intro. |