Library CoLoR.PolyInt.PolyChecker

CoLoR, a Coq library on rewriting and termination. See the COPYRIGHTS and LICENSE files.
  • Adam Koprowski, 2009-03-24
A termination solver using the polynomial interpretations method.


Set Implicit Arguments.

Section PolySolver.

Variable Sig : Signature.

checking polynomial interpretation and converting it to dependently typed interpretation with constraints

Program Definition check_mono (n : nat) (m : monomial) : option (Z * monom n) :=
  match m with
  | (coef, vars) =>
      match eq_nat_dec n (List.length vars) with
      | left _ => Some (coef, vec_of_list vars)
      | right _ => None
      end
  end.

Definition check_poly (n : nat) (p : polynomial) : option (poly n) :=
  map_opt (@check_mono n) p.

Definition polyInt n := { p : poly n | pweak_monotone p }.

Notation symPI := (symInt Sig polyInt).

Program Definition symbol_poly_int (f : Sig) (p : polynomial) : option symPI :=
  match check_poly (arity f) p with
  | None => None
  | Some fi =>
      match pweak_monotone_check fi with
      | None => None
      | Some _ => Some (buildSymInt Sig polyInt f fi)
      end
  end.

Definition defaultPoly n : poly n :=
  pconst n 1 ++ list_of_vec (Vbuild (fun i (ip : i < n) => (1%Z, mxi ip))).

Lemma defaultPoly_mxi_1 n i (H : i < n) : List.In (1%Z, mxi H) (defaultPoly n).

Lemma defaultPoly_wm n : pweak_monotone (defaultPoly n).

Lemma defaultPoly_sm n : pstrong_monotone (defaultPoly n).

Program Definition defaultInt n : polyInt n := defaultPoly n.


Program Definition interpret n (fi : polyInt n) : naryFunction1 D n :=
  @peval_D n fi _.


weak and strong monotonicity checking

Program Definition poly_wm (fi : symPI) := True.
Program Definition poly_sm (fi : symPI) := pstrong_monotone (projT2 fi).

Lemma sm_imp_wm (fi : symPI) : poly_sm fi -> poly_wm fi.

Program Definition check_wm (fi : symPI) : option (poly_wm fi) :=
  Some _.


Lemma wm_ok : forall fi, poly_wm fi -> Vmonotone1 (interpret (projT2 fi)) Dge.

Program Definition check_sm (fi : symPI) : option (poly_sm fi) :=
  pstrong_monotone_check (projT2 fi).

Lemma sm_ok : forall fi, poly_sm fi -> Vmonotone1 (interpret (projT2 fi)) Dgt.

Let buildSymInt := buildSymInt Sig polyInt.
Let defaultIntForSymbol := defaultIntForSymbol Sig polyInt defaultInt.

Lemma default_sm : forall f, poly_sm (buildSymInt (defaultIntForSymbol f)).

Definition wm_spec := Build_monSpec interpret poly_wm check_wm wm_ok.
Definition sm_spec := Build_monSpec interpret poly_sm check_sm sm_ok.

rule compatibility with orders.

Section Orders.

Variable i : forall f : Sig, polyInt (arity f).

Definition I := makeI Sig D0 polyInt interpret i.

Let succ := IR I Dgt.
Let succeq := IR I Dge.

Program Definition check_succ (r : rule Sig) : option (succ (lhs r) (rhs r)) :=
  match coef_pos_check (rulePoly_gt i r) with
  | None => None
  | Some _ => Some _
  end.


Program Definition check_succeq (r : rule Sig) : option (succeq (lhs r) (rhs r)) :=
  match coef_pos_check (rulePoly_ge i r) with
  | None => None
  | Some _ => Some _
  end.


End Orders.

solver for the technique of polynomial interpretations.