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.

Module Coinduction