# Library CoLoR.Term.Lambda.LCall

CoLoR, a Coq library on rewriting and termination.
See the COPYRIGHTS and LICENSE files.

- Frederic Blanqui, 2013-08-16

# Function calls

We assume given a set F for function symbols and a set X for
variables.

Variables F X : Type.

Notation Te := (@Te F X).

Notation Var := (@Var F X).

Notation Fun := (@Fun F X).

Notation Tes := (vector Te).

A call is made of a function symbol f and a vector of terms.

We assume given a set So of type constants.

We assume given a type for each function symbol.

A max_call is a call mk_call f ts with ts of length
arity (typ f), that is, the maximum number of arguments that
f can take.

Record max_call : Type := build_max_call {

max_call_call :> call;

max_call_eq :

call_nb_args max_call_call = arity (typ (call_fun max_call_call)) }.

Definition mk_max_call f (ts : TypArgs f) :=

build_max_call (mk_call f ts) Logic.eq_refl.

Parameters for alpha-equivalence.

Variables (eq_fun_dec : forall x y : F, {x=y}+{~x=y})

(eq_var_dec : forall x y : X, {x=y}+{~x=y})

(ens_X : Ens X) (var_notin : Ens_type ens_X -> X).

Notation aeq := (@aeq F X eq_fun_dec eq_var_dec ens_X var_notin).

Notation clos_vaeq :=

(@clos_vaeq F X eq_fun_dec eq_var_dec ens_X var_notin).

Extension of alpha-equivalence to calls.

Inductive caeq : relation call :=

| caeq_intro : forall f n (ts us : Tes n),

Vforall2 aeq ts us -> caeq (mk_call f ts) (mk_call f us).

Definition mcaeq : relation max_call := caeq.

Inductive gt_red R : relation call :=

| gt_red_intro : forall f n (ts us : Tes n),

restrict (SN (clos_vaeq R)) (clos_vaeq R) ts us ->

gt_red R (mk_call f ts) (mk_call f us).

# Dependant lexicographic quasi-ordering on calls.

- to use, for each equivalence class modulo =F, a filter, that is, a
vector of natural numbers of fixed length indicating which arguments
should be taken into account in the comparisons;
- to replace each missing argument by some new constant and compare arguments by using the option extension opt of a relation.

For each code, we assume given a filter, that is, a vector of
natural numbers indicating which arguments (the 1st argument is
denoted by 0, etc.) have to be taken into account when
comparing two function calls.

We define the ordering on calls by first comparing the codes
of function symbols and then the arguments. For typing reasons,
we also use the type call for arguments. To this end, we
reuse the Coq standard library lexprod and inverse the
relations using transp (because, for wellfoundedness, CoLoR
and Coq relations are oriented differently).

Definition gt_call (gt_args : C -> relation call) : relation call :=

Rof (transp (lexprod (transp gtC) (fun r => transp (gt_args r))))

(fun c => @existT _ _ (code (call_fun c)) c).

Finally, we define a lexicographic ordering on arguments.
Given a code r, gt_args_lex r compares two calls mk_call f
ts and mk_call g us by filtering ts and us with
Vopt_filter (filter r) and comparing lexicographically the
resulting vectors.
To compare filtered arguments, we use the
Finally, note that, in this definition, r does not need to be a
code for f and g. We do this since, for typing reasons, we
cannot define a relation on vectors of different lengths.

*irreflexive*relation opt, with which the value None used for missing arguments is comparable to no value and thus not to itself. It is important to do so because, otherwise, we could get problems when comparing partial function calls with non sorted filters. For instance, with filter r = Vcons 2 (Vcons 1 Vnil), we could have mk_call f (Vcons t1 Vnil) > mk_call f (Vcons u1 Vnil) since Vcons None (Vcons (Some t1) Vnil) > Vcons None (Vcons (Some u1) Vnil), and mk_call f (Vcons t1 (Vcons t2 Vnil)) < mk_call f (Vcons u1 (Vcons u2 Vnil)) since Vcons (Some t2) (Vcons (Some t1) Vnil) < Vcons (Some u2) (Vcons (Some u1) Vnil). But the opposite is necessary since a decrease in the computability closure must imply a decrease in the induction ordering on maximally applied function calls used in the termination proof (see LCompClos). Said otherwise, the ordering on function calls must be invariant when adding arguments, that is compatible with the definition of computability: if t is computable then, for all computable term u, App t u is computable. Using opt makes Vcons None (Vcons (Some t1) Vnil) > Vcons None (Vcons (Some u1) Vnil) impossible, and thus gt_args_lex compatible with computability.Definition gt_args_lex (gt : relation Te) r : relation call := Rof

(lexv (opt aeq) (opt gt))

(fun c => Vopt_filter (filter r) (call_args c)).

End call.

End Def.

We assume given a type C of codes for function symbols (two
symbols having the same code can be considered as equivalent).

We assume given a wellfounded relation >C on codes.

For each code, we assume given a filter, that is, a vector of
natural numbers indicating which arguments have to be taken into
account when comparing two function calls.

Notations.

Notation gt_call := (@gt_call F X C code gtC).

Notation gt_args_lex := (@gt_args_lex F X FOrd.eq_dec XOrd.eq_dec ens_X

var_notin C filter_arity filter).

End DLQO_Struct.

Module Make (Export ST : ST_Struct).

Module Export A := LAlpha.Make ST.L.

Notation call := (@call F X).

Notation mk_call := (@mk_call F X).

Notation max_call := (@max_call F X So typ).

Notation max_call_call := (@max_call_call F X So typ).

Notation mk_max_call := (@mk_max_call F X So typ).

Notation build_max_call := (@build_max_call F X So typ).

Notation caeq := (@caeq F X FOrd.eq_dec XOrd.eq_dec ens_X var_notin).

Notation mcaeq := (@mcaeq F X So typ FOrd.eq_dec XOrd.eq_dec ens_X var_notin).

Notation gt_red := (@gt_red F X FOrd.eq_dec XOrd.eq_dec ens_X var_notin).

Inversion lemmas and tactics for caeq.

Lemma caeq_inv : forall f n (ts : Tes n) g p (us : Tes p),

caeq (mk_call f ts) (mk_call g us) -> exists f0 n0 (ts1 us1 : Tes n0),

ts1 ~~~ us1 /\ f0 = f /\ n0 = n /\ existT ts1 = existT ts

/\ f = g /\ n = p /\ existT us1 = existT us.

Ltac inv_caeq r g p :=

let f0 := fresh "f" in let ts1 := fresh "ts" in let us1 := fresh "us" in

let h1 := fresh "h" in let h2 := fresh "h" in let h3 := fresh "h" in

let h4 := fresh "h" in let h5 := fresh "h" in let h6 := fresh "h" in

let h7 := fresh "h" in let n0 := fresh "n" in

destruct (caeq_inv r)

as [f0 [n0 [ts1 [us1 [h1 [h2 [h3 [h4 [h5 [h6 h7]]]]]]]]]];

subst f0 n0 g p;

(apply inj_existT in h4; [subst ts1|exact eq_nat_dec]);

(apply inj_existT in h7; [subst us1|exact eq_nat_dec]).

caeq and mcaeq are equivalence relations.

Properties of mk_call amd mk_max_call.

Instance mk_call_vaeq f n :

Proper (vaeq ==> caeq) (mk_call f (call_nb_args:=n)).

Instance mk_max_call_vaeq f : Proper (vaeq ==> mcaeq) (mk_max_call f).

Lemma mk_call_cast : forall f n (ts : Tes n) p (h : n=p),

mk_call f (Vcast ts h) = mk_call f ts.

Inversion lemma and tactic for gt_red.

Import RelUtil.

Lemma gt_red_inv : forall R f n (ts : Tes n) g p (us : Tes p),

gt_red R (mk_call f ts) (mk_call g us) -> exists f0 n0 (ts1 us1 : Tes n0),

restrict (SN (clos_vaeq R)) (clos_vaeq R) ts1 us1

/\ f0 = f /\ n0 = n /\ existT ts1 = existT ts

/\ f = g /\ n = p /\ existT us1 = existT us.

Ltac inv_gt_red r g p :=

let f0 := fresh "f" in let ts1 := fresh "ts" in let us1 := fresh "us" in

let h1 := fresh "h" in let h2 := fresh "h" in let h3 := fresh "h" in

let h4 := fresh "h" in let h5 := fresh "h" in let h6 := fresh "h" in

let h7 := fresh "h" in let h8 := fresh "h" in let n0 := fresh "n" in

destruct (gt_red_inv r)

as [f0 [n0 [ts1 [us1 [[h1 h2] [h3 [h4 [h5 [h6 [h7 h8]]]]]]]]]];

subst f0 n0 g p;

(apply inj_existT in h5; [subst ts1|exact eq_nat_dec]);

(apply inj_existT in h8; [subst us1|exact eq_nat_dec]).

gt_red is wellfounded.

gt_red is invariant by caeq.

Module Lex (Export CO : DLQO_Struct).

Module Export M := Make CO.ST.

Section gt_call.

Variable gt_args : C -> relation call.

gt_call preserves wellfoundedness.

gt_call preserves compatibility with caeq.

Global Instance gt_call_caeq :

(forall r, Proper (caeq ==> caeq ==> impl) (gt_args r)) ->

Proper (caeq ==> caeq ==> impl) (gt_call gt_args).

End gt_call.

Section gt_args_lex.

Variables (gt : relation Te) (gt_aeq : Proper (aeq ==> aeq ==> impl) gt).

gt_args_lex preserves wellfoundedness.

gt_args_lex preserves compatibility with caeq.

gt_args_lex S r absorbs gt_red R if S is transitive,
compatible with aeq and contains restrict (SN (clos_aeq R))
(clos_aeq R).