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 ♦
    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 ♦
    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
    Apr 29, 2022 at 11:25
  • $\begingroup$ *sum.rec or sum.rec_on $\endgroup$
    – Nico
    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.
    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.
    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$

Your Answer

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

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