summaryrefslogtreecommitdiff
path: root/theories/Classes/SetoidAxioms.v
diff options
context:
space:
mode:
authorGravatar Samuel Mimram <smimram@debian.org>2008-07-25 15:12:53 +0200
committerGravatar Samuel Mimram <smimram@debian.org>2008-07-25 15:12:53 +0200
commita0cfa4f118023d35b767a999d5a2ac4b082857b4 (patch)
treedabcac548e299fee1da464c93b3dba98484f45b1 /theories/Classes/SetoidAxioms.v
parent2281410e38ef99d025ea77194585a9bc019fdaa9 (diff)
Imported Upstream version 8.2~beta3+dfsgupstream/8.2.beta3+dfsg
Diffstat (limited to 'theories/Classes/SetoidAxioms.v')
-rw-r--r--theories/Classes/SetoidAxioms.v35
1 files changed, 35 insertions, 0 deletions
diff --git a/theories/Classes/SetoidAxioms.v b/theories/Classes/SetoidAxioms.v
new file mode 100644
index 00000000..9264b6d2
--- /dev/null
+++ b/theories/Classes/SetoidAxioms.v
@@ -0,0 +1,35 @@
+(* -*- coq-prog-args: ("-emacs-U" "-nois") -*- *)
+(************************************************************************)
+(* 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 - UniversitÃcopyright Paris Sud
+ * 91405 Orsay, France *)
+
+(* $Id: SetoidAxioms.v 10739 2008-04-01 14:45:20Z herbelin $ *)
+
+Require Import Coq.Program.Program.
+
+Set Implicit Arguments.
+Unset Strict Implicit.
+
+Require Export Coq.Classes.SetoidClass.
+
+(* Application of the extensionality axiom to turn a goal on leibinz equality to
+ a setoid equivalence. *)
+
+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.