# Library CoLoR.PolyInt.APolyInt

CoLoR, a Coq library on rewriting and termination. See the COPYRIGHTS and LICENSE files.
• Sebastien Hinderer, 2004-04-20
• Frederic Blanqui, 2004-12-13
proof of the termination criterion based on polynomial interpretations

Set Implicit Arguments.

Section S.

Variable Sig : Signature.

Notation bterm := (bterm Sig).

Definition PolyInterpretation := forall f : Sig, poly (arity f).

polynomial associated to a bterm

Section pi.

Variable PI : PolyInterpretation.

Fixpoint termpoly k (t : bterm k) : poly (S k) :=
match t with
| BVar H => ((1)%Z, mxi (gt_le_S (le_lt_n_Sm H))) :: List.nil
| BFun f v => pcomp (PI f) (Vmap (@termpoly k) v)
end.

monotony properties

Definition PolyWeakMonotone := forall f : Sig, pweak_monotone (PI f).
Definition PolyStrongMonotone := forall f : Sig, pstrong_monotone (PI f).

Section fin_Sig.

Variables (Fs : list Sig) (Fs_ok : forall f : Sig, List.In f Fs).

Lemma fin_PolyWeakMonotone :
forallb (fun f => bpweak_monotone (PI f)) Fs = true -> PolyWeakMonotone.

End fin_Sig.

coefficients are positive

Variables (PI_WM : PolyWeakMonotone) (PI_SM : PolyStrongMonotone).

Section coef_pos.

Let P := fun (k : nat) (t : bterm k) => coef_pos (termpoly t).
Let Q := fun (k n : nat) (ts : vector (bterm k) n) => Vforall (@P k) ts.

Lemma bterm_poly_pos : forall (k : nat) (t : bterm k), P t.

End coef_pos.

interpretation in D

Definition Int_of_PI := mkInterpretation D0 (fun f => peval_D (PI_WM f)).

Let I := Int_of_PI.

interpretation monotony

Lemma pi_monotone : monotone I Dgt.

Lemma pi_monotone_eq : monotone I Dge.

reduction ordering

Let succ := IR I Dgt.

Lemma pi_red_ord : reduction_ordering succ.

reduction pair

Let succ_eq := IR I Dge.

Lemma pi_absorb : absorbs_left succ succ_eq.

Definition rp := @mkReduction_pair Sig

succ

succ_eq

(@IR_substitution_closed _ I Dgt)

(@IR_substitution_closed _ I Dge)

(@IR_context_closed _ _ _ pi_monotone)

(@IR_context_closed _ _ _ pi_monotone_eq)

pi_absorb

(@IR_WF _ I _ WF_Dgt).

equivalence between (xint) and (vec_of_val xint)

Let f1 (xint : valuation I) k (t : bterm k) := proj1_sig (bterm_int xint t).

Let f2 (xint : valuation I) k (t : bterm k) :=
proj1_sig (peval_D (bterm_poly_pos t) (vec_of_val xint (S k))).

Let P (xint : valuation I) k (t : bterm k) := f1 xint t = f2 xint t.

Let Q (xint : valuation I) k n (ts : vector (bterm k) n) :=
Vforall (@P xint k) ts.

Lemma termpoly_v_eq_1 : forall x k (H : (x<=k)%nat),
termpoly (BVar H) = (1%Z, mxi (gt_le_S (le_lt_n_Sm H))) :: pzero (S k).

Lemma termpoly_v_eq_2 :
forall x k (H : (x<=k)%nat) (v : vector Z (S k)),
peval (termpoly (BVar H)) v = meval (mxi (gt_le_S (le_lt_n_Sm H))) v.

Lemma PI_bterm_int_eq : forall xint k (t : bterm k), P xint t.

Lemma PI_term_int_eq : forall (xint : valuation I) t k
(H : (maxvar t <= k)%nat),
proj1_sig (term_int xint t)
= proj1_sig (peval_D (bterm_poly_pos (inject_term H))
(vec_of_val xint (S k))).

polynomial associated to a rule

Infix "+" := pplus : poly_scope.
Notation "- y" := (popp y) : poly_scope.
Notation "x - y" := (x + (- y))%poly : poly_scope.
Notation "'0'" := (pconst _ 0) : poly_scope.
Notation "'1'" := (pconst _ 1) : poly_scope.

Local Open Scope poly_scope.

Hint Unfold maxvar_le.
Hint Resolve le_max_l le_max_r.

Program Definition rulePoly_ge rule :=
let l := lhs rule in let r := rhs rule in
let m := max (maxvar l) (maxvar r) in
termpoly (@inject_term _ m l _) - termpoly (@inject_term _ m r _).

Definition rulePoly_gt rule := rulePoly_ge rule - 1.

compatibility

Lemma pi_compat_rule : forall r,
coef_pos (rulePoly_gt r) -> succ (lhs r) (rhs r).

Lemma pi_compat_rule_weak : forall r,
coef_pos (rulePoly_ge r) -> succ_eq (lhs r) (rhs r).

Lemma pi_compat : forall R,
lforall (fun r => coef_pos (rulePoly_gt r)) R -> compat succ R.

termination

Lemma polyInterpretationTermination : forall R,
lforall (fun r => coef_pos (rulePoly_gt r)) R -> WF (red R).

End pi.

default polynomial interpretation

Definition default_poly n :=
List.map (fun x => (1%Z, mxi (N_prf x))) (L n).

Definition default_pi (f : Sig) := default_poly (arity f).

Lemma pweak_monotone_default : PolyWeakMonotone default_pi.

End S.

tactics

Ltac PolyWeakMonotone Fs_ok :=
match goal with
| |- PolyWeakMonotone ?PI =>
apply (fin_PolyWeakMonotone PI Fs_ok);
(check_eq || fail 10 "could not prove monotony")
end.