module BreadthFirst.Lemmas where
open import Coinduction
open import Function
open import Data.List.NonEmpty as List⁺ using (List⁺; [_]; _∷_; _⁺++⁺_)
import Data.Vec as Vec
open import Data.Colist as Colist using (Colist; []; _∷_; concat; _++_)
open import Data.Product using (_,_)
open import Relation.Binary.PropositionalEquality as PropEq
using (_≡_) renaming (refl to ≡-refl)
open import BreadthFirst.Universe
open import BreadthFirst.Programs
open import Tree using (leaf; node; map)
open import Stream using (Stream; _≺_) renaming (_++_ to _++∞_)
zipWith : ∀ {A B} (f : A → B → B) → Colist A → Stream B → Stream B
zipWith f [] ys = ys
zipWith f (x ∷ xs) (y ≺ ys) = f x y ≺ ♯ zipWith f (♭ xs) (♭ ys)
_⁺++∞_ : ∀ {A} → List⁺ A → Stream A → Stream A
xs ⁺++∞ ys = Colist.fromList (Vec.toList $ List⁺.toVec xs) ++∞ ys
_⁺++_ : ∀ {A} → List⁺ A → Colist A → Colist A
xs ⁺++ ys = Colist.fromList (Vec.toList $ List⁺.toVec xs) ++ ys
refl : ∀ {a} x → Eq a x x
refl {a = tree a} leaf = leaf
refl {a = tree a} (node l x r) = node (♯ refl (♭ l)) (refl x) (♯ refl (♭ r))
refl {a = stream a} (x ≺ xs) = refl x ≺ ♯ refl (♭ xs)
refl {a = colist a} [] = []
refl {a = colist a} (x ∷ xs) = refl x ∷ ♯ refl (♭ xs)
refl {a = a ⊗ b} (x , y) = (refl x , refl y)
refl {a = ⌈ A ⌉} x = ⌈ PropEq.refl ⌉
sym : ∀ {a x y} → Eq a x y → Eq a y x
sym {a = tree a} leaf = leaf
sym {a = tree a} (node l≈l′ x≈x′ r≈r′) = node (♯ sym (♭ l≈l′)) (sym x≈x′) (♯ sym (♭ r≈r′))
sym {a = stream a} (x≈x′ ≺ xs≈xs′) = sym x≈x′ ≺ ♯ sym (♭ xs≈xs′)
sym {a = colist a} [] = []
sym {a = colist a} (x≈x′ ∷ xs≈xs′) = sym x≈x′ ∷ ♯ sym (♭ xs≈xs′)
sym {a = a ⊗ b} (x≈x′ , y≈y′) = (sym x≈x′ , sym y≈y′)
sym {a = ⌈ A ⌉} ⌈ x≡x′ ⌉ = ⌈ PropEq.sym x≡x′ ⌉
trans : ∀ {a x y z} → Eq a x y → Eq a y z → Eq a x z
trans {a = tree a} leaf leaf = leaf
trans {a = tree a} (node l≈l′ x≈x′ r≈r′)
(node l′≈l″ x′≈x″ r′≈r″) = node (♯ trans (♭ l≈l′) (♭ l′≈l″))
(trans x≈x′ x′≈x″)
(♯ trans (♭ r≈r′) (♭ r′≈r″))
trans {a = stream a} (x≈x′ ≺ xs≈xs′)
(x′≈x″ ≺ xs′≈xs″) = trans x≈x′ x′≈x″ ≺ ♯ trans (♭ xs≈xs′) (♭ xs′≈xs″)
trans {a = colist a} [] [] = []
trans {a = colist a} (x≈x′ ∷ xs≈xs′)
(x′≈x″ ∷ xs′≈xs″) = trans x≈x′ x′≈x″ ∷ ♯ trans (♭ xs≈xs′) (♭ xs′≈xs″)
trans {a = a ⊗ b} (x≈x′ , y≈y′)
(x′≈x″ , y′≈y″) = (trans x≈x′ x′≈x″ , trans y≈y′ y′≈y″)
trans {a = ⌈ A ⌉} ⌈ x≡x′ ⌉ ⌈ x′≡x″ ⌉ = ⌈ PropEq.trans x≡x′ x′≡x″ ⌉
infixr 5 _≺_ _∷_
infixr 2 _≈⟨_⟩_ _≊⟨_⟩_
infix 2 _∎
data EqP : ∀ a → El a → El a → Set₁ where
leaf : ∀ {a} → EqP (tree a) leaf leaf
node : ∀ {a x x′ l l′ r r′}
(l≈l′ : ∞ (EqP (tree a) (♭ l) (♭ l′)))
(x≈x′ : Eq a x x′ )
(r≈r′ : ∞ (EqP (tree a) (♭ r) (♭ r′))) →
EqP (tree a) (node l x r) (node l′ x′ r′)
_≺_ : ∀ {a x x′ xs xs′}
(x≈x′ : Eq a x x′ )
(xs≈xs′ : ∞ (EqP (stream a) (♭ xs) (♭ xs′))) →
EqP (stream a) (x ≺ xs) (x′ ≺ xs′)
[] : ∀ {a} → EqP (colist a) [] []
_∷_ : ∀ {a x x′ xs xs′}
(x≈x′ : Eq a x x′ )
(xs≈xs′ : ∞ (EqP (colist a) (♭ xs) (♭ xs′))) →
EqP (colist a) (x ∷ xs) (x′ ∷ xs′)
_,_ : ∀ {a b x x′ y y′}
(x≈x′ : Eq a x x′) (y≈y′ : Eq b y y′) →
EqP (a ⊗ b) (x , y) (x′ , y′)
⌈_⌉ : ∀ {A x x′} (x≡x′ : x ≡ x′) → EqP ⌈ A ⌉ x x′
_≊⟨_⟩_ : ∀ {a} x {y z}
(x≈y : EqP a x y) (y≈z : EqP a y z) → EqP a x z
zipWith-cong :
∀ {a b} {f : El a → El b → El b}
(cong : ∀ {x x′ y y′} →
Eq a x x′ → Eq b y y′ → Eq b (f x y) (f x′ y′))
{xs xs′ ys ys′}
(xs≈xs′ : EqP (colist a) xs xs′)
(ys≈ys′ : EqP (stream b) ys ys′) →
EqP (stream b) (zipWith f xs ys) (zipWith f xs′ ys′)
data EqW : ∀ a → El a → El a → Set₁ where
leaf : ∀ {a} → EqW (tree a) leaf leaf
node : ∀ {a x x′ l l′ r r′}
(l≈l′ : EqP (tree a) (♭ l) (♭ l′))
(x≈x′ : Eq a x x′ )
(r≈r′ : EqP (tree a) (♭ r) (♭ r′)) →
EqW (tree a) (node l x r) (node l′ x′ r′)
_≺_ : ∀ {a x x′ xs xs′}
(x≈x′ : Eq a x x′ )
(xs≈xs′ : EqP (stream a) (♭ xs) (♭ xs′)) →
EqW (stream a) (x ≺ xs) (x′ ≺ xs′)
[] : ∀ {a} → EqW (colist a) [] []
_∷_ : ∀ {a x x′ xs xs′}
(x≈x′ : Eq a x x′ )
(xs≈xs′ : EqP (colist a) (♭ xs) (♭ xs′)) →
EqW (colist a) (x ∷ xs) (x′ ∷ xs′)
_,_ : ∀ {a b x x′ y y′}
(x≈x′ : Eq a x x′) (y≈y′ : Eq b y y′) →
EqW (a ⊗ b) (x , y) (x′ , y′)
⌈_⌉ : ∀ {A x x′} (x≡x′ : x ≡ x′) → EqW ⌈ A ⌉ x x′
⟦_⟧≈⁻¹ : ∀ {a} {x y : El a} → Eq a x y → EqP a x y
⟦ leaf ⟧≈⁻¹ = leaf
⟦ node l≈l′ x≈x′ r≈r′ ⟧≈⁻¹ = node (♯ ⟦ ♭ l≈l′ ⟧≈⁻¹) x≈x′ (♯ ⟦ ♭ r≈r′ ⟧≈⁻¹)
⟦ x≈x′ ≺ xs≈xs′ ⟧≈⁻¹ = x≈x′ ≺ ♯ ⟦ ♭ xs≈xs′ ⟧≈⁻¹
⟦ [] ⟧≈⁻¹ = []
⟦ x≈x′ ∷ xs≈xs′ ⟧≈⁻¹ = x≈x′ ∷ ♯ ⟦ ♭ xs≈xs′ ⟧≈⁻¹
⟦ (x≈x′ , y≈y′) ⟧≈⁻¹ = (x≈x′ , y≈y′)
⟦ ⌈ x≡x′ ⌉ ⟧≈⁻¹ = ⌈ x≡x′ ⌉
whnf≈ : ∀ {a xs ys} → EqP a xs ys → EqW a xs ys
whnf≈ leaf = leaf
whnf≈ (node l≈l′ x≈x′ r≈r′) = node (♭ l≈l′) x≈x′ (♭ r≈r′)
whnf≈ (x≈x′ ≺ xs≈xs′) = x≈x′ ≺ ♭ xs≈xs′
whnf≈ [] = []
whnf≈ (x≈x′ ∷ xs≈xs′) = x≈x′ ∷ ♭ xs≈xs′
whnf≈ (x≈x′ , y≈y′) = (x≈x′ , y≈y′)
whnf≈ ⌈ x≡x′ ⌉ = ⌈ x≡x′ ⌉
whnf≈ ( _ ≊⟨ x≈y ⟩ y≈z) with whnf≈ x≈y | whnf≈ y≈z
whnf≈ (._ ≊⟨ x≈y ⟩ y≈z) | leaf | leaf = leaf
whnf≈ (._ ≊⟨ x≈y ⟩ y≈z) | node l≈l′ x≈x′ r≈r′
| node l′≈l″ x′≈x″ r′≈r″ = node (_ ≊⟨ l≈l′ ⟩ l′≈l″) (trans x≈x′ x′≈x″) (_ ≊⟨ r≈r′ ⟩ r′≈r″)
whnf≈ (._ ≊⟨ x≈y ⟩ y≈z) | [] | [] = []
whnf≈ (._ ≊⟨ x≈y ⟩ y≈z) | x≈y′ ∷ xs≈ys′ | y≈z′ ∷ ys≈zs′ = trans x≈y′ y≈z′ ∷ (_ ≊⟨ xs≈ys′ ⟩ ys≈zs′)
whnf≈ (._ ≊⟨ x≈y ⟩ y≈z) | x≈y′ ≺ xs≈ys′ | y≈z′ ≺ ys≈zs′ = trans x≈y′ y≈z′ ≺ (_ ≊⟨ xs≈ys′ ⟩ ys≈zs′)
whnf≈ (._ ≊⟨ x≈y ⟩ y≈z) | (x≈x′ , y≈y′) | (x′≈x″ , y′≈y″) = (trans x≈x′ x′≈x″ , trans y≈y′ y′≈y″)
whnf≈ ( _ ≊⟨ x≈y ⟩ y≈z) | ⌈ x≡x′ ⌉ | ⌈ x′≡x″ ⌉ = ⌈ PropEq.trans x≡x′ x′≡x″ ⌉
whnf≈ (zipWith-cong cong xs≈xs′ ys≈ys′) with whnf≈ xs≈xs′ | whnf≈ ys≈ys′
... | [] | ys≈ys″ = ys≈ys″
... | x≈x′ ∷ xs≈xs″ | y≈y′ ≺ ys≈ys″ =
cong x≈x′ y≈y′ ≺ zipWith-cong cong xs≈xs″ ys≈ys″
mutual
value≈ : ∀ {a xs ys} → EqW a xs ys → Eq a xs ys
value≈ leaf = leaf
value≈ (node l≈l′ x≈x′ r≈r′) = node (♯ ⟦ l≈l′ ⟧≈) x≈x′ (♯ ⟦ r≈r′ ⟧≈)
value≈ (x≈x′ ≺ xs≈xs′) = x≈x′ ≺ ♯ ⟦ xs≈xs′ ⟧≈
value≈ [] = []
value≈ (x≈x′ ∷ xs≈xs′) = x≈x′ ∷ ♯ ⟦ xs≈xs′ ⟧≈
value≈ (x≈x′ , y≈y′) = (x≈x′ , y≈y′)
value≈ ⌈ x≡x′ ⌉ = ⌈ x≡x′ ⌉
⟦_⟧≈ : ∀ {a xs ys} → EqP a xs ys → Eq a xs ys
⟦ xs≈ys ⟧≈ = value≈ (whnf≈ xs≈ys)
_≈⟨_⟩_ : ∀ {a} x {y z}
(x≈y : Eq a x y) (y≈z : EqP a y z) → EqP a x z
x ≈⟨ x≈y ⟩ y≈z = x ≊⟨ ⟦ x≈y ⟧≈⁻¹ ⟩ y≈z
_∎ : ∀ {a} x → EqP a x x
x ∎ = ⟦ refl x ⟧≈⁻¹
infixr 2 _≋⟨_⟩_ _⊑⟨_⟩_
data PrefixOfP (a : U) :
Colist (El a) → Stream (El a) → Set₁ where
[] : ∀ {ys} → PrefixOfP a [] ys
⁺++-mono : ∀ xs {ys ys′} (ys⊑ys′ : ∞ (PrefixOfP a ys ys′)) →
PrefixOfP a (xs ⁺++ ys) (xs ⁺++∞ ys′)
_≋⟨_⟩_ : ∀ xs {ys zs} (xs≈ys : Eq (colist a) xs ys)
(ys⊑zs : PrefixOfP a ys zs) → PrefixOfP a xs zs
_⊑⟨_⟩_ : ∀ xs {ys zs} (xs⊑ys : PrefixOfP a xs ys)
(ys≈zs : EqP (stream a) ys zs) → PrefixOfP a xs zs
data PrefixOfW (a : U) :
Colist (El a) → Stream (El a) → Set₁ where
[] : ∀ {ys} → PrefixOfW a [] ys
_∷_ : ∀ {x y xs ys}
(x≈y : Eq a x y) (p : PrefixOfP a (♭ xs) (♭ ys)) →
PrefixOfW a (x ∷ xs) (y ≺ ys)
whnf⊑ : ∀ {a xs ys} →
PrefixOfP a xs ys → PrefixOfW a xs ys
whnf⊑ [] = []
whnf⊑ (⁺++-mono [ x ] ys⊑ys′) = refl x ∷ ♭ ys⊑ys′
whnf⊑ (⁺++-mono (x ∷ xs) ys⊑ys′) = refl x ∷ ⁺++-mono xs ys⊑ys′
whnf⊑ (._ ≋⟨ [] ⟩ _ ) = []
whnf⊑ (._ ≋⟨ x≈y ∷ xs≈ys ⟩ ys⊑zs) with whnf⊑ ys⊑zs
... | y≈z ∷ ys⊑zs′ = trans x≈y y≈z ∷ (_ ≋⟨ ♭ xs≈ys ⟩ ys⊑zs′)
whnf⊑ (._ ⊑⟨ xs⊑ys ⟩ ys≈zs) with whnf⊑ xs⊑ys | whnf≈ ys≈zs
... | [] | _ = []
... | x≈y ∷ xs⊑ys′ | y≈z ≺ ys≈zs′ = trans x≈y y≈z ∷ (_ ⊑⟨ xs⊑ys′ ⟩ ys≈zs′)
mutual
value⊑ : ∀ {a xs ys} → PrefixOfW a xs ys → PrefixOf a xs ys
value⊑ [] = []
value⊑ (x≈y ∷ xs⊑ys) = x≈y ∷ ♯ ⟦ xs⊑ys ⟧⊑
⟦_⟧⊑ : ∀ {a xs ys} → PrefixOfP a xs ys → PrefixOf a xs ys
⟦ xs⊑ys ⟧⊑ = value⊑ (whnf⊑ xs⊑ys)
⁺++∞-cong : ∀ {a xs xs′ ys ys′} →
Eq ⌈ List⁺ (El a) ⌉ xs xs′ →
Eq (stream a) ys ys′ →
Eq (stream a) (xs ⁺++∞ ys) (xs′ ⁺++∞ ys′)
⁺++∞-cong {xs = [ x ]} ⌈ ≡-refl ⌉ ys≈ys′ = refl x ≺ ♯ ys≈ys′
⁺++∞-cong {xs = x ∷ xs} ⌈ ≡-refl ⌉ ys≈ys′ =
refl x ≺ ♯ ⁺++∞-cong {xs = xs} ⌈ ≡-refl ⌉ ys≈ys′
++-assoc : ∀ {a} xs ys zs →
Eq (stream a) (xs ⁺++∞ (ys ⁺++∞ zs)) ((xs ⁺++⁺ ys) ⁺++∞ zs)
++-assoc [ x ] ys zs = refl x ≺ ♯ refl (ys ⁺++∞ zs)
++-assoc (x ∷ xs) ys zs = refl x ≺ ♯ ++-assoc xs ys zs
zip-++-assoc : ∀ {a} xss yss (zss : Stream (Stream (El a))) →
Eq (stream (stream a))
(zipWith _⁺++∞_ ⟦ xss ⟧ (zipWith _⁺++∞_ ⟦ yss ⟧ zss))
(zipWith _⁺++∞_ ⟦ longZipWith _⁺++⁺_ xss yss ⟧ zss)
zip-++-assoc xss yss (zs ≺ zss) with whnf xss | whnf yss
... | [] | [] = refl _
... | [] | ys ∷ yss′ = refl _
... | xs ∷ xss′ | [] = refl _
... | ⌈ xs ⌉ ∷ xss′ | ⌈ ys ⌉ ∷ yss′ =
++-assoc xs ys zs ≺ ♯ zip-++-assoc (♭ xss′) (♭ yss′) (♭ zss)
concat-lemma : ∀ {a} xs xss →
Eq (colist a) (concat (xs ∷ xss))
(xs ⁺++ concat (♭ xss))
concat-lemma [ x ] xss = refl x ∷ ♯ refl (concat (♭ xss))
concat-lemma (x ∷ xs) xss = refl x ∷ ♯ concat-lemma xs xss