Zulip Chat Archive

Stream: new members

Topic: Induction on a submonoid


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?

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

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

Eric Wieser (Nov 11 2020 at 16:57):

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

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

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.

Eric Wieser (Nov 11 2020 at 17:02):

Ah, that's good to know

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

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

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

Kevin Buzzard (Nov 11 2020 at 17:58):

unfold_coes, simp does the first one

Kevin Buzzard (Nov 11 2020 at 17:58):

as does unfold_coes, refl

Kevin Buzzard (Nov 11 2020 at 17:59):

and ext, unfold_coes, refl does the second one

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

Eric Wieser (Nov 11 2020 at 18:02):

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

Eric Wieser (Nov 11 2020 at 18:08):

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

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,
...

Kevin Buzzard (Nov 11 2020 at 18:13):

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

Reid Barton (Nov 11 2020 at 18:13):

Rather than if then else, you can probably use forall

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)

Kevin Buzzard (Nov 11 2020 at 18:16):

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

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

Kevin Buzzard (Nov 11 2020 at 18:18):

I don't understand Reid's comment

Eric Wieser (Nov 11 2020 at 18:18):

Yep, I can finish up from there

Eric Wieser (Nov 11 2020 at 18:18):

Me neither

Kevin Buzzard (Nov 11 2020 at 18:18):

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

Reid Barton (Nov 11 2020 at 18:18):

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

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

Eric Wieser (Nov 11 2020 at 18:19):

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

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?

Kevin Buzzard (Nov 11 2020 at 18:23):

Quantify over proofs everywhere.

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

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

Kevin Buzzard (Nov 11 2020 at 18:27):

oops

Kevin Buzzard (Nov 11 2020 at 18:27):

Maybe my idea doesn't work.

Reid Barton (Nov 11 2020 at 18:27):

maybe \exists is better then?

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"

Kevin Buzzard (Nov 11 2020 at 18:30):

Isn't that what we're proving?

Eric Wieser (Nov 11 2020 at 18:30):

I mean basically yes, it is

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

Kevin Buzzard (Nov 11 2020 at 18:31):

You're using the wrong induction procedure

Kevin Buzzard (Nov 11 2020 at 18:31):

(deleted)

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

Kevin Buzzard (Nov 11 2020 at 18:34):

I think my C' approach is doomed to failure.

Eric Wieser (Nov 11 2020 at 18:34):

It was a nice idea

Reid Barton (Nov 11 2020 at 18:35):

I think you should try with \exists instead

Reid Barton (Nov 11 2020 at 18:35):

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

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,
...

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'

Eric Wieser (Nov 11 2020 at 18:40):

Will try that

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

Eric Wieser (Nov 11 2020 at 18:42):

Yep

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

Eric Wieser (Nov 11 2020 at 18:56):

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

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

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

Eric Wieser (Nov 12 2020 at 09:34):

#4984


Last updated: Dec 20 2023 at 11:08 UTC