# 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.