function on sums

Stream: general

[j_lean]

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.

[Reid Barton]

What did you try that involved existsi?

[Kenny Lau]

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⟩

[Kenny Lau]

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

[j_lean]

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