Library CoLoR.PolyInt.APolyInt_MA

CoLoR, a Coq library on rewriting and termination. See the COPYRIGHTS and LICENSE files.
  • Adam Koprowski and Hans Zantema, 2007-04-25
Polynomial interpretations in the setting of monotone algebras.

Require Import APolyInt AMonAlg ZUtil RelUtil PositivePolynom ATrs ListForall
  MonotonePolynom LogicUtil BoolUtil.

Module Type TPolyInt.
  Parameter sig : Signature.
  Parameter trsInt : PolyInterpretation sig.
  Parameter trsInt_wm : PolyWeakMonotone trsInt.
End TPolyInt.

Module PolyInt (Export PI : TPolyInt).

  Module Export MonotoneAlgebra <: MonotoneAlgebraType.

    Definition Sig := sig.

    Definition I := Int_of_PI trsInt_wm.

    Definition succ := Dgt.
    Definition succeq := Dge.

    Definition refl_succeq := refl_Dge.
    Definition trans_succ := trans_Dgt.
    Definition trans_succeq := trans_Dge.

    Lemma monotone_succeq : AWFMInterpretation.monotone I succeq.

    Definition succ_wf := WF_Dgt.

    Lemma succ_succeq_compat : absorbs_left succ succeq.

    Definition rulePoly_gt l r := rulePoly_gt trsInt (@mkRule sig l r).

    Definition succ' l r := coef_pos (rulePoly_gt l r).

    Definition bsucc' l r := bcoef_pos (rulePoly_gt l r).

    Lemma bsucc'_ok : forall l r, bsucc' l r = true <-> succ' l r.

    Lemma succ'_dec : rel_dec succ'.

    Definition rulePoly_ge l r := rulePoly_ge trsInt (@mkRule sig l r).

    Definition succeq' l r := coef_pos (rulePoly_ge l r).

    Definition bsucceq' l r := bcoef_pos (rulePoly_ge l r).

    Lemma bsucceq'_ok : forall l r, bsucceq' l r = true <-> succeq' l r.

    Lemma succeq'_dec : rel_dec succeq'.

    Lemma succ'_sub : succ' << IR I succ.

    Lemma succeq'_sub : succeq' << IR I succeq.

    Section ExtendedMonotoneAlgebra.

      Lemma monotone_succ : PolyStrongMonotone trsInt ->
        AWFMInterpretation.monotone I succ.

    End ExtendedMonotoneAlgebra.

    Require Import List.

    Section fin_Sig.

      Variable Fs : list Sig.
      Variable Fs_ok : forall f : Sig, In f Fs.

      Lemma fin_monotone_succ :
        forallb (fun f => bpstrong_monotone (trsInt f)) Fs = true ->
        AWFMInterpretation.monotone I succ.

    End fin_Sig.

  End MonotoneAlgebra.

tactics for Rainbow

  Implicit Arguments fin_monotone_succ [Fs].

  Ltac prove_cc_succ Fs_ok :=
    apply IR_context_closed; apply (fin_monotone_succ Fs_ok);
      (check_eq || fail 10 "could not prove the monotony of this polynomial interpretation").

End PolyInt.