# 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.

Require Import ATerm ABterm ListUtil ListForall VecUtil
PositivePolynom AInterpretation ZUtil NaryFunction ARelation RelUtil
LogicUtil SN Polynom MonotonePolynom NatUtil ATrs Max BoundNat.

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

Require Import AWFMInterpretation.

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))).

Implicit Arguments PI_term_int_eq [t 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.

Open Local 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

Require Import ZUtil.

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).

Require Import ACompat.

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

termination

Require Import AMannaNess.

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.

Implicit Arguments fin_PolyWeakMonotone [Sig Fs].

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.