Induction on a submonoid

Stream: new members

[Eric Wieser]

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]

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

[Reid Barton]

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]

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

[Eric Wieser]

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]

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]

Ah, that's good to know

[Eric Wieser]

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]

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]

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]

unfold_coes, simp does the first one

[Kevin Buzzard]

as does unfold_coes, refl

[Kevin Buzzard]

and ext, unfold_coes, refl does the second one

[Eric Wieser]

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

[Eric Wieser]

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

[Eric Wieser]

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

[Kevin Buzzard]

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]

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

[Reid Barton]

Rather than if then else, you can probably use forall

[Eric Wieser]

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]

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

[Kevin Buzzard]

  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]

I don't understand Reid's comment

[Eric Wieser]

Yep, I can finish up from there

[Eric Wieser]

Me neither

[Kevin Buzzard]

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

[Reid Barton]

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

[Kevin Buzzard]

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

[Eric Wieser]

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

[Kevin Buzzard]

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]

Quantify over proofs everywhere.

[Eric Wieser]

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

[Eric Wieser]

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]

oops

[Kevin Buzzard]

Maybe my idea doesn't work.

[Reid Barton]

maybe \exists is better then?

[Eric Wieser]

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]

Isn't that what we're proving?

[Eric Wieser]

I mean basically yes, it is

[Eric Wieser]

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]

You're using the wrong induction procedure

[Kevin Buzzard]

(deleted)

[Eric Wieser]

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

[Kevin Buzzard]

I think my C' approach is doomed to failure.

[Eric Wieser]

It was a nice idea

[Reid Barton]

I think you should try with \exists instead

[Reid Barton]

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

[Kevin Buzzard]

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]

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

[Eric Wieser]

Will try that

[Kevin Buzzard]

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

[Eric Wieser]

Yep

[Eric Wieser]

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]

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

[Eric Wieser]

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]

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]

#4984