Seven Trees in One, or How to formalize the Semiring of Types?

Question

This is somewhat conceptual beginner's question about proof assistants.

I've been re-reading the famous Seven Trees in One / Objects of categories as complex numbers. The gist: The type $T$ of binary trees admits an explict, combinatorial ismorphism $T \cong T^7$.

One way to see this is that in every commutative semiring, the equation $x = x^2+1$ implies $x = x^7$ (straightforward equational reasoning). We can then construct what the second paper calls the Burnside rig, the commutative semiring of isomorphism classes of types. Because we have an isomorphism $T \cong T^2+1$, the equivalence class $[T]$ in this semiring satisfies $[T] = [T]^7$, hence $T \cong T^7$.

This suggests to me a nice modular way to construct the seven-trees-in-one isomorphism

1. Formalize the Burnside rig
2. use an existing semiring tactic to solve the equational reasoning part
3. extract the isomorphism

For the sake of this question, I will take it as a given that the appropriate semiring tactic exists and can solve (x = x^2 + 1) -> (x = x^7). (I know ring tactics exists, but semiring is slightly more subtle).

My question is thus about the remaining aspects of the formalization. How would we go about this problem in different proof assistants (Coq, Agda, Lean)?

1. Lean has quotients. Can we form the Burnside rig as is? Will we still be able to compute the isomorphism?
2. Would Coq require that its ring tactic does not use vanilla = but setoids?
3. Am I correct to think that under univalence, universes are commutative semirings on the nose? Does this simplify the proof, say in Cubical Agda? I've enjoyed Computing with Semirings and Weak Rig Groupoids but can it be used here in practical terms?

Answer 1

The main subtlety is that it doesn't seem easy to automate the semigroup equational reasoning required by Seven Trees in One, but if we put that process aside (like, accepting to do it by hand, which could still look decent if just associativity and commutativity were handled automatically), I would expect the rest to go as you would expect. I don't know about Lean's quotient, but your given approaches for Coq (generalizing up to proof-relevant equivalence relations) and Agda (using univalence) seem reasonable.

Here's an implementation in Agda, though it does not extract a completely working bijection: one direction generates many applications of transp that Agda doesn't want to reduce for some reason. This might also affect the other direction, but I haven't found an example in my limited number of tests. If you tell it what the right normal term is, it is accepted (thanks to Dan Doel for pointing this out!); that slightly defeats the point of the exercise, hence it's "not completely working".

A neat trick is that you can define the quotient ℕ[X]/(X≡X²+1) directly as a higher inductive type and prove the equation X^7=X in that concrete structure once and for all instead of parameterizing the proof by an abstract semiring. Initiality (aka. "fold") then transports that equation to other semirings with an element satisfying x = x^2+1.

-- 1. Prove X⁷≡X in the polynomial quotient semiring ℕ[X]/(X≡X²+1)
-- 2. Define a map toType : ℕ[X]/(X≡X²+1) → Type,
--    using the semiring structure of Type and the fact that
--    the equation T≡T²+1 holds for the type of binary trees T,
--    thanks to univalence.
-- 3. We deduce T⁷ ≡ T, by T⁷ ≡ toType X⁷ ≡ toType X ≡ T
-- 4. ???
-- 5. Profit

{-# OPTIONS --cubical #-}
module S where

open import Cubical.Core.Everything
open import Cubical.Foundations.Isomorphism
open import Cubical.Foundations.Univalence
open import Cubical.Foundations.Structure
open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Function
open import Cubical.Foundations.Transport
open import Cubical.Foundations.HLevels
open import Cubical.Data.Sigma
open import Cubical.Data.Sum
open import Cubical.Data.Unit
open import Cubical.Data.Nat using (ℕ; zero; suc)

pattern 3+_ n = suc (suc (suc n))
pattern 2+_ n = suc (suc n)
pattern 1+_ n = suc n

infixl 6 _+_

-- * Part 1: X ≡ X²+1 → X⁷ ≡ X
--
-- (X⁷≡X is the name of the final theorem.)
-- The proof follows Seven Trees in One (p 6) https://arxiv.org/pdf/math/9405205.pdf
--
-- X^7 = X^7 + X^4 + X = X
--     by lemma X^(1+r) = X^(1+r) + X^(k+3) + X^k
--     used twice, with r=6,k=1 and with r=0,k=4.
--     (here we only give ad hoc proofs for those two instances)

-- The semiring ℕ[X]/(X≡X²+1)
-- This actually only requires a minimal set of axioms (weaker than semirings)
-- to prove X⁷≡X.
data ℕ[X]/tree : Type where
  _+_ : ℕ[X]/tree → ℕ[X]/tree → ℕ[X]/tree
  X^ : ℕ → ℕ[X]/tree
  +-comm : {a b : ℕ[X]/tree} → a + b ≡ b + a
  +-assoc : {a b c : ℕ[X]/tree} → a + b + c ≡ a + (b + c)
  tree : ∀ n → X^ (1+ n) ≡ X^ (2+ n) + X^ n

treeʳ : ∀ {a} n → a + X^ (suc n) ≡ a + X^ (suc (suc n)) + X^ n
treeʳ {a} n =
  a + X^ (suc n) ≡[ i ]⟨ a + tree n i ⟩
  a + (X^ (suc (suc n)) + X^ n) ≡⟨ sym +-assoc ⟩
  a + X^ (suc (suc n)) + X^ n ∎

-- X^ (n + i) + ... + X^ n (left associated)
X^[_+_] : ℕ → ℕ → ℕ[X]/tree
X^[ n + suc i ] = X^[ suc n + i ] + X^ n
X^[ n + zero ] = X^ n

X²≡X²+X³+1 : ∀ {a} n → a + X^ (2+ n) ≡ a + X^ (2+ n) + X^ (3+ n) + X^ n
X²≡X²+X³+1 {a} n =
  a + X^ (suc (suc n)) ≡⟨ treeʳ (suc n) ⟩
  a + X^ (suc (suc (suc n))) + X^ (suc n) ≡⟨ treeʳ n ⟩
  a + X^ (suc (suc (suc n))) + X^ (suc (suc n)) + X^ n ≡⟨ cong (_+ X^ n) +-assoc ⟩
  a + (X^ (suc (suc (suc n))) + X^ (suc (suc n))) + X^ n ≡⟨ cong (λ x → a + x + X^ n) +-comm ⟩
  a + (X^ (suc (suc n)) + X^ (suc (suc (suc n)))) + X^ n ≡⟨ cong (_+ X^ n) (sym +-assoc) ⟩
  a + X^ (suc (suc n)) + X^ (suc (suc (suc n))) + X^ n ∎

X⁷≡X⁷+X⁴+X : X^ 7 ≡ X^ 7 + X^ 4 + X^ 1
X⁷≡X⁷+X⁴+X =
  X^ 7 ≡⟨ expand-X⁷ ⟩
  X^[ 5 + 3 ] + X^ 3 ≡⟨ X²≡X²+X³+1 1 ⟩
  X^[ 5 + 3 ] + X^ 3 + X^ 4 + X^ 1 ≡[ i ]⟨ expand-X⁷ (~ i) + X^ 4 + X^ 1 ⟩
  X^ 7 + X^ 4 + X^ 1 ∎
  where
    expand-X⁷ : X^ 7 ≡ X^[ 5 + 3 ] + X^ 3
    expand-X⁷ =
                    X^ 7 ≡⟨ tree 6 ⟩
      X^ 8        + X^ 6 ≡⟨ treeʳ 5 ⟩
      X^[ 7 + 1 ] + X^ 5 ≡⟨ treeʳ 4 ⟩
      X^[ 6 + 2 ] + X^ 4 ≡⟨ treeʳ 3 ⟩
      X^[ 5 + 3 ] + X^ 3 ∎

treeˡ : ∀ {a} n → X^ (suc n) + a ≡ X^ (suc (suc n)) + (X^ n + a)
treeˡ {a} n =
  X^ (suc n) + a ≡[ i ]⟨ tree n i + a ⟩
  X^ (suc (suc n)) + X^ n + a ≡⟨ +-assoc ⟩
  X^ (suc (suc n)) + (X^ n + a) ∎

X³+1+X≡X : ∀ {a} n → X^ (3+ n) + X^ n + (X^ (1+ n) + a) ≡ X^ (1+ n) + a
X³+1+X≡X {a} n =
  X^ (3+ n) + X^ n + (X^ (1+ n) + a) ≡⟨ cong (_+ (X^ (1+ n) + a)) +-comm ⟩
  X^ n + X^ (3+ n) + (X^ (1+ n) + a) ≡⟨ sym +-assoc ⟩
  X^ n + X^ (3+ n) + X^ (1+ n) + a ≡⟨ cong (_+ a) (sym (treeʳ (1+ n))) ⟩
  X^ n + X^ (2+ n) + a ≡⟨ cong (_+ a) +-comm ⟩
  X^ (2+ n) + X^ n + a ≡⟨ cong (_+ a) (sym (tree n)) ⟩
  X^ (1+ n) + a ∎

X⁷+X⁴+X≡X : X^ 7 + X^ 4 + X^ 1 ≡ X^ 1
X⁷+X⁴+X≡X =
  X^ 7 + X^ 4 +  X^ 1      ≡[ i ]⟨ X^ 7 + X^ 4 + expand-X i ⟩
  X^ 7 + X^ 4 + (X^ 5 + _) ≡⟨ X³+1+X≡X 4 ⟩
                 X^ 5 + _  ≡⟨ sym expand-X ⟩
                 X^ 1 ∎
  where
    expand-X : X^ 1 ≡ X^ 5 + _
    expand-X =
      X^ 1     ≡⟨ tree 0 ⟩
      X^ 2 + _ ≡⟨ treeˡ 1 ⟩
      X^ 3 + _ ≡⟨ treeˡ 2 ⟩
      X^ 4 + _ ≡⟨ treeˡ 3 ⟩
      X^ 5 + (X^ 3 + (X^ 2 + (X^ 1 + X^ 0))) ∎

X⁷≡X : X^ 7 ≡ X^ 1
X⁷≡X =
  X^ 7               ≡⟨ X⁷≡X⁷+X⁴+X ⟩
  X^ 7 + X^ 4 + X^ 1 ≡⟨ X⁷+X⁴+X≡X ⟩
  X^ 1 ∎

-- * Part 2: Tree as a solution of the equation X ≡ X²+1
--
-- (toType is the name of the final theorem.)
-- (univalence is used via isoToPath)

data Tree : Type where
  Leaf : Tree
  Node : Tree → Tree → Tree

⊎-comm : ∀ {A B : Type} → A ⊎ B ≡ B ⊎ A
⊎-comm = isoToPath ⊎-swap-Iso

⊎-assoc : ∀ {A B C : Type} → (A ⊎ B) ⊎ C ≡ A ⊎ (B ⊎ C)
⊎-assoc = isoToPath ⊎-assoc-Iso

open Iso

Iso-Tree-tree : (A : Type) → Iso (Tree × A) ((Tree × Tree × A) ⊎ A)
Iso-Tree-tree A .fun (Node t₁ t₂ , a) = inl (t₁ , t₂ , a)
Iso-Tree-tree A .fun (Leaf , a) = inr a
Iso-Tree-tree A .inv (inl (t₁ , t₂ , a)) = Node t₁ t₂ , a
Iso-Tree-tree A .inv (inr a) = Leaf , a
Iso-Tree-tree A .rightInv (inl (t₁ , t₂ , a)) = refl
Iso-Tree-tree A .rightInv (inr a) = refl
Iso-Tree-tree A .leftInv (Node t₁ t₂ , a) = refl
Iso-Tree-tree A .leftInv (Leaf , a) = refl

Tree-tree : (A : Type) → (Tree × A) ≡ ((Tree × Tree × A) ⊎ A)
Tree-tree A = isoToPath (Iso-Tree-tree A)

Tree^ : (n : ℕ) → Type
Tree^ 0 = Unit
Tree^ (1+ n) = Tree × Tree^ n

-- This is essentially a way to define a semiring using a HIT,
-- although this particular formulation only covers the substructure
-- generated by Tree.
-- Under univalence (which is used by isoToPath), Type is a semiring.
toType : ℕ[X]/tree → Type
toType (a + b) = toType a ⊎ toType b
toType (X^ n) = Tree^ n
toType (+-comm {a} {b} i) = ⊎-comm {toType a} {toType b} i
toType (+-assoc {a} {b} {c} i) = ⊎-assoc {toType a} {toType b} {toType c} i
toType (tree n i) = Tree-tree (toType (X^ n)) i

-- * Part 3: X⁷≡X ⇒ toType X⁷ ≡ toType X ⇒ Tree⁷ ≡ Tree ⇒ Iso Tree⁷ Tree

Iso-Tree⁷-Tree : Iso (Tree^ 7) Tree
Iso-Tree⁷-Tree =
  Tree^ 7  Iso⟨ pathToIso (λ i → toType (X⁷≡X i)) ⟩
  Tree × Unit  Iso⟨ rUnit×Iso ⟩
  Tree ∎Iso

-- * Examples

f = Iso-Tree⁷-Tree

_ : fun f (Leaf , Leaf , Leaf , Leaf , Leaf , Leaf , Leaf , tt) ≡ Leaf
_ = refl

_ : fun f (Leaf , Leaf , Leaf , Leaf , Leaf , Leaf , Node Leaf Leaf , tt)
  ≡ Node Leaf Leaf
_ = refl

_ : fun f (Node Leaf Leaf , Leaf , Leaf , Leaf , Leaf , Leaf , Leaf , tt)
  ≡ Node (Node  (Node (Node (Node (Node (Node Leaf Leaf) Leaf) Leaf) Leaf) Leaf)  Leaf) Leaf
_ = refl

_ : fun f (Node Leaf Leaf , Node Leaf Leaf , Leaf , Leaf , Leaf , Leaf , Leaf , tt)
  ≡ Node (Node (Node (Node (Node (Node (Node Leaf Leaf) (Node Leaf Leaf)) Leaf) Leaf) Leaf)  Leaf) Leaf
_ = refl

_ : inv f Leaf ≡ (Leaf , Leaf , Leaf , Leaf , Leaf , Leaf , Leaf , tt)
_ = refl -- When you ask Agda to normalize this goal, it gets stuck on transp, lots of transp. But refl still typechecks.

_ : inv f (Node Leaf Leaf) ≡ (Leaf , Leaf , Leaf , Leaf , Leaf , Leaf , Node Leaf Leaf , tt)
_ = refl

Code on Gist: https://gist.github.com/Lysxia/24bc08e7c95aa5594d51e70b9d3842eb