open classical

Stream: general

[Thanos Tsouanas]

In a lot of documentation I see open classical mentioned as a requirement to use some non-constructive tactics like by_cases, by_contradiction, etc. I was hoping that deleting open classical from such examples would result to an error, but everything compiled fine. Digging a bit I saw that my lean/library/init dir has a default.lean file that seems to be auto-included or something, and in it I see an import line importing init.classical (among other stuff).
What's the recommended way to proceed if I want Lean to complain (or, even better, to throw a warning) when non-constructive proofs are present in a .lean file? I saw that I can add a prelude line to "not import anything", but I was suppose there's a more standard way for achieving this.
Any pointers to documentation or some relevant conversation here on Zulip, would be very helpful!

[Alex J. Best]

open classical should only open the namespace and just make lemmas accessible via shorter names, open_locale classical will actually add classical instances to the typeclass system locally and therefore subtly affect proofs

[Eric Rodriguez]

Those comments are not too accurate - by_cases and by_contradiction will work intuitionalistically if the required decidable instances are there. So I'd start by checking #print axioms (your decl) and seeing whether classical.choice is actually used

[Alex J. Best]

I think there are a few users commands on zulip for printing all the axioms in a file and stuff liek that, here is one by @Reid Barton https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/not.20equals/near/209186002, I thought @Mario Carneiro had something doing a similar task at some point too? Not sure if anything ever made it to mathlib

[Alex J. Best]

It wouldn't be too difficult to make a version that fails if a certain axiom is present I guess

[Thanos Tsouanas]

Ok, this is pretty much my first contact with lean on my computer (just fiddled with the natural numbers game via my browser up to now).
I used leanpkg to make a new Lean package, and simply adding #print axioms (nothing more than that) on a file shows:

quot.sound : ∀ {α : Sort u} {r : α → α → Prop} {a b : α}, r a b → quot.mk r a = quot.mk r b
classical.choice : Π {α : Sort u}, nonempty α → α
propext : ∀ {a b : Prop}, (a ↔ b) → a = b

So I guess classical logic is available?

[Eric Rodriguez]

classical logic is available, but you can always choose to ignore it

[Thanos Tsouanas]

I'm trying to understand what @Eric Rodriguez mentioned about «the required decidable instances are there».

[Eric Rodriguez]

wrong eric;b so for example, if you're doing by_cases : a = b for a b : ℕ, Lean will let you anyways, because there is an algorithm that can decide whether two nats are equal

[Thanos Tsouanas]

Ah, I see. But can I suppose I can choose to not have it available, so that non-constructive proofs would not be accepted?

[Eric Rodriguez]

the best way to go about that is check your decls to make sure no axioms are used (or quot.sound/propext aren't used, not sure how pure you want to be)

[Eric Rodriguez]

also note that quot.sound actually is how functional extensionality is proved in lean

[Thanos Tsouanas]

I understand what you said about nat equality, but this

theorem test (p : Prop) : p ∨ ¬p :=
begin
  by_cases hp: p,
    left, assumption,
    right, assumption,
end

compiled. Is there a "standard" way to have it... not compile, or issue a warning?

[Eric Wieser]

There is a thread somewhere with some code for a tactic that detects that. There's nothing built in.

[Eric Rodriguez]

there was a change here that made by_cases default to classical logic when the decidable instances aren't available :/ i think the easiest is still just #print axioms test sadly

[Eric Wieser]

@Mario Carneiro, could you make a "please adopt" PR with the axiom-checking meta code I'm thinking of to make it easier to find in future? I'm pretty sure it was yours and called @[intuit]

[Thanos Tsouanas]

Thanks Eric Rodriguez ! I saw the change now and it's starting to make more sense.

[Thanos Tsouanas]

Thanks for the pointer of that code @Eric Wieser , I just found the intuit message of Mario!

[Thanos Tsouanas]

I will read that thread now ( #new members > intuitionistic logic ). :D

[Mario Carneiro]

Sure, I will do that shortly

[Thanos Tsouanas]

Playing with adding/removing open classical, I see that this:

theorem lem1 : A ∨ ¬ A :=
by_contradiction
  (assume h1 : ¬ (A ∨ ¬ A),
    have h2 : ¬ A, from
      assume h3 : A,
      have h4 : A ∨ ¬ A, from or.inl h3,
      show false, from h1 h4,
    have h5 : A ∨ ¬ A, from or.inr h2,
    show false, from h1 h5)

fails without open classical, but this:

theorem lem2 : A ∨ ¬ A :=
begin
  by_contradiction,
  have h2 : ¬ A, assume h3 : A,
  have h4 : A ∨ ¬ A, from or.inl h3, contradiction,
  have h4 : A ∨ ¬ A, from or.inr h2, contradiction,
end

succeeds.
I suppose the first one is trying to work by writing the "proof term" directly, and it fails because the by_contradiction here is not a tactic but some kind of term which is not included (since there was no open classical); while on the second code with the begin/end the thing compiles because here by_contradiction is a tactic, and the change that @Eric Rodriguez pointed at, had the tactic auto-open classical (and I suppose the by_contradiction tactic uses the by_contradiction term under the hood).
Is this, more or less, what's going on here?

[Kyle Miller]

In particular, the first is using docs#classical.by_contradiction, which is what open classical is letting you access without qualifying it with the classical namespace:

theorem lem1 : A ∨ ¬ A :=
classical.by_contradiction
  (assume h1 : ¬ (A ∨ ¬ A),
    have h2 : ¬ A, from
      assume h3 : A,
      have h4 : A ∨ ¬ A, from or.inl h3,
      show false, from h1 h4,
    have h5 : A ∨ ¬ A, from or.inr h2,
    show false, from h1 h5)

[Kyle Miller]

tactic#by_contradiction ends up using this tactic:

meta def by_contradiction (H : name) : tactic expr :=
do tgt ← target,
  tgt_wh ← whnf tgt reducible, -- to ensure that `not` in `ne` is found
  (match_not tgt_wh $> ()) <|>
  (mk_mapp `decidable.by_contradiction [some tgt, none] >>= eapply >> skip) <|>
  (mk_mapp `classical.by_contradiction [some tgt] >>= eapply >> skip) <|>
  fail "tactic by_contradiction failed, target is not a proposition",
  intro H

This tries using decidable.by_contradiction if it can find a way to constructively do it (using the decidable system), and otherwise it falls back on using the classical.by_contradiction lemma that's proved using docs#classical.choice

[Kyle Miller]

A way you can trigger the first case is to put [decidable (A ∨ ¬ A)] as an argument to lem2.

[Thanos Tsouanas]

Thanks Kyle, this was super clear!