[Further work on the ReverseComposition theory. Nils Anders Danielsson **20101123005422 Ignore-this: f7e4cc16120e4199614629af6eb9e540 ] hunk ./ReverseComposition.agda 15 +open import Data.Unit using (tt) hunk ./ReverseComposition.agda 84 +-- The equality is complete with respect to propositional equality. +-- For (a limited form of) soundness, see !-cong. + +complete : ∀ {ℓ As} {B : Set ℓ} {f g : As ⇨ B} → f ≡ g → f ≈ g +complete P.refl = refl _ + hunk ./ReverseComposition.agda 137 +η₀ : ∀ {ℓ} {A : Set ℓ} {x : [] ⇨ A} → return (! x) ≡ x +η₀ {x = return x} = P.refl + hunk ./ReverseComposition.agda 294 + return∥-cong : ∀ {As} {B : Set ℓ} {x₁ x₂ : B} → + x₁ ≡ x₂ → return∥ {As = As} x₁ ≈ return∥ {As = As} x₂ + return∥-cong {As = []} x₁≡x₂ = return x₁≡x₂ + return∥-cong {As = A ∷ As} x₁≡x₂ = Λ λ _ → return∥-cong x₁≡x₂ + hunk ./ReverseComposition.agda 301 - _>>=∥-cong_ : ∀ {As} {B₁ C₁ B₂ C₂ : Set ℓ} - {f₁ : As ⇨ B₁} {g₁ : B₁ → As ⇨ C₁} - {f₂ : As ⇨ B₂} {g₂ : B₂ → As ⇨ C₂} → + _>>=∥-cong_ : ∀ {As₁ As₂} {B₁ C₁ B₂ C₂ : Set ℓ} + {f₁ : As₁ ⇨ B₁} {g₁ : B₁ → As₁ ⇨ C₁} + {f₂ : As₂ ⇨ B₂} {g₂ : B₂ → As₂ ⇨ C₂} → hunk ./ReverseComposition.agda 333 + hunk ./ReverseComposition.agda 337 + hunk ./ReverseComposition.agda 342 -map : ∀ {ℓ As B} {C : Set ℓ} → (B → C) → As ⇨ B → As ⇨ C +map : ∀ {ℓ As} {B C : Set ℓ} → (B → C) → As ⇨ B → As ⇨ C hunk ./ReverseComposition.agda 347 -_⊛∥_ : ∀ {ℓ As B} {C : Set ℓ} → As ⇨ (B → C) → As ⇨ B → As ⇨ C +_⊛∥_ : ∀ {ℓ As} {B C : Set ℓ} → As ⇨ (B → C) → As ⇨ B → As ⇨ C hunk ./ReverseComposition.agda 354 --- const⋆ could have been derived if, for instance, the constructors --- of _⇨_ had not quantified over sets. - hunk ./ReverseComposition.agda 355 -const⋆ [] f = f -const⋆ (A ∷ As) f = Λ λ _ → const⋆ As f +const⋆ As f = return∥ {As = As} (lift tt) >>= const f hunk ./ReverseComposition.agda 374 + const⋆-return∥ : ∀ As {Bs} {C : Set ℓ} (x : C) → + const⋆ As (return∥ {As = Bs} x) ≈ + return∥ {As = As ++ Bs} x + const⋆-return∥ As x = >>=-return∥ (return∥ {As = As} (lift tt)) x + hunk ./ReverseComposition.agda 423 + map-cong : ∀ {As} {B C : Set ℓ} {f₁ f₂ : B → C} {g₁ g₂ : As ⇨ B} → + (∀ x → f₁ x ≡ f₂ x) → g₁ ≈ g₂ → map f₁ g₁ ≈ map f₂ g₂ + map-cong f₁≡f₂ g₁≈g₂ = g₁≈g₂ >>=∥-cong′ λ x → return∥-cong (f₁≡f₂ x) + where open MonadLaws∥ + + infixl 10 _⊛∥-cong_ + + _⊛∥-cong_ : ∀ {As} {B C : Set ℓ} + {f₁ f₂ : As ⇨ (B → C)} {g₁ g₂ : As ⇨ B} → + f₁ ≈ f₂ → g₁ ≈ g₂ → f₁ ⊛∥ g₁ ≈ f₂ ⊛∥ g₂ + f₁≈f₂ ⊛∥-cong g₁≈g₂ = + f₁≈f₂ >>=∥-cong λ h₁≅h₂ → + map-cong (λ x → P.cong (λ f → f x) (H.≅-to-≡ h₁≅h₂)) g₁≈g₂ + where open MonadLaws∥ + + zipWith∥-cong : ∀ {As} {B C D : Set ℓ} {f₁ f₂ : B → C → D} + {g₁ g₂ : As ⇨ B} {h₁ h₂ : As ⇨ C} → + (∀ x y → f₁ x y ≡ f₂ x y) → g₁ ≈ g₂ → h₁ ≈ h₂ → + zipWith∥ f₁ g₁ h₁ ≈ zipWith∥ f₂ g₂ h₂ + zipWith∥-cong f₁≡f₂ (return P.refl) (return P.refl) = + return (f₁≡f₂ _ _) + zipWith∥-cong f₁≡f₂ (Λ g₁≈g₂) (Λ h₁≈h₂) = Λ λ x → + zipWith∥-cong f₁≡f₂ (g₁≈g₂ x) (h₁≈h₂ x) + hunk ./ReverseComposition.agda 462 +infixr 6 _then_else_ + hunk ./ReverseComposition.agda 473 +infixr 8 _⊕_ + hunk ./ReverseComposition.agda 480 -module MLaws {ℓ} where +module LawsM {ℓ} where hunk ./ReverseComposition.agda 491 - >>=M-cong {g₁ = g₁} {g₂ = g₂} f₁≈f₂ g₁j≈g₂j g₁n≈g₂n = - f₁≈f₂ >>=-cong′ lemma - where - open MonadLaws + >>=M-cong f₁≈f₂ g₁j≈g₂j g₁n≈g₂n = + f₁≈f₂ >>=-cong′ maybe g₁j≈g₂j g₁n≈g₂n + where open MonadLaws + + maybe-cong : ∀ {Bs₁ Bs₂} {B C₁ C₂ : Set ℓ} + {s₁ : B → Bs₁ ⇨M C₁} {f₁} + {s₂ : B → Bs₂ ⇨M C₂} {f₂} → + (∀ x → s₁ x ≈ s₂ x) → f₁ ≈ f₂ → + ∀ x → maybe s₁ f₁ x ≈ maybe s₂ f₂ x + maybe-cong s₁≈s₂ f₁≈f₂ (just x) = s₁≈s₂ x + maybe-cong s₁≈s₂ f₁≈f₂ nothing = f₁≈f₂ hunk ./ReverseComposition.agda 503 - lemma : ∀ x → g₁ x ≈ g₂ x - lemma (just x) = g₁j≈g₂j x - lemma nothing = g₁n≈g₂n + infixr 6 _then_else-cong_ + + _then_else-cong_ : ∀ {As₁ Bs₁ As₂ Bs₂} {B C₁ C₂ : Set ℓ} + {g₁ : As₁ ⇨M B} {s₁ : B → Bs₁ ⇨M C₁} {f₁} + {g₂ : As₂ ⇨M B} {s₂ : B → Bs₂ ⇨M C₂} {f₂} → + g₁ ≈ g₂ → (∀ x → s₁ x ≈ s₂ x) → f₁ ≈ f₂ → + g₁ then s₁ else f₁ ≈ g₂ then s₂ else f₂ + g₁≈g₂ then s₁≈s₂ else-cong f₁≈f₂ = + g₁≈g₂ >>=-cong′ maybe-cong s₁≈s₂ f₁≈f₂ + where open MonadLaws + + zeroM-cong : ∀ {As} {B : Set ℓ} → + zeroM {As = As} {B = B} ≈ zeroM {As = As} {B = B} + zeroM-cong = MonadLaws∥.return∥-cong P.refl + + infixr 8 _⊕-cong_ + + _⊕-cong_ : ∀ {As} {B : Set ℓ} {f₁ f₂ : As ⇨M B} {g₁ g₂ : As ⇨M B} → + f₁ ≈ f₂ → g₁ ≈ g₂ → f₁ ⊕ g₁ ≈ f₂ ⊕ g₂ + f₁≈f₂ ⊕-cong g₁≈g₂ = + MoreLaws∥.zipWith∥-cong (λ _ _ → P.refl) f₁≈f₂ g₁≈g₂ hunk ./ReverseComposition.agda 546 - (g : As ⇨M B) (s : B → Bs ⇨M C) (f : Bs ⇨M C) - (s′ : C → Cs ⇨M D) (f′ : Cs ⇨M D) → - (g then s else f) then s′ else f′ ≈ - g then (λ x → s x then s′ else f′) - else (f then s′ else f′) - distrib g s f s′ f′ = - (g >>= maybe s f) >>= c′ ≈⟨ MonadLaws.assoc g (maybe s f) c′ ⟩ - g >>= (λ x → maybe s f x >>= c′) ≈⟨ >>=M-cong (refl g) (λ x → refl (s x >>= c′)) (refl (f >>= c′)) ⟩ - g >>= maybe (λ x → s x >>= c′) (f >>= c′) ∎ - where c′ = maybe s′ f′ + (g : As ⇨M B) (s : B → Bs ⇨M C) {f : Bs ⇨M C} + {h : Maybe C → Cs ⇨M D} → + (g then s else f) >>= h ≈ + g then (λ x → s x >>= h) else (f >>= h) + distrib g s {f} {h} = + (g >>= maybe s f) >>= h ≈⟨ MonadLaws.assoc g (maybe s f) h ⟩ + g >>= (λ x → maybe′ s f x >>= h) ≈⟨ >>=M-cong (refl g) (λ x → refl (s x >>= h)) (refl (f >>= h)) ⟩ + g >>= maybe (λ x → s x >>= h) (f >>= h) ∎ hunk ./ReverseComposition.agda 585 + + -- In the nullary case _⊕_ can be expressed concisely in terms of + -- _then_else_. + + ⊕₀ : ∀ {B : Set ℓ} (f g : [] ⇨M B) → + f ⊕ g ≈ f then returnM else g + ⊕₀ (return (just x)) (return _) = refl _ + ⊕₀ (return nothing) (return y) = refl _ + + -- Another lemma which applies in the nullary case. + + then-else-·₀ : + ∀ {Bs} {A B C : Set ℓ} + (g : [] ⇨M A) (s : A → B ∷ Bs ⇨M C) {f : B ∷ Bs ⇨M C} {x} → + (g then s else f) · x ≡ g then (λ y → s y · x) else f · x + then-else-·₀ (return (just x)) _ = P.refl + then-else-·₀ (return nothing) _ = P.refl + +-- Monoid-like operators. + +identityM : ∀ {ℓ} {A : Set ℓ} → A ∷ [] ⇨M A +identityM = Λ λ x → returnM x + +infixr 9 _⊙M_ + +_⊙M_ : ∀ {ℓ As Bs} {B C : Set ℓ} → + As ⇨M B → (B ∷ Bs) ⇨M C → As ++ Bs ⇨M C +f ⊙M g = f then _·_ g else zeroM + +-- Laws for the monoid-like operators. + +module MonoidLawsM {ℓ} where + + open ≈-Reasoning + + right-identity : ∀ {As} {B : Set ℓ} + (f : As ⇨M B) → f ⊙M identityM ≈ f + right-identity f = + f ⊙M identityM ≡⟨ P.refl ⟩ + f then returnM else zeroM ≈⟨ LawsM.right-identities f ⟩ + f ∎ + + -- Note that the type of f is not completely general. + + left-identity : ∀ {As} {A B : Set ℓ} + (f : A ∷ As ⇨M B) → identityM ⊙M f ≈ f + left-identity f = + identityM ⊙M f ≡⟨ P.refl ⟩ + (Λ λ x → returnM x) then _·_ f else zeroM ≡⟨ P.refl ⟩ + (Λ λ x → returnM x then _·_ f else zeroM) ≡⟨ P.refl ⟩ + (Λ λ x → f · x) ≡⟨ η ⟩ + f ∎ + + -- Note that the types of g and h are not completely general. + + assoc : ∀ {As Bs Cs} {B C D : Set ℓ} + (f : As ⇨M B) (g : B ∷ Bs ⇨M C) (h : C ∷ Cs ⇨M D) → + (f ⊙M g) ⊙M h ≈ f ⊙M (g ⊙M h) + assoc {Bs = Bs} f (Λ g) h = + (f ⊙M Λ g) ⊙M h ≡⟨ P.refl ⟩ + (f then g else zeroM) then _·_ h else zeroM ≈⟨ MonadLaws.assoc f _ _ ⟩ + f >>= (λ x → maybe′ g zeroM x then _·_ h else zeroM) ≈⟨ LawsM.>>=M-cong (refl f) (λ _ → refl _) + (LawsM.left-zero Bs (_·_ h) zeroM) ⟩ + f >>= maybe (λ x → g x then _·_ h else zeroM) (const⋆ Bs zeroM) ≈⟨ LawsM.>>=M-cong (refl f) (λ _ → refl _) + (MoreLaws∥.const⋆-return∥ Bs nothing) ⟩ + f >>= maybe (λ x → g x then _·_ h else zeroM) zeroM ≡⟨ P.refl ⟩ + f ⊙M (Λ g ⊙M h) ∎ + + infixr 9 _⊙M-cong_ + + _⊙M-cong_ : ∀ {As₁ As₂ Bs} {B C : Set ℓ} + {f₁ : As₁ ⇨M B} {g₁ : B ∷ Bs ⇨M C} + {f₂ : As₂ ⇨M B} {g₂ : B ∷ Bs ⇨M C} → + f₁ ≈ f₂ → g₁ ≈ g₂ → f₁ ⊙M g₁ ≈ f₂ ⊙M g₂ + f₁≈f₂ ⊙M-cong g₁≈g₂ = + f₁≈f₂ then (λ x → g₁≈g₂ ·-cong H.refl) else-cong zeroM-cong + where open LawsM + + identityM-cong : {A : Set ℓ} → identityM {A = A} ≈ identityM {A = A} + identityM-cong = refl identityM