Library CoLoR.Util.Relation.InfSeq

CoLoR, a Coq library on rewriting and termination. See the COPYRIGHTS and LICENSE files.
  • Sidi Ould-Biha, 2010-04-27
  • Frederic Blanqui, 2011-05-11
Definitions and properties of infinite sequences, possibly modulo some relation. Uses classical logic and the axiom of indefinite description, and the axiom WF_notIS for WF_absorb

Set Implicit Arguments.


Section S.

  Variables (A : Type) (eq_dec : forall x y : A, {x=y}+{~x=y}).

given a sequence f having an infinite number of occurrences of a, returns the sub-sequence of those occurrences

  Section enum.

    Variables (f : nat -> A) (a : A)
      (H : forall i, exists j, j >= i /\ f j = a).

    Fixpoint g i :=
      match i with
        | 0 => proj1_sig (ch_min (H 0))
        | S i' => proj1_sig (ch_min (H (S (g i'))))
      end.

    Lemma g_mon : forall i, g i < g (S i).

    Lemma g_correct : forall i, f (g i) = a.

    Lemma g_ge_id : forall i, g i >= i.

    Lemma g_neq : forall i j, g i < j < g (S i) -> f j <> a.

    Lemma g_complete : forall i, f i = a -> exists j, i = g j.

  End enum.


sorted list of indices j such that f j = a /\ j < i

  Section indices.

    Variables (f : nat -> A) (a : A).

    Fixpoint indices_aux acc i :=
      match i with
        | 0 => acc
        | S i' => indices_aux (if eq_dec (f i') a then i' :: acc else acc) i'
      end.

    Definition indices := indices_aux nil.

    Lemma In_indices_aux_elim : forall i x acc,
      In x (indices_aux acc i) -> In x acc \/ (f x = a /\ x < i).


    Lemma indices_correct : forall i x, In x (indices i) -> f x = a /\ x < i.

    Lemma In_indices_aux_intro : forall i x acc,
      In x acc -> In x (indices_aux acc i).

    Lemma indices_aux_complete : forall i x acc,
      x < i -> f x = a -> In x (indices_aux acc i).

    Lemma indices_complete : forall i x, x < i -> f x = a -> In x (indices i).

    Lemma indices_aux_length : forall i acc,
      length (indices_aux acc i) <= i + length acc.

    Lemma indices_length : forall i, length (indices i) <= i.


    Lemma indices_aux_Sorted : forall i acc,
      Sorted lt acc -> HdRel le i acc -> Sorted lt (indices_aux acc i).

    Lemma indices_Sorted : forall i, Sorted lt (indices i).

  End indices.


given an infinite sub-sequence g of f for the indices i>=i0 such that f i = a, returns a sub-sequence for the indices i>=0 such that f i = a

  Section prefix.

    Variables (f : nat -> A) (a : A) (i0 : nat) (g : nat -> nat).

    Notation indices := (indices f a).

    Let d := 0.

    Definition prefix i := let is := indices i0 in
      let n := length is in if lt_dec i n then nth i is d else i0 + g (i - n).

    Lemma prefix_correct :
      (forall i, f (i0 + g i) = a) -> (forall i, f (prefix i) = a).


    Lemma prefix_mon :
      (forall i, g i < g (S i)) -> (forall i, prefix i < prefix (S i)).

    Lemma prefix_complete :
      (forall i, i >= i0 -> f i = a -> exists j, i = i0 + g j) ->
      (forall i, f i = a -> exists j, i = prefix j).

  End prefix.

building a constant infinite sub-sequence from an infinite sequence on a finite codomain

  Lemma finite_codomain : forall As (f : nat -> A),
    (forall i, In (f i) As) -> exists a, exists g,
      (forall i, g i < g (S i)) /\ (forall i, f (g i) = a)
      /\ (forall i, f i = a -> exists j, i = g j).

build an infinite sequence by iterating a function

Section iter.

  Variables (a : A) (f : A -> A).

  Lemma IS_iter : forall R : relation A,
    (forall x, R x (f x)) -> IS R (iter a f).

End iter.

building an infinite E-sequence from an infinite E!-sequence

Section TransIS.

  Variables (E : relation A) (h : nat -> A) (HEh : IS (E!) h).

  Lemma IS_tc : exists h', IS E h' /\ h' 0 = h 0.

End TransIS.

building an infinite R-sequence modulo E from an infinite E@R-sequence

Section ISCompSplit.

  Variables (E R : relation A) (f : nat -> A).

  Lemma ISComp_split : IS (E @ R) f -> exists g, ISMod E R f g.

End ISCompSplit.

building an infinite R-sequence from an infinite E#@R-sequence if R@E<<R

Section absorb.

  Variables (E R : relation A) (ab : R @ E << R).

  Lemma IS_absorb : forall f, IS (E# @ R) f -> EIS R.

  Lemma WF_absorb : WF R -> WF (E# @ R).

End absorb.

Lemma WF_mod_rev2 : forall E S : relation A, WF (S @ E#) -> WF (E# @ S).

building an infinite R-sequence modulo E from an infinite E@R-sequence modulo E if E is transitive

Section ISModComp.

  Variables (E R : relation A) (f g : nat -> A)
    (hyp1 : ISMod E (E @ R) f g) (TE : transitive E).

  Lemma ISMod_comp : exists g', ISMod E R f g'.

End ISModComp.

building an infinite R-sequence modulo E from an infinite EUR-sequence modulo E with infinitely many R-steps

Section ISModUnion.

  Variables (E R : relation A) (f g : nat -> A)
    (hyp1 : ISMod E (E U R) f g)
    (hyp2 : forall i, exists j, i <= j /\ R (g j) (f (S j)))
    (TE : transitive E).

  Lemma ISMod_union : exists f', exists g', ISMod E R f' g'
    /\ forall i, (exists k, g' i = g k) /\ (exists k, f' i = f k).

End ISModUnion.

building an infinite E-sequence from an infinite R-sequence modulo E if R@E<<E

Section ISModCommute.

  Variables (E R : relation A) (f g : nat -> A)
    (hyp1 : ISMod E R f g) (hyp2 : R @ E @ R << E @ R).

  Lemma existEdom_proof :
    forall x i, R x (f (S i)) -> exists y, E x y /\ R y (f (S (S i))).

  Fixpoint ISOfISMod_rec n : { x : A * nat | R (fst x) (f (S (snd x))) } :=
    let P := fun x : A * nat => R (fst x) (f (S (snd x))) in
      match n with
        | S n' => let (t, Pt) := ISOfISMod_rec n' in
          let H := existEdom_proof Pt in
            let s := constructive_indefinite_description _ H in
              let (t', Pt') := s in (@exist _ P (t', (S (snd t))) (proj2 Pt'))
        | 0 => @exist _ P (g 0, 0) (proj2 (hyp1 0))
      end.

  Lemma ISOfISMod_rec_spec : forall i,
    E (fst (proj1_sig (ISOfISMod_rec i)))
    (fst (proj1_sig (ISOfISMod_rec (S i)))).

  Definition ISOfISMod n :=
    match n with
      | S n' => (fst (proj1_sig (ISOfISMod_rec n')))
      | 0 => f 0
    end.

  Lemma ISOfISMod_spec : IS E ISOfISMod.

End ISModCommute.

building an infinite R-sequence modulo E! from an infinite R-sequence modulo E#

Section ISModTrans.

  Variables (E R : relation A) (f g : nat -> A)
    (hyp1 : ISMod (E #) R f g) (NISR : forall h, ~IS R h)
    (TrsR : transitive R).

  Lemma build_trs_proof : forall i, exists j, i <= j /\ E! (f j) (g j).

  Lemma trc_ISMod : exists f', exists g', ISMod (E!) R f' g' /\
    (exists k, g' 0 = g k) /\ (f' 0 = f 0 \/ R (f 0) (f' 0)).

End ISModTrans.

End S.