annotate src/Axioms.v @ 278:e7ed2fddd29a
Some improvements to installation instructions, based on Mitch Wand's feedback
author |
Adam Chlipala <adam@chlipala.net> |
date |
Fri, 01 Oct 2010 13:39:05 -0400 |
parents |
094bd1e353dd |
children |
|
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.
|
adamc@190
|
37
|
adamc@190
|
38
|
adamc@190
|
39 Theorem eta : forall (A B : Type) (f : A -> B),
|
adamc@190
|
40 (fun x => f x) = f.
|
adamc@190
|
41 intros; ext_eq; trivial.
|
adamc@190
|
42 Qed.
|