Morgan Arnold

Stream: new members

[Morgan Arnold]

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]

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

1. 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.

2. 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.

[Morgan Arnold]

Pardon my wall of text!

[Aaron Liu]

Use docs#CoeFun or docs#FunLike

[Aaron Liu]

I suggest docs#FunLike

[Eric Paul]

For your second issue, I imagine the tactic norm_cast would be useful, a #mwe for that situation would be helpful

[suhr]

Keep in mind #general > ✔ Classical is now open by default? How to disable it?

[Morgan Arnold]

suhr said:

Keep in mind #general > ✔ Classical is now open by default? How to disable it?

Oh, that's absolutely bizarre. In fact, I just checked, and it seems like even in my definition of regular sequences classical choice is somehow being looped into the mix. According to #print axioms RegularSeq, 'RegularSeq' depends on axioms: [propext, Classical.choice, Quot.sound]. propext makes sense, and Quot.sound makes sense because of the rationals being presumably defined as a quotient, but I can't for the life of me see why this definition requires Classical.choice!

[Yan Yablonovskiy 🇺🇦]

Morgan Arnold said:

suhr said:

Keep in mind #general > ✔ Classical is now open by default? How to disable it?

Oh, that's absolutely bizarre. In fact, I just checked, and it seems like even in my definition of regular sequences classical choice is somehow being looped into the mix. According to #print axioms RegularSeq, 'RegularSeq' depends on axioms: [propext, Classical.choice, Quot.sound]. propext makes sense, and Quot.sound makes sense because of the rationals being presumably defined as a quotient, but I can't for the life of me see why this definition requires Classical.choice!

Will need to see more of it i think to say for sure. Without more info i would say check the type signature of the | | there and also division of one.

[Ruben Van de Velde]

docs#Rat.sub_def already requires choice, so there doesn't seem to be much of a chance to avoid it

[Morgan Arnold]

Ruben Van de Velde said:

docs#Rat.sub_def already requires choice, so there doesn't seem to be much of a chance to avoid it

Hm, is choice required here to select a representative of the equivalence class or something?

[Louis Cabarion]

Isn’t it simply the case that -- even if a result doesn’t theoretically require Classical.choice-- Mathlib contributors typically make no special effort to avoid using it in practice?

[Louis Cabarion]

In other words, seeing 'foo' depends on axioms: […, Classical.choice, …] should not be taken to mean that Mathlib’s contributors couldn’t find a way to prove foo without using Classical.choice.

[Ruben Van de Velde]

Isak Colboubrani said:

Isn’t it simply the case that -- even if a result doesn’t theoretically require Classical.choice-- Mathlib contributors typically make no special effort to avoid using it in practice?

Certainly

[Ruben Van de Velde]

(Though this is core lean, even)

[suhr]

Yeah, but this is not a mathlib issue. This is core lean.

[suhr]

Ruben Van de Velde said:

docs#Rat.sub_def already requires choice

Thanks for saying that. So I will need to avoid Batteries as well in my project.

[Ruben Van de Velde]

Following the rabbit hole even further, docs#Int.tdiv_eq_ediv is one source of choice, and that's in core

[Ruben Van de Velde]

I recommend asking yourself why you'd want to avoid choice

[suhr]

That's easy: I want to do both constructive and classical mathematics, while keeping the clear distinction between them.

[Morgan Arnold]

I find myself in a similar camp. My interest in proof verification tools like Lean stems in large part from an interest in constructive mathematics. Indeed, I'm trying to learn Lean by formalizing theorems from a book on constructive analysis. That seems a bit moot if I can't prevent Lean from including non-constructive classical results willy-nilly. I was also hoping that it would be possible to maintain a clear distinction between constructive results and classical results.

[suhr]

It is possible with a certain hack: https://lean-ja.github.io/lean-by-example/Diagnostic/Print.html#%E8%88%9E%E5%8F%B0%E8%A3%8F.

But it sucks when trivially constructive lemmas in the standard library implicitly depend on choice.

[Morgan Arnold]

It does seem to make it a bit tricky to actually do explicitly constructive mathematics in Lean, which is a real shame.

[suhr]

Yeah. I still find Lean much nicer to work with than other proof assistants, so I would prefer using this hack and implementing things myself over using Rocq, for example.

[Niels Voss]

Keep in mind that Lean maintains a distinction between constructive mathematics and computable mathematics, and while the former is hard to do given that nearly all of Mathlib depends on choice, the latter is definitely achievable.

[Niels Voss]

Are you trying to do constructive mathematics so that you can run your code, or just because you don't like the law of the excludes middle?

[Morgan Arnold]

@Niels Voss mostly because I don't like LEM. I'm also trying to formalize parts of a book on constructive mathematics, so I find it a bit aesthetically unpleasant if Lean implicitly pulls all of this non-constructive stuff. I'm trying to do constructive math, so I'd like Lean to offer the guarantee that it's constructive. That's all.

[suhr]

Niels Voss said:

Keep in mind that Lean maintains a distinction between constructive mathematics and computable mathematics, and while the former is hard to do given that nearly all of Mathlib depends on choice, the latter is definitely achievable.

For me it's both. I'd like to preserve the constructive meaning of ∃ and also like when things are computable.

[Morgan Arnold]

Unfortunately, the more I read the more it seems like Lean is really not very well-suited to doing explicitly constructivist mathematics. At a minimum it seems like I would need to re-implement a ton of stuff from mathlib because of just how much of it depends on choice, plus be very vigilant to ensure that the built-in tactics don't introduce choice in my proofs. It's just unmanageable.

[Niels Voss]

You can write metaprograms that detect whether choice is included in your proof. (I think the Lean ground zero project does something similar; maybe you should check it out). It's more of a question of how much work you want to do yourself

[Luigi Massacci]

Morgan Arnold said:

Unfortunately, the more I read the more it seems like Lean is really not very well-suited to doing explicitly constructivist mathematics. At a minimum it seems like I would need to re-implement a ton of stuff from mathlib because of just how much of it depends on choice, plus be very vigilant to ensure that the built-in tactics don't introduce choice in my proofs. It's just unmanageable.

Right, I wanted to say this to you when I saw your post yesterday but didn't have time. You are much better off sticking to Coq if you want to do Bishop style math

[Luigi Massacci]

You will not be able to use most of mathlib (addition of polynomials depends on choice...) or even most tactics (many of which introduce lem sneakily)

[Luigi Massacci]

While Coq already has some awfully sophistiacated libraries for constructive analysis, and a rich community interested in this line of work

[Louis Cabarion]

In open-source communities, forking a project and letting your version shine often beats trying to convince maintainers to reverse long-standing fundamental choices. Has anyone eager for a purely "non-classical" Lean or Mathlib ever actually given it a try, or has the effort stayed at just persuading maintainers?

[Luigi Massacci]

Isak Colboubrani said:

In open-source communities, forking a project and letting your version shine often beats trying to convince maintainers to reverse long-standing fundamental choices. Has anyone eager for a purely "non-classical" Lean or Mathlib ever actually given it a try, or has the effort stayed at just persuading maintainers?

Forking Lean/mathlib is more or less discouraged by the mantainers

[Luigi Massacci]

The fact that it's all one huge construction is arguably one of mathlib's major strengths after all

[Henrik Böving]

Isak Colboubrani said:

In open-source communities, forking a project and letting your version shine often beats trying to convince maintainers to reverse long-standing fundamental choices. Has anyone eager for a purely "non-classical" Lean or Mathlib ever actually given it a try, or has the effort stayed at just persuading maintainers?

Classical reasoning is just so ingrained into the core of Lean that any attempt at building a non-classical mathlib would require modifying substantial parts of Lean. There is not many people that can and want to do this work. Additionally if such a fork wants to profit from the work that the Mathlib community and Lean FRO is putting into the two projects it would need lots of dedicated people to backport changes, otherwise it just gets left behind in a few months.

[Louis Cabarion]

@Henrik Böving I completely agree -- it’s a massive undertaking (and personally, I’m not convinced it’s even necessary -- I’m perfectly happy with classical logic). I’m just curious whether anyone committed to non-classical logic has taken concrete steps beyond simply appealing to the maintainers.

[Niels Voss]

I'm not sure if this is constructive, but the ground zero project has an extra type checker bolted on to Lean to make sure that subsingleton elimination, which is inconsistent with univalence, is not used.

[Morgan Arnold]

Isak Colboubrani said:

In open-source communities, forking a project and letting your version shine often beats trying to convince maintainers to reverse long-standing fundamental choices. Has anyone eager for a purely "non-classical" Lean or Mathlib ever actually given it a try, or has the effort stayed at just persuading maintainers?

I should probably clarify that I'm not making any effort to persuade anyone to do any work on this. It's entirely the prerogative of Lean's maintainers to focus on classical logic, and doing so probably makes sense given its primary status in actual mathematics. I was just asking if an effective means of segregating the classical and non-classical results in Lean and mathlib already existed. It seems like the answer is no. If I really want to ensure that I'm doing purely constructive mathematics, it probably makes more sense to either stick with Rocq or learn Agda or something.

[Louis Cabarion]

Niels Voss said:

I'm not sure if this is constructive, but the ground zero project has an extra type checker bolted on to Lean to make sure that subsingleton elimination, which is inconsistent with univalence, is not used.

Is that https://github.com/forked-from-1kasper/ground_zero?

[Ruben Van de Velde]

I would say the effective means of segregating is assuming everything in mathlib is classical :)

[suhr]

Isak Colboubrani said:

Has anyone eager for a purely "non-classical" Lean or Mathlib ever actually given it a try, or has the effort stayed at just persuading maintainers?

Together with my book I will write my little "mathlib at home". No intent to compete with large mathlib though, just enough stuff to support the book.

And no desire to persuade anyone either (it's useless).

Henrik Böving said:

Classical reasoning is just so ingrained into the core of Lean

Lean core as described in the reference is pretty much constructive. So the only thing one needs to care about are tactics.

[suhr]

Morgan Arnold said:

it probably makes more sense to either stick with Rocq or learn Agda or something.

Take a look at Cubical Agda.

[Henrik Böving]

suhr said:

Henrik Böving said:

Classical reasoning is just so ingrained into the core of Lean

Lean core as described in the reference is pretty much constructive. So the only thing one needs to care about are tactics.

This amounts to the tactics and everything that is proven with them which is pretty much everything. If you want to do fully constructive things in Lean you will have to ignore basically everything that has been built.

[suhr]

Yeah. But so far things are not that bad, and I can just guard against Classical.choice instead of reimplementing everything.

If things are not going to become much worse quickly, I can just reimplement things by need.