Coproducts in Lean

Question

All,

I am using Lean. I am hoping to obtain a coproduct construction which works something like this:

A : Type
B : Type
COPRODUCT(A, B) : Type
a : A \rightarrow C
b : B \rightarrow C
COPROD(a, b) : COPRODUCT(A, B) \rightarrow C
FIRST : A \rightarrow COPRODUCT(A, B)
SECOND : B \rightarrow COPRODUCT(A, B)
t : COPRODUCT(A, B) \rightarrow C
t \circ FIRST = a
t \circ SECOND = b

Is the easiest way here to use dependent sum over Bool?

Note that this follows pretty literally the universal property for coproduct, which is what I'm aiming for.

Answer 1

To add a bit more commentary to Junyan Xu's answer, yes the built in sum is the right way to go with coproducts, but of course for some applications you just want to make your own new coproduct type or a variation there of. With Lean this is trivial using inductive types. (This is Lean 3 syntax, but with Lean 4 it is similar.)

inductive coproduct (A B : Type*)
| first : A -> coproduct
| second : B -> coproduct

-- type type constructors are automatically created
#print coproduct.first  -- constructor coproduct.first : Π {A : Type u_1} {B : Type u_2}, A → coproduct A B
#print coproduct.second -- constructor coproduct.second : Π {A : Type u_1} {B : Type u_2}, B → coproduct A B

def coprod {A B C : Type*} (f : A -> C) (g : B -> C) : coproduct A B -> C
| (coproduct.first a)  := f a
| (coproduct.second b) := g b

Note, you will almost never need to use the coprod function directly, and I would greatly caution against doing so except in special circumstances. Instead the notation I used to prove coprod is quite general and easy to use. It matches similar match notation used in other functional programming languages. Here are two more examples using both the notation for recursive functions and match notation:

-- this is a recursive function
def coproduct_swap {A B : Type*} : coproduct A B -> coproduct B A
| (coproduct.first a)  := coproduct.second a
| (coproduct.second b) := coproduct.first b

def coproduct_and_function {A B : Type*} (cop : coproduct A B) (f : A -> B) : B :=
-- this example uses match notation
match cop with
| (coproduct.first a)  := f a
| (coproduct.second b) := b
end

---

Given your many questions so far on basic points of the syntax and logic, I would highly recommend that your read and work through the examples in the tutorial "Theorem Proving in Lean" (Lean 3 version, Lean 4 version). I think it would help you a lot with all of your questions. But if you still have follow up questions, feel free to ask them here or on the Lean Zulip.

Answer 2

• COPRODUCT(A, B) is sum
• COPROD(a, b) is sum.elim
• FIRST is sum.inl
• SECOND is sum.inr
• COPROD(a, b) \circ FIRST = a and COPROD(a, b) \circ SECOND = b are sum.elim_inl and sum.elim_inr.