## 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):

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

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


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

(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'

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

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: May 09 2021 at 20:11 UTC