## Stream: maths

### Topic: Induction on subsets of a finset

#### Thomas Browning (Nov 22 2020 at 21:18):

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 (Nov 22 2020 at 22:29):

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 (Nov 22 2020 at 22:35):

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 (Nov 22 2020 at 22:36):

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 (Nov 22 2020 at 22:38):

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 (Nov 22 2020 at 22:46):

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


should I PR it?

#### Eric Wieser (Nov 22 2020 at 22:47):

I think you can combine the suffices and the let

#### Eric Wieser (Nov 22 2020 at 22:48):

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

#### Thomas Browning (Nov 22 2020 at 22:53):

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 (Nov 22 2020 at 22:57):

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 (Nov 22 2020 at 22:58):

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 (Nov 22 2020 at 22:58):

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

#### Thomas Browning (Nov 22 2020 at 23:00):

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 (Nov 22 2020 at 23:00):

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


A huge difference, in some sense.

#### Mario Carneiro (Nov 22 2020 at 23:01):

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 (Nov 22 2020 at 23:03):

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 (Nov 22 2020 at 23:03):

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

#### Kevin Buzzard (Nov 22 2020 at 23:05):

Length of proof is disconcertingly similar to length of statement.

#### Mario Carneiro (Nov 22 2020 at 23:06):

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

#### Kevin Buzzard (Nov 22 2020 at 23:07):

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.

#5087

#### Kevin Buzzard (Nov 22 2020 at 23:09):

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 (Nov 22 2020 at 23:10):

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

#### Kevin Buzzard (Nov 22 2020 at 23:13):

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

#### Eric Wieser (Nov 22 2020 at 23:15):

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 (Nov 22 2020 at 23:47):

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

Last updated: May 18 2021 at 06:15 UTC