Data.Set.Enumerate

Stream: mathlib4

[Rémi Bottinelli]

Hey, I've got a "working" port of this file, but I had to do some bricolage e.g. to get it there without wlog.
It's a bit uglier than it was in mathlib3 (I'm still figuring out lean4) so I don't know if I should PR it or not? Or if it's even worth working on it some more.

/-
Copyright (c) 2017 Johannes Hölzl. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Johannes Hölzl
-/
import Mathlib.Data.Nat.Order.Basic
import Mathlib.Data.Set.Basic
import Mathlib.Tactic.SwapVar

/-!
# Set enumeration
This file allows enumeration of sets given a choice function.
The definition does not assume `sel` actually is a choice function, i.e. `sel s ∈ s` and
`sel s = none ↔ s = ∅`. These assumptions are added to the lemmas needing them.
-/


noncomputable section

open Function

namespace Set

section Enumerate

variable {α : Type _} (sel : Set α → Option α)

/-- Given a choice function `sel`, enumerates the elements of a set in the order
`a 0 = sel s`, `a 1 = sel (s \ {a 0})`, `a 2 = sel (s \ {a 0, a 1})`, ... and stops when
`sel (s \ {a 0, ..., a n}) = none`. Note that we don't require `sel` to be a choice function. -/
def enumerate : Set α → ℕ → Option α
  | s, 0 => sel s
  | s, n + 1 => do
    let a ← sel s
    enumerate (s \ {a}) n
#align set.enumerate Set.enumerate

theorem enumerate_eq_none_of_sel {s : Set α} (h : sel s = none) : ∀ {n}, enumerate sel s n = none
  | 0 => by simp [h, enumerate]
  | n + 1 => by (simp [h, enumerate] ; rfl)
#align set.enumerate_eq_none_of_sel Set.enumerate_eq_none_of_sel

theorem enumerate_eq_none :
    ∀ {s n₁ n₂}, enumerate sel s n₁ = none → n₁ ≤ n₂ → enumerate sel s n₂ = none
  | s, 0, m => fun h _ => enumerate_eq_none_of_sel sel h
  | s, n + 1, m => fun h hm => by
    cases hs : sel s
    · exact enumerate_eq_none_of_sel sel hs
    · cases m
      case zero =>
        have : n + 1 = 0 := Nat.eq_zero_of_le_zero hm
        contradiction
      case succ m' =>
        simp [hs, enumerate] at h ⊢
        have hm : n ≤ m' := Nat.le_of_succ_le_succ hm
        exact enumerate_eq_none h hm
#align set.enumerate_eq_none Set.enumerate_eq_none

theorem enumerate_mem (h_sel : ∀ s a, sel s = some a → a ∈ s) :
    ∀ {s n a}, enumerate sel s n = some a → a ∈ s
  | s, 0, a => h_sel s a
  | s, n + 1, a => by
    cases h : sel s
    case none => simp [enumerate_eq_none_of_sel, h]
    case some a' =>
      simp [enumerate, h]
      exact fun h' : enumerate sel (s \ {a'}) n = some a =>
        have : a ∈ s \ {a'} := enumerate_mem h_sel h'
        this.left
#align set.enumerate_mem Set.enumerate_mem

theorem enumerate_inj {n₁ n₂ : ℕ} {a : α} {s : Set α} (h_sel : ∀ s a, sel s = some a → a ∈ s)
    (h₁ : enumerate sel s n₁ = some a) (h₂ : enumerate sel s n₂ = some a) : n₁ = n₂ := by
  rcases le_total n₁ n₂ with (hn|hn)
  on_goal 2 => swap_var n₁ ↔ n₂, h₁ ↔ h₂
  all_goals
    rcases Nat.le.dest hn with ⟨m, rfl⟩
    clear hn
    induction n₁ generalizing s
    case zero =>
      cases m
      case zero => rfl
      case succ m =>
        have h' : enumerate sel (s \ {a}) m = some a := by
          simp_all only [enumerate, Nat.zero_eq, Nat.add_eq, zero_add]; exact h₂
        have : a ∈ s \ {a} := enumerate_mem sel h_sel h'
        simp_all [Set.mem_diff_singleton]
    case succ k ih =>
      cases h : sel s
      case none =>
        simp_all only [add_comm, self_eq_add_left, Nat.add_succ, enumerate_eq_none_of_sel _ h]
      case some _ =>
        simp_all only [add_comm, self_eq_add_left, enumerate, Option.some.injEq,
                       Nat.add_succ, enumerate._eq_2, Nat.succ.injEq]
        exact ih h₁ h₂

#align set.enumerate_inj Set.enumerate_inj

end Enumerate

end Set

[Mario Carneiro]

yes, uglier is fine as long as you make a porting note whenever you uglified the proof relative to the lean 3 version

[Rémi Bottinelli]

OK, then I'll do that, thanks!

[Rémi Bottinelli]

https://github.com/leanprover-community/mathlib4/pull/1041 <- I interpreted "porting note" simply as comments in the code.

[Kevin Buzzard]

"porting note" means "put comments in the file and these comments should contain the string porting note"

[Scott Morrison]

Ideally where you change a proof you actually preserve the old proof in the comments, in a format that allows someone to try restoring it without having to go back to mathlib3port or mathlib3..

[Scott Morrison]

(No need to do this it is is "minor" --- only do this when you expect that once a major tactic is implemented the original proof should work.)

[Rémi Bottinelli]

Noted. In this case, the change is not that big: instead of a wlog n₁ ≤ n₁I do a case on le_total, swap some arguments in one of the goals, and then keep essentially the same proof.