Stream: general

Topic: Map from sum in standard lib?

Benedikt Ahrens (Mar 18 2020 at 19:49):

Is a function similar to this one (and a notation for it) available in the standard library?

def map_from_sum {A B C : Type} (f : A → C) (g : B → C) : (A ⊕ B) → C
| (sum.inl a) := f a
| (sum.inr b) := g b


Thanks, Benedikt

Kevin Buzzard (Mar 18 2020 at 20:00):

You're really here to check that your students aren't cheating in your Lean course, right? ;-)

Kevin Buzzard (Mar 18 2020 at 20:01):

I was expecting to lay my hands on that function at once, but I can't immediately find it.

Kevin Buzzard (Mar 18 2020 at 20:01):

or.elim : ∀ {a b c : Prop}, a ∨ b → (a → c) → (b → c) → c but I couldn't spot sum.elim

Kevin Buzzard (Mar 18 2020 at 20:03):

oh found it, it's in data.sum

Kevin Buzzard (Mar 18 2020 at 20:03):

ha ha, I didn't even know that file existed.

import data.sum

#check @sum.elim
/-
sum.elim : Π {α : Type u_1} {β : Type u_2} {γ : Sort u_3}, (α → γ) → (β → γ) → α ⊕ β → γ
-/


Reid Barton (Mar 18 2020 at 20:04):

Nice, I didn't know this existed either. Non-dependent eliminators are frequently more convenient, I wish Lean would generate them automatically.

Bryan Gin-ge Chen (Mar 18 2020 at 20:26):

I was surprised that suggest didn't help:

import tactic
import data.sum

def map_from_sum {A B C : Type} (f : A → C) (g : B → C) : (A ⊕ B) → C := by suggest
/- There are no applicable declarations
state:
A B C : Type,
f : A → C,
g : B → C
⊢ A ⊕ B → C -/


Kevin Buzzard (Mar 18 2020 at 20:28):

Might be because it's data not a prop?

Bryan Gin-ge Chen (Mar 18 2020 at 20:41):

Ah, that makes sense. This reminds me of how we couldn't use cc on your "random types" challenge.

Benedikt Ahrens (Mar 22 2020 at 15:27):

I tried hard to find empty.elim (or another map of type empty -> C), but have not been successful. Is such a map pre-defined?

Rob Lewis (Mar 22 2020 at 15:35):

empty.elim does exist (in mathlib, logic.basic, one of the very first imports). There's also empty.rec and empty.rec_on in core.

Bryan Gin-ge Chen (Mar 22 2020 at 15:36):

It's just logic.basic, not data.logic.basic.

Rob Lewis (Mar 22 2020 at 15:38):

I was also surprised suggest didn't find this. Maybe suggest shouldn't filter out Sort * declarations? @Scott Morrison

Last updated: Dec 20 2023 at 11:08 UTC