Term Evaluation

(* Term evalutation for closed terms. *)
(* Venanzio Capretta, January 1999    *)
(* Coq version 6.2.3                  *)

Require Export Term_Algebras.
Require Export Homomorphisms.

Implicit Arguments On.

Section Term_Algebras_Evaluation.

Variable sigma : Signature.

Variable A : (Algebra sigma).
Local T : (Algebra sigma) := (Term_algebra sigma).

Local As := (sorts A).
Local Ts := (sorts T).

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

Section Function_Evaluation.

Variable i : (Finite m).
Local fi := (nth_function i).
Local r := (nth_result i).

Variable args : (Fun_arg_arguments T i).
Local fiT := (functions T i).

(* The term obtained by applying the function i to the arguments args. *)
Local t : (Ts r) := (fiT args).

(* We assume that the argument function on A corresponding to args    has already been defined recursively. *)
Variable args' : (Fun_arg_arguments A i).
Local fiA := (functions A i).

(* So the evaluation of t is just given by applying the interpretation    of the function symbol i in A to args'. *)
Definition t_evaluation : (As r) := (fiA args').

End Function_Evaluation.

Fixpoint term_evaluation [s : (Finite n); t : (Ts s)] : (As s) :=
<[s:(Finite n); t:(Ts s)](s_el (As s))>
Cases t of
  (g_tree i args) => (t_evaluation [x:(Finite (nth_arity i))]
                                   (term_evaluation (args x)))
end.

(* Term_evaluation is a family of setoid functions. *)

(* We prove that it is well defined by induction on the proof of    equality for terms.    The equality relation has two constructors tree_eq_intro and    tree_eq_trans. We consider separately the two cases. *)

Section Term_Evaluation_Well_Defined_Intro.

Variable i : (Finite m).

Local fi := (nth_function i) : (Function_type n).
Local r := (nth_arity i) : nat.
Local a := (nth_arg 2!i) : (Finite r) -> (Finite n).
Local h := (nth_result i) : (Finite n).

Variables args1, args2 : (Fun_arg_arguments T i).
Variable arg_eq : (j : (Finite r)) (args1 j) [=] (args2 j).

Local args1' : (Fun_arg_arguments A i)
             := [j](term_evaluation (args1 j)).
Local args2' : (Fun_arg_arguments A i)
             := [j](term_evaluation (args2 j)).

(* Now the induction hypothesis. *)
Variable ev_args_eq :
  (j : (Finite r)) (args1' j) [=] (args2' j).

(* First of all we prove that the argument functions obtained by applying    term_evaluation to args1 and args2 are equal. *)

Remark ev_args_setoid_eq : args1' [=] args2'.

(* Now the term obtained by an application of fi are also equal. *)

Local fiA := (functions A i)
          : (Fun_arg_function r (Function_arguments_sorts A 3!i) (As h)).
Local a1 : (As h) := (fiA args1').
Local a2 : (As h) := (fiA args2').

Remark fi_args_eq : a1 [=] a2.

Local fiT := (functions T i)
          : (Fun_arg_function r (Function_arguments_sorts T 3!i) (Ts h)).
Local t1 := (fiT args1).
Local t2 := (fiT args2).

(* Since a1 is equal to the interpretation of t1 and a2 is equal    to the interpretation of t2 we have the desire equality. *)

Lemma ev_app_eq : (term_evaluation t1) [=] (term_evaluation t2).

End Term_Evaluation_Well_Defined_Intro.

Lemma term_evaluation_well_defined :
  (s : (Finite n))(fun_well_defined (term_evaluation 1!s)).

Definition term_ev_setoid : (s : (Finite n))(S_Fun (Ts s) (As s)) :=
  [s : (Finite n)](setoid_function (term_evaluation_well_defined 1!s)).

(* Now we have to prove that term_evaluation is a homomorphism. *)

Section Term_Evaluation_is_Homomorphism.

Variable i : (Finite m).

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

Local fiT := (functions T i).
Local fiA := (functions A i).

Variable args : (Fun_arg_arguments T i).

Local ev_args : (Fun_arg_arguments A i)
                 := [j](term_evaluation (args j)).
Local fi_args : (Ts h)
                 := (fiT args).
Local fi_ev_args : (As h)
                 := (fiA ev_args).
Local ev_fi_args : (As h)
                 := (term_evaluation fi_args).

(* We want to prove that fi_ev_args is equal to ev_fi_args. *)

Lemma term_evaluation_commutes_with_functions :
  fi_ev_args [=] ev_fi_args.

End Term_Evaluation_is_Homomorphism.

Lemma term_evaluation_is_homomorphism :
  (Is_homomorphism 2!T 3!A term_ev_setoid).

Definition term_ev : (Homomorphism T A) :=
  (homomorphism term_evaluation_is_homomorphism).

End Term_Algebras_Evaluation.

Implicit Arguments Off.

25/02/99, 14:36