Module Coinduction

Appendix: comparing inductive and coinductive defitions

Require Import SfLib.

Inductive natinf : Type :=
| Fin: nat -> natinf
| Inf: natinf.

Definition succ (x: natinf) : natinf :=
match x with
| Fin a => Fin (S a)
| Inf => Inf
end.

Consider the following two inference rules, intended to define a predicate even over the type natinf (natural numbers extended with a point at infinity).
```                             even n
even 0             ------------------
even(succ(succ n))```
It is clear that the predicate even must satisfy the following specification:

Definition even_spec (even: natinf -> Prop) : Prop :=
forall n, even n <-> (n = Fin 0 \/ exists m, n = succ(succ m) /\ even m).

However, there are several predicates satisfying even_spec.

Definition even_1 (x: natinf) : Prop :=
exists m, x = Fin(m + m).

Definition even_2 (x: natinf) : Prop :=
x = Inf \/ even_1 x.

Lemma even_1_satisfies_spec:
even_spec even_1.
Proof.
unfold even_spec, even_1.
firstorder.
subst n. destruct x.
left. auto.
right. exists (Fin (x + x)). split.
simpl. f_equal. omega.
exists x; auto.
subst n. exists 0; auto.
subst x. subst n. simpl. exists (S x0). f_equal. omega.
Qed.

Lemma even_2_satisfies_spec:
even_spec even_2.
Proof.
unfold even_spec, even_2. intros.
generalize (even_1_satisfies_spec n).
firstorder.
subst n. right. exists Inf; auto.
subst x. simpl in H2. auto.
Qed.

When we transcribe the inference rules as a Coq inductive predicate, what we get is the smallest (least defined) predicate satisfying even_spec.

Inductive even: natinf -> Prop :=
| even_0: even (Fin 0)
| even_succ: forall n, even n -> even (succ (succ n)).

Lemma even_satisfies_spec:
even_spec even.
Proof.
unfold even_spec. intro. split.
intros. inversion H.
left; auto.
right. exists n0. auto.
intros [A | [m [B C]]].
subst n. apply even_0.
subst n. apply even_succ; auto.
Qed.

Lemma even_smallest_fixpoint:
forall (P: natinf -> Prop), even_spec P ->
forall n, even n -> P n.
Proof.
unfold even_spec; intros P FIXPOINT.
induction 1.
rewrite FIXPOINT. auto.
rewrite FIXPOINT. right. exists n; auto.
Qed.

Alternatively, we can ask Coq to define a coinductive predicate. Note that the two constructors have exactly the same types in even and coeven.

CoInductive coeven: natinf -> Prop :=
| coeven_0: coeven (Fin 0)
| coeven_succ: forall n, coeven n -> coeven (succ (succ n)).

coeven satisfies the specification just like even.
Lemma coeven_satisfies_spec:
even_spec coeven.
Proof.
unfold even_spec. intro. split.
intros. inversion H.
left; auto.
right. exists n0. auto.
intros [A | [m [B C]]].
subst n. apply coeven_0.
subst n. apply coeven_succ; auto.
Qed.

However, coeven is a different predicate than even. Indeed, coeven Inf holds.

Lemma Inf_coeven:
coeven Inf.
Proof.
cofix COINDHYP.
change Inf with (succ (succ Inf)).
apply coeven_succ.
apply COINDHYP.
Qed.

... while even Inf does not hold.

Lemma Inf_not_even:
~(even Inf).
Proof.
red. intros.
assert (even_1 Inf).
apply even_smallest_fixpoint.
apply even_1_satisfies_spec.
auto.
red in H0. destruct H0 as [m EQ]. congruence.
Qed.

coeven is actually the greatest (most defined) predicate that satisfies even_spec.

Lemma coeven_greatest_fixpoint:
forall (P: natinf -> Prop), even_spec P ->
forall n, P n -> coeven n.
Proof.
unfold even_spec; intros P FIXPOINT.
cofix COINDHYP. intros.
rewrite FIXPOINT in H.
destruct H as [A | [m [B C]]].
subst n. apply coeven_0.
subst n. apply coeven_succ. apply COINDHYP. auto.
Qed.