Solver based on https://webspace.science.uu.nl/~swier004/publications/2021-jfp-submission.pdf

DiffSolver.agda

{-# OPTIONS --without-K --postfix-projections --safe #-}
module DiffSolver where

open import Algebra
open import Function.Base
open import Relation.Binary.PropositionalEquality as ≡ using (_≡_)

module WithMonoid {c ℓ} (monoid : Monoid c ℓ) where
  open Monoid monoid
  open import Relation.Binary.Reasoning.Setoid setoid

  infixl 5 _∙D_

  DiffCarrier : Set c
  DiffCarrier = Carrier → Carrier

  reify : DiffCarrier → Carrier
  reify x = x ε

  reflect : Carrier → DiffCarrier
  reflect x = x ∙_

  reify-reflect : (x : Carrier) → reify (reflect x) ≈ x
  reify-reflect x = identityʳ x

  εD : DiffCarrier
  εD = id

  _∙D_ : (x y : DiffCarrier) → DiffCarrier
  x ∙D y = x ∘ y

  data Expr : Set c where
    ι : Carrier → Expr
    εS : Expr
    _∙S_ : (M N : Expr) → Expr

  ⟦_⟧ : Expr → Carrier
  ⟦ ι x ⟧ = x
  ⟦ εS ⟧ = ε
  ⟦ M ∙S N ⟧ = ⟦ M ⟧ ∙ ⟦ N ⟧

  ⟦_⟧D : Expr → DiffCarrier
  ⟦ ι x ⟧D = reflect x
  ⟦ εS ⟧D = εD
  ⟦ M ∙S N ⟧D = ⟦ M ⟧D ∙D ⟦ N ⟧D

  sound′ : ∀ M z → ⟦ M ⟧D z ≈ ⟦ M ⟧ ∙ z
  sound′ (ι x) z = refl
  sound′ εS z = sym (identityˡ z)
  sound′ (M ∙S N) z = begin
    ⟦ M ⟧D (⟦ N ⟧D z)    ≈⟨ sound′ M _ ⟩
    ⟦ M ⟧ ∙ (⟦ N ⟧D z)   ≈⟨ ∙-congˡ (sound′ N _) ⟩
    ⟦ M ⟧ ∙ (⟦ N ⟧ ∙ z) ≈˘⟨ assoc _ _ _ ⟩
    (⟦ M ⟧ ∙ ⟦ N ⟧) ∙ z  ∎

  sound : ∀ M → reify ⟦ M ⟧D ≈ ⟦ M ⟧
  sound M = begin
    reify ⟦ M ⟧D  ≡⟨⟩
    ⟦ M ⟧D ε   ≈⟨ sound′ M ε ⟩
    ⟦ M ⟧ ∙ ε  ≈⟨ identityʳ _ ⟩
    ⟦ M ⟧      ∎

  solve : (M N : Expr) → ⟦ M ⟧D ≡ ⟦ N ⟧D → ⟦ M ⟧ ≈ ⟦ N ⟧
  solve M N q = begin
    ⟦ M ⟧        ≈˘⟨ sound M ⟩
    reify ⟦ M ⟧D  ≡⟨ ≡.cong reify q ⟩
    reify ⟦ N ⟧D  ≈⟨ sound N ⟩
    ⟦ N ⟧         ∎

  test : (x y : Carrier) → (ε ∙ x) ∙ (y ∙ ε) ≈ x ∙ (ε ∙ y)
  test x y = solve ((εS ∙S ι x) ∙S (ι y ∙S εS)) (ι x ∙S (εS ∙S ι y)) ≡.refl