Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-05-07 09:30 6fc8b2a9

View on Github →

refactor(*): more choice-free proofs (#7455) Now that lean v3.30 has landed (and specifically leanprover-community/lean#560), we can finally make some progress on making a significant fraction of mathlib foundations choice-free. This PR does the following:

  • No existing theorem statements have changed (except linear_nonneg_ring as noted below).
  • A number of new theorems have been added to the decidable namespace, proving choice-free versions of lemmas under the assumption that something is decidable. These are primarily concentrated in partial orders and ordered rings, because total orders are already decidable, but there are some interesting lemmas about partial orders that require decidability of le.
  • linear_nonneg_ring was changed to include decidability of nonneg, for consistency with linear ordered rings. No one is using this anyway so there shouldn't be any fallout.
  • A lot of the ordered_semiring lemmas need decidable versions now because one of the core axioms, mul_le_mul_of_nonneg_left, is derived by LEM from an equivalent statement about lt instead of being an actual axiom. If this is refactored, these theorems can be removed again.
  • The main files which were scoured of choicy proofs are: algebra.ordered_group, algebra.ordered_ring, data.nat.basic, data.int.basic, data.list.basic, and computability.halting.
  • The end goal of this was to prove computable_pred.halting_problem without assuming choice, finally validating a claim I made more than two years ago in my paper on the formalization. I have not yet investigated a linter for making sure that these proofs stay choice-free; this can be done in a follow-up PR.

Estimated changes

modified theorem add_le_mul_two_add
deleted theorem decidable.mul_le_mul_left
modified theorem le_mul_of_one_le_left
modified theorem le_mul_of_one_le_right
modified theorem le_of_mul_le_of_one_le
modified theorem lt_mul_of_one_lt_left
modified theorem lt_mul_of_one_lt_right
modified theorem mul_le_mul
modified theorem mul_le_mul_of_nonneg_left
modified theorem mul_le_mul_of_nonneg_right
modified theorem mul_le_mul_of_nonpos_left
modified theorem mul_le_mul_of_nonpos_right
modified theorem mul_le_of_le_one_left
modified theorem mul_le_of_le_one_right
modified theorem mul_le_one
modified theorem mul_lt_mul''
modified theorem mul_lt_mul'
modified theorem mul_lt_mul
modified theorem mul_nonneg
modified theorem mul_nonneg_le_one_le
modified theorem one_lt_mul
modified theorem one_lt_mul_of_le_of_lt
modified theorem one_lt_mul_of_lt_of_le
modified theorem ordered_ring.mul_nonneg
modified theorem partrec.fix
added theorem partrec.fix_aux
modified theorem partrec.sum_cases_left
modified theorem partrec.sum_cases_right
added def int.least_of_bdd
modified theorem list.eq_or_ne_mem_of_mem
modified theorem list.lex.ne_iff
modified theorem nat.lt_of_div_lt_div
modified theorem lt_top_iff_ne_top