Zulip Chat Archive

Stream: maths

Topic: Induction on subsets of a finset


view this post on Zulip 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 :=

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Thomas Browning (Nov 22 2020 at 22:47):

should I PR it?

view this post on Zulip Eric Wieser (Nov 22 2020 at 22:47):

I think you can combine the suffices and the let

view this post on Zulip Eric Wieser (Nov 22 2020 at 22:48):

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

view this post on Zulip 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)

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip Mario Carneiro (Nov 22 2020 at 22:58):

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

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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)

view this post on Zulip 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)

view this post on Zulip Kevin Buzzard (Nov 22 2020 at 23:03):

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

view this post on Zulip Kevin Buzzard (Nov 22 2020 at 23:05):

Length of proof is disconcertingly similar to length of statement.

view this post on Zulip Mario Carneiro (Nov 22 2020 at 23:06):

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

view this post on Zulip 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.

view this post on Zulip Thomas Browning (Nov 22 2020 at 23:08):

#5087

view this post on Zulip 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 :-)

view this post on Zulip Thomas Browning (Nov 22 2020 at 23:10):

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

view this post on Zulip Kevin Buzzard (Nov 22 2020 at 23:13):

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

view this post on Zulip 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...

view this post on Zulip 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