Induction on subsets of a finset

Stream: maths

[Thomas Browning]

Is there a way to do induction on subsets of a finset? Something like:

theorem induction_on' {α : Type*} {p : finset α → Prop} [decidable_eq α]
  (S : finset α) (h₁ : p ∅) (h₂ : ∀ {a ∈ S} {s ⊆ S}, a ∉ s → p s → p (insert a s)) : p S :=

[Kevin Buzzard]

This works:

import tactic

theorem induction_on' {α : Type*} {p : finset α → Prop} [decidable_eq α]
  (S : finset α) (h₁ : p ∅) (h₂ : ∀ {a ∈ S} {s ⊆ S}, a ∉ s → p s → p (insert a s)) : p S :=
begin
  let q : finset α → Prop := λ T, T ⊆ S → p T,
  suffices : ∀ T : finset α, q T,
    apply this S (by refl),
  have hq₁ : q ∅,
    rintro -, exact h₁,
  refine finset.induction hq₁ _,
  intros a s has hqs,
  rintro hs,
  apply h₂ has,
  { apply hqs,
    refine finset.subset.trans _ hs,
    exact finset.subset_insert a s },
  { apply hs,
    exact finset.mem_insert_self a s },
  { refine finset.subset.trans _ hs,
    exact finset.subset_insert a s}
end

and I'm sure it can be golfed. The idea is to beef p up into a predicate q which is true for all finsets and then prove it by the finset induction lemma in mathlib. Might be worth a PR if you can tidy up the proof a bit?

[Thomas Browning]

that seems like a decent way to do it. I was trying to do it by working on finset (subtype (λ x, x ∈ S)), but it wasn't pretty

[Kevin Buzzard]

An analogous question came up recently (Eric, Reid and I were talking about some induction principle for submodules) and the same sort of idea worked there, that's why I went for it first on this occasion.

[Kevin Buzzard]

I have really got into the habit of using apply to take shortcuts (why use refine h _ _ when you can just apply h?) but actually I am now coming back to refine. Lean's unifier works best if it knows exactly what goal it is supposed to be proving. If you turn the applys into refines by inserting the appropriate _s then you will be able to compress this a bunch.

[Thomas Browning]

theorem induction_on' {α : Type*} {p : finset α → Prop} [decidable_eq α]
  (S : finset α) (h₁ : p ∅) (h₂ : ∀ {a ∈ S} {s ⊆ S}, a ∉ s → p s → p (insert a s)) : p S :=
begin
  let q : finset α → Prop := λ T, T ⊆ S → p T,
  suffices : q S,
  { exact this (finset.subset.refl S) },
  apply finset.induction_on S,
  { exact λ _, h₁ },
  intros a s has hqs hs,
  refine h₂ has (hqs (finset.insert_subset.1 hs).2),
  { exact (finset.insert_subset.1 hs).1, },
  { exact (finset.insert_subset.1 hs).2, }
end

[Thomas Browning]

should I PR it?

[Eric Wieser]

I think you can combine the suffices and the let

[Eric Wieser]

The similar lemma Kevin is referring to is docs#submonoid.closure_induction'

[Thomas Browning]

Before I PR, what's preferable for mathlib: The above tactic mode proof of this term mode proof?

theorem induction_on' {α : Type*} {p : finset α → Prop} [decidable_eq α]
  (S : finset α) (h₁ : p ∅) (h₂ : ∀ {a ∈ S} {s ⊆ S}, a ∉ s → p s → p (insert a s)) : p S :=
@finset.induction_on α (λ T, T ⊆ S → p T) _ S (λ _, h₁) (λ a s has hqs hs,
  (@h₂ a (finset.insert_subset.1 hs).1 s (finset.insert_subset.1 hs).2
  has (hqs (finset.insert_subset.1 hs).2))) (finset.subset.refl S)

[Kevin Buzzard]

finset was mostly written by Mario and I can guess what he'd prefer, from induction:

@[elab_as_eliminator]
protected theorem induction {α : Type*} {p : finset α → Prop} [decidable_eq α]
  (h₁ : p ∅) (h₂ : ∀ ⦃a : α⦄ {s : finset α}, a ∉ s → p s → p (insert a s)) : ∀ s, p s
| ⟨s, nd⟩ := multiset.induction_on s (λ _, h₁) (λ a s IH nd, begin
    cases nodup_cons.1 nd with m nd',
    rw [← (eq_of_veq _ : insert a (finset.mk s _) = ⟨a ::ₘ s, nd⟩)],
    { exact h₂ (by exact m) (IH nd') },
    { rw [insert_val, ndinsert_of_not_mem m] }
  end) nd

[Kevin Buzzard]

Oh actually that is mostly tactic mode :-) But I'd say the term mode proof. It's not like that there's anything mathematically complex going on. Why not set_option profiler true and see if the term mode version is faster?

[Mario Carneiro]

You can golf it a bit more by pattern matching finset.insert_subset.1 hs

[Thomas Browning]

Mario Carneiro said:

You can golf it a bit more by pattern matching finset.insert_subset.1 hs

I can't quite see how to do it. What's the trick?

[Kevin Buzzard]

elaboration of induction_on'_tactic took 32.1ms
elaboration of induction_on'_term took 4.68ms

A huge difference, in some sense.

[Mario Carneiro]

theorem induction_on' {α : Type*} {p : finset α → Prop} [decidable_eq α]
  (S : finset α) (h₁ : p ∅) (h₂ : ∀ {a ∈ S} {s ⊆ S}, a ∉ s → p s → p (insert a s)) : p S :=
@finset.induction_on α (λ T, T ⊆ S → p T) _ S (λ _, h₁) (λ a s has hqs hs,
  let ⟨hS, sS⟩ := finset.insert_subset.1 hs in @h₂ a hS s sS has (hqs sS)) (finset.subset.refl S)

[Mario Carneiro]

I would also change the implicit binders a bit:

theorem induction_on' {α : Type*} {p : finset α → Prop} [decidable_eq α]
  (S : finset α) (h₁ : p ∅) (h₂ : ∀ {a s}, a ∈ S → s ⊆ S → a ∉ s → p s → p (insert a s)) : p S :=
@finset.induction_on α (λ T, T ⊆ S → p T) _ S (λ _, h₁) (λ a s has hqs hs,
  let ⟨hS, sS⟩ := finset.insert_subset.1 hs in h₂ hS sS has (hqs sS)) (finset.subset.refl S)

[Kevin Buzzard]

See? It was an easy two-liner after all :P

[Kevin Buzzard]

Length of proof is disconcertingly similar to length of statement.

[Mario Carneiro]

I wonder what percentage of mathlib theorems are longer than their proofs

[Kevin Buzzard]

More interesting would to see how the answers changed as you move further down the heirarchy. IIRC most of the proofs in data.complex.basic are by ext; simp whereas most of the proofs in discrete_valuation_ring are 10 line tactic proofs.

[Thomas Browning]

#5087

[Kevin Buzzard]

I was looking through old branches of mine today and I found this; golfing data.complex.basic. I never PR'ed it because I wasn't sure there was much point :-)

[Thomas Browning]

was this back when you were working on the complex number game?

[Kevin Buzzard]

lol Eric and I had the same thought whilst reviewing :-)

[Eric Wieser]

My only experience with recursor is it not working for the case I cared about and no one responding to my #mwe showing the failure...

[Kenny Lau]

there will be this issue that you won't be able to touch the goal while proving the induction hypothesis if you have classical.dec as local instance