Library CoLoR.MatrixInt.AMatrixBasedInt

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

Set Implicit Arguments.


Section MatrixLinearFunction.

  Variables (A : Type) (matrix : nat -> nat -> Type) (dim argCnt : nat).

  Record matrixInt : Type := mkMatrixInt {
    const : vector A dim;
    args : vector (matrix dim dim) argCnt }.

End MatrixLinearFunction.


Module Type MatrixMethodConf.

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

  Parameter sig : Signature.
  Parameter dim : nat.
  Parameter dim_pos : dim > 0.

  Notation vec := (vec dim).
  Notation eq_vec := (Vforall2 eqA (n:=dim)).
  Notation "x =v y" := (eq_vec x y).
  Notation mat_eqA := (@mat_eqA dim dim).
  Notation mat_eqA_st := (@mat_eqA_equiv dim dim).
  Notation matrixInt := (matrixInt A matrix).
  Notation mint := (matrixInt dim).
  Notation mat := (matrix dim dim).
  Notation eq_vec_st := (Vforall2_equiv eqA_Equivalence dim).
  Notation eq_vec_mat_eqA_st := (Vforall2_equiv mat_eqA_st).

  Parameter trsInt : forall f : sig, mint (arity f).
  Parameter vec_invariant : vec -> Prop.
  Parameter inv_id_matrix :
    vec_invariant (Vreplace (Vconst A0 dim) dim_pos A1).

End MatrixMethodConf.

Module MatrixBasedInt (Export MC : MatrixMethodConf).

  Instance eq_vec_eq_vec_rel k : Equivalence (Vforall2 eq_vec (n:=k)).


  Instance eq_vec_mat_eqA_rel k : Equivalence (Vforall2 mat_eqA (n:=k)).


  Definition eq_mint k (mi1 mi2 : mint k) :=
    let (c1, args1) := mi1 in
    let (c2, args2) := mi2 in
      c1 =v c2 /\ Vforall2 mat_eqA args1 args2.

  Notation "x =i y" := (eq_mint x y) (at level 70).

  Instance eq_mint_refl k : Reflexive (@eq_mint k).


  Instance eq_mint_sym k : Symmetric (@eq_mint k).


  Instance eq_mint_trans k : Transitive (@eq_mint k).


  Instance eq_mint_equiv k : Equivalence (@eq_mint k).


  Instance mkMatrix_mor k : Proper (eq_vec ==> Vforall2 mat_eqA ==> @eq_mint k)
    (@mkMatrixInt A matrix dim k).


  Instance const_mor k : Proper (@eq_mint k ==> eq_vec) (@const A matrix dim k).


  Instance args_mor k :
    Proper (@eq_mint k ==> Vforall2 mat_eqA) (@args A matrix dim k).


  Section MBI.

    Definition vec_at0 (v : vec) := Vnth v dim_pos.

    Definition dom := { v : vec | vec_invariant v }.

    Definition dom2vec (d : dom) : vec := proj1_sig d.

    Definition add_matrices i m n (v : vector (matrix m n) i) :=
      Vfold_left_rev (@mat_plus m n) (zero_matrix m n) v.

    Notation mat_vec_prod := (@mat_vec_prod dim dim).

    Definition mi_eval_aux n (mi : mint n) (v : vector vec n) : vec :=
      add_vectors (Vmap2 mat_vec_prod (args mi) v) [+] const mi.

    Global Instance mi_eval_aux_mor n :
      Proper (@eq_mint n ==> Vforall2 eq_vec ==> eq_vec) (@mi_eval_aux n).


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

    Definition mi_eval f (v : vector dom (arity f)) : dom :=
      exist (mi_eval_ok f v).

    Lemma mi_eval_cons : forall n (mi : mint (S n)) v vs,
      mi_eval_aux mi (Vcons v vs) =v
        mat_vec_prod (Vhead (args mi)) v [+]
        mi_eval_aux (mkMatrixInt (const mi) (Vtail (args mi))) vs.

    Definition dom_zero : dom.


    Definition I := @mkInterpretation sig dom dom_zero mi_eval.

    Definition succeq := Rof (Vforall2 ge) dom2vec.

    Instance refl_succeq : Reflexive succeq.


    Instance trans_succeq : Transitive succeq.


Monotonicity

    Section VecMonotonicity.

      Variables (f : matrix dim dim -> vec -> vec)
                (f_mon : forall M v1 v2, v1 >=v v2 -> f M v1 >=v f M v2)
                (a b : vec).

      Lemma vec_add_weak_monotone_map2 : forall n1 (v1 : vector vec n1) n2
        (v2 : vector vec n2) n (M : vector (matrix dim dim) n) i_j, a >=v b ->
        add_vectors (Vmap2 f M (Vcast (Vapp v1 (Vcons a v2)) i_j)) >=v
        add_vectors (Vmap2 f M (Vcast (Vapp v1 (Vcons b v2)) i_j)).

    End VecMonotonicity.

    Lemma monotone_succeq : monotone I succeq.

    Lemma succeq_dec : rel_dec succeq.

decidability of order on terms induced by matrix interpretations

    Section OrderDecidability.

      Import ABterm.

      Notation bterm := (bterm sig).

symbolic computation of term interpretation

      Definition mat_matrixInt_prod n M (mi : mint n) : mint n :=
        mkMatrixInt (mat_vec_prod M (const mi)) (Vmap (mat_mult M) (args mi)).

      Definition combine_matrices n k (v : vector (vector mat k) n) :=
        Vbuild (fun i ip => add_matrices (Vmap (fun v => Vnth v ip) v)).

      Lemma combine_matrices_nil : forall i,
        combine_matrices Vnil = Vconst (@zero_matrix dim dim) i.

      Lemma combine_matrices_cons :
        forall k n v (vs : vector (vector mat k) n),
          combine_matrices (Vcons v vs) =
          Vmap2 (@mat_plus _ _) (combine_matrices vs) v.

      Fixpoint mi_of_term k (t : bterm k) : mint (S k) :=
        match t with
          | BVar ip =>
            let zero_int := Vconst (zero_matrix dim dim) (S k) in
            let args_int := Vreplace zero_int (le_lt_S ip) (id_matrix dim) in
            mkMatrixInt (@zero_vec dim) args_int
          | BFun f v =>
            let f_int := trsInt f in
            let args_int := Vmap (@mi_of_term k) v in
            let args_int' := Vmap2 (@mat_matrixInt_prod (S k))
                                   (args f_int) args_int in
            let res_const := add_vectors (Vcons (const f_int)
              (Vmap (@const A matrix dim (S k)) args_int')) in
            let res_args := combine_matrices (Vmap (@args A matrix dim (S k))
              args_int') in
            mkMatrixInt res_const res_args
        end.

      Import ATrs.

      Definition rule_mi r :=
        let mvl := maxvar (lhs r) in
        let mvr := maxvar (rhs r) in
        let m := max mvl mvr in
        let lt := inject_term (le_max_l mvl mvr) in
        let rt := inject_term (le_max_r mvl mvr) in
          (mi_of_term lt, mi_of_term rt).

order characteristic for symbolically computed interpretation and its decidability

      Notation mat_ge := (@mat_ge dim dim).
      Notation vec_ge := (@Vforall2 ge dim).

      Definition mint_ge n (l r : mint n) :=
        Vforall2 mat_ge (args l) (args r) /\ Vforall2 ge (const l) (const r).

      Definition term_ord (ord : forall n, relation (mint n)) l r :=
        let (li, ri) := rule_mi (mkRule l r) in ord _ li ri.

      Variable mint_gt : forall n (l r : mint n), Prop.
      Variable mint_gt_dec : forall n, rel_dec (@mint_gt n).

      Definition term_ge := term_ord mint_ge.
      Definition term_gt := term_ord mint_gt.

      Lemma mint_ge_dec : forall n, rel_dec (@mint_ge n).

      Lemma term_ge_dec : rel_dec term_ge.

      Lemma term_gt_dec : rel_dec term_gt.

      Notation IR_succeq := (IR I succeq).

      Definition mint_eval (val : valuation I) k (mi : mint k) : vec :=
        let coefs := Vbuild (fun i (ip : i < k) => dom2vec (val i)) in
        add_vectors (Vcons (const mi) (Vmap2 mat_vec_prod (args mi) coefs)).

      Global Instance mint_eval_mor k val :
        Proper (@eq_mint k ==> eq_vec) (@mint_eval val k).


      Lemma mint_eval_split : forall val k (mi : mint k),
        let coefs := Vbuild (fun i (ip : i < k) => dom2vec (val i)) in
          mint_eval val mi =v const mi [+]
          add_vectors (Vmap2 mat_vec_prod (args mi) coefs).

      Lemma mint_eval_var_aux : forall M i k (v : vector vec k) (ip : i < k),
        add_vectors (Vmap2 mat_vec_prod (Vreplace (Vconst
          (zero_matrix dim dim) k) ip M) v) =v
          col_mat_to_vec (M <*> (vec_to_col_mat (Vnth v ip))).

      Lemma mint_eval_eq_term_int_var : forall v (val : valuation I) k
                                               (t_b : maxvar_le k (Var v)),
        dom2vec (bterm_int val (inject_term t_b)) =v
        mint_eval val (mi_of_term (inject_term t_b)).

      Lemma mint_eval_const : forall val k (c : vec),
        mint_eval (k:=k) val (mkMatrixInt c (combine_matrices Vnil)) =v c.

      Lemma mint_eval_cons : forall n k val c_hd c_tl a_hd
                                    (a_tl : vector (vector mat k) n),
        mint_eval val (mkMatrixInt (c_hd [+] c_tl)
          (combine_matrices (Vcons a_hd a_tl))) =v
        mint_eval val (mkMatrixInt c_hd a_hd) [+]
        mint_eval val (mkMatrixInt c_tl (combine_matrices a_tl)).

      Lemma mint_eval_mult_factor : forall k val M (mi : mint k),
        mint_eval val (mat_matrixInt_prod M mi) =v
        mat_vec_prod M (mint_eval val mi).

      Lemma mint_eval_eq_bterm_int_fapp : forall k i fi val
                                                 (v : vector (bterm k) i),
        let arg_eval := Vmap2 (@mat_matrixInt_prod (S k)) (args fi)
          (Vmap (@mi_of_term k) v) in
          mi_eval_aux fi (Vmap
            (fun t : bterm k => mint_eval val (mi_of_term t)) v) =v
          mint_eval val (mkMatrixInt
            (add_vectors (Vcons (const fi) (Vmap
              (@const A matrix dim (S k)) arg_eval)))
            (combine_matrices (Vmap (@args A matrix dim (S k)) arg_eval))).

      Lemma mint_eval_eq_bterm_int : forall (val : valuation I) t k
                                            (t_b : maxvar_le k t),
        dom2vec (bterm_int val (inject_term t_b))
        =v mint_eval val (mi_of_term (inject_term t_b)).

      Lemma mint_eval_eq_term_int t (val: valuation I) k (t_b: maxvar_le k t) :
        dom2vec (term_int val t)
        =v mint_eval val (mi_of_term (inject_term t_b)).

      Lemma mint_eval_equiv : forall l r (val : valuation I),
        let (li, ri) := rule_mi (mkRule l r) in
        let lev := term_int val l in
        let rev := term_int val r in
        let lv := mint_eval val li in
        let rv := mint_eval val ri in
          lv =v dom2vec lev /\ rv =v dom2vec rev.

      Lemma mint_eval_mon_succeq_args : forall k (val : vector vec k)
        (mi mi' : mint k), mint_ge mi mi' ->
        add_vectors (Vmap2 mat_vec_prod (args mi) val)
        >=v add_vectors (Vmap2 mat_vec_prod (args mi') val).

      Lemma mint_eval_mon_succeq (val : valuation I) k (mi mi' : mint k) :
        mint_ge mi mi' -> mint_eval val mi >=v mint_eval val mi'.

      Lemma term_ge_incl_succeq : term_ge << IR_succeq.

      Definition succeq' := term_ge.
      Definition succeq'_sub := term_ge_incl_succeq.
      Definition succeq'_dec := term_ge_dec.

    End OrderDecidability.

  End MBI.

End MatrixBasedInt.