```{-
Mixing induction and coinduction in Agda
Thorsten Altenkirch

(based on joint work with Nils Anders Danielsson)

School of Computer Science
University of Nottingham

-}

module Tallinn10 where
open import Relation.Binary.PropositionalEquality
open import Relation.Nullary
open import Data.Nat hiding (_+_)

{- 0. Introducing Agda -}

{- To see the inductive definition of Nat, just click on it. -}

{- We can define programs by structural recursion: -}
_+_ : ℕ → ℕ → ℕ
zero + n = n
suc n + n' = suc (n + n')
{- If we replace the last line by
suc n + n' = suc ((suc n) + n')
the termination checker will complain. -}

{- We can do proofs by structural recursion. -}
+0 : (n : ℕ) → n + zero ≡ n
+0 zero = refl
+0 (suc n) = cong suc (+0 n)

+suc : (m n : ℕ) → m + (suc n) ≡ suc (m + n)
+suc zero n = refl
+suc (suc m) n = cong suc (+suc m n)

+-comm : (m n : ℕ) → m + n ≡ n + m
+-comm m zero    = +0 m
+-comm m (suc n) = trans (+suc m n) (cong suc (+-comm m n))

{- +-comm always retruns refl, hence running it is useless.
A more interesting example is the proof of decidability of
equality for natural numbers. -}

_≡?_ : (m n : ℕ) → Dec (m ≡ n)
zero ≡? zero = yes refl
zero ≡? suc n = no (λ ())
suc n ≡? zero = no (λ ())
suc n ≡? suc m with n ≡? m
suc n ≡? suc m | yes p = yes (cong suc p)
suc n ≡? suc m | no ¬p = no (λ sn≡sm → ¬p (cong pred sn≡sm))

{- ≤ is defined inductively (click on the symbol)
we can prove properties by structural recursion over this definition.
-}

≤-trans : ∀ {l m n} → l ≤ m → m ≤ n → l ≤ n
≤-trans z≤n m≤n = z≤n
≤-trans (s≤s m≤n) (s≤s n≤n') = s≤s (≤-trans m≤n n≤n')

{- 1. Coinductive definitions, eg. Streams -}

open import Coinduction

infixr 5 _∷_

{- We define "coinductive types" like streams by using
∞, where ∞ A stands for the type of delayed computations
of type A. -}

data Stream (A : Set) : Set where
_∷_ : (x : A) (xs : ∞ (Stream A)) → Stream A

{- ∞ comes with two basic operations:
-- ♯ : A → ∞ A (delay)
-- ♭ : ∞ A → A (force)
-}

{- e.g. using ♯ we can define a function computing the stream of natural
numbers starting with n. Note that this recursion is permitted because the
recursive call is guarded by ♯.
The termination checker views functions with coinductive results as functions
with an additionional (virtual) argument which gets decreased each time
♯ is used.
-}

from : ℕ → Stream ℕ
from n = n ∷ (♯ from (suc n))

{- defining head and tail, not that we use ♭ in tail. -}

head : ∀ {A} → Stream A → A
head (a ∷ as) = a

tail : forall {A} → Stream A → Stream A
tail (x ∷ xs) = ♭ xs

{- bad is not guarded. The termination checker will refuse to accept
this program because the recursive call is inside the call to tail
and tail does not preserve guardedness. -}

{-
bad :  ℕ → Stream ℕ
-}

infixr 4 _~_

{- We define equality of streams which is called "bisimilarity"
The idea is two streams are equal if there is a stream of equality proofs
showing that any two corresponding elements are equal. Indeed, we have to
use ∞ in the definition of ~.
-}

data _~_ {A} : (xs ys : Stream A) → Set where
_∷_ : ∀ {x y} {xs ys} → x ≡ y → ∞ (♭ xs ~ ♭ ys) → x ∷ xs ~ y ∷ ys

{- As an example of a proof involving ~ we show that from (suc n)
is the same as map suc (from n) where map is defined below.
-}

map : ∀ {A B} → (A → B) → Stream A → Stream B
map f (x ∷ xs) = f x ∷ ♯ map f (♭ xs)

fromLem : (n : ℕ) → from (suc n) ~ map suc (from n)
fromLem n = refl ∷ (♯ fromLem (suc n))

{- We compare ~ with the traditional definition using bisimulations: -}

record Bisim {A : Set}(_R_ : Stream A → Stream A → Set) : Set where
field
hd : ∀ {as bs} → as R bs → head as ≡ head bs
tl : ∀ {as bs} → as R bs → tail as R tail bs

{- If we switch off uinverse checking, i.e. put
{-#  OPTIONS --type-in-type #-}
on the top of the file we can define ~' as the largest bisimulation:

data _~'_ {A} : (xs ys : Stream A) → Set where
bisim : ∀ {x y : Stream A}(_R_ : Stream A → Stream A → Set)
→ Bisim _R_ → x R y → x ~' y

I would argue that the 1st definition of ~ is simpler, easier to use
and doesn't require impredicativity.
-}

{- The next function is an example of a function which is actually total
but the termination checker fails to recognize this.
-}
{-
bad' : ℕ → Stream ℕ
-}

{- 2. Mixed definitions, e.g. SP -}

{- We define the type of stream processors SP A B
representing functions from Stream A to Stream B.
SP is used inductively for the first constructor and
coinductively -}

data SP (A B : Set) : Set where
get  : (A → SP A B)    → SP A B
put  : B → ∞ (SP A B)  → SP A B

{-
On the top level mixed definitions correspond to nested ν μ
in the categorical sense. E.g.
SP A B = ν X.μ Y. (A → Y) + (B × X)
more general:
data A = F (A , ∞ A)
means A = ν X.μ Y.F(Y,X)
-}

{- As an example: the function pure produces a stream processor that
applies a function f pointweise to a strams. -}

pure : ∀ {A B} → (A → B) → SP A B
pure f = get (λ a → put (f a) (♯ (pure f)))

{- A more interesting example is the semantics of a stream processor as
a function. -}

⟦_⟧ : ∀ {A B} → SP A B → Stream A → Stream B
--                                    ℕ → B
⟦ get f     ⟧ (a ∷ as)  = ⟦ f a ⟧ (♭ as)
⟦ put b sp  ⟧ as        = b ∷ ♯ ⟦ ♭ sp ⟧ as

{- The definition uses a lexical product of the inductive order on get
and the coinductive order implied by the fact that the result type
is stream. This can be visualized by viewing streams as functions
over the natural numbers.
-}

{- Two other examples are the two possible definitions of composition
of stream processor.
The reader is invited to derive both from categorical combinators
fold, unfold to realize how much effort is saved by using Agda.
-}

-- match left: data driven
_>>>_ : ∀ {A B C} → SP A B → SP B C → SP A C
get f >>> tq = get (λ a → f a >>> tq)
put a sp >>> get f = ♭ sp >>> f a
put a sp >>> put b tq = put b (♯ put a sp >>> ♭ tq)

-- match right: demand driven
_>>>'_ : ∀ {A B C} → SP A B → SP B C → SP A C
get g >>>' get f = get (λ a → g a >>>' get f)
put b sp >>>' get f = ♭ sp >>>' f b
sp >>>' put c tq = put c (♯ (sp >>>' ♭ tq))

{- An example for a mixed definition of a relation is the definition of
weak bisimilarity for the partiality monad. -}

{- A ν represents (possibly non-terminating) computations over A. -}
data _ν (A : Set) : Set where
now    : A        → A ν
later  : ∞ (A ν)  → A ν

⊥ : ∀ {A} → A ν
⊥ = later (♯ ⊥)

infix 4 _≈_

{- We identify two computations which only differ by a finite amount
of laters. This leads naturally to a mixed coinductive/inductive
definition since the cogruence for later has to be coinductive
while the rules introducing finite delay have to be inductive.
-}
data _≈_ {A : Set} : A ν → A ν → Set where
now     : ∀ {v}                         → now v    ≈ now v
later   : ∀ {x y} → ∞ (  ♭  x  ≈ ♭  y) → later x  ≈ later y
laterʳ  : ∀ {x y} →         x  ≈ ♭  y   → x        ≈ later y
laterˡ  : ∀ {x y} →      ♭  x  ≈    y   → later x  ≈ y

{- 3. The nesting problem -}

{- Finally, we discuss an issue which arises when nesting coinductive
definitions inside inductive ones. -}

{- Consider the type below which allows only a finite number of [0]
in between any two [1]s. However, there can be infinitely many [0]s
alltogether, e.g. the infinite sequnce 0,1,0,1... -}

data O∞ : Set where
[0] : O∞ → O∞
[1] : ∞ O∞ → O∞

[01]∞ : O∞
[01]∞ = [0] ([1] (♯ [01]∞))

{- we read this as ν X.μ Y.[0]:Y + [1]:X -}

{- What happens, if we switch the quantfiers?
O = μ Y.ν X.[0]:Y + [1]:X
corresponds to sequences which may only contain a finite number
of 0s, ever sequence will end with an infinite sequence of 1s.

In particular, we should not be able to define 0,1,0,1,...
However, when we try to encode this in Agda something strange happens.
-}

{- We use a parametrized definition for the inside
O = μ Y. Z O
where Z O = ν X.[0]:O + [1]:X
-}
data Z (O : Set) : Set where
[0] : O    → Z O
[1] : ∞ (Z O) → Z O

data O : Set where
↓ : Z O → O

{- However, we are still able to define the infinite sequence 0,1,0,1,.. -}

01^ω : O
01^ω = ↓ ([1] (♯ [0] 01^ω))

{- The termination checker considers this definition as guarded, because
indeed the recursive call is guarded by ♯. However, the ♯ was intended
to be used for recursive definitions only involving Z O not O as well.
-}

{- On the other hand the termination checker doesn't allow us
to derive the fold for O. Here is an attempt: -}
{-
mutual
Ofold : ∀ {A} → (Z A → A) → O → A
Ofold f (↓ x) = f (ZmapOfold f x)
--  Ofold f (↓ x) = f (Zmap (Ofold f) x)

ZmapOfold : ∀ {A} → (Z A → A) → Z O → Z A
ZmapOfold f ([0] x) = [0] (Ofold f x)
ZmapOfold f ([1] x) = [1] (♯ ZmapOfold f (♭ x))
-}
-- if we could define Ofold, we would have a diverging computation.
-- however, the termination checker doesn't accept this definition
-- because there are recursive paths Ofold --> Ofold which pass
-- through #.

-- we would prefer the dual: 01^ω should be rejected but Ofold
-- should be accepted.

{- 4. References:
All jointly with Nils Anders Danielsson.

Mixing Induction and Coinduction