Library CoLoR.MatrixInt.ATropicalInt

CoLoR, a Coq library on rewriting and termination. See the COPYRIGHTS and LICENSE files.
  • Adam Koprowski and Johannes Waldmann, 2010-04

Set Implicit Arguments.


Module Import TropicalMatrix := Matrix TropicalOrdSemiRingT.

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

Condition for a tropical interpretation to be valid

Section Somewhere_tfinite.

  Variable dim : nat.
  Variable dim_pos : dim > 0.

  Definition somewhere_tfinite n (fi : matrixInt dim n) :=
    Vexists (fun m => get_elem m dim_pos dim_pos <> PlusInf) (args fi)
    \/ Vnth (const fi) dim_pos <> PlusInf.

  Definition bsomewhere_tfinite n (fi : matrixInt dim n) :=
    bVexists
    (fun m => tropical_is_finite (get_elem m dim_pos dim_pos)) (args fi)
    || tropical_is_finite (Vnth (const fi) dim_pos).

  Lemma bsomewhere_tfinite_ok : forall n (fi : matrixInt dim n),
    bsomewhere_tfinite fi = true <-> somewhere_tfinite fi.

  Variable sig : Signature.
  Variable trsInt : forall f : sig, matrixInt dim (arity f).


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

  Lemma fin_somewhere_tfinite :
    forallb (fun f => bsomewhere_tfinite (trsInt f)) Fs = true ->
    forall f : sig, somewhere_tfinite (trsInt f).

End Somewhere_tfinite.


Ltac somewhere_tfinite Fs_ok :=
  apply (fin_somewhere_tfinite _ _ Fs_ok);
    (check_eq || fail 10 "invalid tropical interpretation").

Module type for proving termination with a tropical interpretation

Module Type TTropicalInt.

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

End TTropicalInt.

Module TropicalInt (Import AI : TTropicalInt).

  Module AB <: TTropicalBasedInt.

    Module OSR := TropicalOrdSemiRingT.
    Module M := TropicalMatrix.
    Definition sig := sig.
    Definition dim := dim.
    Definition dim_pos := dim_pos.
    Definition trsInt := trsInt.

  End AB.

  Module Export AIBase := TropicalBasedInt AB.

  Module Export MonotoneAlgebra <: MonotoneAlgebraType.

    Definition Sig := Sig.

    Lemma mat_times_vec_at0_positive : forall n (m : matrix n n)
      (v : vector A n) (dim_pos : n > 0),
      get_elem m dim_pos dim_pos <> PlusInf ->
      Vnth v dim_pos <> PlusInf ->
      Vnth (mat_vec_prod m v) dim_pos <> PlusInf.

    Notation mat_times_vec := (@mat_vec_prod dim dim).
    Notation mint := (matrixInt dim).

    Notation "x >_0 y" := (gtx x y) (at level 70).

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

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

    Lemma eval_some_notInf : forall n (mi : mint n) (v : vector dom n),
      Vexists (fun m => get_elem m dim_pos dim_pos <> PlusInf) (args mi) ->
      Vfold_left_rev Aplus A0
      (Vmap (fun v => Vnth v dim_pos)
        (Vmap2 mat_times_vec (args mi) (Vmap dom2vec v))) <> PlusInf.

    Lemma mi_eval_at0 : forall n (mi : matrixInt dim n) (v : vector dom n),
      somewhere_tfinite dim_pos mi ->
      vec_at0 (mi_eval_aux mi (Vmap dom2vec v)) <> PlusInf.

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

    Definition I := I mi_eval_ok.

    Definition succ := AIBase.succ.
    Definition succ' := AIBase.succ'.
    Definition succ'_sub := @AIBase.succ'_sub gtx_plus_compat gtx_mult_compat
      mi_eval_ok.
    Definition succ'_dec := AIBase.succ'_dec.

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

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

    Definition succ_succeq_compat := AIBase.succ_succeq_compat ge_gt_eq.

    Lemma succ_wf : WF succ.

    Instance trans_succ : Transitive succ.


  End MonotoneAlgebra.

  Ltac prove_cc_succ Fs_ok :=
    fail 10 "tropical matrices cannot be used for proving total termination".

End TropicalInt.