Mercurial > cpdt > repo

annotate src/Axioms.v @ 190:094bd1e353dd

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Import predicative Impure example
author Adam Chlipala <adamc@hcoop.net>
date Tue, 18 Nov 2008 12:44:46 -0500
parents 7fd470d8a788
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.