biapply-predicatezipper.agda

-- Proof that my somewhat unusual Biapplicative instance for
-- PredicateZipper is lawful in
-- https://github.com/Mercerenies/lambda-games/blob/master/src/Lambda/Type/Relation.purs

open import Relation.Binary.PropositionalEquality
open import Function

record RawBifunctor (F : Set → Set → Set) : Set₁ where
  field
    bimap : ∀ {A A′ B B′ : Set} → (A → A′) → (B → B′) → F A B → F A′ B′

record Bifunctor (F : Set → Set → Set) : Set₁ where
  field
    is-raw-bifunctor : RawBifunctor F

  open RawBifunctor is-raw-bifunctor public

  -- According to
  -- https://hackage.haskell.org/package/base-4.19.1.0/docs/Data-Bifunctor.html,
  -- we only need to prove the identity law, and we get the
  -- composition law by free theorems.
  field
    bimap-id : ∀ {A B : Set} (x : F A B) → bimap id id x ≡ x

record RawBiapplicative (F : Set → Set → Set) : Set₁ where
  field
    bipure : ∀ {A B : Set} → A → B → F A B
    _⟪*⟫_ : ∀ {A A′ B B′ : Set} → F (A → A′) (B → B′) → F A B → F A′ B′

  infixl 40 _⟪*⟫_

record Biapplicative (F : Set → Set → Set) : Set₁ where
  field
    is-bifunctor : Bifunctor F
    is-raw-biapplicative : RawBiapplicative F

  open Bifunctor is-bifunctor public
  open RawBiapplicative is-raw-biapplicative public

  field
    -- Pulling these laws from https://a-manning.github.io/posts/2020-08-12-generalizing-biapplicatives/
    bipure-id : ∀ {A B : Set} (v : F A B) → bipure id id ⟪*⟫ v ≡ v
    bipure-homo : ∀ {A A′ B B′ : Set} (f : A → A′) (g : B → B′) (x : A) (y : B) →
                  bipure f g ⟪*⟫ bipure x y ≡ bipure (f x) (g y)
    bipure-interchange : ∀ {A A′ B B′ : Set} (u : F (A → A′) (B → B′)) (x : A) (y : B) →
                         u ⟪*⟫ bipure x y ≡ bipure (_$ x) (_$ y) ⟪*⟫ u
    bipure-∘ : ∀ {A A′ A′′ B B′ B′′} (u : F (A′ → A′′) (B′ → B′′)) (v : F (A → A′) (B → B′)) (w : F A B) →
               bipure _∘′_ _∘′_ ⟪*⟫ u ⟪*⟫ v ⟪*⟫ w ≡ u ⟪*⟫ (v ⟪*⟫ w)

postulate
  Predicate String TType : Set

data PredicateZipper (A B : Set) : Set where
  PEquals : A → B → PredicateZipper A B
  PImplies : Predicate → PredicateZipper A B → PredicateZipper A B
  PForall : String → TType → PredicateZipper A B → PredicateZipper A B

zipper-bimap : ∀ {A A′ B B′ : Set} → (A → A′) → (B → B′) → PredicateZipper A B → PredicateZipper A′ B′
zipper-bimap f g (PEquals a b) = PEquals (f a) (g b)
zipper-bimap f g (PImplies lhs rhs) = PImplies lhs (zipper-bimap f g rhs)
zipper-bimap f g (PForall x t zipper) = PForall x t (zipper-bimap f g zipper)

instance
  RawBifunctorPredicateZipper : RawBifunctor PredicateZipper
  RawBifunctor.bimap RawBifunctorPredicateZipper = zipper-bimap

module _ where

  open RawBifunctor RawBifunctorPredicateZipper

  zipper-bimap-id : ∀ {A B : Set} (x : PredicateZipper A B) →
                    bimap id id x ≡ x
  zipper-bimap-id (PEquals _ _) = refl
  zipper-bimap-id (PImplies x zipper) = cong (PImplies x) (zipper-bimap-id zipper)
  zipper-bimap-id (PForall x x₁ zipper) = cong (PForall x x₁) (zipper-bimap-id zipper)

instance
  BifunctorPredicateZipper : Bifunctor PredicateZipper
  Bifunctor.is-raw-bifunctor BifunctorPredicateZipper = RawBifunctorPredicateZipper
  Bifunctor.bimap-id BifunctorPredicateZipper = zipper-bimap-id

zipper-biapply : ∀ {A A′ B B′ : Set} →
                 PredicateZipper (A → A′) (B → B′) → PredicateZipper A B → PredicateZipper  A′ B′
zipper-biapply (PEquals f g) (PEquals a b) = PEquals (f a) (g b)
zipper-biapply (PEquals f g) (PImplies lhs rhs) = PImplies lhs (zipper-biapply (PEquals f g) rhs)
zipper-biapply (PEquals f g) (PForall name ttype rhs) = PForall name ttype (zipper-biapply (PEquals f g) rhs)
zipper-biapply (PImplies lhs rhs) pab = PImplies lhs (zipper-biapply rhs pab)
zipper-biapply (PForall name ttype rhs) pab = PForall name ttype (zipper-biapply rhs pab)

instance
  RawBiapplicativePredicateZipper : RawBiapplicative PredicateZipper
  RawBiapplicative.bipure RawBiapplicativePredicateZipper = PEquals
  RawBiapplicative._⟪*⟫_ RawBiapplicativePredicateZipper = zipper-biapply

module _ where

  open RawBiapplicative RawBiapplicativePredicateZipper

  zipper-bipure-id : ∀ {A B : Set} (v : PredicateZipper A B) → bipure id id ⟪*⟫ v ≡ v
  zipper-bipure-id (PEquals _ _) = refl
  zipper-bipure-id (PImplies lhs rhs) = cong (PImplies lhs) (zipper-bipure-id rhs)
  zipper-bipure-id (PForall a t body) = cong (PForall a t) (zipper-bipure-id body)

  zipper-bipure-homo : ∀ {A A′ B B′ : Set} (f : A → A′) (g : B → B′) (x : A) (y : B) →
                       bipure f g ⟪*⟫ bipure x y ≡ bipure (f x) (g y)
  zipper-bipure-homo _ _ _ _ = refl

  zipper-bipure-interchange : ∀ {A A′ B B′ : Set} (u : PredicateZipper (A → A′) (B → B′)) (x : A) (y : B) →
                              u ⟪*⟫ bipure x y ≡ bipure (_$ x) (_$ y) ⟪*⟫ u
  zipper-bipure-interchange (PEquals _ _) _ _ = refl
  zipper-bipure-interchange (PImplies lhs rhs) x y = cong (PImplies lhs) (zipper-bipure-interchange rhs x y)
  zipper-bipure-interchange (PForall v t u) x y = cong (PForall v t) (zipper-bipure-interchange u x y)

  zipper-bipure-∘ : ∀ {A A′ A′′ B B′ B′′} (u : PredicateZipper (A′ → A′′) (B′ → B′′))
                    (v : PredicateZipper (A → A′) (B → B′)) (w : PredicateZipper A B) →
                    bipure _∘′_ _∘′_ ⟪*⟫ u ⟪*⟫ v ⟪*⟫ w ≡ u ⟪*⟫ (v ⟪*⟫ w)
  zipper-bipure-∘ (PEquals ua ub) (PEquals va vb) (PEquals wa wb) = refl
  zipper-bipure-∘ (PEquals ua ub) (PEquals va vb) (PImplies wlhs wrhs) = cong (PImplies wlhs) (zipper-bipure-∘ (PEquals ua ub) (PEquals va vb) wrhs)
  zipper-bipure-∘ (PEquals ua ub) (PEquals va vb) (PForall wx wt wbody) = cong (PForall wx wt) (zipper-bipure-∘ (PEquals ua ub) (PEquals va vb) wbody)
  zipper-bipure-∘ (PEquals ua ub) (PImplies vlhs vrhs) w = cong (PImplies vlhs) (zipper-bipure-∘ (PEquals ua ub) vrhs w)
  zipper-bipure-∘ (PEquals ua ub) (PForall vx vt vbody) w = cong (PForall vx vt) (zipper-bipure-∘ (PEquals ua ub) vbody w)
  zipper-bipure-∘ (PImplies ulhs urhs) v w = cong (PImplies ulhs) (zipper-bipure-∘ urhs v w)
  zipper-bipure-∘ (PForall ux ut ubody) v w = cong (PForall ux ut) (zipper-bipure-∘ ubody v w)

instance
  BiapplicativePredicateZipper : Biapplicative PredicateZipper
  Biapplicative.is-bifunctor BiapplicativePredicateZipper = BifunctorPredicateZipper
  Biapplicative.is-raw-biapplicative BiapplicativePredicateZipper = RawBiapplicativePredicateZipper
  Biapplicative.bipure-id BiapplicativePredicateZipper = zipper-bipure-id
  Biapplicative.bipure-homo BiapplicativePredicateZipper = zipper-bipure-homo
  Biapplicative.bipure-interchange BiapplicativePredicateZipper = zipper-bipure-interchange
  Biapplicative.bipure-∘ BiapplicativePredicateZipper = zipper-bipure-∘