module InductiveStreamEquality {A : Set} where
open import Codata.Musical.Notation
open import Codata.Musical.Stream hiding (_∈_; lookup)
open import Data.List
open import Data.List.Membership.Propositional
open import Data.List.Relation.Unary.All as All
open import Data.List.Relation.Unary.Any using (here; there)
open import Data.Product
open import Relation.Binary.PropositionalEquality using (_≡_; refl)
infixr 5 _∷_
infix 4 _⊢_≈_ _≈P_ _≈W_
data _⊢_≈_ (H : List (Stream A × Stream A)) :
Stream A → Stream A → Set where
_∷_ : ∀ x {xs ys} →
(x ∷ xs , x ∷ ys) ∷ H ⊢ ♭ xs ≈ ♭ ys →
H ⊢ x ∷ xs ≈ x ∷ ys
hyp : ∀ {xs ys} → (xs , ys) ∈ H → H ⊢ xs ≈ ys
trans : ∀ {xs ys zs} → H ⊢ xs ≈ ys → H ⊢ ys ≈ zs → H ⊢ xs ≈ zs
repeat-refl : (x : A) → [] ⊢ repeat x ≈ repeat x
repeat-refl x = x ∷ hyp (here refl)
Valid : (Stream A → Stream A → Set) → Stream A × Stream A → Set
Valid _R_ (xs , ys) = xs R ys
mutual
data _≈P_ : Stream A → Stream A → Set where
sound : ∀ {A xs ys} → All (Valid _≈W_) A → A ⊢ xs ≈ ys → xs ≈P ys
trans : ∀ {xs ys zs} → xs ≈P ys → ys ≈P zs → xs ≈P zs
data _≈W_ : Stream A → Stream A → Set where
_∷_ : ∀ x {xs ys} → ∞ (♭ xs ≈P ♭ ys) → x ∷ xs ≈W x ∷ ys
transW : ∀ {xs ys zs} → xs ≈W ys → ys ≈W zs → xs ≈W zs
transW (x ∷ xs≈ys) (.x ∷ ys≈zs) = x ∷ ♯ trans (♭ xs≈ys) (♭ ys≈zs)
soundW : ∀ {A xs ys} → All (Valid _≈W_) A → A ⊢ xs ≈ ys → xs ≈W ys
soundW valid (hyp h) = All.lookup valid h
soundW valid (trans xs≈ys ys≈zs) = transW (soundW valid xs≈ys)
(soundW valid ys≈zs)
soundW valid (x ∷ xs≈ys) = proof
where
proof : _ ≈W _
proof = x ∷ ♯ sound (proof ∷ valid) xs≈ys
whnf : ∀ {xs ys} → xs ≈P ys → xs ≈W ys
whnf (sound valid xs≈ys) = soundW valid xs≈ys
whnf (trans xs≈ys ys≈zs) = transW (whnf xs≈ys) (whnf ys≈zs)
mutual
⟦_⟧W : ∀ {xs ys} → xs ≈W ys → xs ≈ ys
⟦ x ∷ xs≈ys ⟧W = refl ∷ ♯ ⟦ ♭ xs≈ys ⟧P
⟦_⟧P : ∀ {xs ys} → xs ≈P ys → xs ≈ ys
⟦ xs≈ys ⟧P = ⟦ whnf xs≈ys ⟧W
mutual
completeP : ∀ {xs ys} → xs ≈ ys → xs ≈P ys
completeP xs≈ys = sound (completeW xs≈ys ∷ []) (hyp (here refl))
completeW : ∀ {xs ys} → xs ≈ ys → xs ≈W ys
completeW (refl ∷ xs≈ys) = _ ∷ ♯ completeP (♭ xs≈ys)
reallySound : ∀ {A xs ys} → All (Valid _≈_) A → A ⊢ xs ≈ ys → xs ≈ ys
reallySound valid xs≈ys =
⟦ sound (All.map (λ {p} → done p) valid) xs≈ys ⟧P
where
done : ∀ p → Valid _≈_ p → Valid _≈W_ p
done (xs , ys) = completeW