3
$\begingroup$

I would like to write constructive proofs in Lean 4, so I don't want my proofs to depend on Classical.choice, the axiom of choice. However, one of my proofs does, as shown by the command #print axioms substring_unpack, and it's not obvious to me why that is. I have removed tactics like omega and by_cases which I know may rely on choice, but it's possible that a simp somewhere is pulling in a lemma which depends on choice.

The proof is quite long.

How can I determine where this axiom is being snuck in?

Improve this question
$\endgroup$
6
  • 1
    $\begingroup$ Not a very elegant solution, but try to replace part of your proof by sorry and see what happens. Of course this will add sorry as an axiom, but at some point choice should disappear. $\endgroup$
    – Ricky
    Commented Feb 18 at 11:28
  • 2
    $\begingroup$ I would even start by replacing the full proof by sorry, to check that the statement doesn't somehow uses choice. $\endgroup$
    – Ricky
    Commented Feb 18 at 11:29
  • 2
    $\begingroup$ I hate to say, this but the are many ways the axiom of choice can sneak into a Lean proof. Trying to do constructive math in Lean 4 is very painful. $\endgroup$
    – Jason Rute
    Commented Feb 18 at 12:29
  • $\begingroup$ Well, if you start using a lot of mathlib then I agree, but otherwise it should be more or less fine. $\endgroup$
    – Ricky
    Commented Feb 18 at 12:37
  • 2
    $\begingroup$ @Ricky. No. It is true in even base lean. Macros, automatic termination proofs, and common tactics can all add choice unexpectedly. $\endgroup$
    – Jason Rute
    Commented Feb 18 at 14:54

1 Answer 1

Reset to default
3
$\begingroup$

I tried to replace parts of the proof with sorry, but I was getting confused by the results of doing so, so I made a small private lemma with the part of the proof that seemed to be at issue, and again tried to replace parts of the smaller proof with sorry.

I again got confused, so I tried to print my lemma and copied and pasted the output of print and renamed the resulting lemma. It didn't actually type-check, but I put in a few more sorrys and got something that type-checked. Then I replaced more and more of the raw proof term with sorry until I had narrowed it down further.

At some point I stumbled on a clue, and realised that I needed to set_option pp.all true to see the full (gory) details.

It turned out that I had indeed relied on a theorem from Mathlib - and while this theorem itself did not rely on the axiom of choice, my use of it did, because it implicitly summoned into play some type class instances which did. After some digging I found that:

OrderedCancelAddCommMonoid.toContravariantClassLeft

was a/the culprit, which uses

contravariant_lt_of_contravariant_le

which uses

contravariant_le_iff_contravariant_lt_and_eq

which uses

LE.le.lt_or_eq, which is an alias for lt_or_eq_of_le

which uses

Classical.propDecidable which says that all Props are Decidable (with my constructivist hat on I disagree with this!)

which uses

Classical.em, the law of the excluded middle

which uses

Classical.choose

which uses

Classical.indefiniteDescription, which uses the axiom of choice (in some way I don't understand)

My plan of attack now is to use constructive instances, or define them myself if they don't already exist, using priority to ensure they are picked up first.

Improve this answer
$\endgroup$
4
  • 1
    $\begingroup$ Is it a huge secret what it is that you're proving? Perhaps someone already did it in one of the constructively valid proof assistants. And also, what's the point of formalizing constructive math in a proof assistant that is riddled with secret sneaky uses of choice and excluded middle? $\endgroup$
    – Andrej Bauer
    Commented Feb 19 at 0:05
  • $\begingroup$ Your persistence is admirable. $\endgroup$
    – hardmath
    Commented Feb 19 at 13:54
  • 1
    $\begingroup$ Aside: Classical.indefiniteDescription is just another name for the axiom of choice. $\endgroup$
    – François G. Dorais
    Commented Feb 19 at 19:00
  • 1
    $\begingroup$ Classical.propDecidable also directly uses choice. Classical.indefiniteDescription and choice both lift Prop to Type*, and they are equivalent without axioms. $\endgroup$
    – Junyan Xu
    Commented Feb 19 at 19:58

Not the answer you're looking for? Browse other questions tagged or ask your own question.