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
  • Adam Koprowski, 2007-04-26, 2008-05-27
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)

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
      (@IR_substitution_closed _ I Dgt)
      (@IR_substitution_closed _ I Dge)
      (@IR_context_closed _ _ _ pi_monotone)
      (@IR_context_closed _ _ _ pi_monotone_eq)
      (@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.


    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.


    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 := (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].


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