Zulip Chat Archive

Stream: general

Topic: function on sums


view this post on Zulip j_lean (Jun 26 2019 at 21:57):

Hi all,

I need to define a function on a sum of two types in a proof, but I am not sure how to do it. Does anyone know how to do that?

I'd like to prove this theorem:

theorem sumfunc: ∃ f : sum ℕ ℤ → ℕ, ∀ a : ℕ, f (sum.inl a) = 0 ∧ ∀ b : ℤ, f (sum.inr b) = 1 :=

The function should be f x = 0 if x : \nat and f x = 1 if x : \int. I have used the tactic "existsi", but I am not successful.

Although I can't define the function inside the proof, but I can define it as a definition in Lean. Here it is:

definition f (x : sum ℕ ℤ) : ℕ := sum.cases_on x (λ x, 0) (λ x, 1).

Thanks.

view this post on Zulip Reid Barton (Jun 26 2019 at 21:59):

What did you try that involved existsi?

view this post on Zulip Kenny Lau (Jun 26 2019 at 22:00):

theorem sumfunc :  f : sum    , ( a : , f (sum.inl a) = 0)  ( b : , f (sum.inr b) = 1) :=
sum.rec (λ n, 0) (λ n, 1), λ n, rfl, λ n, rfl

view this post on Zulip Kenny Lau (Jun 26 2019 at 22:01):

definition f (x : sum  ) :  := sum.cases_on x (λ x, 0) (λ x, 1)

theorem sumfunc :  f : sum    , ( a : , f (sum.inl a) = 0)  ( b : , f (sum.inr b) = 1) :=
begin
  existsi f, split; intros; refl
end

view this post on Zulip j_lean (Jun 28 2019 at 20:20):

Thanks Kenny Lau. It's nice to define the function before the theorem.


Last updated: May 11 2021 at 12:15 UTC