Clarification on constructibility

Stream: lean4

[Ioannis Konstantoulas]

I have been reading a question on the Std4 stream regarding classical logic in Std4.. As I understand it, by sticking to term-based proofs, you do not run the risk of accidentally invoking classical logic; however, simpin Std4 uses classical lemmata, if I read that stream correctly.

Is this also true for tactics in bare Lean 4? That is, if I have no imports on my file, does invoking simp or other tactics run the risk of having my proofs be dependent on classical logic, without me manually opening the Classical namespace?

[Damiano Testa]

I don't think this is so much an issue of tactics, rather than whether you use, directly or indirectly, a result that is proved using an axiom that you do not want.

Tactics may use such a result without you realising it. But, unless you inspect every theorem that you use, you run the same risk by writing your own proof.

[Alex J. Best]

The answer is yes, there are tactics in core that use classical, e.g https://github.com/leanprover/lean4/blob/master/src/Init/Classical.lean#L129. As for simp, anyone could prove a lemma with excluded middle and tag it with simp and simp will use it, namespaces are simply an organizational feature they don't control whether simp will apply lemmas or not. I am not sure if there are such simp lemmas in core but I would guess there are indeed. Simp also uses propositional extensionality internally so that's another source of non-classicality.

[Ioannis Konstantoulas]

Damiano Testa said:

I don't think this is so much an issue of tactics, rather than whether you use, directly or indirectly, a result that is proved using an axiom that you do not want.

Tactics may use such a result without you realising it. But, unless you inspect every theorem that you use, you run the same risk by writing your own proof.

I am not using external theorems except for elementary Nat theorems from core that, as far as I know, are all valid constructively. I do not use any imports, and am implementing notions of divisibility, primality etc. from first principles as an exercise; I want to do this completely constructively.

[Ioannis Konstantoulas]

Alex J. Best said:

The answer is yes, there are tactics in core that use classical, e.g https://github.com/leanprover/lean4/blob/master/src/Init/Classical.lean#L129. As for simp, anyone could prove a lemma with excluded middle and tag it with simp and simp will use it, namespaces are simply an organizational feature they don't control whether simp will apply lemmas or not. I am not sure if there are such simp lemmas in core but I would guess there are indeed. Simp also uses propositional extensionality internally so that's another source of non-classicality.

Could you avoid those lemmas in simp using simp only? More to the point, I got the impression from the beginning chapters of TPIL that one could stick to a constructive logic for proving basic propositions about Prop and Nat. If simp introduces accidental classicality, the exercises with/without Classical in the first few chapters make no sense.

[Damiano Testa]

I suspect that you will find that, while theoretically possible to stay constructive, it is in practice essentially impossible. It might work for a very small project, but anything larger scale is unlikely to succeed.

At least, this is my personal opinion.

[Ioannis Konstantoulas]

This is fine, I want to prove the infinitude of prime numbers constructively.

[François G. Dorais]

All the uses of classical axioms come from Lean core. Tactics in Std currently don't add more but they could if the alternative is inconvenient.

The one tactic in core that always uses classical axioms is by_cases, this is partly fixed in Std. The split tactic uses classical axioms to split if statements. The simp tactic calls split in some circumstances. As a result, many theorems in Lean core and Std use classical axioms even when they are not necessary.

To avoid classical axioms the easy way, you can use semorrison/lean4:release-2023-08-17-split-ifs as your lean toolchain, but then you will not get the benefit of recent Lean updates. The more difficult route is to avoid by_cases completely, avoid split for if statements, inspect every simp use carefully, inspect every theorem you use that's not your own and reprove any one that unnecessarily uses classical axioms.

[Ioannis Konstantoulas]

Thank you for the directions, @François G. Dorais. For my modest goal, I think I can follow your advice.

[Jason Rute]

I don’t know how linters work, but has anyone made a linter which warns if a theorem is not constructive and if so where the sources of nonconstructivity are?

[Eric Wieser]

!3#10954

[Eric Wieser]

The lean 3 meta code is of course worthless and not very portable

[Richard Copley]

If there's not a lot of stuff to check, you can get by with manual checks,

import Std.Logic

-- (3) The classical theorem ¬(p ↔ q) → (¬p ↔ q) is equivalent to dne.

theorem part3
: (∀ p q : Prop, ¬(p ↔ q) → (¬p ↔ q)) ↔ (∀ p : Prop, ¬¬p → p) := ⟨
  fun h p => (h (¬p) p not_iff_self).mp,
  fun hdne _ q hneq => have ⟨hl, hr⟩ := part1.mp hneq ; ⟨hdne q ∘ hl, hr⟩⟩

#print axioms part3 -- 'part3' does not depend on any axioms

[Jun Yoshida]

Another source of Classical is, surprisingly, recursion. You will see the following even if you use semorrison/lean4:release-2023-08-17-split-ifs toolchain:

def test : List Nat → Nat
| [] => 0
| 0 :: l => test l
| (n+1) :: l => 1 + test (n :: l)

-- 'test' depends on axioms: [Classical.choice, Quot.sound, propext]
#print axioms test

[François G. Dorais]

Fascinating example! The termination proof somehow uses classical axioms but I don't know why. This is worth investigating...

[Jun Yoshida]

Lean internally convert the def of test into well-founded recursion (see e.g. #print test). The termination proof depends on theorems in Init.Data.Nat.Linear where you see a lot of by_casess.

[François G. Dorais]

Indeed, by_cases ends up being the culprit. This is really interesting because indiscriminately using classical axioms in termination proofs is not sound. Fortunately, it appears that all of these uses are not essential since the definition makes it past the kernel.

[Jun Yoshida]

Yeah, almost all uses of by_cases in Init.Nat.Data.Linear are virtually equivalent to cases. So, if you want to make the file Classical-free, it would be a trivial (but maybe boring) work. I am not sure if it impacts the performance of the kernel.

[Mario Carneiro]

There is no possible way this could impact the performance of the kernel