Subalgebras
(* Definition of Subalgebras of a given algebra. *)
(* Venanzio Capretta, January 1999 *)
(* Coq version 6.2.3 *)
Require Export Algebras.
Implicit Arguments On.
Section Subalgebra_Definition.
Variable sigma : Signature.
Variable A : (Algebra sigma).
Local n := (sorts_num sigma).
Local m := (fun_num sigma).
Local fs := (function_types sigma).
Local As := (sorts A).
Local Afs := (functions A).
(* A subalgebra consists first of all of a family of subsetoids
of the sorts of A.
*)
Variable P : (i : (Finite n))(Setoid_predicate (As i)).
Local Bs : (Sorts_interpretation n) :=
[i:(Finite n)](subsetoid (P i)).
(* Now let us assume that we have an algebra with sorts Bs,
i. e. we have an interpretation of the functions for sorts Bs.
*)
Variable Bfs : (Function_list_interpretation Bs fs).
(* Thus we have a new algebra. *)
Local B : (Algebra sigma) := (algebra Bfs).
(* For B to be a subalgebra of A it is necessary that the functions of
B are restrictions of those of A. This is defined in the following.
*)
Section Function_Restriction.
Variable i : (Finite m). (* we choose the i-th function *)
Local fi := (nth_function i).
Local h := (nth_result i).
(* We now considere the interpretations of fi in A and B,
in the form of functions with functional arguments.
*)
Local giA := (functions A i).
Local giB := (functions B i).
(* Now we have to require that giA and giB behave in the same way
on arguments coming from B.
*)
Definition
giB_restriction_of_giA :=
(args : (Fun_arg_arguments B i))
(s_inj (giB args)) [=] (giA ([j](s_inj (args j)))).
End Function_Restriction.
(* We now must require that every function of B is the restriction
of the corresponding function of A.
*)
Definition
is_Subalgebra := (i : (Finite m))(giB_restriction_of_giA i).
(* In general we will construct the subalgebra B by just proving that
Bs is closed under the functions of A.
*)
Section Closure_Under_Functions.
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
function_closure :=
(args : (Fun_arg_arguments A i))
((j : (Finite h))((P (a j)) (args j)))
-> ((P r) (fiA args)).
End Closure_Under_Functions.
Definition
Fun_closure :=
(i : (Finite m))(function_closure i).
(* Let us then suppose that Bs is closed under the functions. *)
Variable B_closed : Fun_closure.
(* We then define the subalgebra with sorts Bs and functions the restrictions
of the functions of A.
*)
Section Function_Interpretation.
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).
Definition
fiB_fun : ((j : (Finite h))(Bs (a j))) -> (Bs r) :=
[args]
(exist (As r) (P r)
(fiA [j:(Finite h)](proj1_sig ? ? (args j)))
(!B_closed i
[j:(Finite h)](proj1_sig (As (a j)) (P (a j)) (args j))
[j:(Finite h)](proj2_sig (As (nth_arg j))
(P (nth_arg j))
(args j)
)
)
).
Remark fiB_fun_well_defined :
(fun_well_defined 1!(FF_setoid h [j:(Finite h)](Bs (a j)))
fiB_fun).
Definition
subalgebra_functions : (Function_type_interpretation Bs fi) :=
(setoid_function fiB_fun_well_defined).
End Function_Interpretation.
Definition
Subalgebra : (Algebra sigma) :=
(algebra subalgebra_functions).
End Subalgebra_Definition.
(* We still have to prove that Subalgebra is a subalgebra. *)
Section Subalgebra_Is_Subalgebra.
Variable sigma : Signature.
Local n := (sorts_num sigma).
Variable A : (Algebra sigma).
Local As := (sorts A).
Variable P : (i:(Finite n))(Setoid_predicate (As i)).
Variable P_closed : (Fun_closure P).
Local B := (Subalgebra P_closed).
Lemma
subalgebra_is_subalgebra :
(is_Subalgebra (functions B)).
End Subalgebra_Is_Subalgebra.
Implicit Arguments Off.
25/02/99, 14:36