tactic to apply induction on finite sets

Stream: mathlib4

[Miguel Marco]

In lean3, if i wanted to prove a property for finite sets i could apply induction_on directly. But in mathlib4 i get an error failed to elaborate eliminator, expected type is not availableif i try this:

import Mathlib.Tactic

open Nat
open Set.Finite

class espacio_topologico (X : Type) where
  abiertos : Set (Set X)
  abierto_total : univ ∈ abiertos
  abierto_vacio : ∅ ∈ abiertos
  abierto_union : ∀ (ℱ : Set (Set X)) (h: ℱ ⊆ abiertos) , ⋃₀ ℱ ∈ abiertos
  abierto_interseccion : ∀ (ha : A ∈ abiertos) (hb : B ∈ abiertos), A ∩ B ∈ abiertos

open espacio_topologico

variable {X : Type}
variable [espacio_topologico X]

def abierto (A : Set X) := A ∈ abiertos

lemma abierto_interseccion_finita (ℱ : Set (Set X)) (hfin : ℱ.Finite) (hℱ : ℱ ⊆ abiertos) :
abierto (⋂₀ ℱ ) := by
  revert hℱ
  apply induction_on hfin

any clue on how to do this?

[Kevin Buzzard]

Try refine induction_on hfin ?_ ?_ ?_ (with the right number of ?_s)

[Miguel Marco]

thanks, it works (I hope the syntax is not too confusing to my students)

[Kevin Buzzard]

Lean 4 is worse at inferring motives than Lean 3; it's a shame that apply doesn't fall back on the above when it fails.

[Eric Wieser]

induction s using finset.induction_on is better

[Eric Wieser]

Oh, this is finite not finset

[Eric Wieser]

Still, in general you should use the induction tactic

[Kevin Buzzard]

abierto_vacio is implied by abierto_union with ℱ empty, by the way

[Miguel Marco]

Kevin Buzzard said:

abierto_vacio is implied by abierto_union with ℱ empty, by the way

yes, but I am trying to follow exacty the notes of our course. We use a set of axioms that is not minimal, but it is hopefully easier to grasp by the students.

[Miguel Marco]

Eric Wieser said:

induction s using finset.induction_on is better

sshould be the hypothesis that states that the set is finite in this case?

[Miguel Marco]

It doens't work in my case : induction' hfin using Set.Finite.induction_on produces an error failed to infer implicit target, it contains unresolved metavariables ?m.751

[Eric Wieser]

Does induction hfin work? docs#Set.Finite.induction_on

[Eric Wieser]

Ah, I think you need induction hfin using Finite.dinduction_on

[Miguel Marco]

no, it changes the the hypothesis to Fintype ↑ℱ

[Miguel Marco]

Eric Wieser said:

Ah, I think you need induction hfin using Finite.dinduction_on

that fails too:

Expected type
⊢ ∀ {α : Type u} {C : (s : Set α) → Set.Finite s → Prop} (s : Set α) (h : Set.Finite s),
  C ∅ (_ : Set.Finite ∅) →
    (∀ {a : α} {s : Set α}, ¬a ∈ s → ∀ (h : Set.Finite s), C s h → C (insert a s) (_ : Set.Finite (insert a s))) → C s h

[Eric Wieser]

... then that lemma is wrong

[Eric Wieser]

This is what it should be:

@[elab_as_elim]
theorem Finite.dinduction_on' {C : ∀ s : Set α, s.Finite → Prop}
    (H0 : C ∅ finite_empty)
    (H1 : ∀ {a s}, a ∉ s → ∀ h : Set.Finite s, C s h → C (insert a s) (h.insert a))  {s : Set α} (h : s.Finite) : C s h :=
  have : ∀ h : s.Finite, C s h :=
    Finite.induction_on h (fun _ => H0) fun has hs ih _ => H1 has hs (ih _)
  this h

[Miguel Marco]

that works.

maybe that lemma should be included in mathlib?

[Miguel Marco]

although I cannot access the names of the hypothesis in the induction step

[Miguel Marco]

I created PR #6674 to include this, but I am not sure of the procedure to follow.

[Anatole Dedecker]

@Miguel Marco We don't accept PRs from forks. I've just given you push-access to non-master branches of mathlib4, please create a branch and open a PR from there.

[Eric Wieser]

Note also that you don't need to add a new Finite.dinduction_on'; you should just change the statement of the existing lemma to have the arguments in the right order

[Eric Wieser]

In fact, I think I might have jumped to conclusions; the original lemma works fine after all, as:

induction ℱ, hfin using Set.Finite.dinduction_on