11
$\begingroup$

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?
$\endgroup$
3
  • 1
    $\begingroup$ As for your last point, yes and no! It would be a semiring if you naïvely define that. But note that usually a semiring or any algebraic structure is defined on a set, which a universe is not. Also, the tactic will indeed directly give the (computable) isomorphisms when given a equality on types. $\endgroup$
    – Trebor
    Nov 1, 2022 at 13:31
  • 1
    $\begingroup$ Lean’s quotients use “Prop” in their signature: correspoding equivalence relation for Burnside rig will be in the form “∃ (f : T₁ → T₂), f is bijection” (where ∃ : Π (A : U), (A → U) → Prop), so there will be no way to extract an actual function T₁ → T₂ from [T₁] = [T₂] without affecting canonicity or soundness of type checker. $\endgroup$
    – siegment
    Nov 1, 2022 at 14:48
  • 1
    $\begingroup$ It doesn't appear to me that the Agda solver will work. It doesn't allow you to direct the search by supplying $T = T^2 + 1$ as an input. Rather, you just give it the equation to solve, and it gives you any new goal it can find. In this case, it doesn't make any progress, and just requires a variant of $T = T^7$. If it did somehow figure out the right subgoal, it would work in cubical Agda, though (the 'semiring' structure required would be lax enough). Actually writing the appropriate solver might be quite a hard problem, though. $\endgroup$
    – Dan Doel
    Nov 1, 2022 at 15:14

1 Answer 1

8
$\begingroup$

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

$\endgroup$
3
  • 1
    $\begingroup$ It's not exactly stuck, even though telling Agda to normalize the expression displays a bunch of transp. You can fill in the inv f Leaf case with a 7-tuple of Leaf, and the last case with a 6 copies of Leaf followed by Node Leaf Leaf. Both equations are provable by refl. I'm not really sure why it doesn't reduce this way. $\endgroup$
    – Dan Doel
    Nov 3, 2022 at 5:22
  • $\begingroup$ Huh. thanks for the save! $\endgroup$
    – Li-yao Xia
    Nov 3, 2022 at 5:55
  • $\begingroup$ Very nice idea to axiomatize the quotient semiring directly! And thanks for the working example. $\endgroup$
    – Dario
    Nov 3, 2022 at 18:10

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.