# Library CoLoR.Term.Lambda.LCompClos

CoLoR, a Coq library on rewriting and termination.
• Frederic Blanqui, 2013-05-02

# Computability closure

and proof that it enforces termination of higher-order rewrite systems.
After "Inductive-data-type Systems", F. Blanqui, J.-P. Jouannaud and M. Okada, Theoretical Computer Science 272, p. 41-68, 2002, http://dx.doi.org/10.1016/S0304-3975(00)00347-9.

Set Implicit Arguments.

Module Export Def.

# Abstract definition of the computability closure.

Section cc.

We assume given a set F for function symbols, a set X for variables, and a set So for type constants.

Variables F X : Type.

Notation Te := (@Te F X).
Notation Var := (@Var F X).
Notation Fun := (@Fun F X).
Notation Tes := (vector Te).
Notation call := (@call F X).

Variable So : Type.

Notation Ty := (@Ty So).
Notation Tys := (vector Ty).

We assume given a structure for finite sets on X.

Variable ens_X : Ens X.

Notation In := (Ens_In ens_X).
Notation fvs := (@fvs F X ens_X).

We assume given a set En for typing environments equipped with the following functions:

Variable env : Env X So.

Notation En := (Env_type env).
Notation MapsTo := (Env_MapsTo env).

We assume given a type for each function symbol.

Variable typ : F -> Ty.

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

For each symbol f, we assume given a finite number of accessible arguments.

Variables (Acc : F -> nat -> Prop)
(Acc_arity : forall g i, Acc g i -> i < arity (typ g)).

We assume given an environment-indexed family of relations on calls.

Variable gt1 : En -> relation call.

## Definition of the computability closure for a call mk_callfls.

Section cc_def.

Variables (f : F) (n : nat) (ls : Tes n).

Inductive cc : En -> Te -> Ty -> Prop :=

| cc_arg : forall E i (i1 : i < n) (i2 : i < arity (typ f)),
cc E (Vnth ls i1) (Vnth (inputs (typ f)) i2)

| cc_var : forall E x T,
MapsTo x T E -> ~In x (fvs ls) -> cc E (Var x) T

| cc_app : forall E t u A B,
cc E t (A ~~> B) -> cc E u A -> cc E (App t u) B

| cc_lam : forall E x A v B,
~In x (fvs ls) -> cc (add x A E) v B -> cc E (Lam x v) (A ~~> B)

| cc_acc : forall E g (us : TypArgs g) i (hi : Acc g i),
cc E (apps (Fun g) us) (Base (output_base (typ g))) ->
cc E (Vnth us (Acc_arity hi)) (Vnth (inputs (typ g)) (Acc_arity hi))

| cc_call : forall E g p (us : Tes p),
0+p <= arity (typ g) -> gt1 E (mk_call f ls) (mk_call g us) ->
(forall i (i1 : i < p) (i2 : i < arity (typ g)),
cc E (Vnth us i1) (Vnth (inputs (typ g)) i2)) ->
cc E (apps (Fun g) us) (output (typ g) p).

Variants of cc constructors for proving that some term is in cc.

Lemma cc_arg' E v V i (i1 : i < n) (i2 : i < arity (typ f)) :
v = Vnth ls i1 -> V = Vnth (inputs (typ f)) i2 -> cc E v V.

Lemma cc_acc' E v V g (us : TypArgs g) i (hi : Acc g i) :
cc E (apps (Fun g) us) (Base (output_base (typ g))) ->
v = Vnth us (Acc_arity hi) ->
V = Vnth (inputs (typ g)) (Acc_arity hi) -> cc E v V.

Lemma cc_call' E v V g p (us : Tes p) :
0+p <= arity (typ g) -> gt1 E (mk_call f ls) (mk_call g us) ->
(forall i (i1 : i < p) (i2 : i < arity (typ g)),
cc E (Vnth us i1) (Vnth (inputs (typ g)) i2)) ->
v = apps (Fun g) us -> V = output (typ g) p -> cc E v V.

Inversion lemma and tactic for cc.

Lemma inv_cc : forall E t T, cc E t T ->
(exists i (i1 : i < n) (i2 : i < arity (typ f)),
t = Vnth ls i1 /\ T = Vnth (inputs (typ f)) i2)
\/ (exists x, t = Var x /\ MapsTo x T E /\ ~In x (fvs ls))
\/ (exists v V u, t = App u v /\ cc E u (V ~~> T) /\ cc E v V)
\/ (exists x v A B, t = Lam x v /\ T = A ~~> B /\ ~In x (fvs ls)
/\ cc (add x A E) v B)
\/ (exists g (us : TypArgs g) i (hi : Acc g i),
t = Vnth us (Acc_arity hi) /\ T = Vnth (inputs (typ g)) (Acc_arity hi)
/\ cc E (apps (Fun g) us) (Base (output_base (typ g))))
\/ (exists g p (us : Tes p),
t = apps (Fun g) us /\ T = output (typ g) p
/\ 0+p <= arity (typ g) /\ gt1 E (mk_call f ls) (mk_call g us)).

End cc_def.

Lemma cc_cast : forall f n (ls : Tes n) p (h : n=p) E v V,
cc f (Vcast ls h) E v V <-> cc f ls E v V.

End cc.

Ltac inv_cc h := apply inv_cc in h;
let i := fresh "i" in let g := fresh "g" in let us := fresh "us" in
let x := fresh "x" in let u := fresh "u" in let v := fresh "v" in
let A := fresh "A" in let B := fresh "B" in let p := fresh "p" in
let h1 := fresh "h" in let h2 := fresh "h" in
let h3 := fresh "h" in let h4 := fresh "h" in
destruct h as
[[i [h1 [h2 [h3 h4]]]]
|[[x [h1 [h2 h3]]]
|[[v [A [u [h1 [h2 h3]]]]]
|[[x [v [A [B [h1 [h2 [h3 h4]]]]]]]
|[[g [us [i [h1 [h2 [h3 h4]]]]]]
|[g [p [us [h1 [h2 [h3 h4]]]]]]]]]]].

End Def.

# Ingredients of a computability closure.

Module Type CC_Struct.

We assume given a BI structure.

Declare Module Export BI : BI_Struct.

Some notations.

Notation caeq := (@caeq F X FOrd.eq_dec XOrd.eq_dec ens_X var_notin).
Notation cc := (@cc F X So ens_X env typ Acc Acc_arity).

End CC_Struct.

# Axiomatic proof of correctness of the computability closure.

Module Comp (Export CC : CC_Struct)
(Export CP : CP_Struct with Module L := CC.BI.ST.L).

Module Export CS := LCompSimple.Make CC.BI.ST CP.
Module Export C := LCall.Make CC.BI.ST.

Section comp.

Variables

We assume given an interpretation of base types as computability predicates.

(I : So -> set Te) (I_cp : forall b, cp (I b))

We assume that the accessible arguments of a computable term of the form apps (Fun g) ts are computable.

(comp_acc : forall g (ts : Tes (arity (typ g))),
int I (Base (output_base (typ g))) (apps (Fun g) ts) ->
forall i (hi : Acc g i),
int I (Vnth (inputs (typ g)) (Acc_arity hi)) (Vnth ts (Acc_arity hi)))

We assume given an environment-indexed family of relations on calls.
We assume given a relation gt2 on max calls that is wellfounded, compatible with mcaeq and decreases whenever gt1 decreases.

(gt2 : relation max_call) (gt2_wf : WF gt2)
(gt2_mcaeq : Proper (mcaeq ==> mcaeq ==> impl) gt2)
(gt2_gt1 : forall E f n (ls : Tes n) g p (us : Tes p),
n <= arity (typ f) -> p <= arity (typ g) ->
gt1 E (mk_call f ls) (mk_call g us) ->
forall s (ts' : Tes (arity (typ f) - n)) (us' : Tes (arity (typ g) - p))
(nf : n + (arity (typ f) - n) = arity (typ f))
(pg : p + (arity (typ g) - p) = arity (typ g)),
vint I (inputs (typ f)) (Vapp (Vmap (subs s) ls) ts') ->
(forall x A, MapsTo x A E -> ~XSet.In x (fvs ls) -> int I A (s x)) ->
gt2 (mk_max_call f (Vcast (Vapp (Vmap (subs s) ls) ts') nf))
(mk_max_call g (Vcast (Vapp (Vmap (subs s) us) us') pg)))

Induction hypothesis: we assume that, given a mk_max_call f ts such that ts are computable, every call mk_max_call g us smaller in gt2, is computable whenever us are computable.

(f : F) (ts : TypArgs f) (hts : vint I (inputs (typ f)) ts)
(IH : forall g (us : TypArgs g),
gt2 (mk_max_call f ts) (mk_max_call g us) ->
vint I (inputs (typ g)) us ->
int I (output (typ g) (arity (typ g))) (apps (Fun g) us))

We assume given some terms ls and some substitution s0 such that Vmap (subs s0) ls is alpha-equivalent to a prefix of ts.

(n : nat) (ls : Tes n) (s0 : X -> Te) (h : 0+n <= arity (typ f))
(hls : Vmap (subs s0) ls ~~~ Vsub ts h).

## Correctness proof:

we prove that, if v is in the closure of mk_call f ls and E, and s is a substitution equal to s0 on fvs ls and computable on variables of E not in fvs ls, then subs s v is computable.

Lemma cc_comp : forall E v V, cc gt1 f ls E v V -> forall s,
(forall x, XSet.In x (fvs ls) -> s x = s0 x) ->
(forall x A, MapsTo x A E -> ~XSet.In x (fvs ls) -> int I A (s x)) ->
int I V (subs s v).

End comp.

End Comp.

# Axiomatic proof of the termination of a rewrite system

whose right hand-sides are in the computability closure of their corresponding left hand-sides.

Module Termin (Export CC : CC_Struct)
(Export RS : RS_Struct with Module L := CC.BI.ST.L).

Module Export CR := LCompRewrite.Make RS.

We use the CP structure for the union of beta-reduction and rewriting defined in LCompRewrite.

Module CP := CP_beta_eta_rewrite RS.

Module Export C := Comp CC CP.

Section termin.

Variables

We assume given an interpretation of base types as computability predicates.

(I : So -> set Te) (I_cp : forall b, cp (I b))

We assume that the accessible arguments of a computable term of the form apps (Fun g) ts are computable.

(comp_acc : forall g (ts : TypArgs g),
int I (Base (output_base (typ g))) (apps (Fun g) ts) ->
forall i (hi : Acc g i),
int I (Vnth (inputs (typ g)) (Acc_arity hi)) (Vnth ts (Acc_arity hi)))

We assume that apps (Fun f) ts is computable if all its reducts and arguments ts are computable.

(comp_fun : forall f (ts : TypArgs f),
vint I (inputs (typ f)) ts ->
(forall u, apps (Fun f) ts =>R u -> I (output_base (typ f)) u) ->
I (output_base (typ f)) (apps (Fun f) ts))

We assume given an environment-indexed family of relations on calls.
We assume given a relation gt2 on max calls that is wellfounded, compatible with mcaeq and clos_vaeq, and decreases whenever gt1 decreases.

(gt2 : relation max_call) (gt2_wf : WF gt2)
(gt2_mcaeq : Proper (mcaeq ==> mcaeq ==> impl) gt2)
(gt2_gt1 : forall E f n (ls : Tes n) g p (us : Tes p),
n <= arity (typ f) -> p <= arity (typ g) ->
gt1 E (mk_call f ls) (mk_call g us) ->
forall s (ts' : Tes (arity (typ f) - n)) (us' : Tes (arity (typ g) - p))
(nf : n + (arity (typ f) - n) = arity (typ f))
(pg : p + (arity (typ g) - p) = arity (typ g)),
vint I (inputs (typ f)) (Vapp (Vmap (subs s) ls) ts') ->
(forall x A, MapsTo x A E -> ~XSet.In x (fvs ls) -> int I A (s x)) ->
gt2 (mk_max_call f (Vcast (Vapp (Vmap (subs s) ls) ts') nf))
(mk_max_call g (Vcast (Vapp (Vmap (subs s) us) us') pg)))
(gt2_clos_vaeq : forall f ts us, vint I (inputs (typ f)) ts ->
ts ==>R us -> gt2 (mk_max_call f ts) (mk_max_call f us))

We assume that, for every rule, the right hand-side is in the computability closure of the left hand-side.

(lhs_cc_rhs : forall l r (h : rule l r),
cc gt1 (lhs_fun h) (lhs_args h) XMap.empty r
(output (typ (lhs_fun h)) (lhs_nb_args h))).

## Termination proof.

Lemma tr_sn_cc : forall E v V, E |- v ~: V -> SN R_aeq v.

End termin.

End Termin.

# Termination proof of a rewrite system

whose right hand-sides are in the computability closure of their corresponding left hand-sides, using the interpretation of types as computability predicates defined in LCompInt, and a DLQO based on the accessible supterm ordering for comparing function calls.

Module SN_rewrite (Export CC : CC_Struct)
(Export RS : RS_Struct with Module L := CC.BI.ST.L)
(Export CO : DLQO_Struct with Module ST := CC.BI.ST).

Module Import T := Termin CC RS.

Module Export CI := LCompInt.Make CC.BI.ST CP BI.

Module Import L := LCall.Lex CO.

For gt1, i.e. for comparing function calls in the computability closure, we use gt_call (gt_args_lex gt) where gt is the alpha-closure of the accessibility subterm ordering.

Definition gt := clos_aeq (supterm_acc!).

Definition gt1 (E : En) := gt_call (gt_args_lex gt).

Lemma gt1_wf E : WF (gt1 E).

Instance gt1_aeq E : Proper (caeq ==> caeq ==> impl) (gt1 E).

For gt2, i.e. for the termination proof, we use a variant of gt1 that is compatible with ==>R: we use gt_call on the union of gt_args_lex (gt0)! and gt_red R, where gt0 is the restriction on wellfounded terms of gt U R_aeq.

Definition gt0 := RelUtil.restrict (SN R_aeq) (gt U R_aeq).

Definition gt2c := gt_call (fun r => gt_args_lex (gt0!) r U gt_red R).

Definition gt2 := Rof gt2c max_call_call.

Properties of gt0.

Lemma gt0_wf : WF gt0.

Instance gt0_aeq : Proper (aeq ==> aeq ==> impl) gt0.

We check that gt2 is invariant by mcaeq.

Instance gt2c_caeq : Proper (caeq ==> caeq ==> impl) gt2c.

Instance gt2_mcaeq : Proper (mcaeq ==> mcaeq ==> impl) gt2.

We prove that gt2 is wellfounded.

Import Lexicographic_Product.
Import Union.

Lemma gt2_wf : WF gt2.

We check that gt2 is compatible with ==>R.

Lemma gt2_clos_vaeq : forall f (ts us : TypArgs f),
vint I (inputs (typ f)) ts -> ts ==>R us ->
gt2 (mk_max_call f ts) (mk_max_call f us).

We check that gt1 makes gt2 decrease.

Import Lexico.

Lemma gt2_gt1 : forall E f n (ls : Tes n) g p (us : Tes p),
n <= arity (typ f) -> p <= arity (typ g) ->
gt1 E (mk_call f ls) (mk_call g us) ->
forall s (ts' : Tes (arity (typ f) - n)) (us' : Tes (arity (typ g) - p))
(nf : n + (arity (typ f) - n) = arity (typ f))
(pg : p + (arity (typ g) - p) = arity (typ g)),
vint I (inputs (typ f)) (Vapp (Vmap (subs s) ls) ts') ->
(forall x A, MapsTo x A E -> ~XSet.In x (fvs ls) -> int I A (s x)) ->
gt2 (mk_max_call f (Vcast (Vapp (Vmap (subs s) ls) ts') nf))
(mk_max_call g (Vcast (Vapp (Vmap (subs s) us) us') pg)).

Termination theorem.

Section termin.

Variables
(lhs_cc_rhs : forall l r (h : rule l r),
cc gt1 (lhs_fun h) (lhs_args h)
XMap.empty r (output (typ (lhs_fun h)) (lhs_nb_args h))).

Lemma tr_sn_beta_eta_rewrite_aeq : forall E v V, E |- v ~: V -> SN R_aeq v.

End termin.

End SN_rewrite.