diff options
Diffstat (limited to 'theories/Classes/SetoidAxioms.v')
| -rw-r--r-- | theories/Classes/SetoidAxioms.v | 35 |
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. |