------------------------------------------------------------------------ -- A sound, inductive approximation of stream equality ------------------------------------------------------------------------ -- The point of this module is to give a short (not entirely faithful) -- illustration of the technique used to establish soundness of -- RecursiveTypes.Subtyping.Axiomatic.Inductive._⊢_≤_ with respect to -- RecursiveTypes.Subtyping.Axiomatic.Coinductive._≤_. 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_ ------------------------------------------------------------------------ -- An approximation of stream equality -- Streams do not need to be regular, so _⊢_≈_ is not complete with -- respect to _≈_. 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 -- Example. repeat-refl : (x : A) → [] ⊢ repeat x ≈ repeat x repeat-refl x = x ∷ hyp (here refl) ------------------------------------------------------------------------ -- Soundness Valid : (Stream A → Stream A → Set) → Stream A × Stream A → Set Valid _R_ (xs , ys) = xs R ys -- Programs and WHNFs. 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) -- The programs and WHNFs are sound with respect to _≈_. 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 -- The programs and WHNFs are also complete with respect to _≈_. 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) -- Finally we get the intended soundness result for _⊢_≈_. 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