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 available
if 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 byabierto_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
s
should 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