Sequences
Xavier Leroy's Sequences Library
Set Implicit Arguments.
Require Import Classical.
Section SEQUENCES.
Variable A: Type. (**r the type of states *)
Variable R: A → A → Prop. (**r the transition relation, from one state to the next *)
Finite sequences of transitions
Inductive star: A → A → Prop :=
| star_refl: ∀ a,
star a a
| star_step: ∀ a b c,
R a b → star b c → star a c.
Lemma star_one:
∀ (a b: A), R a b → star a b.
Proof.
eauto using star.
Qed.
Lemma star_trans:
∀ (a b: A), star a b → ∀ c, star b c → star a c.
Proof.
induction 1; eauto using star.
Qed.
One or several transitions: transitive closure of R.
Inductive plus: A → A → Prop :=
| plus_left: ∀ a b c,
R a b → star b c → plus a c.
Lemma plus_one:
∀ a b, R a b → plus a b.
Proof.
eauto using star, plus.
Qed.
Lemma plus_star:
∀ a b,
plus a b → star a b.
Proof.
intros. inversion H. eauto using star.
Qed.
Lemma plus_star_trans:
∀ a b c, plus a b → star b c → plus a c.
Proof.
intros. inversion H. eauto using plus, star_trans.
Qed.
Lemma star_plus_trans:
∀ a b c, star a b → plus b c → plus a c.
Proof.
intros. inversion H0. inversion H; eauto using plus, star, star_trans.
Qed.
Lemma plus_right:
∀ a b c, star a b → R b c → plus a c.
Proof.
eauto using star_plus_trans, plus_one.
Qed.
Infinite sequences of transitions
However, this is not the notion we are trying to characterize: that, starting
from a, there exists one infinite sequence of transitions
a --> a1 --> a2 --> ... → aN → ....
Indeed, consider A = nat and R such that R 0 0 and R 0 1.
all_seq_inf 0 does not hold, because a sequence 0 -->* 1 cannot be extended.
Yet, R admits an infinite sequence, namely 0 --> 0 --> ....
Another attempt would be to represent the sequence of states
a0 --> a1 --> a2 --> ... → aN → ... explicitly, as a function
f: nat → A such that f i is the i-th state ai of the sequence.
This is a correct characterization of the existence of an infinite sequence
of reductions. However, it is very inconvenient to work with this definition
in Coq's constructive logic: in most use cases, the function f is not
computable and therefore cannot be defined in Coq.
To obtain a practical definition of infinite sequences, we use the following
coinductive definition of the predicate infseq a.
An inductive predicate such as star a b holds iff there exists a finite
derivation of the conclusion star a b that uses the constructors
star_refl and star_step a finite number of times.
A coinductive predicate is similar, but holds iff there exists a finite
OR INFINITE derivation of the conclusion that uses the constructors
of the predicate a finite OR INFINITE number of times.
In other words, an inductive predicate is a smallest fixpoint: the smallest predicate
that satisfies its constructors; a coinductive predicate is a greatest fixpoint:
the largest predicate that satisfies its constructors.
The infseq predicate above must be defined coinductively. Indeed, if
we define it inductively, the predicate would be empty (always false),
since there are no base cases!
Coq provides some primitive support for constructing infinite derivations
of facts such as infseq a. Such constructions are proofs by coinduction.
For example, we can prove the following:
Remark cycle_infseq:
∀ a, R a a → infseq a.
Proof.
intros. cofix COINDHYP. apply infseq_step with a. auto. apply COINDHYP.
Qed.
This style of proof by coinduction, using the cofix tactic, is effective
but can run into limitations of Coq's proof engine (the so-called
"guard condition"). However, we can derive more conventional
coinduction principles that are often easier to use.
Consider a set X of states A, that is, a predicate X: A → Prop.
Assume that for every a in X, we can make one R transition to a b
that is still in X. Then, starting from a in X, we can transition
to some a1 in X, then to some a2 still in X, then... It is clear
that we are just building an infinite sequence of transitions starting from
a. Therefore infseq a should hold. Let's prove this!
Lemma infseq_coinduction_principle:
∀ (X: A → Prop),
(∀ a, X a → ∃ b, R a b ∧ X b) →
∀ a, X a → infseq a.
Proof.
intros X P. cofix COINDHYP; intros.
destruct (P a H) as [b [U V]]. apply infseq_step with b; auto.
Qed.
An even more useful variant of this coinduction principle considers a
set X where for every a in X, we can make one *or several* transitions
to reach a b in X.
Lemma infseq_coinduction_principle_2:
∀ (X: A → Prop),
(∀ a, X a → ∃ b, plus a b ∧ X b) →
∀ a, X a → infseq a.
Proof.
intros.
apply infseq_coinduction_principle with
(X := fun a ⇒ ∃ b, star 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.
∃ b0; split. auto. ∃ c; auto.
+ ∃ b0; split. auto. ∃ b; auto.
- ∃ a; split. apply star_refl. auto.
Qed.
Here is an example of use of infseq_coinduction_principle:
if all finite transition sequences starting at a can be extended,
infseq a holds.
Lemma infseq_if_all_seq_inf:
∀ a, all_seq_inf a → infseq a.
Proof.
apply infseq_coinduction_principle.
intros. destruct (H a) as [b Rb]. constructor.
∃ b; split; auto.
unfold all_seq_inf; intros. apply H. apply star_step with b; auto.
Qed.
Likewise, the function-based characterization infseq_with_function
implies infseq.
Lemma infseq_from_function:
∀ a, infseq_with_function a → infseq a.
Proof.
apply infseq_coinduction_principle.
intros. destruct H as [f [P Q]].
∃ (f 1); split.
subst a. apply Q.
∃ (fun n ⇒ f (1 + n)); split. auto. intros. apply Q.
Qed.
Consider the transition sequences starting at state a.
They can be infinite, or they can be finite: after a number of transitions,
we reach a state from with no transition is possible. It is intuitively
obvious that at least one of the two cases must hold.
It is however impossible to prove this fact in Coq's constructive logic.
Indeed, a constructive proof would be isomorphic (by the Curry-Howard isomorphism)
to a terminating function that solves Turing's halting problem!
To prove this fact, we must enrich Coq with axioms from classical logic,
namely the axiom of excluded middle: for all propositions P,
either P or ¬P hold. The Coq standard library provides such axioms
in the module named Classical, which we imported above.
Definition irred (a: A) : Prop := ∀ b, ~(R a b).
Lemma infseq_or_finseq:
∀ a, infseq a ∨ ∃ b, star a b ∧ irred b.
Proof.
intros.
destruct (classic (∀ b, star a b → ∃ c, R b c)).
- left. apply infseq_if_all_seq_inf; auto.
- right.
apply not_all_ex_not in H. destruct H as [b P].
apply imply_to_and in P. destruct P as [U V].
∃ b; split. auto.
red; intros; red; intros. elim V. ∃ b0; auto.
Qed.
Determinism properties for functional transition relations.
Uniqueness of finite transition sequences.
Lemma star_star_inv:
∀ a b, star a b → ∀ c, star a c → star b c ∨ star c b.
Proof.
induction 1; intros.
- auto.
- inversion H1; subst.
+ right. eauto using star.
+ assert (b = b0) by (eapply R_functional; eauto). subst b0.
apply IHstar; auto.
Qed.
Lemma finseq_unique:
∀ a b b',
star a b → irred b →
star a b' → irred 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.
A state cannot both diverge and terminate on an irreducible state.
Lemma infseq_star_inv:
∀ a b, star a b → infseq a → infseq b.
Proof.
induction 1; intros.
- auto.
- inversion H1; subst.
assert (b = b0) by (eapply R_functional; eauto). subst b0.
apply IHstar; auto.
Qed.
Lemma infseq_finseq_excl:
∀ a b,
star a b → irred b → infseq a → False.
Proof.
intros.
assert (infseq b) by (eapply infseq_star_inv; eauto).
inversion H2. elim (H0 b0); auto.
Qed.
If there exists an infinite sequence of transitions from a,
all sequences of transitions arising from a are infinite.
Lemma infseq_all_seq_inf:
∀ a, infseq a → all_seq_inf a.
Proof.
intros. unfold all_seq_inf. intros.
assert (infseq b) by (eapply infseq_star_inv; eauto).
inversion H1. subst. ∃ b0; auto.
Qed.
End SEQUENCES.