Zulip Chat Archive

Stream: new members

Topic: Induction on a submonoid


view this post on Zulip Eric Wieser (Nov 11 2020 at 16:42):

I'm having trouble inducting over elements of a submonoid, and assume I must be doing something wrong. The mwe is:

import algebra.algebra.basic

variables (R : Type*) (M : Type*) (A : Type*) [comm_semiring R] [semiring A] [algebra R A]

def my_fun (m : M) : A := sorry  -- not relevant

def my_monoid := submonoid.closure $ set.range (my_fun M A)

@[simp] lemma my_fun_mem (m : M) : my_fun M A m  my_monoid M A :=
submonoid.subset_closure $ set.mem_range_self m

lemma induction {C : my_monoid M A  Prop}
  (h_one : C 1, submonoid.one_mem (my_monoid M A)⟩)
  (h_fun :  (m : M), C my_fun M A m, my_fun_mem M A m⟩)
  (h_mul :  a b, C a  C b  C (a * b))
  (v : my_monoid M A) :
  C v :=
begin
  rw subtype.coe_eta v v.prop,
  exact submonoid.closure_induction v.prop
    (λ x hx, by {
      obtain a, rfl := set.mem_range.mpr hx,
      convert h_fun a, apply subtype.eq, refl })
    (by { convert h_one, apply subtype.eq, simp only [ring_hom.map_one]})
    (λ x y hx hy, by {
      sorry,
    })
end

Alarmingly, this gives a type error at the word lemma, rather than telling me which of my tactics failed.

What am I missing here?

view this post on Zulip Reid Barton (Nov 11 2020 at 16:55):

I think Lean's error reporting might have difficulty with this ~5-tuply interleaved term/tactic mode proof

view this post on Zulip Reid Barton (Nov 11 2020 at 16:56):

but anyways, I think the real issue is that you can't apply submonoid.closure_induction directly because its motive C isn't allowed to depend on the proof of membership

view this post on Zulip Eric Wieser (Nov 11 2020 at 16:57):

I tried various levels of unweaving, and none seemed to help with the error message

view this post on Zulip Eric Wieser (Nov 11 2020 at 16:58):

Presumably I need to use docs#submonoid.dense_induction, and show that under the subtype my_monoid , the closure of set.range (my_fun M A) after coercion is \top

view this post on Zulip Reid Barton (Nov 11 2020 at 17:00):

Well for example, if you replace the whole exact tactic with apply submonoid.closure_induction v.prop, then you get an error message on apply.

view this post on Zulip Eric Wieser (Nov 11 2020 at 17:02):

Ah, that's good to know

view this post on Zulip Eric Wieser (Nov 11 2020 at 17:04):

I think I need to start by proving

example  (A : Type*) [monoid A] (s : set A) : submonoid.closure (coe ⁻¹' s : set (submonoid.closure s)) =  := sorry

so that I have the first argument to dense_induction

view this post on Zulip Eric Wieser (Nov 11 2020 at 17:50):

This is proving difficult:

example (A : Type*) [monoid A] (s : set A) : submonoid.closure (coe ⁻¹' s : set (submonoid.closure s)) =  :=
begin
  ext,
  simp,
  apply subtype.rec_on x,
  intros x xprop,
  refine submonoid.closure_induction xprop (λ y hy, _) _ (λ a b ha hb, _),
  { simp_rw submonoid.mem_coe,
    apply submonoid.subset_closure,
    simp_rw set.mem_preimage,
    have := subtype.coe_mk y hy,
    rw this at hy,
    convert hy,
    },
  { convert submonoid.one_mem _,
    ext,
    sorry, -- ↑⟨1, xprop⟩ = ↑1
  },
  { convert submonoid.mul_mem _ ha hb,
    sorry, -- ⟨a * b, xprop⟩ = ⟨a, xprop⟩ * ⟨b, xprop⟩
  }
end

Both the remaining goals are something I'd hope to close with refl, but I can't and I don't know what to do next

view this post on Zulip Eric Wieser (Nov 11 2020 at 17:52):

If I add ext before the last sorry, then I get a type error at the word example again

Nevermind, the type error was there anyway and I missed it

view this post on Zulip Kevin Buzzard (Nov 11 2020 at 17:58):

unfold_coes, simp does the first one

view this post on Zulip Kevin Buzzard (Nov 11 2020 at 17:58):

as does unfold_coes, refl

view this post on Zulip Kevin Buzzard (Nov 11 2020 at 17:59):

and ext, unfold_coes, refl does the second one

view this post on Zulip Eric Wieser (Nov 11 2020 at 17:59):

Turns out it's irrelevant, the tactic state was telling me to keep going even though a type error had already appeared

view this post on Zulip Eric Wieser (Nov 11 2020 at 18:02):

But thanks, that does indeed close the goals! (despite not fixing the type error)

view this post on Zulip Eric Wieser (Nov 11 2020 at 18:08):

In fact, I seem to run into exactly the same problem I had before

view this post on Zulip Kevin Buzzard (Nov 11 2020 at 18:10):

What do you think about this approach:

lemma induction {C : my_monoid M A  Prop}
  (h_one : C 1, submonoid.one_mem (my_monoid M A)⟩)
  (h_fun :  (m : M), C my_fun M A m, my_fun_mem M A m⟩)
  (h_mul :  a b, C a  C b  C (a * b))
  (v : my_monoid M A) :
  C v :=
begin
  classical,
  set C' : A  Prop := λ a, if ha : a  my_monoid M A then C a, ha else true with hC',
  cases v with v hv,
  suffices : C' v,
  { rw hC' at this,
    split_ifs at this,
      exact this,
    exact this,
  },
  apply submonoid.closure_induction,
...

view this post on Zulip Kevin Buzzard (Nov 11 2020 at 18:13):

apply submonoid.closure_induction hv, might be an even better last line

view this post on Zulip Reid Barton (Nov 11 2020 at 18:13):

Rather than if then else, you can probably use forall

view this post on Zulip Eric Wieser (Nov 11 2020 at 18:16):

I get stuck trying to unfold C' in the goal there, from

this: C my_fun M A a, _
 C' (my_fun M A a)

view this post on Zulip Kevin Buzzard (Nov 11 2020 at 18:16):

That's why I used set not let -- you can rw hC'

view this post on Zulip Kevin Buzzard (Nov 11 2020 at 18:18):

  apply submonoid.closure_induction hv; rw hC',
  { intros x hx,
    split_ifs, swap, trivial,
    rcases hx with m, rfl⟩,
    exact h_fun _,
  },

There's the first one

view this post on Zulip Kevin Buzzard (Nov 11 2020 at 18:18):

I don't understand Reid's comment

view this post on Zulip Eric Wieser (Nov 11 2020 at 18:18):

Yep, I can finish up from there

view this post on Zulip Eric Wieser (Nov 11 2020 at 18:18):

Me neither

view this post on Zulip Kevin Buzzard (Nov 11 2020 at 18:18):

Oh, probably "for all proofs that it's in your submonoid..."

view this post on Zulip Reid Barton (Nov 11 2020 at 18:18):

set C' : A → Prop := λ a, \all ha : a ∈ my_monoid M A, C ⟨a, ha⟩

view this post on Zulip Kevin Buzzard (Nov 11 2020 at 18:19):

that's nicer because you'll have those to hand and won't need the split_ifs

view this post on Zulip Eric Wieser (Nov 11 2020 at 18:19):

Does this belong in mathlib somewhere? submonoid.closure_induction'?

view this post on Zulip Kevin Buzzard (Nov 11 2020 at 18:23):

This has something to do with your two submonoids and you want to quotient out one by the other, right? My instinct when I look at your lemma is "why not use Reid's trick to define your C and have things like a and b in h_mul quantify over all of A rather than just the submonoid", but perhaps this is not convenient for you in your situation?

view this post on Zulip Kevin Buzzard (Nov 11 2020 at 18:23):

Quantify over proofs everywhere.

view this post on Zulip Eric Wieser (Nov 11 2020 at 18:24):

I don't think I can finish off the last part of the proof with reid's trick

view this post on Zulip Eric Wieser (Nov 11 2020 at 18:25):

lemma induction {C : my_monoid M A  Prop}
  (h_one : C 1, submonoid.one_mem (my_monoid M A)⟩)
  (h_fun :  (m : M), C my_fun M A m, my_fun_mem M A m⟩)
  (h_mul :  a b, C a  C b  C (a * b))
  (v : my_monoid M A) :
  C v :=
begin
  classical,
  set C' : A  Prop := λ a,  ha : a  my_monoid M A, C a, ha with hC',
  cases v with v hv,
  suffices : C' v,
  { rw hC' at this,
    exact this _,
  },
  apply submonoid.closure_induction hv,
  { intros x hx,
    rw hC',
    intro ha,
    obtain a, rfl := set.mem_range.mpr hx,
    exact h_fun a, },
  { rw hC', intro ha, exact h_one },
  { intros x y hx hy, rw hC', intros ha,
    rw hC' at hx hy,
    sorry, },
end

view this post on Zulip Kevin Buzzard (Nov 11 2020 at 18:27):

oops

view this post on Zulip Kevin Buzzard (Nov 11 2020 at 18:27):

Maybe my idea doesn't work.

view this post on Zulip Reid Barton (Nov 11 2020 at 18:27):

maybe \exists is better then?

view this post on Zulip Eric Wieser (Nov 11 2020 at 18:29):

Are we missing some important lemma? It seems like there should be something that says "within a submonoid.closure s, the elements of s when embedded in the subtype are the generators of the entire subtype"

view this post on Zulip Kevin Buzzard (Nov 11 2020 at 18:30):

Isn't that what we're proving?

view this post on Zulip Eric Wieser (Nov 11 2020 at 18:30):

I mean basically yes, it is

view this post on Zulip Eric Wieser (Nov 11 2020 at 18:31):

That's what my submonoid.closure (coe ⁻¹' s : set (submonoid.closure s)) = ⊤ statement above was attempting to be - my hope was that eliminating the my_fun stuff would make it simpler to prove

view this post on Zulip Kevin Buzzard (Nov 11 2020 at 18:31):

You're using the wrong induction procedure

view this post on Zulip Kevin Buzzard (Nov 11 2020 at 18:31):

(deleted)

view this post on Zulip Eric Wieser (Nov 11 2020 at 18:32):

It would be great if lemmas could be tagged with "this is an induction procedure" to help me find the right one

view this post on Zulip Kevin Buzzard (Nov 11 2020 at 18:34):

I think my C' approach is doomed to failure.

view this post on Zulip Eric Wieser (Nov 11 2020 at 18:34):

It was a nice idea

view this post on Zulip Reid Barton (Nov 11 2020 at 18:35):

I think you should try with \exists instead

view this post on Zulip Reid Barton (Nov 11 2020 at 18:35):

that way you're proving membership and C at the same time

view this post on Zulip Kevin Buzzard (Nov 11 2020 at 18:39):

begin
  classical,
  set C' : A  Prop := λ a,  ha : a  my_monoid M A, C a, ha with hC',
  cases v with v hv,
  suffices : C' v,
  { cases this with m hm,
    convert hm },
  apply submonoid.closure_induction hv,
...

view this post on Zulip Kevin Buzzard (Nov 11 2020 at 18:40):

I think Reid's right. This won't have the problems which mul had with my original C'

view this post on Zulip Eric Wieser (Nov 11 2020 at 18:40):

Will try that

view this post on Zulip Kevin Buzzard (Nov 11 2020 at 18:40):

I think my original C' was logically equivalent to Reid's forall C', but this is different. Mul works, for starters

view this post on Zulip Eric Wieser (Nov 11 2020 at 18:42):

Yep

view this post on Zulip Eric Wieser (Nov 11 2020 at 18:42):

lemma induction {C : my_monoid M A  Prop}
  (h_one : C 1, submonoid.one_mem (my_monoid M A)⟩)
  (h_fun :  (m : M), C my_fun M A m, my_fun_mem M A m⟩)
  (h_mul :  a b, C a  C b  C (a * b))
  (v : my_monoid M A) :
  C v :=
begin
  set C' : A  Prop := λ a,  ha : a  my_monoid M A, C a, ha with hC',
  cases v with v hv,
  suffices : C' v,
  { obtain _, h := this,
    exact h,
  },
  apply submonoid.closure_induction hv,
  { intros x hx,
    use submonoid.subset_closure hx,
    obtain a, rfl := set.mem_range.mpr hx,
    exact h_fun a, },
  { rw hC', use submonoid.one_mem _, exact h_one },
  { rintros x y hx', hx hy', hy⟩,
    use submonoid.mul_mem _ hx' hy',
    exact h_mul _ _ hx hy, },
end

view this post on Zulip Eric Wieser (Nov 11 2020 at 18:56):

I'll try to distil to something more generally applicable tomorrow

view this post on Zulip Eric Wieser (Nov 12 2020 at 08:51):

Golfed to

lemma induction' {s : set A} {C : submonoid.closure s  Prop}
  (h_one : C 1, (submonoid.closure s).one_mem⟩)
  (h_closure :  a (h : a  s), C a, submonoid.subset_closure h⟩)
  (h_mul :  a b, C a  C b  C (a * b))
  (v : submonoid.closure s) :
  C v :=
subtype.rec_on v $ λ v hv, begin
  refine exists.elim _ (λ (hv : v  submonoid.closure s) (hc : C v, hv⟩), hc),
  exact submonoid.closure_induction hv
    (λ x hx, submonoid.subset_closure hx, h_closure x hx⟩)
    submonoid.one_mem _, h_one
    (λ x y hx hy, exists.elim hx $ λ hx' hx, exists.elim hy $ λ hy' hy,
      submonoid.mul_mem _ hx' hy', h_mul _ _ hx hy⟩),
end

view this post on Zulip Eric Wieser (Nov 12 2020 at 09:12):

And the other lemma,

lemma closure_coe_preimage_eq_top (A : Type*) [monoid A] (s : set A) : submonoid.closure (coe ⁻¹' s : set (submonoid.closure s)) =  :=
begin
  ext v,
  simp only [iff_true, submonoid.mem_top],
  cases v with v hv,
  suffices :  ha : v  submonoid.closure s, (⟨v, ha : submonoid.closure s)  submonoid.closure (coe ⁻¹' s),
  { obtain _, h := this,
    exact h, },
  exact submonoid.closure_induction hv
    (λ x hx, submonoid.subset_closure hx, submonoid.subset_closure $ set.mem_preimage.mpr hx⟩)
    submonoid.one_mem _, submonoid.one_mem _
    (λ x y hx hy, exists.elim hx $ λ hx' hx, exists.elim hy $ λ hy' hy,
      submonoid.mul_mem _ hx' hy', submonoid.mul_mem _ hx hy⟩),
end

view this post on Zulip Eric Wieser (Nov 12 2020 at 09:34):

#4984


Last updated: May 09 2021 at 20:11 UTC