## Stream: maths

### Topic: Inductive construction

#### Bhavik Mehta (Jan 27 2020 at 23:03):

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 (Jan 27 2020 at 23:11):

You need to use choice recursively to construct the sequence

#### Mario Carneiro (Jan 27 2020 at 23:11):

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

#### Reid Barton (Jan 27 2020 at 23:14):

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 (Jan 27 2020 at 23:15):

(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 (Jan 27 2020 at 23:16):

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

#### Mario Carneiro (Jan 27 2020 at 23:17):

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

#### Bhavik Mehta (Jan 27 2020 at 23:18):

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 (Jan 27 2020 at 23:20):

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 (Jan 27 2020 at 23:22):

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 (Jan 27 2020 at 23:23):

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

#### Mario Carneiro (Jan 27 2020 at 23:25):

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

Fair point!

#### Chris Hughes (Jan 28 2020 at 00:52):

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 (Jan 28 2020 at 00:54):

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

#### Mario Carneiro (Jan 28 2020 at 01:01):

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 (Jan 28 2020 at 09:28):

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 (Jan 28 2020 at 09:32):

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 (Jan 28 2020 at 09:34):

I guess I have assumed additionally that < is transitive.

#### Alistair Tucker (Jan 28 2020 at 09:35):

Anyway it would be great to see this in mathlib

#### Bhavik Mehta (Jan 28 2020 at 10:29):

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 (Jan 30 2020 at 12:05):

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

Last updated: May 12 2021 at 08:14 UTC