{- Computer Aided Formal Reasoning (G53CFR, G54CFR) Thorsten Altenkirch Lecture 15: Coinductive definitions In this lecture we look at infinite structures, in particular streams which are infinite sequences (similar to lists which are finite sequences). We are using Agdas type of delayed computations (∞ A) to represent infinite structures. Applying the Curry-Howard isomorphism we can also represent infinite proofs. We are using this to define bisimilarity, i.e. extensional equality of streams. -} module l15 where open import Coinduction open import Data.Nat open import Data.List open import Relation.Binary.PropositionalEquality {- Agda doesn't permit the construction of infinite lists (as in Haskell) because lists are defined inductively, hence all lists must be constructable with a finite amount of constructors. As a consequence Agda rejects the following program: from : ℕ → List ℕ from n = n ∷ from (suc n) -} {- To represent infinite sequences we define the type of streams using ∞ X which represents "delayed computations of X". Because we are not constructing the whole stream now we can represent an infinite objects. This is reminiscent of the definition of a function - we don't calculate its values yet but only when required. -} infix 5 _∷_ data Stream (A : Set) : Set where _∷_ : A → ∞ (Stream A) → Stream A {- ∞ comes with two basic operations ♯ : A → ∞ A (delay, turn a term into a delayed computation) ♭ : ∞ A → A (forcing a delayed computation to evaluate) ∞ = \infty, ♯ = \sharp, ♭ = \flat -} {- We can now define ℕ by delaying the recursive computation of the tail of the stream.-} from : ℕ → Stream ℕ from n = n ∷ ♯ (from (suc n)) {- We can access the tails of the stream using: -} tail : ∀ {A} → Stream A → Stream A tail (a ∷ as) = ♭ as {- Or more generally we can obtain a list of the first n elements of a stream. -} taken : ∀ {A} → Stream A → ℕ → List A taken (a ∷ as) zero = [] taken (a ∷ as) (suc n) = a ∷ taken (♭ as) n {- Try "taken (from 0) 10" -} {- It is important that a recursive definition computing a stream (such as from) is "productive", i.e. whenever we want to access any component of the stream we can do this by forcing previously delayed computation. -} {- The following is an example of a non-productive definition which is rejected by Agda bad : Stream ℕ bad = 0 ∷ (♯ (tail bad)) While we can compute the head of bad (0) we cannot calculate its tail, because it is just defined by itself (bad recursion). Agda recognizes productive definitions, if they are "guarded". I.e. ♯ guards a recursive call and there are only constructors in between ♯ and the recursive call, not arbitrary functions like tail. Note that there are cases of productive definitions which are not guarded. Agda will reject them and we have to find another way to calculate the result. This is similar to recursive definitions which are structurally recursive but this is not always recognized by Agda. -} {- Let's prove a simple theorem about "from". First of all we notice that Stream like List is a "functor", i.e. we can "map" a function over a stream: -} mapStream : {A B : Set} → (A → B) → Stream A → Stream B mapStream f (a ∷ as) = f a ∷ ♯ (mapStream f (♭ as)) {- "mapStream f as" applies the function f to each of the components of as. Note that the definition of mapStream is guarded and that each time we force the output (i.e. force the delayed computation "♯ (mapStream f (♭ as)") this will in turn force further computation of the input by evaluating "♭ as". -} {- The theorem we want to prove is that mapping suc to from n is the "same" as from (suc n): (n : ℕ) → mapStream suc (from n) ≡ from (suc n) However, we are unable to prove the theorem in the above form. The reason is that Agdas propositional equality (≡) is too "intensional". Consider "mapStream suc (from zero)" this evaluates to something like "1 ∷ .l15.♯-2 suc 0 (.l15.♯-0 0)" "from (suc zero)" this evaluates to something like "1 ∷ .l15.♯-0 1" While the heads of the streams (1) are clearly definitionally equal the tails are different delayed computation. Moreover both expressions are closed and hence the only way to prove "mapStream suc (from zero) ≡ from (suc zero)" would be by refl but this is only possible if they are definitionally equal. Hence we need a different "extensional" equality for streams. This equality should identify two streams which have identical components. The main idea for the definition is to apply the idea of a delayed computation into the delayed computation of a stream. Hence we define: -} infix 4 _~_ data _~_ {A} : (xs ys : Stream A) → Set where _∷_ : ∀ {x y xs ys} → (x ≡ y) → ∞ (♭ xs ~ ♭ ys) → x ∷ xs ~ y ∷ ys {- The idea is that to prove that two streams are equal we show that the heads are equal and provide a delayed computation proving that the tails are equal. -} infix 4 _≈_ {- The definition used in the Agda library gets rid of the equality proofs by noting that we can just identitfy x and y. It is easy to show that both are equivalent. -} data _≈_ {A} : (xs ys : Stream A) → Set where _∷_ : ∀ x {xs ys} (xs≈ : ∞ (♭ xs ≈ ♭ ys)) → x ∷ xs ≈ x ∷ ys {- For historic reasons the relation _≈_ is called "bisimularity" because it is conventionally defined via "bisimulation". Our definition using Curry-Howard and the idea of a delayed computation is an alternative. -} {- It is now surprisingly easy to prove the reformulated nthLem: -} nthLem : (n : ℕ) → mapStream suc (from n) ≈ from (suc n) nthLem n = suc n ∷ ♯ nthLem (suc n) {- We simply observe that the heads of both sides are identical and that the tails are an instance of the theorem we are just about to prove. Hence we can construct an infinite proof that both streams are equal. -} {- We show that ≈ is an equivalence relation using infinite proofs again. -} refl≈ : ∀ {A} → (as : Stream A) → as ≈ as refl≈ (a ∷ as) = a ∷ ♯ (refl≈ (♭ as)) sym≈ : ∀ {A} → {as bs : Stream A} → as ≈ bs → bs ≈ as sym≈ (a ∷ as≈bs) = a ∷ ♯ sym≈ (♭ as≈bs) trans≈ : ∀ {A} → {as bs cs : Stream A} → as ≈ bs → bs ≈ cs → as ≈ cs trans≈ (a ∷ as≈bs) (.a ∷ bs≈cs) = a ∷ ♯ (trans≈ (♭ as≈bs) (♭ bs≈cs))