(************************************************************************)
(*  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        *)
(************************************************************************)

(** * Order Theory with Classes.

   Definitions of operations and standard properties on them.

   Author: Matthieu Sozeau <sozeau@lri.fr>
   Institution: LRI, CNRS UMR 8623 - Université Paris Sud
                91405 Orsay, France 

*)

Require Import Equivalence.
Require Import Setoid.

Open Local Scope equiv_scope.

Fixpoint nary_operation n A : Type := 
  match n with
    | 0 => A
    | S n' => A -> nary_operation n' A
  end.

Definition unary_operation := nary_operation 1.
Definition binary_operation := nary_operation 2.
Definition ternary_operation := nary_operation 3.

(** We define properties of [operation]s up-to an arbitrary setoid equality on the carrier.
   Note how we generalize statements to avoid implicit use of the leibniz equality. *)


Definition associative `{equ : Equivalence A} (op : binary_operation A) := 
  forall x₁ x₂ x₃, op x₁ (op x₂ x₃) === op (op x₁ x₂) x₃.

Definition commutative `{equ : Equivalence A} (op : binary_operation A) := 
  forall x₁ x₂, op x₁ x₂ === op x₂ x₁.

Definition idempotent `{equ : Equivalence A} (op : binary_operation A) := 
  forall x, op x x === x.

Definition neutral `{equ : Equivalence A} (op : binary_operation A) (e : A) := 
  forall x, op e x === x.

Definition injective `{equA : Equivalence A} `{equB : Equivalence B}
                     (f : A -> B) :=
  forall x₁ x₂, f x₁ === f x₂ -> x₁ === x₂.

Definition surjective A `{Equivalence B} (f : A -> B) :=
  forall y, exists x, f x === y.