# Zulip Chat Archive

## 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

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

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 typesimport 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