Counting Ways to Choose

Stream: new members

[Nathan]

I want to state this problem in lean:

657746365446619146.png

Is this a good way to do it?

import Mathlib.Data.Int.Init
import Mathlib.Data.Set.Card
import Mathlib.Order.Interval.Set.Defs

def B := Set.Icc (-100) 100
def S := {p : Set ℤ | ∃ a b : ℤ, p = {a, b} ∧ a ≠ b ∧ a ∈ B ∧ b ∈ B ∧ a + b > a * b}

theorem POTD2415 : S.encard = 10199 := sorry

[Ruben Van de Velde]

It might be easier to work with \Z \times \Z, but I guess there's a question whether 1,100 and 100,1 are different solutions

[Nathan]

they're the same solution

[Nathan]

i started doing the proof with ZxZ before i realized that

[Robin Arnez]

What about docs#Sym2​?

[Robin Arnez]

(i.e. the type of unordered pairs)

[Nathan]

oh interesting

[Nathan]

thanks :pray:

[Axel Boldt]

But Sym2 will also include {a,a}, which you don't want.

[Robin Arnez]

Well, you can always use docs#Sym2.IsDiag

[Kevin Buzzard]

At this point I'm wondering whether it's just easiest to demand $-100\leq a<b\leq 100$ and have done with it; otherwise you'll just end up with several lines of boilerplate reducing you to this case at the beginning of the proof, which is enough to put people off. Clearly this rephrasing is equivalent.

[Nathan]

but i'm interested in using lean to prove that they're equivalent

[Kevin Buzzard]

I would say that the informal question itself is ambiguous. It's not clear to me that choosing (-1,2) is the same as, or different to, choosing (2,-1). I don't think you can argue that it's clear from the wording because I claim that "In how many ways can we choose two different integers between -100 and 100 inclusive such that the first is less than the second" is also a perfectly reasonable English statement, and would be interpreted as unordered pairs because of what happens next in the sentence. So one could even argue that sticking as closely as possible to the informal statement is impossible because you'd have to write an ambiguous formal statement, which isn't possible ;-)

However, if you are convinced that you know what the informal statement means, and that it means "unordered pair", then one way to proceed would be
(1) use docs#Sym2 and docs#Sym2.IsDiag in the statement
(2) decide how you're going to formalize the proof (e.g. perhaps you want to count $-100\leq a<b\leq 100$ in practice)
(3) prove an auxiliary lemma saying that there's a bijection between the contorted set that you want to work with and the ordered pairs which I'm suggesting
(4) start the proof of your contorted statement by rewriting to make it into the formally nice statement.

[Vlad]

An easy way to express the statement is to use a list and an easy way to prove it is to use native_decide:

def xs : List (ℤ × ℤ) := do
  let range := List.range 201 |>.map (· - (100 : ℤ))
  let a ← range; let b ← range
  guard $ a < b ∧ a * b < a + b
  return (a, b)

example : xs.length = 10199 := by
  native_decide

[Kenny Lau]

you should not use native_decide

[Vlad]

Proving that this formulation is equivalent to the set-theoretic approach is more involved:

Proof

import Mathlib

def B := Set.Icc (-100) 100
def S := {p : Set ℤ | ∃ a b : ℤ, p = {a, b} ∧ a ≠ b ∧ a ∈ B ∧ b ∈ B ∧ a + b > a * b}

section helper_lemmas

theorem ne_symm' {α : Type*} {a b : α} (h : ¬(a = b)) : ¬(b = a) := by tauto

noncomputable
def Nonempty.inhabited {α : Type*} (h : Nonempty α) : Inhabited α :=
  Classical.inhabited_of_nonempty h

theorem epsilon_eq_of_exiu {α : Type*} [ha : Inhabited α] {p : α → Prop} {x}
(h₁ : p x) (h₂ : ∃! x, p x) : Classical.epsilon p = x := by
  have hp : p = λ y => x = y
  · ext y; obtain ⟨z, h₂, h₃⟩ := h₂; constructor <;> intro h₄
    rw [h₃ _ h₁, h₃ _ h₄]; rwa [←h₄]
  have h₃ := Classical.epsilon_spec h₂
  dsimp at h₃; subst hp; simp at h₃; exact h₃.symm

theorem epsilon_eq_of {α : Type*} [ha : Inhabited α] {p : α → Prop} {x}
(h₁ : p x) (h₂ : ∀ y, p y → y = x) : Classical.epsilon p = x := by
  apply epsilon_eq_of_exiu h₁; use x

attribute [simp] List.nodup_range

def List.toSet {α : Type*} (xs : List α) : Set α := {x | x ∈ xs}

@[simp]
theorem List.mem_toSet {α : Type*} {xs : List α} {x} : x ∈ xs.toSet ↔ x ∈ xs := by
  simp [toSet]

@[simp]
theorem List.toSet_nil {α : Type*} : ([] : List α).toSet = ∅ := by simp [toSet]

@[simp]
theorem List.toSet_cons {α : Type*} {xs : List α} {x} : (x :: xs).toSet = insert x xs.toSet := by
  simp [toSet]; aesop

@[simp]
theorem List.flatMap_fn_singletonc {α β : Type*} {xs : List α} {f : α → β} :
xs.flatMap ([f ·]) = xs.map f := by
  induction xs; rfl; simpa

@[simp]
theorem List.eq_nil_of_isEmpty {α : Type*} [ha : IsEmpty α] {xs : List α} : xs = [] := by
  cases xs; rfl; simp; apply ha.1; assumption

theorem List.nodup_flatMap_flatMap_pair {α : Type*} [ha : LinearOrder α] {xs ys : List α}
{r : α → α → Prop} [hp : DecidableRel r]
(hxs : xs.Nodup) (hys : ys.Nodup) :
(xs.flatMap (λ x => ys.flatMap $ λ y =>
if x < y ∧ r x y then [(x, y)] else [])).Nodup := by
  by_cases h₀ : IsEmpty α; simp; push_neg at h₀; have := h₀.inhabited
  rw [nodup_flatMap]; symm; split_ands
  · unfold Function.onFun Disjoint; simp; induction xs; simp
    rename_i x xs ih; simp at hxs ⊢; rcases hxs with ⟨h₁, h₂⟩
    specialize ih h₂; simp [ih]; intros; simp_all only
  intro x hx; rw [nodup_flatMap]; symm; split_ands
  · unfold Function.onFun Disjoint; simp; induction ys; simp
    rename_i y hy ih; simp at hys ⊢; rcases hys with ⟨h₁, h₂⟩
    specialize ih h₂; simp [ih]; intros; rintro rfl; simp_all only
  intro y hy; split_ifs <;> simp

theorem List.nodup_flatMap_flatMap_upair {α : Type*} [ha : LinearOrder α] {xs ys : List α}
{r : α → α → Prop} [hp : DecidableRel r]
(hxs : xs.Nodup) (hys : ys.Nodup) :
(xs.flatMap (λ x => ys.flatMap $ λ y =>
if x < y ∧ r x y then [({x, y} : Set α)] else [])).Nodup := by
  by_cases h₀ : IsEmpty α; simp; push_neg at h₀; have := h₀.inhabited
  generalize hA : (λ x => ys.flatMap $ λ y =>
    if x < y ∧ r x y then [({x, y} : Set α)] else []) = A
  symm at hA; rw [funext_iff] at hA; generalize hf : (λ (s : Set α) =>
    ( Classical.epsilon $ λ x => x ∈ s ∧ ∀ y ∈ s, x ≤ y
    , Classical.epsilon $ λ x => x ∈ s ∧ ∀ y ∈ s, y ≤ x)) = f
  generalize hB : (xs.flatMap A).map f = B; suffices h : B.Nodup
  subst hB; exact Nodup.of_map _ h; replace hB : B = xs.flatMap
    (λ x => ys.flatMap $ λ y => if x < y ∧ r x y then [(x, y)] else [])
  rotate_left; subst hB; exact nodup_flatMap_flatMap_pair hxs hys
  subst hB; rw [map_flatMap]; congr; ext x :1; rw [hA, map_flatMap]
  congr; ext y :1; rw [apply_ite (f := map f)]; simp; split_ifs with h₁ <;> simp
  replace h₁ := h₁.1; subst hf; simp; have h₂ := le_of_lt h₁
  rw [epsilon_eq_of (x := x), epsilon_eq_of (x := y)] <;> simp [h₂]
  all_goals intro h₃; apply le_antisymm <;> assumption

theorem Set.finite_of_subset_finset {α : Type*} {set : Set α}
(s : Finset α) (h : ∀ x ∈ set, x ∈ s) : set.Finite := by
  classical apply Finite.ofFinset (s := s.filter (· ∈ set)); simpa

@[simp]
theorem Set.finite_toSet_list {α : Type*} {xs : List α} : xs.toSet.Finite := by
  classical apply Set.finite_of_subset_finset xs.toFinset; simp

@[simp]
instance {α : Type*} {xs : List α} : Finite xs.toSet := by
  apply Fintype.finite; apply Set.Finite.fintype; simp

theorem Set.ncard_toSet_list_of_nodup {α : Type*} {xs : List α}
(h : xs.Nodup) : xs.toSet.ncard = xs.length := by
  classical induction xs; simp; rename_i x xs ih; simp at h ⊢
  rcases h with ⟨h₁, h₂⟩; specialize ih h₂
  simpa [Set.ncard_insert_eq_ite, h₁]

end helper_lemmas

def bList : List ℤ :=
  List.range 201 |>.map (· - 100)

def sList : List (Set ℤ) := do
  let a ← bList
  let b ← bList
  guard $ a < b ∧ a * b < a + b
  return {a, b}

theorem B_eq_toSet_bList : B = bList.toSet := by
  ext n; simp [B, bList]; constructor
  · rintro ⟨h₁, h₂⟩; use n + 100 |>.toNat; omega
  · rintro ⟨n, h₁, rfl⟩; omega

theorem S_eq_toSet_sList : S = sList.toSet := by
  ext s; simp [S, B_eq_toSet_bList, bList, sList]; constructor
  · rintro ⟨a, b, rfl, h₁, hb, ha, h⟩; by_cases h₂ : a < b
    · use a, by omega, b, by omega;
      simp [h₂, Set.ext_iff, guard]; rw [if_pos]
      simp; omega; ring_nf at h ⊢; exact h
    · use b, by omega, a, by omega
      simp [show b < a by omega, h]
  · simp [guard, failure]; rintro a ha b hb h h₁ rfl; simp [Set.ext_iff]
    use a, b; simp [ne_symm' $ ne_of_lt h, ha, hb];
    split_ands; intro x; omega; ring_nf at h₁ ⊢; exact h₁

theorem nodup_bList : bList.Nodup := by
  simp [bList]; rw [List.nodup_map_iff]; simp; intro x y h; simp at h; exact h

theorem nodup_sList : sList.Nodup := by
  simp [sList, guard, failure, apply_ite (f := List.length)]; have h : ∀ (a b : ℤ),
    List.replicate (if a < b ∧ a * b < a + b then 1 else 0) {a, b} =
    if a < b ∧ a * b < a + b then [({a, b} : Set ℤ)] else []
  · intro a b; split_ifs <;> simp
  simp [h]; apply List.nodup_flatMap_flatMap_upair <;> exact nodup_bList

example : S.encard = 10199 := by
  classical rw [←Set.Finite.cast_ncard_eq $ S.finite_of_subset_finset
    sList.toFinset $ by simp [S_eq_toSet_sList]]; norm_cast
  rw [S_eq_toSet_sList, Set.ncard_toSet_list_of_nodup nodup_sList]
  native_decide

[Vlad]

you should not use native_decide

The documentation is clear regarding what native_decide does. It is left to the users to decide to what extent they trust lean compiler in addition to the kernel.

[Alfredo Moreira-Rosa]

I think Kenny meant, you should not use native_decide if you want to integrate your work to mathlib. Plus be aware that native_decide, since it's not checked by the kernel, that it's not considered to be a valid formal proof.

[Kenny Lau]

def f := false

@[implemented_by f]
def g := true

example : False :=
  have h₁ : g = true := rfl
  have h₂ : g = false := by native_decide
  absurd (h₁.symm.trans h₂) (by decide)