------------------------------------------------------------------------ -- An implementation of the Fibonacci sequence using tail ------------------------------------------------------------------------ module SingletonChunks where open import Coinduction open import Data.Bool open import Data.Nat open import Data.Stream as S using (Stream; _≈_; _∷_) open import Data.Vec as V using (Vec; []; _∷_) import Relation.Binary.PropositionalEquality as P ------------------------------------------------------------------------ -- Stream programs -- StreamP b A encodes programs generating streams in chunks of size -- (at least) 1. The first chunk may be empty if b is false. infixr 5 _∷_ data StreamP : Bool → Set → Set₁ where [_] : ∀ {A} (xs : ∞ (StreamP true A)) → StreamP false A _∷_ : ∀ {A} (x : A) (xs : StreamP false A) → StreamP true A forget : ∀ {A} (xs : StreamP true A) → StreamP false A tail : ∀ {A} (xs : StreamP true A) → StreamP false A zipWith : ∀ {b A B C} (f : A → B → C) (xs : StreamP b A) (ys : StreamP b B) → StreamP b C data StreamW : Bool → Set → Set₁ where [_] : ∀ {A} (xs : StreamP true A) → StreamW false A _∷_ : ∀ {A} (x : A) (xs : StreamW false A) → StreamW true A forgetW : ∀ {A} → StreamW true A → StreamW false A forgetW (x ∷ [ xs ]) = [ x ∷ forget xs ] tailW : ∀ {A} → StreamW true A → StreamW false A tailW (x ∷ xs) = xs zipWithW : ∀ {b A B C} → (A → B → C) → StreamW b A → StreamW b B → StreamW b C zipWithW f [ xs ] [ ys ] = [ zipWith f xs ys ] zipWithW f (x ∷ xs) (y ∷ ys) = f x y ∷ zipWithW f xs ys whnf : ∀ {b A} → StreamP b A → StreamW b A whnf [ xs ] = [ ♭ xs ] whnf (x ∷ xs) = x ∷ whnf xs whnf (forget xs) = forgetW (whnf xs) whnf (tail xs) = tailW (whnf xs) whnf (zipWith f xs ys) = zipWithW f (whnf xs) (whnf ys) mutual ⟦_⟧W : ∀ {A} → StreamW true A → Stream A ⟦ x ∷ [ xs ] ⟧W = x ∷ ♯ ⟦ xs ⟧P ⟦_⟧P : ∀ {A} → StreamP true A → Stream A ⟦ xs ⟧P = ⟦ whnf xs ⟧W ------------------------------------------------------------------------ -- The Fibonacci sequence fib : StreamP true ℕ fib = 0 ∷ [ ♯ (1 ∷ zipWith _+_ (forget fib) (tail fib)) ] ------------------------------------------------------------------------ -- The definition of fib is correct -- ⟦_⟧ is homomorphic with respect to zipWith/S.zipWith. zipWith-hom : ∀ {A B C} (_∙_ : A → B → C) xs ys → ⟦ zipWith _∙_ xs ys ⟧P ≈ S.zipWith _∙_ ⟦ xs ⟧P ⟦ ys ⟧P zipWith-hom _∙_ xs ys with whnf xs | whnf ys zipWith-hom _∙_ xs ys | x ∷ [ xs′ ] | y ∷ [ ys′ ] = P.refl ∷ ♯ zipWith-hom _∙_ xs′ ys′ -- forget is the identity on streams. open import MapIterate as M using (_≈P_; _∷_; _≈⟨_⟩_; _∎) open import Relation.Binary.PropositionalEquality as P using (_≡_; [_]) forget-lemma : ∀ {A} x (xs : StreamP true A) → ⟦ x ∷ forget xs ⟧P ≈P x ∷ ♯ ⟦ xs ⟧P forget-lemma x xs with whnf xs | P.inspect whnf xs ... | y ∷ [ ys ] | [ eq ] = x ∷ ♯ helper eq where helper : whnf xs ≡ y ∷ [ ys ] → ⟦ y ∷ forget ys ⟧P ≈P ⟦ xs ⟧P helper eq rewrite eq = _ ≈⟨ forget-lemma y ys ⟩ (y ∷ ♯ (_ ∎)) -- The stream ⟦ fib ⟧P satisfies its intended defining equation. open import Relation.Binary module SS {A : Set} = Setoid (S.setoid A) fib-correct : ⟦ fib ⟧P ≈ 0 ∷ ♯ (1 ∷ ♯ S.zipWith _+_ ⟦ fib ⟧P (S.tail ⟦ fib ⟧P)) fib-correct = P.refl ∷ ♯ (P.refl ∷ ♯ SS.trans (zipWith-hom _+_ (0 ∷ forget fib′) fib′) (S.zipWith-cong _+_ (SS.trans (M.soundP (forget-lemma 0 fib′)) (P.refl ∷ ♯ SS.refl)) SS.refl)) where fib′ = 1 ∷ zipWith _+_ (forget fib) (tail fib) ------------------------------------------------------------------------ -- An equality proof language infix 4 _≈[_]P_ _≈[_]W_ infix 3 _∎ infixr 2 _≈⟨_⟩_ data _≈[_]P_ : {A : Set} → Stream A → Bool → Stream A → Set₁ where [_] : ∀ {A} {xs ys : Stream A} (xs≈ys : ∞ (xs ≈[ true ]P ys)) → xs ≈[ false ]P ys _∷_ : ∀ {b A} (x : A) {xs ys : ∞ (Stream A)} (xs≈ys : ♭ xs ≈[ b ]P ♭ ys) → x ∷ xs ≈[ true ]P x ∷ ys forget : ∀ {A} {xs ys : Stream A} (xs≈ys : xs ≈[ true ]P ys) → xs ≈[ false ]P ys _≈⟨_⟩_ : ∀ {b A} (xs : Stream A) {ys zs} (xs≈ys : xs ≈[ b ]P ys) (ys≈zs : ys ≈[ b ]P zs) → xs ≈[ b ]P zs _∎ : ∀ {A} (xs : Stream A) → xs ≈[ true ]P xs tail : ∀ {A} {xs ys : Stream A} (xs≈ys : xs ≈[ true ]P ys) → S.tail xs ≈[ false ]P S.tail ys zipWith : ∀ {b A B C} (f : A → B → C) {xs xs′ ys ys′} (xs≈xs′ : xs ≈[ b ]P xs′) (ys≈ys′ : ys ≈[ b ]P ys′) → S.zipWith f xs ys ≈[ b ]P S.zipWith f xs′ ys′ -- Completeness. completeP : ∀ {A : Set} {xs ys : Stream A} → xs ≈ ys → xs ≈[ true ]P ys completeP (P.refl ∷ xs≈ys) = _ ∷ [ ♯ completeP (♭ xs≈ys) ] -- Weak head normal forms. data _≈[_]W_ {A : Set} : Stream A → Bool → Stream A → Set₁ where [_] : {xs ys : Stream A} (xs≈ys : xs ≈[ true ]P ys) → xs ≈[ false ]W ys _∷_ : ∀ (x : A) {xs ys} (xs≈ys : ♭ xs ≈[ true ]P ♭ ys) → x ∷ xs ≈[ true ]W x ∷ ys consW≈ : ∀ {A b} (x : A) {xs ys} → ♭ xs ≈[ b ]W ♭ ys → x ∷ xs ≈[ true ]W x ∷ ys consW≈ x xs≈ys = x ∷ helper xs≈ys where helper : ∀ {A b} {xs ys : Stream A} → xs ≈[ b ]W ys → xs ≈[ true ]P ys helper [ xs≈ys ] = xs≈ys helper (x ∷ xs≈ys) = x ∷ xs≈ys forgetW≈ : ∀ {A} {xs ys : Stream A} → xs ≈[ true ]W ys → xs ≈[ false ]W ys forgetW≈ (x ∷ xs≈ys) = [ x ∷ forget xs≈ys ] transW≈ : ∀ {A b} {xs ys zs : Stream A} → xs ≈[ b ]W ys → ys ≈[ b ]W zs → xs ≈[ b ]W zs transW≈ [ xs≈ys ] [ ys≈zs ] = [ _ ≈⟨ xs≈ys ⟩ ys≈zs ] transW≈ (x ∷ xs≈ys) (.x ∷ ys≈zs) = x ∷ (_ ≈⟨ xs≈ys ⟩ ys≈zs) reflW≈ : ∀ {A} (xs : Stream A) → xs ≈[ true ]W xs reflW≈ (x ∷ xs) = x ∷ (♭ xs ∎) tailW≈ : ∀ {A} {xs ys : Stream A} → xs ≈[ true ]W ys → S.tail xs ≈[ false ]W S.tail ys tailW≈ (x ∷ xs≈ys) = [ xs≈ys ] zipWithW≈ : ∀ {A B C b} (_∙_ : A → B → C) {xs₁ ys₁ xs₂ ys₂} → xs₁ ≈[ b ]W ys₁ → xs₂ ≈[ b ]W ys₂ → S.zipWith _∙_ xs₁ xs₂ ≈[ b ]W S.zipWith _∙_ ys₁ ys₂ zipWithW≈ _∙_ [ xs₁≈ys₁ ] [ xs₂≈ys₂ ] = [ zipWith _∙_ xs₁≈ys₁ xs₂≈ys₂ ] zipWithW≈ _∙_ (x₁ ∷ xs₁≈ys₁) (x₂ ∷ xs₂≈ys₂) = (x₁ ∙ x₂) ∷ zipWith _∙_ xs₁≈ys₁ xs₂≈ys₂ whnf≈ : ∀ {A : Set} {xs ys : Stream A} {b} → xs ≈[ b ]P ys → xs ≈[ b ]W ys whnf≈ [ xs≈ys ] = [ ♭ xs≈ys ] whnf≈ (x ∷ xs≈ys) = consW≈ x (whnf≈ xs≈ys) whnf≈ (forget xs≈ys) = forgetW≈ (whnf≈ xs≈ys) whnf≈ (xs ≈⟨ xs≈ys ⟩ ys≈zs) = transW≈ (whnf≈ xs≈ys) (whnf≈ ys≈zs) whnf≈ (xs ∎) = reflW≈ xs whnf≈ (tail xs≈ys) = tailW≈ (whnf≈ xs≈ys) whnf≈ (zipWith f xs≈xs′ ys≈ys′) = zipWithW≈ f (whnf≈ xs≈xs′) (whnf≈ ys≈ys′) -- Soundness. mutual soundW : {A : Set} {xs ys : Stream A} → xs ≈[ true ]W ys → xs ≈ ys soundW (x ∷ xs≈ys) = P.refl ∷ ♯ soundP xs≈ys soundP : {A : Set} {xs ys : Stream A} → xs ≈[ true ]P ys → xs ≈ ys soundP xs≈ys = soundW (whnf≈ xs≈ys) ------------------------------------------------------------------------ -- The equation given for fib has a unique solution fib-rhs : Stream ℕ → Stream ℕ fib-rhs ns = 0 ∷ ♯ (1 ∷ ♯ S.zipWith _+_ ns (S.tail ns)) fib-unique : ∀ ms ns → ms ≈ fib-rhs ms → ns ≈ fib-rhs ns → ms ≈[ true ]P ns fib-unique ms ns ms≈ ns≈ = ms ≈⟨ completeP ms≈ ⟩ fib-rhs ms ≈⟨ 0 ∷ [ ♯ (1 ∷ zipWith _+_ (forget (fib-unique ms ns ms≈ ns≈)) (tail (fib-unique ms ns ms≈ ns≈))) ] ⟩ fib-rhs ns ≈⟨ completeP (SS.sym ns≈) ⟩ ns ∎