Library CoLoR.MatrixInt.AArcticBZInt

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.

Import ArcticBZMatrix.

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

Condition for an arctic BZ interpretation to be valid

Section Absolute_finite.

  Variable dim : nat.
  Variable dim_pos : (dim > 0)%nat.

  Definition absolute_finite n (fi : matrixInt dim n) :=
    Vnth (const fi) dim_pos >>= A1.

  Definition babsolute_finite n (fi : matrixInt dim n) :=
    is_above_zero (Vnth (const fi) dim_pos).

  Lemma babsolute_finite_ok : forall n (fi : matrixInt dim n),
    babsolute_finite fi = true <-> absolute_finite 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_absolute_finite :
    forallb (fun f => babsolute_finite (trsInt f)) Fs = true ->
    forall f : sig, absolute_finite (trsInt f).

End Absolute_finite.

Module type for proving termination with matrix interpretations

Module Type TArcticBZInt.

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

End TArcticBZInt.

Module ArcticBZInt (Import AI : TArcticBZInt).

  Module AB <: TArcticBasedInt.

    Module OSR := ArcticBZOrdSemiRingT.
    Module M := ArcticBZMatrix.
    Definition sig := sig.
    Definition dim := dim.
    Definition dim_pos := dim_pos.
    Definition trsInt := trsInt.

  End AB.

  Module Export AIBase := ArcticBasedInt AB.

  Module Export MonotoneAlgebra <: MonotoneAlgebraType.

    Definition Sig := Sig.

    Lemma mi_eval_at0 : forall n (mi : matrixInt dim n) (v : vector dom n),
      absolute_finite dim_pos mi ->
      vec_at0 (mi_eval_aux mi (Vmap dom2vec v)) >>= A1.

    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 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 trans_succ := AIBase.trans_succ.

    Definition succ_succeq_compat := AIBase.succ_succeq_compat ge_gt_eq.

    Lemma succ_wf : WF succ.

  End MonotoneAlgebra.

tactics

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

End ArcticBZInt.


Ltac absolute_finite Fs_ok :=
  apply (fin_absolute_finite _ _ Fs_ok);
    (check_eq || fail 10 "invalid below-zero arctic interpretation").