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_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: Dec 20 2023 at 11:08 UTC