# How to prove in Lean that sums are distributive?

Assume we are given three types in Lean.

constants A B C : Type


There is a canonical map of the following form.

definition can : sum (A × B) (A × C) → A × (sum B C) :=
λ x , sum.cases_on x  (λ y : A × B, ⟨y.fst, sum.inl y.snd⟩)
(λ y : A × C, ⟨y.fst, sum.inr y.snd⟩)


I believe that this map should have an inverse (according to B. Jacobs book Categorical Logic and Type Theory page 143 coproducts in type theory are automatically distributive). I have trouble constructing the inverse in Lean, because I do not understand how sum.rec works, and I have trouble relating Jacobs unpack P as ... notation to the inductive definition of sums in Lean.

Can someone show me how I can define the inverse of can in Lean using sum.rec?

• You can use triple backquotes () to enclose your code. That makes them easier to visually distinguish and copy.
– Trebor
Apr 29, 2022 at 11:17
• For what it's worth, Lean 3's mathlib contains both directions of this result as equiv.prod_sum_distrib, for which the interesting implementation is here (with A on the right instead of left)
– Eric
Apr 29, 2022 at 20:32

Likely the most idiomatic option is the equation compiler:

variables {A B C : Type}

open sum

def can : sum (A × B) (A × C) → A × (sum B C)
| (inl ⟨a, b⟩) := ⟨a, inl b⟩
| (inr ⟨a, c⟩) := ⟨a, inr c⟩


It may also be worth writing the forward map like this:

variables {A B C : Type}

open sum

def can : sum (A × B) (A × C) → A × (sum B C)
| (inl ab) := ⟨ab.1, inl ab.2⟩
| (inr ac) := ⟨ac.1, inr ac.2⟩


as it probably has a better definitional expansion (Lean 3 doesn't have definitional eta, Lean4 does). I wonder if it's now clear how to write the inverse now, I'll attach it below if not:


def nac : A × (sum B C) → sum (A × B) (A × C)
| ⟨a, inl b⟩ := inl ⟨a, b⟩
| ⟨a, inr c⟩ := inr ⟨a, c⟩


• Yes, I tested it and it works. Thx! I would be especially interested to understand how the notation above expands into the recursor of sum. If you have time, could also explain how I can define nac using nat.rec?
– Nico
Apr 29, 2022 at 11:25
• *sum.rec or sum.rec_on
– Nico
Apr 29, 2022 at 11:32
• You can see the full term mode using the #print command, e.g. #print nac Apr 29, 2022 at 11:36
• I will say that I honestly don't know what term mode I'd expect from this! Apr 29, 2022 at 11:37

I have figured out how to write the inverse using @sum.cases_on. The rules of @sum.cases_on in lean are nearly identical as the rules of match in Jacobs book. The code is:

definition can (α : Type) (β : Type) (γ : Type)
: sum (α × β) (α  × γ) → α × (sum β γ) :=
λ x , sum.cases_on x  (λ y : α × β, ⟨y.fst, sum.inl y.snd⟩)
(λ y : α × γ, ⟨y.fst, sum.inr y.snd⟩)

definition nac (α : Type) (β : Type) (γ : Type)
: α × (sum β γ) → sum (α × β) (α × γ) :=
λ v : α × (sum β γ),
sum.cases_on v.snd
(λ b : β, sum.inl ⟨v.fst,b⟩) (λ c : γ, sum.inr ⟨v.fst,c⟩)

`

I admit that it does not look as good as the version of It'sNotALie.