Seven Trees in One https://proofassistants.stackexchange.com/questions/1814/seven-trees-in-one-or-how-to-formalize-the-semiring-of-types/1817#1817

S.agda

-- 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.
-- 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.)

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.
-- 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