Library CoLoR.MatrixInt.AArcticBasedInt

CoLoR, a Coq library on rewriting and termination. See the COPYRIGHTS and LICENSE files.
  • Frederic Blanqui, 2009-03-19 (setoid)
  • Adam Koprowski and Johannes Waldmann, 2008-01

Set Implicit Arguments.


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

  Declare Module Export OSR : OrdSemiRingType.
  Module Export M := Matrix OSR.

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

End TArcticBasedInt.

Module ArcticBasedInt (ABI : TArcticBasedInt).

  Export ABI.

  Module Conf <: MatrixMethodConf.

    Module Export M := ABI.M.
    Module Export OSRT := ABI.OSR.

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

    Definition trsInt := trsInt.
    Notation vec := (vec dim).
    Definition vec_at0 (v : vec) := Vnth v dim_pos.

    Definition vec_invariant (v : vec) := vec_at0 v >>= A1.

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

  End Conf.

  Module Export MBI := MatrixBasedInt Conf.

  Section ABI.

    Notation matrixInt := (matrixInt A matrix).
    Notation mint := (matrixInt dim).
    Notation mat := (matrix dim dim).

    Definition Sig := sig.
    Notation MinusInf := A0.

    Variable A0_min : forall x, x >>= MinusInf.
    Variable ge_gt_eq : forall x y, x >>= y -> x >> y \/ x =A= y.

    Definition gtx x y := x >> y \/ (x =A= MinusInf /\ y =A= MinusInf).
    Notation "x >_0 y" := (gtx x y) (at level 70).

    Global Instance gtx_mor : Proper (eqA ==> eqA ==> iff) gtx.


    Instance gtx_trans : Transitive gtx.


    Definition succ_vec {n} := Vforall2 gtx (n:=n).
    Definition succ (x y : dom) := succ_vec (dom2vec x) (dom2vec y).
    Notation "x >v y" := (succ x y) (at level 70).

    Instance trans_succ : Transitive succ.


    Lemma ge_gtx_compat : forall x y z, x >>= y -> y >_0 z -> x >_0 z.

    Variable succ_wf : WF succ.

    Variable gtx_plus_compat : forall m m' n n',
      m >_0 m' -> n >_0 n' -> m + n >_0 m' + n'.

    Variable gtx_mult_compat : forall m m' n n',
      m >_0 m' -> n >>= n' -> m * n >_0 m' * n'.

    Lemma succ_succeq_compat : absorbs_left succ succeq.

    Lemma gtx_dec : rel_dec gtx.

    Lemma succ_dec : rel_dec succ.

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

    Notation I := (MBI.I mi_eval_ok).
    Notation IR_succ := (IR I succ).

    Definition mat_gt := mat_forall2 gtx (m:=dim) (n:=dim).
    Definition vec_gt := Vforall2 gtx (n:=dim).

    Definition mint_gt n (l r : mint n) :=
      Vforall2 mat_gt (args l) (args r) /\ vec_gt (const l) (const r).

    Definition term_gt := MBI.term_gt mint_gt.

    Lemma mat_gt_dec : rel_dec mat_gt.

    Lemma vec_gt_dec : rel_dec vec_gt.

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

    Lemma Vfold_left_rev_gtx_compat : forall n (v v' : vector A n),
      (forall i (ip: i < n), Vnth v ip >_0 Vnth v' ip) ->
      Vfold_left_rev Aplus A0 v >_0 Vfold_left_rev Aplus A0 v'.

    Section Matrix.

      Variables (m n p : nat) (M M' : matrix m n) (N N' : matrix n p).

      Notation vge := (Vforall2 ge).
      Notation vgt := (Vforall2 gtx).
      Notation mge := mat_ge.
      Notation mgt := (mat_forall2 gtx).

      Lemma arctic_dot_product_mon : forall i (v v' w w' : vector A i),
        vgt v v' -> vge w w' -> dot_product v w >_0 dot_product v' w'.

      Lemma mat_arctic_mult_mon :
        mgt M M' -> mge N N' -> mgt (M <*> N) (M' <*> N').

    End Matrix.

    Lemma mat_vec_prod_gt_compat : forall (M M' : mat) m m',
      mat_gt M M' -> m >=v m' ->
      vec_gt (mat_vec_prod M m) (mat_vec_prod M' m').

    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.

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

  End ABI.

End ArcticBasedInt.