Zulip Chat Archive

Stream: maths

Topic: Inductive construction


view this post on Zulip 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

view this post on Zulip Mario Carneiro (Jan 27 2020 at 23:11):

You need to use choice recursively to construct the sequence

view this post on Zulip Mario Carneiro (Jan 27 2020 at 23:11):

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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Bhavik Mehta (Jan 27 2020 at 23:16):

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

view this post on Zulip Mario Carneiro (Jan 27 2020 at 23:17):

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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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)

view this post on Zulip Bhavik Mehta (Jan 27 2020 at 23:23):

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

view this post on Zulip Mario Carneiro (Jan 27 2020 at 23:25):

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

view this post on Zulip Bhavik Mehta (Jan 27 2020 at 23:25):

Fair point!

view this post on Zulip 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⟩⟩

view this post on Zulip Mario Carneiro (Jan 28 2020 at 00:54):

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

view this post on Zulip 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))

view this post on Zulip 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

view this post on Zulip 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)

view this post on Zulip Alistair Tucker (Jan 28 2020 at 09:34):

I guess I have assumed additionally that < is transitive.

view this post on Zulip Alistair Tucker (Jan 28 2020 at 09:35):

Anyway it would be great to see this in mathlib

view this post on Zulip 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

view this post on Zulip 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