Mercurial > cpdt > repo
annotate src/Axioms.v @ 220:15501145d696
Ported Match
author | Adam Chlipala <adamc@hcoop.net> |
---|---|
date | Mon, 16 Nov 2009 10:32:04 -0500 |
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. |