Stream: new members

Topic: Casting and inductions

Gareth Ma (Feb 03 2023 at 16:36):

Hi. Just a disclaimer, I know I probably shouldn't worry about tactics in lean 3 too much, but I was just curious + I need to prove the results for my use case.
I am trying to read the proof of ∀ m n, ((m * n : ℤ) : α) = m * n := at https://github.com/leanprover-community/mathlib/blob/bed4f0529aa52e2b169d5c2359eef2849e306028/src/data/int/cast/lemmas.lean#L47, but I don't understand their syntax. In particular, how can I turn the proof into interactive mode while still using int.induction_on'?

Kyle Miller (Feb 03 2023 at 16:40):

@Gareth Ma Here's a tactic proof:

import data.int.cast.lemmas

variables {α : Type*}

@[simp, norm_cast] theorem cast_mul [non_assoc_ring α] (m n : ℤ) : ((m * n : ℤ) : α) = m * n :=
begin
induction m using int.induction_on' with k _ ih k _ ih,
{ exact 0 },
{ simp },
{ simp [sub_mul, ih] },
end


Gareth Ma (Feb 03 2023 at 16:41):

Thank you!! Really helps a lot :heart:

Kyle Miller (Feb 03 2023 at 16:43):

You'll probably more likely see something like this, using refine rather than induction:

@[simp, norm_cast] theorem cast_mul [non_assoc_ring α] (m n : ℤ) : ((m * n : ℤ) : α) = m * n :=
begin
refine int.induction_on' m 0 _ _ _,
{ simp },
{ intros _ ih, simp [add_mul, ih] },
{ intros _ ih, simp [sub_mul, ih] },
end


Kyle Miller (Feb 03 2023 at 16:45):

I guess there's a one-lie tactic proof, where you apply simp to every goal with the contextual option (which allows it to use left sides of implications to simplify right sides).

@[simp, norm_cast] theorem cast_mul [non_assoc_ring α] (m n : ℤ) : ((m * n : ℤ) : α) = m * n :=
begin
refine int.induction_on' m 0 _ _ _; simp { contextual := tt },
end


Last updated: Dec 20 2023 at 11:08 UTC