1
(************************************************************************)
2
(* v * The Coq Proof Assistant / The Coq Development Team *)
3
(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
4
(* \VV/ **************************************************************)
5
(* // * This file is distributed under the terms of the *)
6
(* * GNU Lesser General Public License Version 2.1 *)
7
(************************************************************************)
9
(* Extensionality axioms that can be used when reasoning with setoids.
11
* Author: Matthieu Sozeau
12
* Institution: LRI, CNRS UMR 8623 - UniversitÃcopyright Paris Sud
13
* 91405 Orsay, France *)
15
(* $Id: SetoidAxioms.v 12083 2009-04-14 07:22:18Z herbelin $ *)
17
Require Import Coq.Program.Program.
19
Set Implicit Arguments.
20
Unset Strict Implicit.
22
Require Export Coq.Classes.SetoidClass.
24
(* Application of the extensionality axiom to turn a goal on
25
Leibniz equality to a setoid equivalence (use with care!). *)
27
Axiom setoideq_eq : forall `{sa : Setoid a} (x y : a), x == y -> x = y.
29
(** Application of the extensionality principle for setoids. *)
31
Ltac setoid_extensionality :=
33
[ |- @eq ?A ?X ?Y ] => apply (setoideq_eq (a:=A) (x:=X) (y:=Y))