## 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

/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_homs to add_monoid_homs).

#### 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