How do I prove this about Nat.nth?

Stream: new members

[Ching-Tsun Chou]

The following proposition is intuitively obvious. But how do I prove it? I haven't been able to get any ideas from the existing results about Nat.nth in mathlib.

example {φ : ℕ → ℕ} (hm : StrictMono φ) (n : ℕ) :
    φ n = Nat.nth (range φ) n := by
  sorry

[Yakov Pechersky]

First, you shouldn't use range (the Set) as Nat -> Prop, that is piercing through a defeq that isn't meant to be used that way.

[Yakov Pechersky]

Looks like docs#Nat.nth_eq_sInf could help

[Ching-Tsun Chou]

Thanks for the pointer! Nat.nth has the following type:

Nat.nth (p : ℕ → Prop) (n : ℕ) : ℕ

What do you suggest I use instead of range φ for its first argument?

[Kenny Lau]

Ching-Tsun Chou said:

Thanks for the pointer! Nat.nth has the following type:

Nat.nth (p : ℕ → Prop) (n : ℕ) : ℕ

What do you suggest I use instead of range φ for its first argument?

fun x => x ∈ range φ

[Ching-Tsun Chou]

Isn’t that just ugly?

[Kenny Lau]

Ching-Tsun Chou said:

Isn’t that just ugly?

you can also use (· ∈ range φ)

[Ching-Tsun Chou]

I think it has been a mistake for Lean to distinguish between sets and predicates. It’s a distinction without substance and just introduces unnecessary work and complexity.

[Edward van de Meent]

Ching-Tsun Chou said:

just introduces unnecessary work and complexity.

i'm not so sure about that... i think that since most mathematicians think about sets and not predicates, having something which represents that seems like the logical thing to do. Once you have sets, it also makes sense to try to consistently distinguish between predicates and sets because a lot of notation which makes sense for one does not at all make sense for the other. I would hate to see something like x ∈ (fun y => Even y) in lean, nobody writes math like that.

[Jireh Loreaux]

Ching-Tsun Chou said:

I think it has been a mistake for Lean to distinguish between sets and predicates. It’s a distinction without substance and just introduces unnecessary work and complexity.

No, if anything we should make the distinction stronger (e.g., by making Set irreducible or a one-field structure) in order to prevent defeq abuse. The only way to make the distinction any weaker would be to make Set an abbrev, which would be a mess (e.g., all instances would be visible to both).

[Kyle Miller]

If you make no distinction between sets and predicates, then what happens is that the correct thing for Lean to do would be to always simplify x ∈ s to s x, or else always pretty print p x as x ∈ p. Having the separate types ensures that one can stick with the language of sets.

[Kenny Lau]

Ching-Tsun Chou said:

I think it has been a mistake for Lean to distinguish between sets and predicates. It’s a distinction without substance and just introduces unnecessary work and complexity.

when was the last time you took the union of two predicates?

[Kyle Miller]

I've taken the sup of predicates before. It's not that odd of a thing to do.

[Kyle Miller]

Here's a proof of the original statement:

import Mathlib

open Set

example {φ : ℕ → ℕ} (hm : StrictMono φ) (n : ℕ) :
    φ n = Nat.nth (· ∈ range φ) n := by
  rw [← Nat.nth_comp_of_strictMono hm (by simp)]
  · simp
  intro hf
  exfalso
  have : (range φ).Infinite :=
    infinite_range_of_injective hm.injective
  exact absurd hf this

[Kenny Lau]

and here's the proof golfed to oblivion:

import Mathlib

open Set

example {φ : ℕ → ℕ} (hm : StrictMono φ) (n : ℕ) :
    φ n = Nat.nth (· ∈ range φ) n := by
  simp_rw [mem_range, ← Nat.nth_comp_of_strictMono hm (by simp)
    (infinite_range_of_injective hm.injective |>.elim ·), exists_apply_eq_apply, Nat.nth_true]

example {φ : ℕ → ℕ} (hm : StrictMono φ) (n : ℕ) :
    φ n = Nat.nth (· ∈ range φ) n := by
  rw [← Nat.nth_comp_of_strictMono hm (by simp)
    (by exact infinite_range_of_injective hm.injective |>.elim ·)]; simp

[Ching-Tsun Chou]

Thanks for providing me with solutions! It saves me a lot of time on trial and error.

But on the subject of sets vs predicates, I beg to differ. In my ideal world, Lean should have just predicates and no sets. Set operations like ∪, ∩, ᶜ , ⊂, etc can be defined directly on predicates and there is no need for ∈ . Nor is there any need for the set comprehension notation, though the notation for enumerated finite sets would still be useful. Perhaps this is unfamiliar to most mathematicians. But the notion that propositions can be regarded as types and proofs as terms is also unfamiliar to most mathematicians. When one learns to formalize math in a formal system, one has to learn to adapt one's conceptual framework.

Also observe that "sets" in Lean are actually quite different from sets in informal mathematics. For example, I believe most mathematicians intuitively think that ℕ is literally a subset of ℤ, which is literally a subset of ℚ, which is literally a subset of ℝ, and so on. But that is definitely not the case in Lean. Similarly, Fin n is not a subset of Fin (n + 1) or ℕ, which I suspect many mathematicians will also find peculiar.

[Jz Pan]

But s : Set X can be converted to subtype implicitly. I think it will cause a big chaos if P : X -> Prop could be also converted to the subtype { x : X // P x } implicitly.

[Ching-Tsun Chou]

True. But if there had never been Set in Lean, I'm sure such implicit conversion would never have existed.

Fundamentally, the formal system implemented by Lean is a type theory, not a set theory. It seems to me better to accept and live with that fact than try to "simulate" set theory in a type theory. But, of course, it is too late to change anything now.

[Kevin Buzzard]

We want to be more friendly to mathematicians, not less friendly. In particular we want to hide type theory as much as possible and let mathematicians think they're dealing with sets, as they are used to. One of the reasons mathlib has been so successful is that it has not prioritised stressing its type-theoretic foundations and has instead been very good at accommodating mathematicians with no training in the foundations of their subject (aka "most mathematicians").

[Ching-Tsun Chou]

I'm not a mathematician, so I don't really know what mathematicians prefer. But it seems to me that once anyone digs just a little deeper into Lean, one quickly realizes that Lean's formal system not only is not a set theory but does not even support real subtypes. (If Lean has real subtypes, x : ℚ should imply x : ℝ and k : Fin n should imply k : Fin (n + 1) and k : ℕ.)

[Johan Commelin]

Otoh, in almost every setup of mathematics in set theory, the inclusions $\N \subseteq \Z \subseteq \mathbb{Q} \subseteq \R \subseteq \mathbb{C}$ are also white lies.

[Philippe Duchon]

They are lies that, to quote Kevin above, "most mathematicians" (by my estimation, the vast majority of them) don't consider to be lies - most would probably consider the "lies" assertion to be, at best, splitting hairs, and at worst, utter nonsense.

Formalization is difficult enough without having to re-learn everything from scratch - at least for those of us who are way past their initial training years. If Lean and Mathlib lie to us just so that we can understand the theorem statements when we need them, and let us write new theorems almost as we would write them on paper, then the lie is, IMHO, a good one, even though it will occasionally come back and make trouble for us.

[Johan Commelin]

@Philippe Duchon I completely agree! And even though Lean doesn't support real subtypes, I think the coercion system gets you pretty far in terms of "write new theorems almost as we would write them on paper"...