Skip to content
{{ message }}

Instantly share code, notes, and snippets.

# gelisam/CategorySolver.agda

Created Apr 5, 2021
Automatically generating proofs which only involve associativity of composition and adding/removing identity morphisms.
 -- Yet another technique for generating proofs in Agda (in addition to the ones -- I've described in https://gist.github.com/gelisam/486d4992c0f3a3f3da2f58ff0e1a3e72): -- transform the proposition into a simpler one which can be proved using refl. -- -- This is the approach I use in my https://github.com/agda/agda-finite-prover -- package, which can prove equations universally-quantified over finite types, -- e.g. proving the commutativity of the boolean function '∧'. I simplify the -- proposition to a long enumeration of all the concrete cases, each of which -- can be proved using refl: -- -- false ∧ false ≡ false ∧ false -- × false ∧ true ≡ true ∧ false -- × true ∧ false ≡ false ∧ true -- × true ∧ true ≡ true ∧ true -- -- This is also the approach used by Tactic.MonoidSolver in the standard library -- (https://github.com/agda/agda-stdlib/blob/master/src/Tactic/MonoidSolver.agda), -- which can prove monoid expresions equivalent if they only differ by the -- placement of the parentheses and the presence of identity elements, e.g. -- -- (0 + x) + (y + 0) ≡ x + 0 + y -- -- It simplifies both sides to their normal form, resulting in a simple -- proposition which can be proved using refl: -- -- x + (y + 0) ≡ x + (y + 0) -- -- In this file, I reimplement the Tactic.MonoidSolver idea, but instead of -- using a monoid with an associative operation and an identity element, I use -- a category, where morphism composition is associative and every object has -- an identity element. That is, I'll be proving -- -- (id >>> f) >>> (g >>> id) ≡ f >>> id >>> g -- -- by rewriting both sides to their normal form: -- -- f >>> (g >>> id) ≡ f >>> (g >>> id) -- -- and then asking the user to provide the easy refl proof of that simplified -- equation. In order to convert this proof into a proof of the original -- equation, we'll need to generate a proof that each side is equal to its -- simplified form. module CategorySolver where open import Data.Fin using (Fin; zero; suc) open import Data.Nat using (ℕ; zero; suc; _+_) open import Data.Vec using (Vec; []; _∷_) open import Relation.Binary.PropositionalEquality import Data.Fin as Fin import Data.Vec as Vec open ≡-Reasoning -- The algorithm is parameterized over an arbitrary category, so we ask the -- user to specify objects, morphisms, identity morphisms, and morphism -- composition. We also ask the user to prove that the identity morphism is an -- identity for morphism composition, and that morphism composition is -- associative. module _ (Object : Set) (Morphism : Object → Object → Set) (id : ∀ {a} → Morphism a a) (_>>>_ : ∀ {a b c} → Morphism a b → Morphism b c → Morphism a c) (let infixr 5 _>>>_; _>>>_ = _>>>_) (id->>> : ∀ {a b} → {f : Morphism a b} → id >>> f ≡ f) (>>>-id : ∀ {a b} → {f : Morphism a b} → f >>> id ≡ f) (>>>->>> : ∀ {a b c d} → {f : Morphism a b} {g : Morphism b c} {h : Morphism c d} → (f >>> g) >>> h ≡ f >>> (g >>> h)) where -- In Agda, the syntax for applying a proof (x≡y : x ≡ y) to prove that -- (x + z) ≡ (y + z) looks like this: -- -- begin -- x + z -- ≡⟨ cong (λ – → – + z) x≡y ⟩ -- y + z -- ∎ -- -- cong asks for a function specifying where we want to apply our proof. I -- find its API a bit too verbose; I would prefer to put the proof x≡y where -- the – is. So I define wrappers for all my binary operators, this way I can -- write this instead: -- -- begin -- x + z -- ≡⟨ ⟨ x≡y +⟩ ⟩ -- y + z -- ∎ ⟨>>>_⟩ : ∀ {a b c} → {f : Morphism a b} {g h : Morphism b c} → g ≡ h → f >>> g ≡ f >>> h ⟨>>>_⟩ {f = f} = cong (λ − → f >>> −) ⟨_>>>⟩ : ∀ {a b c} → {f g : Morphism a b} {h : Morphism b c} → f ≡ g → f >>> h ≡ g >>> h ⟨_>>>⟩ {h = h} = cong (λ − → − >>> h) -- We'll need to be able to pattern-match on the canonical representation -- (f >>> g >>> id). We can't do that if we represent it using a value of -- type Morphism, because the user might have instantiated Morphism to an -- opaque type such as _→_. So we instead represent it as (f ∷ g ∷ []), a -- list-like value which enforces that consecutive morphisms have compatible -- types... data Canon : Object → Object → Set where [] : ∀ {a} → Canon a a _∷_ : ∀ {a b c} → Morphism a b → Canon b c → Canon a c -- ...and which can easily be converted to (f >>> (g >>> id)) when needed. runCanon : ∀ {a b} → Canon a b → Morphism a b runCanon [] = id runCanon (f ∷ fs) = f >>> runCanon fs -- One big advantage of this representation is that it is composable. -- With Morphism, even though (f >>> (g >>> id)) and (h >>> id) are both in -- canonical form, their composition (f >>> (g >>> id)) >>> (h >>> id) is -- not. With the Canon representations (f ∷ g ∷ []) and (h ∷ []), we can -- easily obtain the composition (f ∷ g ∷ h ∷ []) using list-concatenation. -- Which we can now easily implement using pattern-matching. _++_ : ∀ {a b c} → Canon a b → Canon b c → Canon a c [] ++ gs = gs (f ∷ fs) ++ gs = f ∷ (fs ++ gs) -- Note that while (f >>> (g >>> id)) >>> (h >>> id) is not canonical, the -- associativity and identity laws we have assumed for _>>>_ allow us to -- conclude that (f >>> (g >>> id)) >>> (h >>> id) is equal to the canonical -- representation (f >>> (g >>> (h >>> id))), a.k.a. runCanon [f ∷ g ∷ h ∷ id]. -- This will be very helpful in a moment when we prove that each side is -- equal to its canonical form. runCanon-++ : ∀ {a b c} → (fs : Canon a b) → (gs : Canon b c) → runCanon (fs ++ gs) ≡ runCanon fs >>> runCanon gs runCanon-++ [] gs = begin runCanon ([] ++ gs) ≡⟨⟩ runCanon gs ≡⟨ sym id->>> ⟩ id >>> runCanon gs ≡⟨⟩ runCanon [] >>> runCanon gs ∎ runCanon-++ (f ∷ fs) gs = begin runCanon ((f ∷ fs) ++ gs) ≡⟨⟩ runCanon (f ∷ (fs ++ gs)) ≡⟨⟩ f >>> runCanon (fs ++ gs) ≡⟨ ⟨>>> runCanon-++ fs gs ⟩ ⟩ f >>> (runCanon fs >>> runCanon gs) ≡⟨ sym >>>->>> ⟩ (f >>> runCanon fs) >>> runCanon gs ≡⟨⟩ runCanon (f ∷ fs) >>> runCanon gs ∎ -- We once again have to define a data type so we can pattern-match on it. -- This time, it's so we can match on the two sides of the potential equality -- we want to prove: -- -- (id >>> f) >>> (g >>> id) ≡ f >>> id >>> g -- -- will be represented as -- -- ([id] [>>>] [ f ]) [>>>] ([ g ] [>>>] [id]) -- -- and -- -- [ f ] [>>>] [id] [>>>] [ g ] data Expr : Object → Object → Set where [_] : ∀ {a b} → Morphism a b → Expr a b [id] : ∀ {a} → Expr a a _[>>>]_ : ∀ {a b c} → Expr a b → Expr b c → Expr a c infixr 5 _[>>>]_ -- Of course, we can easily convert -- -- ([id] [>>>] [ f ]) [>>>] ([ g ] [>>>] [id]) -- -- to -- -- (id >>> f) >>> (g >>> id) -- -- when needed. runExpr : ∀ {a b} → Expr a b → Morphism a b runExpr [ f ] = f runExpr [id] = id runExpr (e₁ [>>>] e₂) = runExpr e₁ >>> runExpr e₂ -- We are finally ready to simplify each side to its canonical form: -- -- [ f ] [>>>] [id] [>>>] [ g ] -- -- becomes -- -- f ∷ g ∷ [] canon : ∀ {a b} → Expr a b → Canon a b canon [ f ] = f ∷ [] canon [id] = [] canon (e₁ [>>>] e₂) = canon e₁ ++ canon e₂ -- That is, (f >>> id >>> g) becomes (f >>> (g >>> id)). We are now ready to -- show that those that those two expressions are equivalent; that is, that -- each side is equal to its canonical form. runExpr≡runCanon : ∀ {a b} → (e : Expr a b) → runExpr e ≡ runCanon (canon e) runExpr≡runCanon [ f ] = begin runExpr [ f ] ≡⟨⟩ f ≡⟨ sym >>>-id ⟩ f >>> id ≡⟨⟩ runCanon (f ∷ []) ≡⟨⟩ runCanon (canon [ f ]) ∎ runExpr≡runCanon [id] = begin runExpr [id] ≡⟨⟩ id ≡⟨⟩ runCanon [] ≡⟨⟩ runCanon (canon [id]) ∎ runExpr≡runCanon (e₁ [>>>] e₂) = begin runExpr (e₁ [>>>] e₂) ≡⟨⟩ runExpr e₁ >>> runExpr e₂ ≡⟨ ⟨ runExpr≡runCanon e₁ >>>⟩ ⟩ runCanon (canon e₁) >>> runExpr e₂ ≡⟨ ⟨>>> runExpr≡runCanon e₂ ⟩ ⟩ runCanon (canon e₁) >>> runCanon (canon e₂) ≡⟨ sym (runCanon-++ (canon e₁) (canon e₂)) ⟩ runCanon (canon e₁ ++ canon e₂) ≡⟨⟩ runCanon (canon (e₁ [>>>] e₂)) ∎ -- Now that all the pieces are in place, we provide the user with a magic -- function which automatically proves two Morphism expressions equal, for -- the low-low cost of repeating the expressions in Expr form, and providing -- the easy refl proof that the canonical representations are equal. prove : ∀ {a b} → (e₁ e₂ : Expr a b) → canon e₁ ≡ canon e₂ → runExpr e₁ ≡ runExpr e₂ prove e₁ e₂ canon₁≡canon₂ = begin runExpr e₁ ≡⟨ runExpr≡runCanon e₁ ⟩ runCanon (canon e₁) ≡⟨ cong runCanon canon₁≡canon₂ ⟩ runCanon (canon e₂) ≡⟨ sym (runExpr≡runCanon e₂) ⟩ runExpr e₂ ∎ -- For comparison, here's a proof written by hand: long-example : ∀ {a b c} → (f : Morphism a b) (g : Morphism b c) → (id >>> f) >>> (g >>> id) ≡ f >>> id >>> g long-example f g = begin (id >>> f) >>> (g >>> id) ≡⟨ ⟨ id->>> >>>⟩ ⟩ f >>> (g >>> id) ≡⟨ ⟨>>> >>>-id ⟩ ⟩ f >>> g ≡⟨ ⟨>>> sym id->>> ⟩ ⟩ f >>> (id >>> g) ∎ -- Here's the corresponding proof using our solver: short-example : ∀ {a b c} → (f : Morphism a b) (g : Morphism b c) → (id >>> f) >>> (g >>> id) ≡ f >>> id >>> g short-example f g = prove (([id] [>>>] [ f ]) [>>>] ([ g ] [>>>] [id])) ([ f ] [>>>] [id] [>>>] [ g ]) refl -- And of course, using the "type-aware macro" technique I described in -- https://gist.github.com/gelisam/486d4992c0f3a3f3da2f58ff0e1a3e72, we can -- easily generate the Expr (and the refl) arguments from the equation we -- want to prove, this way we don't have to write it twice: -- -- shortest-example : ∀ {a b c} -- → (f : Morphism a b) (g : Morphism b c) -- → (id >>> f) >>> (g >>> id) -- ≡ f >>> id >>> g -- shortest-example f g = proveAuto
to join this conversation on GitHub. Already have an account? Sign in to comment