Mercurial > cpdt > repo

comparison src/Axioms.v @ 173:7fd470d8a788

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
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.