Library CoLoR.MatrixInt.AMatrixInt

CoLoR, a Coq library on rewriting and termination. See the COPYRIGHTS and LICENSE files.
  • Frederic Blanqui, 2009-04-29 (bigN)
  • Frederic Blanqui, 2009-03-19 (setoid)
  • Adam Koprowski and Hans Zantema, 2007-03-22
Termination criterion based on matrix interpretations.
  • J. Endrullis, J. Waldmann and H. Zantema, "Matrix Interpretations for Proving Termination of Term Rewriting", Proceedings of the 3rd International Joint Conference (IJCAR 2006), 2006.

Set Implicit Arguments.

Import NMatrix.

Module type for proving termination with matrix interpretations
Module Type TMatrixInt.

  Parameter sig : Signature.
  Parameter dim : nat.
  Parameter dim_pos : (dim > 0)%nat.
  Parameter trsInt : forall f : sig, matrixInt nat matrix dim (arity f).

End TMatrixInt.

Definition matrixInt := @matrixInt A matrix.
Definition mkMatrixInt := @mkMatrixInt A matrix.

Module MatrixInt (MI : TMatrixInt).

  Export MI.

  Module Conf <: MatrixMethodConf.

    Module Export OSRT := NOrdSemiRingT.
    Module Export M := Matrix OSRT.

    Definition sig := sig.
    Definition dim := dim.
    Definition dim_pos := dim_pos.

    Definition trsInt := trsInt.
    Notation vec := (vec dim).
    Definition vec_invariant (v : vec) := True.

    Lemma inv_id_matrix :
      vec_invariant (Vreplace (Vconst A0 dim) dim_pos A1).

  End Conf.

  Module Export MBI := MatrixBasedInt Conf.

Monotone algebra instantiated to matrices
  Module Export MonotoneAlgebra <: MonotoneAlgebraType.

    Notation mint := (matrixInt dim).

    Lemma mi_eval_ok : forall f v,
      vec_invariant (mi_eval_aux (trsInt f) (Vmap dom2vec v)).

    Definition I := MBI.I mi_eval_ok.

    Definition succeq := MBI.succeq.

    Definition refl_succeq := MBI.refl_succeq.
    Definition monotone_succeq := @MBI.monotone_succeq mi_eval_ok.
    Definition trans_succeq := MBI.trans_succeq.

    Definition succeq' := MBI.succeq'.
    Definition succeq'_sub := @MBI.succeq'_sub mi_eval_ok.
    Definition succeq'_dec := MBI.succeq'_dec.

    Definition Sig := sig.

    Definition succ_vec v1 v2 := v1 >=v v2 /\ vec_at0 v1 > vec_at0 v2.
    Definition succ := Rof succ_vec dom2vec.

    Lemma succ_wf : WF succ.

    Instance trans_succ : Transitive succ.

    Lemma succ_succeq_compat : absorbs_left succ succeq.

    Lemma succ_dec : rel_dec succ.

    Notation IR_succ := (IR I succ).

    Definition mint_gt n (l r : mint n) :=
      mint_ge l r /\ vec_at0 (const l) > vec_at0 (const r).

    Definition term_gt := MBI.term_gt mint_gt.

    Lemma vec_plus_gt_compat_l : forall vl vl' vr vr',
      vec_at0 vl >= vec_at0 vl' -> vec_at0 vr > vec_at0 vr' ->
      vec_at0 (vl [+] vr) > vec_at0 (vl' [+] vr').

    Lemma mint_eval_mon_succ : forall (val : valuation I) k
      (mi mi' : mint k), mint_gt mi mi' ->
      succ_vec (mint_eval val mi) (mint_eval val mi').

    Lemma term_gt_incl_succ : term_gt << IR_succ.

    Lemma mint_gt_dec : forall n, rel_dec (@mint_gt n).

    Definition succ' := term_gt.
    Definition succ'_sub := term_gt_incl_succ.
    Definition succ'_dec := term_gt_dec mint_gt mint_gt_dec.

    Section ExtendedMonotoneAlgebra.

      Section VecMonotonicity.

        Lemma vec_plus_gt_compat_r : forall vl vl' vr vr',
          vec_at0 vl > vec_at0 vl' -> vec_at0 vr >= vec_at0 vr' ->
          vec_at0 (vl [+] vr) > vec_at0 (vl' [+] vr').

        Variable f : matrix dim dim -> vec -> vec.
        Variable f_mon : forall M v1 v2, get_elem M dim_pos dim_pos > 0 ->
          v1 >=v v2 -> vec_at0 v1 > vec_at0 v2 ->
          vec_at0 (f M v1) > vec_at0 (f M v2).

        Variables (a b : vec).

        Lemma vec_add_monotone_map2 : forall n1 (v1 : vector vec n1) n2
          (v2 : vector vec n2) n (M : vector (matrix dim dim) n) i_j,
          Vforall (fun m => get_elem m dim_pos dim_pos > 0) M ->
          a >=v b -> vec_at0 a > vec_at0 b ->
          vec_at0 (add_vectors
            (Vmap2 f M (Vcast (Vapp v1 (Vcons a v2)) i_j))) >
          vec_at0 (add_vectors
            (Vmap2 f M (Vcast (Vapp v1 (Vcons b v2)) i_j))).

      End VecMonotonicity.

      Lemma dot_product_mon_r : forall i j (jp : (j < i)%nat)
        (v v' w w' : vector nat i),
        v >=v v' -> w >=v w' -> Vnth v jp > A0 ->
        Vnth w jp > Vnth w' jp ->
        dot_product v w > dot_product v' w'.

      Definition monotone_interpretation n (fi : matrixInt dim n) :=
        Vforall (fun m => get_elem m dim_pos dim_pos > 0) (args fi).

      Definition bmonotone_interpretation n (fi : matrixInt dim n) :=
        bVforall (fun m => bgt_nat (get_elem m dim_pos dim_pos) 0) (args fi).

      Lemma bmonotone_interpretation_ok : forall n (fi : matrixInt dim n),
        bmonotone_interpretation fi = true <-> monotone_interpretation fi.

      Lemma monotone_succ :
        (forall f : sig, monotone_interpretation (trsInt f)) ->
        monotone I succ.

      Import List ListUtil.

      Section fin_Sig.

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

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

      End fin_Sig.

    End ExtendedMonotoneAlgebra.

  End MonotoneAlgebra.

  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 matrix interpretation").

End MatrixInt.