A presentation about coinductive types (given at UPenn's PLClub)

coinduction.v

Require Arith.
Require Import List.
Import ListNotations.


(** * Coinductive types and coinduction *)















(** ** Infinite streams *)

CoInductive stream : Type :=
  Cons : nat -> stream -> stream.

(* Lazy data structure to represent infinite sequences of [nat]. *)



















(** ** A simple stream example *)

(* count_from n = Cons n (Cons (1+n) (Cons (2+n) (...))) *)
CoFixpoint count_from (n : nat) : stream :=
  Cons n (count_from (1 + n)).
(* ^
   Constructor guarding the recursive call to [count_from]
 *)




(** ** CoFixpoints don't reduce: they are lazy *)

Compute (count_from 0).
(* Nope! *)

(* Why it would be a bad idea to reduce:

   count_from 0

   = Cons 0 (count_from 1)

   = Cons 0 (Cons 1 (count_from 2))

   = Cons 0 (Cons 1 (Cons 2 (count_from 3)))

   = ...

  Ad infinitum.

  CoFixpoints, such as [count_from], must be normal forms.

 *)
















(** ** Lazy computation must be forced. *)

(** *** First element of a stream*)

Definition head (s : stream) : nat :=
  match s with
  | Cons i _ => i
  end.

(* head (count_from 0)

   = match count_from 0 with
     | Cons i _ => i
     end

     (* [match] "forces" [count_from], unfolding until the pattern matches. *)
   = match Cons 0 (count_from 1) with
     | Cons i _ => i
     end

   = 0
 *)

Compute (head (count_from 0)).
(* 0 *)













(** *** Elements remaining after the first *)

Definition tail (s : stream) : stream :=
  match s with
  | Cons _ s' => s'
  end.

Compute (head (tail (count_from 0))).
(* 1 *)

Compute (head (tail (tail (count_from 0)))).
(* 2 *)








(** ** Approximate streams finitely with lists *)

Fixpoint take (n : nat) (s : stream) : list nat :=
  match n with
  | O => []
  | S n' => head s :: take n' (tail s)
  end.

Compute take 10 (count_from 0).
(* [0; 1; 2; 3; 4; 5; 6; 7; 8; 9] *)


















(** ** Equality of streams *)

(* A variant of [count_from] which outputs two numbers before looping. *)
CoFixpoint count_from2 (n : nat) : stream :=
  Cons n (Cons (1 + n) (count_from2 (2 + n))).

















(** *** Comparing finite approximations *)

Compute take 10 (count_from 0).
(* [0; 1; 2; 3; 4; 5; 6; 7; 8; 9] *)

Compute take 10 (count_from2 0).
(* Same result *)


Lemma count_to_10_eq : take 10 (count_from 0) = take 10 (count_from2 0).
Proof. simpl. reflexivity. Qed.







(** ** Proof that the two streams are actually equal... fails. *)

Lemma count_from_eq : count_from 0 = count_from2 0.
Proof.
  (* Stuck... *) 
  (* unfold count_from. *) (* Doesn't help *)

  (* Problem 1: There is no way to unfold the cofixpoints
     in [count_from] and [count_from2]. *)

  (* Problem 2: The only closed normal form of type [_ = _] is [eq_refl]. *)

  (* Problem 3: Even assuming cofixpoints can be unfolded (which is sound),
     we cannot keep unfolding indefinitely: *)

Axiom unfold_count_from : forall n,
             count_from n = Cons n (count_from (1 + n)).

Axiom unfold_count_from2 : forall n,
             count_from2 n = Cons n (Cons (1 + n) (count_from2 (2 + n))).

  rewrite unfold_count_from, unfold_count_from2.
  f_equal.
  rewrite unfold_count_from.
  f_equal.
  simpl.

Abort.





















(** ** Take away *)

(* [=] in Coq is actually too strong a notion of equality for streams.

   We need to formalize a different one.
 *)















(** ** Formalizing stream equality *)

(** ** First solution: "Approximation equivalence" *)

(* Two streams are equal when all finite approximations are equal. *)
Definition eq_approx (s1 s2 : stream) : Prop
  := forall n, take n s1 = take n s2.








Import Arith.

Lemma count_from_eq : forall m, eq_approx (count_from m) (count_from2 m).
Proof.
  red.
  intros m n. revert m.
  induction n using lt_wf_ind. (* strong induction *)
  intros m.
  destruct n.
  - simpl. reflexivity.
  - simpl. f_equal. destruct n.
    + simpl. reflexivity.
    + simpl. f_equal.
      rewrite H.
      * reflexivity.
      * auto.
Qed.

(* Good: Simple definition *)
(* Bad:  Reasoning about fuel (n) *)

















(** ** Bisimilarity *)

Module Bisim1.

(* Intuitively a good notion of equality [≈] should satisfy:
[[
   s1 ≈ s2    ->     head s1 = head s2   (* nat *)
                  /\ tail s1 ≈ tail s2   (* stream *)
]]
   There are many relations which satisfy that implication.
   These relations are called _bisimulations_.
 *)

Definition is_bisimulation (bis : stream -> stream -> Prop) : Prop :=
  forall s1 s2 : stream,
    bis s1 s2 -> (head s1 = head s2 /\ bis (tail s1) (tail s2)).








(* We can consider two streams [s1] and [s2] "equal" when they are related by
   some bisimulation. We say [s1] and [s2] are (_strongly_) _bisimilar_.
 *)
Definition bisimilar (s1 s2 : stream) : Prop
  := exists bis, is_bisimulation bis /\ bis s1 s2.

Infix "≈" := bisimilar (at level 70) : bisim_scope.
Local Open Scope bisim_scope.

(* Equivalent formulations:

   - Bisimilarity is the union of bisimulations (viewed as sets of pairs);

   - Bisimilarity is the greatest bisimulation (for set inclusion).

 *)










Lemma count_from_eq : forall m, count_from m ≈ count_from2 m.
Proof.
  intros m.
  red.
  exists (fun s1 s2 =>
            exists m,
                 s1 = count_from m
              /\ (  s2 = count_from2 m
                 \/ s2 = Cons m (count_from2 (S m)))).
  split.
  - clear. red. intros s1 s2 [m [Hs1 Hs2]].
    destruct Hs2 as [Hs2 | Hs2].
    + subst s1 s2; simpl; eauto.
    + subst s1 s2; simpl; eauto.
  - eauto.
Qed.

(* To prove bisimilarity, we must find an explicit simulation.
   Already for [count_from2], that's pretty heavyweight.
 *)

End Bisim1.
























(** ** Paco (Parameterized Coinduction) *)

From Paco Require Import paco.

Module Bisim2.

(* When [≈] is bisimilarity, the following is actually an equivalence:
[[
   s1 ≈ s2   <->     head s1 = head s2   (* nat *)
                  /\ tail s1 ≈ tail s2   (* stream *)
]]
   Assimilating [<->] to an equality, we can view [≈] as a fixed point of a
   function [step] between relations:
[[
    (≈) <-> step(≈)
]]
 *)

Definition step (bis : stream -> stream -> Prop) : stream -> stream -> Prop
  := fun s1 s2 => head s1 = head s2 /\ bis (tail s1) (tail s2).

(* Paco gives us a greatest fixed point operator [paco2 _ bot2]: *)
Definition bisimilar : stream -> stream -> Prop := paco2 step bot2.

Infix "≈" := bisimilar (at level 70) : bisim_scope.
Local Open Scope bisim_scope.

(* This operator expects the function to be _monotone_ with respect to
   inclusion of relations. *)
Theorem monotone_step : monotone2 step.
Proof.
  red. intros s1 s2 bis bis' Hs Hbis.
  red in Hs. red.
  split.
  apply Hs.
  apply Hbis.
  apply Hs.
Qed.

Hint Resolve monotone_step : paco.

(* There are three main tactics in paco.

   The first two are applications of the definition of a fixed point [R].
[[
  R = step R
]]
   In particular, here [R = paco2 step bot2].

   1. [punfold H]:
        an assumption       [H : paco2 step bot2]
        becomes (roughly)   [H : step (paco2 step bot2)];

   2. [pfold]:
        the goal            [paco2 step bot2]
        becomes (roughly)   [step (paco2 step bot2)];

   And the last important one:

   3. [pcofix]:
        applies the "coinduction principle" for the greatest fixed point.
 *)

Theorem bisimilarity : Bisim1.is_bisimulation bisimilar.
Proof.
  red.
  intros s1 s2 Hs.

  (* bisimilar s1 s2
     =  paco2 step bot2 s1 s2
     -> step (paco2 step bot2) s1 s2 *)  
  punfold Hs.

  fold (step bisimilar s1 s2).
  eapply monotone_step; eauto.
  intros. (* red in PR. *) pclearbot; auto.
Qed.







(** Bisimilarity of [count_from] and [count_from2],
    for the third and last time. *)

Lemma count_from_eq : forall m, count_from m ≈ count_from2 m.
Proof.
  red.
  pcofix CIH.
  intros.
  pfold. red. split.
  (* ^ one step *)
  - simpl. reflexivity.
  - simpl. red.
    (* right *)
    left.
    pfold. red. split.
    (* ^ one more step *)
    + reflexivity.
    + simpl. red. right. apply CIH.
Qed.

(* No explicit simulation relation to define! *)

End Bisim2.


























(** ** Duality between inductive and coinductive types *)

(* Constructor: [Cons]
   Destructors: [head]/[tail] *)



(* Positive types: - defined by     constructors
                   - works well for inductive types

   Negative types: - defined by     destructors
                   - works well for coinductive types
 *)

CoInductive stream' : Type :=
  { head' : nat
  ; tail' : stream'
  }.

CoInductive stream'' : Type :=
  { unstream : option (nat * stream') }.


Lemma Foo : forall s : stream, s = match s with
                                   | Cons i s' => Cons i s'
                                   end.
Proof.
  intros s.
  destruct s.
  reflexivity.
Defined.

Compute (Foo (count_from 0) : count_from 0 = Cons 0 (count_from 1)).
Fail Check (eq_refl : count_from 0 = Cons 0 (count_from 1)).

Definition Cons' (i : nat) (s : stream') : stream' :=
  {| head' := i
  ;  tail' := s
  |}.





CoFixpoint count_from' (n : nat) : stream' :=
  Cons' n (count_from' (1 + n)).

(* Exactly the same thing *)
CoFixpoint count_from'' (n : nat) : stream' :=
  {| head' := n
  ;  tail' := count_from'' (1 + n)
  |}.







(** ** Fixpoints vs Cofixpoints *)

(** *** Fixpoint = algebra *)

(* One [Fixpoint] to rule them all: we "iterate" _algebras_ to "fold"
   finite objects. *)      (* ↓ this function is called an algebra *)
Fixpoint nat_fold {A : Type} (f : unit + A -> A) (n : nat) : A
  := match n with
     | O => f (inl tt)
     | S n' => f (inr (nat_fold f n'))
     end.

About nat_fold.


(* Algebras of [nat] *)
Module Algebra.

Inductive nat : Type :=
| O : nat
| S : nat -> nat
.

(* [Variant] for nonrecursive sum types. *)
Variant natF (A : Type) : Type :=
| OF : natF A
| SF : A -> natF A
.

(* [unit + A -> A] is isomorphic to [natF A -> A] *)

End Algebra.

Definition fibonacci_algebra : unit + (nat * nat) -> nat * nat
  := fun i =>
       match i with
       | inl tt =>
         (* fibonacci 0, fibonacci 1 *)
         (0, 1)
       | inr (fib_n, fib_n1) =>
         (* fibonacci (1+n), fibonacci (2+n) *)
         (fib_n1, fib_n + fib_n1)
       end.

Definition fibonacci (n : nat) := fst (nat_fold fibonacci_algebra n).

Compute (map fibonacci [0;1;2;3;4;5]).
(* [0; 1; 1; 2; 3; 5] *)




















(** *** Cofixpoint = coalgebra *)

(* One [CoFixpoint] to rule them all: we "iterate" _coalgebras_ to "unfold"
   infinite objects. *)           (* ↓ this function is called a coalgebra *)
CoFixpoint stream_unfold {A : Type} (f : A -> nat * A) (a : A) : stream'
  := let (n, a') := f a in
     {| head' := n
     ;  tail' := stream_unfold f a'
     |}.

(* Coalgebras of [stream] *)
Module Coalgebra.

CoInductive stream : Type :=
  { head : nat
  ; tail : stream
  }.

(* [Record] for nonrecursive product types. *)
Record streamF (A : Type) : Type :=
  { headF : nat
  ; tailF : A
  }.

(* [A -> nat * A] is isomorphic to [A -> streamF A] *)

End Coalgebra.




(* Algebra (for nat):        unit + A -> A
                i.e.,        option A -> A

   Coalgebra (for stream):   A -> nat * A
 *)



Definition count_from_coalgebra : nat -> nat * nat
  := fun n => (n, 1 + n).

Definition count_from3 : nat -> stream'
  := stream_unfold count_from_coalgebra.





About nat_fold.      (* forall A, (unit + A -> A) -> (nat -> A)    *)
About stream_unfold. (* forall A, (A -> nat * A)  -> (A -> stream) *)



(* Category theory has concepts to talk generally and formally
   about fixpoints and cofixpoints:

   - [nat] defines an initial algebra
   - [stream] defines a final coalgebra
 *)



























Module Duality.
(* Just reproducing the definitions next to each other. *)

Fixpoint nat_fold {A : Type} (f : unit + A -> A) (n : nat) : A
  := match n with
     | O => f (inl tt)
     | S n' => f (inr (nat_fold f n'))
     end.

CoFixpoint stream_unfold {A : Type} (f : A -> nat * A) (a : A) : stream'
  := let (n, a') := f a in
     {| head' := n
     ;  tail' := stream_unfold f a'
     |}.




(** ** Pattern-matching is symmetric to record construction *)

(*
   - Pattern-matching _destructs_,
     must be exhaustive in _constructors_ of [nat].
   - Records, or copatterns, _construct_,
     must be exhaustive in _destructors_ (or observations) of [stream].
 *)

(* Like patterns, copatterns can be nested. *)
CoFixpoint count_from2' (n : nat) : stream' :=
  {| head' := n
  ;  tail' := 
       {| head' := (1 + n)
       ;  tail' := count_from2' (2 + n)
       |}
  |}.



(* Induction                  Coinduction

   Structural recursion       Structural recursion

   Termination                Productivity

   Initial algebras           Final coalgebras

   Least fixed points         Greatest fixed points

   Patterns                   Copatterns
 *)

End Duality.

(** ** The end **)














(**)































(** ** Equivalence of bisimilarity and approximation equivalence. *)

Import Bisim1.

(* A bisimulation ensures that two related streams have the same
   approximations. *)
Theorem bisimilar_approx (s1 s2 : stream) :
  bisimilar s1 s2 -> eq_approx s1 s2.
Proof.
  intros Hs.
  red in Hs.
  destruct Hs as [bis [BISIM Hs]].
  red.
  intros n.
  revert s1 s2 Hs.
  induction n.
  - intros. simpl. reflexivity.
  - intros. simpl. red in BISIM.
    f_equal.
    + apply BISIM; auto.
    + apply IHn, BISIM; auto.
Qed.

(* And conversely, approximation equivalence is itself a bisimulation. *)
Theorem approx_bisimilar (s1 s2 : stream) :
  eq_approx s1 s2 -> bisimilar s1 s2.
Proof.
  intros Hx.
  red.
  exists eq_approx.
  split.
  2: assumption.
  clear. red. intros s1 s2 Hs.
  red in Hs.
  split.
  + specialize (Hs 1). simpl in Hs. inversion Hs; auto.
  + red. intros n. specialize (Hs (S n)). simpl in Hs. inversion Hs; auto.
Qed.