Expressions Evaluation

(* EXPRESSIONS EVALUATION           *)
(* Venanzio Capretta, January 1999  *)
(* Coq version 6.2.3                *)

(* Evaluation of (open) expressions. It is similar to term evaluation    for closed terms, but requires an extra parameter for the evaluation    of variables. *)

Require Export Expressions_Algebras.
Require Export Homomorphisms.

Implicit Arguments On.

Section Expressions_Algebras_Evaluation.

Variable sigma : Signature.

Variable A : (Algebra sigma).
Local E : (Algebra sigma) := (Expressions_algebra sigma).

Local As := (sorts A).
Local Es := (sorts E).

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

(* Definition of variable assignment. *)
Definition Assignment := (v : (Var sigma))(As (Fst v)).

Variable ass : Assignment.

Section Function_Evaluation.

Variable i : (Finite m).

Local fi := (nth_function i).
Local r := (nth_result i).

Variable args : (Fun_arg_arguments E i).

Local fiE := (functions E i).

(* The expression obtained by applying the i-th function to args. *)
Local e : (Es r) := (fiE args).

(* We assume that the evaluation of the arguments args have already    been define and we define recursively the evaluation of e. *)
Variable args' : (Fun_arg_arguments A i).

Local fiA := (functions A i).

Definition e_evaluation : (As r) := (fiA args').

End Function_Evaluation.

Definition expression_evaluation : (s:(Finite n))(Es s)->(As s).

(* expression_evaluation is a family of setoid functions. *)
(* We prove that it is well defined by induction on the proof of    equality of expressions.    The equality relation has two constructors tree_eq_intro and    tree_eq_trans. We consider separately the two cases. *)

Section Expression_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 E i).
Variable arg_eq : (j : (Finite r)) (args1 j) [=] (args2 j).

Local args1' : (Fun_arg_arguments A i)
             := [j](expression_evaluation (args1 j)).
Local args2' : (Fun_arg_arguments A i)
             := [j](expression_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    expression_evaluation to args1 and args2 are equal. *)

Remark ev_args_setoid_eq : args1' [=] args2'.

(* Now the expression 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 E i)
          : (Fun_arg_function r (Function_arguments_sorts E 3!i) (Es 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 : (expression_evaluation t1) [=] (expression_evaluation t2).

End Expression_Evaluation_Well_Defined_Intro.

Lemma expression_evaluation_well_defined :
  (s : (Finite n))(fun_well_defined (expression_evaluation 1!s)).

Definition expression_ev_setoid : (s : (Finite n))(S_Fun (Es s) (As s)) :=
  [s : (Finite n)](setoid_function (expression_evaluation_well_defined 1!s)).

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

Section Expression_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 E i).
Local fiA := (functions A i).

Variable args : (Fun_arg_arguments E i).

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

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

Lemma expression_evaluation_commutes_with_functions :
  fi_ev_args [=] ev_fi_args.

End Expression_Evaluation_is_Homomorphism.

Lemma expression_evaluation_is_homomorphism :
  (Is_homomorphism 2!E 3!A expression_ev_setoid).

Definition expression_ev : (Homomorphism E A) :=
  (homomorphism expression_evaluation_is_homomorphism).

End Expressions_Algebras_Evaluation.

25/02/99, 14:36