# Module Sequences

A library of relation operators defining sequences of transitions and useful properties about them.

Set Implicit Arguments.

Section SEQUENCES.

Variable A: Type.

Zero, one or several transitions: reflexive, transitive closure of R.

Inductive star (R: A -> A -> Prop): A -> A -> Prop :=
| star_refl: forall a,
star R a a
| star_step: forall a b c,
R a b -> star R b c -> star R a c.

Lemma star_one:
forall (R: A -> A -> Prop) (a b: A), R a b -> star R a b.
Proof.
intros. econstructor; eauto. constructor.
Qed.

Lemma star_trans:
forall (R: A -> A -> Prop) (a b: A),
star R a b -> forall c, star R b c -> star R a c.
Proof.
induction 1; intros. auto. econstructor; eauto.
Qed.

One or several transitions: transitive closure of R.

Inductive plus (R: A -> A -> Prop): A -> A -> Prop :=
| plus_left: forall a b c,
R a b -> star R b c -> plus R a c.

Lemma plus_one:
forall (R: A -> A -> Prop) a b, R a b -> plus R a b.
Proof.
intros. apply plus_left with b. auto. apply star_refl.
Qed.

Lemma plus_star:
forall (R: A -> A -> Prop) a b,
plus R a b -> star R a b.
Proof.
intros. inversion H. eapply star_step; eauto.
Qed.

Lemma plus_star_trans:
forall (R: A -> A -> Prop) a b c, plus R a b -> star R b c -> plus R a c.
Proof.
intros. inversion H. eapply plus_left; eauto. eapply star_trans; eauto.
Qed.

Lemma star_plus_trans:
forall (R: A -> A -> Prop) a b c, star R a b -> plus R b c -> plus R a c.
Proof.
intros. inversion H0. inversion H. econstructor; eauto.
econstructor; eauto. eapply star_trans; eauto. econstructor; eauto.
Qed.

Lemma plus_trans:
forall (R: A -> A -> Prop) a b c, plus R a b -> plus R b c -> plus R a c.
Proof.
intros. eapply plus_star_trans; eauto. apply plus_star; auto.
Qed.

Lemma plus_right:
forall (R: A -> A -> Prop) a b c, star R a b -> R b c -> plus R a c.
Proof.
intros. eapply star_plus_trans; eauto. apply plus_one; auto.
Qed.

Absence of transitions.

Definition irred (R: A -> A -> Prop) (a: A) : Prop := forall b, ~(R a b).

Infinitely many transitions.

CoInductive infseq (R: A -> A -> Prop): A -> Prop :=
| infseq_step: forall a b,
R a b -> infseq R b -> infseq R a.

Coinduction principles to show the existence of infinite sequences.

Lemma infseq_coinduction_principle:
forall (R: A -> A -> Prop) (X: A -> Prop),
(forall a, X a -> exists b, R a b /\ X b) ->
forall a, X a -> infseq R a.
Proof.
intros R X P. cofix COINDHYP; intros.
destruct (P a H) as [b [U V]]. apply infseq_step with b; auto.
Qed.

Lemma infseq_coinduction_principle_2:
forall (R: A -> A -> Prop) (X: A -> Prop),
(forall a, X a -> exists b, plus R a b /\ X b) ->
forall a, X a -> infseq R a.
Proof.
intros.
apply infseq_coinduction_principle with
(X := fun a => exists b, star R a b /\ X b).
- intros.
destruct H1 as [b [STAR Xb]]. inversion STAR; subst.
destruct (H b Xb) as [c [PLUS Xc]]. inversion PLUS; subst.
exists b0; split. auto. exists c; auto.
exists b0; split. auto. exists b; auto.
- exists a; split. apply star_refl. auto.
Qed.

An example of use of infseq_coinduction_principle.

Lemma infseq_alternate_characterization:
forall (R: A -> A -> Prop) a,
(forall b, star R a b -> exists c, R b c) ->
infseq R a.
Proof.
intros R. apply infseq_coinduction_principle.
intros. destruct (H a) as [b Rb]. constructor.
exists b; split; auto.
intros. apply H. econstructor; eauto.
Qed.

A sequence is either infinite or stops on an irreducible term. This property needs excluded middle from classical logic.

Require Import Classical.

Lemma infseq_or_finseq:
forall (R: A -> A -> Prop) a, infseq R a \/ exists b, star R a b /\ irred R b.
Proof.
intros.
destruct (classic (forall b, star R a b -> exists c, R b c)).
left. apply infseq_alternate_characterization; auto.
right.
destruct (not_all_ex_not _ _ H) as [b P].
destruct (imply_to_and _ _ P) as [U V].
exists b; split. auto.
red; intros; red; intros. elim V. exists b0; auto.
Qed.

Additional properties for deterministic transition relations.

Section DETERMINISM.

Variable R: A -> A -> Prop.
Hypothesis R_determ: forall a b c, R a b -> R a c -> b = c.

Uniqueness of transition sequences.

Lemma star_star_inv:
forall a b, star R a b -> forall c, star R a c -> star R b c \/ star R c b.
Proof.
induction 1; intros.
auto.
inversion H1; subst. right. eapply star_step; eauto.
assert (b = b0). eapply R_determ; eauto. subst b0.
apply IHstar; auto.
Qed.

Lemma finseq_unique:
forall a b b',
star R a b -> irred R b ->
star R a b' -> irred R b' ->
b = b'.
Proof.
intros. destruct (star_star_inv H H1).
inversion H3; subst. auto. elim (H0 _ H4).
inversion H3; subst. auto. elim (H2 _ H4).
Qed.

Lemma infseq_star_inv:
forall a b, star R a b -> infseq R a -> infseq R b.
Proof.
induction 1; intros. auto.
inversion H1; subst. assert (b = b0). eapply R_determ; eauto. subst b0.
apply IHstar. auto.
Qed.

Lemma infseq_finseq_excl:
forall a b,
star R a b -> irred R b -> infseq R a -> False.
Proof.
intros.
assert (infseq R b). eapply infseq_star_inv; eauto.
inversion H2. elim (H0 b0); auto.
Qed.

End DETERMINISM.

End SEQUENCES.

Hint Resolve star_refl star_step star_one star_trans plus_left plus_one
plus_star plus_star_trans star_plus_trans plus_right: sequences.