Library CoLoR.MatrixInt.ABigMatrixInt

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.
References:
  • 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 BigNMatrix.

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 bigN matrix dim (arity f).

End TMatrixInt.

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

Module MatrixInt (Export MI : TMatrixInt).

  Module Conf <: MatrixMethodConf.

    Module Export OSRT := BigNOrdSemiRingT.
    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 MBI := MatrixBasedInt Conf.

Monotone algebra instantiated to matrices
  Module MonotoneAlgebra <: MonotoneAlgebraType.

    Export MBI.

    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 trans_succ : transitive succ.

    Lemma succ_wf : WF 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 bigN 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).

      Variable matrixInt_monotone : forall f : sig,
        monotone_interpretation (trsInt f).

      Lemma monotone_succ : monotone I succ.

    End ExtendedMonotoneAlgebra.

  End MonotoneAlgebra.

  Export MonotoneAlgebra.

  Module Export MAR := MonotoneAlgebraResults MonotoneAlgebra.

  Ltac matrixInt_monotonicity :=
    let f := fresh "f" in
    first
    [ solve [
      apply monotone_succ; intro f; destruct f;
        vm_compute; repeat split; auto with arith
      ]
    | fail 10 "Failed to prove monotonicity of given matrix interpretation"
    ].

  Ltac prove_termination := MAR.prove_termination matrixInt_monotonicity.

End MatrixInt.