Zulip Chat Archive

Stream: new members

Topic: unnecessary axioms


Nick Chopper (Mar 28 2020 at 12:40):

it seems that nat.lt_of_sub_pos in mathlib can simply call nat.add_lt_of_lt_sub_left to avoid use of classical.choice

Nick Chopper (Mar 28 2020 at 12:41):

(deleted)

Patrick Massot (Mar 28 2020 at 12:41):

If you care about avoiding choice you can open a PR.

Kevin Buzzard (Mar 28 2020 at 12:45):

Mathlib has become a classical library for the most part

Patrick Massot (Mar 28 2020 at 12:49):

But he can still open a PR if he cares, right? Certainly I won't fix this because I don't care using choice, but that modification doesn't sound like it would make mathlib more difficult to use.

Nick Chopper (Mar 28 2020 at 13:00):

Not worry much about that... just want to follow https://arxiv.org/abs/1904.09193 with Lean (and avoid classical reasoning at this time)

Mario Carneiro (Mar 28 2020 at 22:20):

You can just use your own version of lt_of_sub_pos if you want it in your local proof

Mario Carneiro (Mar 28 2020 at 22:20):

if it has ended up deeply embedded as a result of, say, the proof that int is a ring, then you will need to PR to fix that


Last updated: Dec 20 2023 at 11:08 UTC