submodule induction

Stream: maths

[Antoine Chambert-Loir]

I found that I had the need of a more general induction procedure for ideals or submodules, similar to docs#submodule.induction_on, when one already knows that the submodule will be contained in a given submodule. In this case, the hypotheses can be weakened. Here is an example:

universes u v
variables {R : Type u} {M : Type v} {F : Type*} {G : Type*}
variables [comm_semiring R] [add_comm_monoid M] [module R M]
variables {I J : ideal R} {N P Q : submodule R M}

theorem submodule.smul_induction_on' {p : M → Prop} (hQ : ∀ x, x ∈ I • N → x ∈ Q) {x} (H : x ∈ I • N)
  (Hb : ∀ (r ∈ I) (n ∈ N), p (r • n))
  (H1 : ∀ (x ∈ Q) (y ∈ Q), p x → p y → p (x + y)) : p x :=
begin
  suffices : x ∈ Q ∧ p x, exact this.2,
  exact submodule.smul_induction_on H
  (λ a ha x hx, ⟨(hQ (a • x) (submodule.smul_mem_smul ha hx)), Hb a ha x hx⟩)
  (λ x y hx hy, ⟨Q.add_mem hx.1 hy.1, H1 x hx.1 y hy.1 hx.2 hy.2⟩),
end

On the other hand one can mimick this everytime. Do you believe that the more general procedure should be added to mathlib ?

[Patrick Massot]

Yes, induction principles are good.

[Antoine Chambert-Loir]

In fact, I realize that docs#submodule.supr_induction should be generalized from

lemma supr_induction {ι : Sort*} (p : ι → submodule R M) {C : M → Prop} {x : M} (hx : x ∈ ⨆ i, p i)
  (hp : ∀ i (x ∈ p i), C x)
  (h0 : C 0)
  (hadd : ∀ x y, C x → C y → C (x + y)) : C x := sorry

to

lemma supr_induction' {ι : Sort*} (p : ι → submodule R M) {C : M → Prop} {x : M} (hx : x ∈ ⨆ i, p i)
  (hp : ∀ i (x ∈ p i), C x)
  (h0 : C 0)
  (hadd : ∀ (x ∈ ⨆ i, p i) (y ∈ ⨆ i, p i), C x → C y → C (x + y)) : C x := sorry

(the proof is easy, up to a similar modification of add_submonoid.supr_induction and possibly going on inductively…)

[Antoine Chambert-Loir]

(The present statement requires that the predicate C be additive, while it is sufficient that it is additive on ⨆ i, p i.

[Eric Wieser]

I think that suggestion is the same as how we extended docs#submodule.span_induction with docs#submodule.span_induction'?

[Eric Wieser]

In fact, submodule.span_induction' suggests a more general form where even the motive depends on (∈ ⨆ i, p i)

[Eric Wieser]

... Which exists already, it's docs#submodule.supr_induction' and I wrote it at the same time as the unprimed version in #11556!

[Eric Wieser]

Based on that, I would say that submodule.smul_induction_on' is a good idea to PR, but it should be generalized to {p : Π (x : M), x ∈ I • N → Prop}

[Antoine Chambert-Loir]

OK, I'll push something.
One remark : it seems to me that the order of the arguments for doc#submodule.span_induction' is a bit strange : since {x} (hx : x ∈ submodule.span R s) are the last one, the function requires four _ to be easily applied. The other induction lemmas have {x} (hx) for their first argument.

[Eric Wieser]

Lemmas tagged with elab_as_eliminator shouldn't be used with apply anyway, as they tend not to infer the motive correctly

[Eric Wieser]

They behave better with refine, but at that point the argument order is irrelevant