Zulip Chat Archive

Howdy! My name is Morgan. I'm a master's student in pure mathematics. I am broadly interested in the rather disparate mathematical fields of (homotopy) type theory, constructive mathematics, and mathematical general relativity. I'm currently working on a thesis on the latter.

I've been interested in type theory for a long time, which is at least partially motivated by my generally constructivist philosophical views. I have more experience with Coq than Lean, but have been trying to learn Lean, mostly due to the larger community working on the formalization of mathematics in Lean.

I'm currently trying to cut my teeth on Lean my formalizing some parts of Bishop's Constructive Analysis. I can't say that it's the smoothest of sailing, but I'm learning!

Morgan Arnold (May 01 2025 at 20:21):

Two questions I've run into in the work I'm doing so far:

Following Bishop, I've defined a RegularSeq to be a

structure RegularSeq where
  seq : ℕ → ℚ
  prop : ∀ m n, |seq m - seq n| ≤ 1 / m + 1 / n

but this doesn't have great ergonomics. For instance, I end up getting really messy-looking terms like |(x.seq n - y.seq n) + (y.seq n - z.seq n)| and such. I was hoping that I would be able to get around this by defining a coersion, like

instance : Coe RegularSeq (ℕ → ℚ) where
  coe x := x.seq

but this simply doesn't seem to work. Maybe it would be more correct to define regular sequences based on a predicate Regular (x : ℕ → ℚ) : Prop instead, but I want to define an equivalence relation on the type of regular sequences to form a quotient, and it's not clear to me how that would be done without defining regular sequences as a structure type like this.

The second problem that I'm having is also to do with coersions, but in a different way this time! I'm working on defining the sum of two regular sequences, and running into some issues with the proof that it's regular. Given two sequences x and y, their sum is λ n ↦ x (2 * n) + y (2 * n), but in proving that this is regular I have some issues. The proof is mostly routine, but once things are split up with the triangle inequality, I am left to prove that |x (2 * m) - x (2 * n)| ≤ 1 / (2 * ↑m) + 1 / (2 * ↑n). This should follow immediately from the regularity of x, but the proposition that that ends up yielding me is instead |x (2 * m) - x (2 * n)| ≤ 1 / ↑(2 * m) + 1 / ↑(2 * n). These are equivalent to the best of my understanding, but cannot be unified due to the different points at which the coersions occur. Presumably I could figure out how to prove that (2 * ↑m) = ↑(2 * m), but having to do that seems like a bit of a smell to me, and I suspect that there is probably a way of doing this that allows me to avoid this mess.