Inductive construction

Stream: maths

[Bhavik Mehta]

I'm trying to formalise this argument: an infinite set contains countably many points. Proof: given infinite s, pick an element x0. Then s1 := s - {x0} is infinite, so we can pick an element x1. Then x2 := s1 - {x1} is infinite, continue inductively.
Here's where I'm at so far

import data.set.finite

local attribute [instance, priority 10] classical.prop_decidable
open set

lemma exists_mem_of_infinite {α : Type*} (s : set α) (hs : set.infinite s) :
  ∃ x, x ∈ s :=
exists_mem_of_ne_empty (λ t, hs (t.symm ▸ finite_empty))

lemma infinite_erase {α : Type*} {s : set α} (hs : set.infinite s) (x : α) :
  set.infinite {t ∈ s | t ≠ x} :=
begin
  intro a, apply hs, by_cases (x ∈ s),
    convert set.finite_insert x a, ext t, simp, split, intro q,
    by_cases (t = x), rw h, simp [h], right, exact ⟨‹_›, ‹_›⟩,
    rintro (rfl | _), exact h, exact a_1.1,
  convert a, ext, simp, split; intro p, refine ⟨p, _⟩, rintro rfl, apply h p,
  exact p.1
end

lemma has_sequence_of_infinite {α : Type*} (s : set ℕ) (hs : set.infinite s) :
  ∃ (a : ℕ → ℕ), (∀ i, a i ∈ s) ∧ (∀ i j, a i = a j → i = j) :=
begin
  sorry
end

I'll add that my question is about how to get this form of inductive construction as proof, rather than a different formalisation of the statement

[Mario Carneiro]

You need to use choice recursively to construct the sequence

[Mario Carneiro]

(this is a principle known as dependent choice in the literature)

[Reid Barton]

This is the kind of thing that https://github.com/rwbarton/lean-model-categories/blob/top-dev/src/logic/crec.lean is supposed to be good for, though it might be a bit awkward in this specific setup

[Bhavik Mehta]

(this is a principle known as dependent choice in the literature)

Yeah I'm aware of this, but I can't get the recursion to work in lean

[Bhavik Mehta]

More generally I'm not sure how I'd do a construction like this one

[Mario Carneiro]

that's just definition by well founded recursion, the equation compiler does it for you

[Bhavik Mehta]

But how can I do it myself? For instance if I had to do that inside a bigger theorem - I can't figure out how to get it then

[Reid Barton]

for example you can do something like this--your lemmas won't help here though

lemma has_sequence_of_infinite {α : Type*} (s : set ℕ) (hs : set.infinite s) :
  ∃ (a : ℕ → ℕ), (∀ i, a i ∈ s) ∧ (∀ i j, a i = a j → i = j) :=
begin
  obtain ⟨a, ha⟩ : {a : ℕ → s // ∀ i j, i < j → (a i).val ≠ (a j).val} :=
    crec' nat.lt_wf (λ _ _ _ (x y : s), x.val ≠ y.val) _,
  swap,
  { rintros a ⟨If, IH⟩,
    change {x : s // ∀ i (h : i < a), (If i h).val ≠ x.val},
    sorry },
  refine ⟨λ n, (a n).val, λ n, (a n).property, λ i j h, _⟩,
  rcases nat.lt_trichotomy i j with h'|h'|h',
  { exact (ha i j h' h).elim },
  { exact h' },
  { exact (ha j i h' h.symm).elim },
end

[Reid Barton]

You have something more like a https://hackage.haskell.org/package/base-4.12.0.0/docs/Data-List.html#v:unfoldr (without the Maybe)

[Bhavik Mehta]

Yeah I was surprised that something so natural in haskell is awkward here

[Mario Carneiro]

haskell doesn't care about proofs, though, which are what make this proof tricky

[Bhavik Mehta]

Fair point!

[Chris Hughes]

Alternative method. We need to unify set.infinite and infinite for types

import data.equiv.denumerable data.set.finite

def seq {α : Type*} (s : set ℕ) [decidable_pred s] (hs : set.infinite s) : denumerable s :=
@denumerable.of_encodable_of_infinite _ _ ⟨λ h, hs ⟨h⟩⟩

[Mario Carneiro]

I think there is also a quick method using the cardinal library

[Mario Carneiro]

import set_theory.cardinal

theorem set.infinite_iff {α} {s : set α} : set.infinite s ↔ infinite s :=
⟨λ h, ⟨λ f, h ⟨f⟩⟩, λ ⟨h⟩ ⟨f⟩, h f⟩

lemma has_sequence_of_infinite {α : Type*} (s : set α) (hs : set.infinite s) :
  ∃ (a : ℕ → α), (∀ i, a i ∈ s) ∧ (∀ i j, a i = a j → i = j) :=
let ⟨f⟩ := cardinal.infinite_iff.1 (set.infinite_iff.1 hs) in
⟨λ i, f ⟨i⟩, λ i, (f ⟨i⟩).2,
  λ i j e, congr_arg ulift.down (f.2 (subtype.eq e))⟩

[Alistair Tucker]

I wanted something like crec' recently, but I think it's not quite general enough? I wanted

parameters {α : Type u} {r : α → α → Prop} (hwf : well_founded r) [is_trans α r]
local infix `<` := r
parameters {C : α → Type v} (q : Π {j : α}, C j → (Π i, i < j → C i) → Prop)
parameters
  (H : Π (a : α)
         (f : {f : Π j, j < a → C j // ∀ j rja, q (f j rja) (λ i rij, f i (trans rij rja))}),
       {x : C a // q x f})
:
def crec' : {f : Π j, C j // ∀ j, q (f j) (λ i rij, f i)} := sorry

[Alistair Tucker]

Given that, the crec' of @Reid Barton can be derived quite easily

parameters {C : α → Type v} (q : Π ⦃i j⦄ (h : i < j), C i → C j → Prop)
parameters
  (H : Π (a : α)
         (f : {f : Π (i : α), i < a → C i // ∀ i j ria rja rij, q rij (f i ria) (f j rja)}),
       {x : C a // ∀ i (ria : i < a), q ria (f.val i ria) x})

def q' : Π j, C j → (Π i, i < j → C i) → Prop :=
λ j fj f, ∀ i rij, q rij (f i rij) fj

def H' : Π (a : α)
           (f : {f : Π j, j < a → C j // ∀ j rja, q' j (f j rja) (λ i rij, f i (trans rij rja))}),
         {x : C a // q' a x f} :=
λ a f, H a ⟨f.1, (λ i j ria rja rij, f.2 j rja i rij)⟩

def old_crec' : {f : Π i, C i // ∀ i j h, q h (f i) (f j)} :=
let f := crec' hwf q' H' in ⟨f.1, (λ i j, f.2 j i)⟩

[Alistair Tucker]

I guess I have assumed additionally that < is transitive.

[Alistair Tucker]

Anyway it would be great to see this in mathlib

[Bhavik Mehta]

Alternative method. We need to unify set.infinite and infinite for types

import data.equiv.denumerable data.set.finite

def seq {α : Type*} (s : set ℕ) [decidable_pred s] (hs : set.infinite s) : denumerable s :=
@denumerable.of_encodable_of_infinite _ _ ⟨λ h, hs ⟨h⟩⟩

Sure, I realise we can get other formalisations of the statement, but I'm asking about how to formalise the proof idea. For instance, the same mathematical proof immediately adapts to show

∃ (a : ℕ → ℕ), (∀ i, a i ∈ s) ∧ (∀ i j, i < j → a i < a j)

or

∃ (a : ℕ → ℕ), (∀ i, a i - 10 ∈ s) ∧ (∀ i j, i < j → a i < a j + 25)

or

∃ (a : ℕ → ℕ), (∀ i, a i ∈ s) ∧ (∀ i j, i < j → (a i)^2 < a j)

but I don't see how to use denumerable to get these - whereas it appears crec' does adapt nicely to these cases

[Bhavik Mehta]

@Reid Barton crec' works for me! Thanks so much