{-
               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  _∷_

{- 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 ℕ
bad n = n ∷ ♯ tail (bad (suc n))
-}

infixr  _~_

{- 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 ℕ
bad' n = n ∷ ♯ map suc (bad' n)
-}

{- 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  _≈_

{- 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
http://www.cs.nott.ac.uk/~nad/publications/danielsson-altenkirch-mixing.html

Subtyping, Declaratively - An Exercise in Mixed Induction and Coinduction
http://www.cs.nott.ac.uk/~txa/publ/danielsson-altenkirch-subtyping.pdf
(to appear in MPC 2010)

Termination Checking Nested Inductive and Coinductive Types
http://www.cs.nott.ac.uk/~txa/publ/InvertedQuantifiers.pdf
(to be presented at PAR 2010)

-}