proof by induction on Z

Stream: general

[Johan Commelin]

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]

That's a funny well founded relation.

[Johan Commelin]

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

[Johan Commelin]

I'm just nesting the inductive property of int and nat.

[Chris Hughes]

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

[Mario Carneiro]

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

[Mario Carneiro]

or use lemmas like chris says

[Chris Hughes]

You could do using_well_founded but proving map_smul first is more sensible

[Johan Commelin]

But why can't I just nest inductive properties?

[Mario Carneiro]

because that's not what you did

[Johan Commelin]

Hmm, so what did I do?

[Mario Carneiro]

you call (n+1) case from -[1+n] case

[Mario Carneiro]

that's not structurally well founded

[Johan Commelin]

Sure, but n+1 is an of_nat, and I had proven those already.

[Mario Carneiro]

that's called a lemma

[Johan Commelin]

/me sighs...

[Mario Carneiro]

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

[Johan Commelin]

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

[Johan Commelin]

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]

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]

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]

I understand why you suggest the other strategy...