Zulip Chat Archive

Stream: general

Topic: proof by induction on Z


view this post on Zulip 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

view this post on Zulip Chris Hughes (Dec 09 2018 at 19:05):

That's a funny well founded relation.

view this post on Zulip Johan Commelin (Dec 09 2018 at 19:06):

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

view this post on Zulip Johan Commelin (Dec 09 2018 at 19:06):

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

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Dec 09 2018 at 19:07):

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

view this post on Zulip Mario Carneiro (Dec 09 2018 at 19:07):

or use lemmas like chris says

view this post on Zulip Chris Hughes (Dec 09 2018 at 19:07):

You could do using_well_founded but proving map_smul first is more sensible

view this post on Zulip Johan Commelin (Dec 09 2018 at 19:07):

But why can't I just nest inductive properties?

view this post on Zulip Mario Carneiro (Dec 09 2018 at 19:07):

because that's not what you did

view this post on Zulip Johan Commelin (Dec 09 2018 at 19:08):

Hmm, so what did I do?

view this post on Zulip Mario Carneiro (Dec 09 2018 at 19:08):

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

view this post on Zulip Mario Carneiro (Dec 09 2018 at 19:08):

that's not structurally well founded

view this post on Zulip Johan Commelin (Dec 09 2018 at 19:08):

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

view this post on Zulip Mario Carneiro (Dec 09 2018 at 19:08):

that's called a lemma

view this post on Zulip Johan Commelin (Dec 09 2018 at 19:09):

/me sighs...

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip 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).

view this post on Zulip 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

view this post on Zulip 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 }

view this post on Zulip 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