Classical theory

Stream: lean4

[Marcus Rossel]

IIRC in Lean 3 there was a way to declare that one's entire project should be able to use classical reasoning, thus alleviating the pain of writing open classical everywhere. Is there a way to do this in Lean 4?

[Henrik Böving]

You do not have to open Classical to actual use classical logic, the axioms etc. are just in a namespace named Classical there is no magic afaik.

[Marcus Rossel]

But I think if I don't open Classical I (for example) don't get certain type class instances automatically (e.g. DecidablePred for every predicate).

[Kyle Miller]

If you do open scoped Classical you get just the instances by the way.

[Kyle Miller]

I'm not recalling what you're talking about for Lean 3 -- I know about open_locale classical and noncomputable theory, but I'd only ever seen those at the top of a file.

[Kevin Buzzard]

Yes, I don't think open classical gives any new instances in lean 3, I think it just literally copies stuff into the root namespace

[Marcus Rossel]

Kevin Buzzard said:

Yes, I don't think open classical gives any new instances

#synth ∀ p, DecidablePred p -- fails

open Classical
#synth ∀ p, DecidablePred p -- works

[Kevin Buzzard]

Oh interesting! This was not a thing in Lean 3 AFAIK

[Henrik Böving]

it doesnt work because the Decidable instance is a scoped one so indeed you have to open the scope to get this to work.

[Marcus Rossel]

Kyle Miller said:

I'm not recalling what you're talking about for Lean 3 -- I know about open_locale classical and noncomputable theory, but I'd only ever seen those at the top of a file.

Perhaps I thought that open_locale_classical behaves like open Classical on every file in the project. Does it not?

[Marcus Rossel]

Henrik Böving said:

it doesnt work because the Decidable instance is a scoped one so indeed you have to open the scope to get this to work.

What is the whole scoped thing about?

[Kyle Miller]

scoped instances are basically a replacement for the open_locale mechanism

[Henrik Böving]

uh, its an attribute you can put on things like notation or instances that says "only make this active if the user has opened the scope".

[Kyle Miller]

The way open_locale worked is that you could register actual Lean code to run when you open a "locale"

[Kyle Miller]

so for example adding notation or running the attribute command

[Marcus Rossel]

Thanks for all this info! I can use it to rephrase my original question :big_smile::
Is there a way to open scoped instances from a given namespace for an entire project instead of a single file?

[Kyle Miller]

I just checked the Lean 3 behavior, and open_locale classical did not work across modules. You had to do it per module.

[Jireh Loreaux]

Kyle, I think this may have been a semi-recent fix. I recall not long ago that there was some problem with open_locale classical infecting downstream files. (Perhaps I'm misremembering, but I recall it distinctly.)

[Kyle Miller]

It has been exactly the same as writing this for a couple years:

local attribute [instance, priority 9] classical.prop_decidable
local attribute [instance, priority 8] eq.decidable

[Kyle Miller]

You might be thinking of the classical tactic infecting later theorems in a file?

[Jireh Loreaux]

Probably.

[Kyle Miller]

@Marcus Rossel Maybe a more general (and still reasonable) question would be "is there a way to run some command at the beginning of every module in my project?"

[Jireh Loreaux]

Marcus, I would assume that there is no way to open a scope for an entire project because it would need to go in the lake manifest, but then lake would somehow need to know about the scopes defined in imported projects. But perhaps people other than me have more clever ideas.

[Kyle Miller]

@Marcus Rossel Actually, it turns out to be easy if you're OK with needing to import something. I just wasn't sure if this was allowed. Create a module containing attribute [instance] Classical.propDecidable and then import it in such a way that every module in your project (transitively) imports it.

[Reid Barton]

Doesn't that only affect the current module (contrary to what one might think)? Or was that only for -instance?

[Kyle Miller]

I guess it was contrary to contrary what one might think for me, since I thought it might work just like -instance, but in the test I did it actually carries over to another module.

[Reid Barton]

I guess that sort of makes sense but really it seems unnecessarily confusing

[Oliver Nash]

Do we wish to discourage open Classical in Mathlib4 the same way we (usually) discouraged open_locale classical in Mathlib3?

[Oliver Nash]

For example:

import Mathlib.Data.Finset.Basic
import Mathlib.Algebra.Parity

noncomputable section

open Classical

def foo (s : Finset ℕ) : Finset ℕ := s.filter Even

set_option pp.explicit true
set_option pp.fullNames true

/-
fun s ↦ @Finset.filter
  ℕ
  (@Even ℕ instAddNat)
  (fun a ↦ Classical.propDecidable (@Even ℕ instAddNat a))
  s
-/
#print foo

[Oliver Nash]

shows that definitions will still pick up the Classical instances if open Classical is active and this presumably causes definitional problems later on.

[Eric Wieser]

I think open Classical should only ever be allowed in the form

open Classical in
def foo := sorry

[Yury G. Kudryashov]

Why does it pick up the classical instances? Should we decrease their priority?

[Kevin Buzzard]

History says that this won't work -- lean will eventually find the bad instances somehow. We now have a good understanding of what we should be doing -- decidable assumptions to make theorem statements compile and the (now not broken) classical tactic in proofs.

[Eric Wieser]

Kevin, there's one more missing piece which is using the classical instances in defs still

[Eric Wieser]

Which is ok, but requires either open Classical in beforehand or letI := Classical.dec _ or similar inside