diff options
author | msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2010-02-11 20:24:10 +0000 |
---|---|---|
committer | msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2010-02-11 20:24:10 +0000 |
commit | 3b5e12a2eb98b34cacc1850f63b702dfea26cd57 (patch) | |
tree | 6807efbe77888bdc235b794208b4c9a1942e0a17 /theories/Classes | |
parent | 7db851616eabbb82ce3608bb3b05c041b5ac3cb3 (diff) |
Cleanup in Classes, removing unsupported code.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12748 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/Classes')
-rw-r--r-- | theories/Classes/Functions.v | 43 | ||||
-rw-r--r-- | theories/Classes/SetoidAxioms.v | 36 | ||||
-rw-r--r-- | theories/Classes/SetoidClass.v | 1 | ||||
-rw-r--r-- | theories/Classes/vo.itarget | 2 |
4 files changed, 0 insertions, 82 deletions
diff --git a/theories/Classes/Functions.v b/theories/Classes/Functions.v deleted file mode 100644 index 5efa4fa8f..000000000 --- a/theories/Classes/Functions.v +++ /dev/null @@ -1,43 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(************************************************************************) - -(** * Functional morphisms. - - Author: Matthieu Sozeau - Institution: LRI, CNRS UMR 8623 - University Paris Sud -*) - -(* $Id$ *) - -Require Import Coq.Classes.RelationClasses. -Require Import Coq.Classes.Morphisms. - -Generalizable Variables A B eqA eqB RA RB f. - -Set Implicit Arguments. -Unset Strict Implicit. - -Class Injective `(m : Proper (A -> B) (RA ++> RB) f) : Prop := - injective : forall x y : A, RB (f x) (f y) -> RA x y. - -Class Surjective `(m : Proper (A -> B) (RA ++> RB) f) : Prop := - surjective : forall y, exists x : A, RB y (f x). - -Definition Bijective `(m : Proper (A -> B) (RA ++> RB) (f : A -> B)) := - Injective m /\ Surjective m. - -Class MonoMorphism `(m : Proper (A -> B) (eqA ++> eqB)) := - monic :> Injective m. - -Class EpiMorphism `(m : Proper (A -> B) (eqA ++> eqB)) := - epic :> Surjective m. - -Class IsoMorphism `(m : Proper (A -> B) (eqA ++> eqB)) := - { monomorphism :> MonoMorphism m ; epimorphism :> EpiMorphism m }. - -Class AutoMorphism `(m : Proper (A -> A) (eqA ++> eqA)) {I : IsoMorphism m}. diff --git a/theories/Classes/SetoidAxioms.v b/theories/Classes/SetoidAxioms.v deleted file mode 100644 index 3789bb66f..000000000 --- a/theories/Classes/SetoidAxioms.v +++ /dev/null @@ -1,36 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(************************************************************************) - -(** * Extensionality axioms that can be used when reasoning with setoids. - - Author: Matthieu Sozeau - Institution: LRI, CNRS UMR 8623 - University Paris Sud -*) - -(* $Id$ *) - -Require Import Coq.Program.Program. - -Set Implicit Arguments. -Unset Strict Implicit. - -Generalizable Variables a. - -Require Export Coq.Classes.SetoidClass. - -(** Application of the extensionality axiom to turn a goal on - Leibniz equality to a setoid equivalence (use with care!). *) - -Axiom setoideq_eq : forall `{sa : Setoid a} (x y : a), x == y -> x = y. - -(** Application of the extensionality principle for setoids. *) - -Ltac setoid_extensionality := - match goal with - [ |- @eq ?A ?X ?Y ] => apply (setoideq_eq (a:=A) (x:=X) (y:=Y)) - end. diff --git a/theories/Classes/SetoidClass.v b/theories/Classes/SetoidClass.v index df1c0f757..c41c57698 100644 --- a/theories/Classes/SetoidClass.v +++ b/theories/Classes/SetoidClass.v @@ -24,7 +24,6 @@ Require Import Coq.Program.Program. Require Import Relation_Definitions. Require Export Coq.Classes.RelationClasses. Require Export Coq.Classes.Morphisms. -Require Import Coq.Classes.Functions. (** A setoid wraps an equivalence. *) diff --git a/theories/Classes/vo.itarget b/theories/Classes/vo.itarget index fcd3a77df..9daf133b4 100644 --- a/theories/Classes/vo.itarget +++ b/theories/Classes/vo.itarget @@ -1,12 +1,10 @@ Equivalence.vo EquivDec.vo -Functions.vo Init.vo Morphisms_Prop.vo Morphisms_Relations.vo Morphisms.vo RelationClasses.vo -SetoidAxioms.vo SetoidClass.vo SetoidDec.vo SetoidTactics.vo |