6
$\begingroup$

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?

Improve this question
$\endgroup$
2
  • $\begingroup$ You can use triple backquotes (`) to enclose your code. That makes them easier to visually distinguish and copy. $\endgroup$
    – Trebor ♦
    Commented Apr 29, 2022 at 11:17
  • 1
    $\begingroup$ 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) $\endgroup$
    – Eric ♦
    Commented Apr 29, 2022 at 20:32

2 Answers 2

Reset to default
4
$\begingroup$

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⟩

Improve this answer
$\endgroup$
4
  • $\begingroup$ 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? $\endgroup$
    – Nico
    Commented Apr 29, 2022 at 11:25
  • $\begingroup$ *sum.rec or sum.rec_on $\endgroup$
    – Nico
    Commented Apr 29, 2022 at 11:32
  • $\begingroup$ You can see the full term mode using the #print command, e.g. #print nac $\endgroup$
    – It'sNotALie.
    Commented Apr 29, 2022 at 11:36
  • $\begingroup$ I will say that I honestly don't know what term mode I'd expect from this! $\endgroup$
    – It'sNotALie.
    Commented Apr 29, 2022 at 11:37
2
$\begingroup$

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.

Improve this answer
$\endgroup$

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