# Zulip Chat Archive

## Stream: general

### Topic: proof by induction on Z

#### Johan Commelin (Dec 09 2018 at 19:01):

Why is a thing like this not possible?

import algebra.group_power theorem map_gsmul {A B} [add_group A] [add_group B] (f : A → B) [is_add_group_hom f] (a : A) : ∀ (n : ℤ), f (gsmul n a) = gsmul n (f a) | (int.of_nat 0) := by simp [gsmul_of_nat, is_add_group_hom.zero f] | (int.of_nat (n+1)) := by simp [gsmul_of_nat, succ_smul, is_add_group_hom.add f]; exact map_gsmul (int.of_nat n) | -[1+n] := begin simp [gsmul_neg, is_add_group_hom.neg f], exact map_gsmul (int.of_nat (n+1)) end

#### Chris Hughes (Dec 09 2018 at 19:05):

That's a funny well founded relation.

#### Johan Commelin (Dec 09 2018 at 19:06):

I wouldn't say it's funny. I think it's very natural.

#### Johan Commelin (Dec 09 2018 at 19:06):

I'm just nesting the inductive property of `int`

and `nat`

.

#### Chris Hughes (Dec 09 2018 at 19:06):

But you haven't told lean what it is. I would just prove `map_smul`

first for naturals

#### Mario Carneiro (Dec 09 2018 at 19:07):

I think you need to be more explicit about the well founded relation

#### Mario Carneiro (Dec 09 2018 at 19:07):

or use lemmas like chris says

#### Chris Hughes (Dec 09 2018 at 19:07):

You could do `using_well_founded`

but proving `map_smul`

first is more sensible

#### Johan Commelin (Dec 09 2018 at 19:07):

But why can't I just nest inductive properties?

#### Mario Carneiro (Dec 09 2018 at 19:07):

because that's not what you did

#### Johan Commelin (Dec 09 2018 at 19:08):

Hmm, so what did I do?

#### Mario Carneiro (Dec 09 2018 at 19:08):

you call `(n+1)`

case from `-[1+n]`

case

#### Mario Carneiro (Dec 09 2018 at 19:08):

that's not structurally well founded

#### Johan Commelin (Dec 09 2018 at 19:08):

Sure, but `n+1`

is an `of_nat`

, and I had proven those already.

#### Mario Carneiro (Dec 09 2018 at 19:08):

that's called a lemma

#### Johan Commelin (Dec 09 2018 at 19:09):

/me sighs...

#### Mario Carneiro (Dec 09 2018 at 19:09):

when you write it all in one big induction lean has no choice but to assume everything depends on everything else

#### Johan Commelin (Dec 09 2018 at 19:10):

But don't you think this is a typical strategy for proving things about Z? Does this deserve special support?

#### Johan Commelin (Dec 09 2018 at 19:11):

Or should I prove `map_smul`

for add_monoid homs? (Btw, I think there is no instance from `add_group_hom`

s to `add_monoid_hom`

s).

#### Kenny Lau (Dec 09 2018 at 19:12):

But don't you think this is a typical strategy for proving things about Z? Does this deserve special support?

I think the typical strategy is to use `int.induction_on`

#### Chris Hughes (Dec 09 2018 at 19:21):

Here's a horrible proof using `using_well_founded`

theorem map_gsmul {A B} [add_group A] [add_group B] (f : A → B) [is_add_group_hom f] (a : A) : ∀ (n : ℤ), f (gsmul n a) = gsmul n (f a) | (int.of_nat 0) := by simp [gsmul_of_nat, is_add_group_hom.zero f] | (int.of_nat (n+1)) := have (n : with_top ℕ) < (n + 1 : ℕ), from with_top.coe_lt_coe.2 (nat.lt_succ_self _), by simp [gsmul_of_nat, succ_smul, is_add_group_hom.add f]; exact map_gsmul (int.of_nat n) | -[1+n] := have ((n + 1 : ℕ) : with_top ℕ) < ⊤, from dec_trivial, begin simp [gsmul_neg, is_add_group_hom.neg f], exact map_gsmul (int.of_nat (n+1)) end using_well_founded {rel_tac := λ _ _, `[exact ⟨_, @inv_image.wf ℤ (with_top ℕ) _ (λ i : ℤ, int.rec_on i coe (λ _, ⊤) : ℤ → with_top ℕ) (with_top.well_founded_lt nat.lt_wf)⟩], dec_tac := tactic.assumption }

#### Johan Commelin (Dec 09 2018 at 19:24):

I understand why you suggest the other strategy...

Last updated: May 15 2021 at 22:14 UTC