Zulip Chat Archive

Stream: mathlib4

Topic: tactic to apply induction on finite sets


Miguel Marco (Jul 20 2023 at 22:55):

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 (Jul 20 2023 at 23:19):

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

Miguel Marco (Jul 20 2023 at 23:25):

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

Kevin Buzzard (Jul 20 2023 at 23:33):

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 (Jul 20 2023 at 23:33):

induction s using finset.induction_on is better

Eric Wieser (Jul 20 2023 at 23:34):

Oh, this is finite not finset

Eric Wieser (Jul 20 2023 at 23:34):

Still, in general you should use the induction tactic

Kevin Buzzard (Jul 20 2023 at 23:35):

abierto_vacio is implied by abierto_union with empty, by the way

Miguel Marco (Jul 20 2023 at 23:46):

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 (Jul 20 2023 at 23:48):

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 (Jul 20 2023 at 23:56):

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 (Jul 20 2023 at 23:56):

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

Eric Wieser (Jul 20 2023 at 23:58):

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

Miguel Marco (Jul 20 2023 at 23:58):

no, it changes the the hypothesis to Fintype ↑ℱ

Miguel Marco (Jul 20 2023 at 23:59):

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 (Jul 21 2023 at 00:00):

... then that lemma is wrong

Eric Wieser (Jul 21 2023 at 00:02):

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 (Jul 21 2023 at 00:06):

that works.

maybe that lemma should be included in mathlib?

Miguel Marco (Jul 21 2023 at 00:08):

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

Miguel Marco (Aug 18 2023 at 23:25):

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

Anatole Dedecker (Aug 18 2023 at 23:41):

@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 (Aug 19 2023 at 00:08):

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 (Aug 19 2023 at 00:10):

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

Last updated: Dec 20 2023 at 11:08 UTC