# Zulip Chat Archive

## 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 `apply`

s into `refine`

s 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
```

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

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.

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

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