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

Last updated: May 09 2021 at 20:11 UTC