Congruences

(* CONGRUENCES AND QUOTIENTS OVER AN ALGEBRA. *)
(* Venanzio Capretta, January 1999            *)
(* Coq version 6.2.3                          *)

Require Export Algebras.

Implicit Arguments On.

Section Algebra_Congruences.

Variable sigma : Signature.
Variable A : (Algebra sigma).

Local n := (sorts_num sigma).
Local m := (fun_num sigma).

Local S := (sorts A).

Variable congr : (s : (Finite n))(Setoid_relation (S s)).

(* We have to require that congr satisfies the substitutivity condition    for every function. *)

Section Substitutivity_Condition.

Variable i : (Finite m).

Local h := (nth_arity i).
Local a := (nth_arg 2!i).
Local r := (nth_result i).

Local fiA := (functions A i).

Definition Substitutivity :=
  (args1, args2 : (Fun_arg_arguments A i))
  ((j : (Finite h))((congr (a j)) (args1 j) (args2 j)))
  -> ((congr r) (fiA args1) (fiA args2)).

End Substitutivity_Condition.

Definition is_Congruence := (i : (Finite m))(Substitutivity i).

End Algebra_Congruences.

(* The type of congruences over an algebra. *)
Record Congruence [sigma : Signature; A : (Algebra sigma)] : Type := congruence
  { cong_relation :> (s : (Finite (sorts_num sigma)))
                       (Setoid_relation (sorts A s));
    cong_equiv : (s : (Finite (sorts_num sigma)))
                       (Equiv (cong_relation s));
    cong_subst : (is_Congruence cong_relation)
  }.

Section Quotients.

Variable sigma : Signature.
Variable A : (Algebra sigma).
Variable cong : (Congruence A).

Local n := (sorts_num sigma).
Local m := (fun_num sigma).

Local As := (sorts A).

Lemma cong_reflexivity : (s : (Finite n))(reflexive (As s) (cong s)).

Lemma cong_symmetry : (s : (Finite n))(symmetric (As s) (cong s)).

Lemma cong_transitivity : (s : (Finite n))(transitive (As s) (cong s)).

Definition quot_sorts : (Sorts_interpretation n) :=
  [i:(Finite n)](setoid (cong_equiv cong i)).

Section Quotient_Functions.

Variable i : (Finite m).

Local fi := (nth_function i).
Local h := (nth_arity i).
Local a := (nth_arg 2!i).

Local r := (nth_result i).

Local fiA := (functions A i).

Local quot_fun_i : (FF_setoid h [j](quot_sorts (a j))) -> (quot_sorts r) :=
  [args](fiA args).

Remark quot_fun_well_defined : (fun_well_defined quot_fun_i).

Definition quot_fun : (Function_type_interpretation quot_sorts fi) :=
  (setoid_function quot_fun_well_defined).

End Quotient_Functions.

Definition quotient : (Algebra sigma) :=
  (algebra quot_fun).

End Quotients.

Implicit Arguments Off.

25/02/99, 14:36