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.



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.