Learning from mathlib (e.g., TPiL 4.6, Q5)

Stream: new members

[Luis O'Shea]

In trying to learn from mathlib I've run into a couple of things I don't understand. For example, say you want to prove (¬∀ x, p x) → ∃ x, ¬p x, where p is a predicate. This is, (modulo decidability) proven in mathlib, so I tried to just copy that approach:

import logic.basic

variables (α : Type) (p q : α → Prop)

open classical

-- Mirrors proof of not_forall in logic/basic.lean:446
example: (¬∀ x, p x) → ∃ x, ¬p x :=
not.imp_symm $ assume nx x, nx.imp_symm $ assume hnpx, ⟨x,hnpx⟩ -- Error: need decidable (p x)

On the one hand the failure is not surprising (since not.imp_symm needs decidability). On the other hand I had hoped open classical would make everything decidable. However, what does work is to make my own version of not.imp_symm:

-- Mirrors proof of not.imp_symm in logic/basic.lean:167
lemma not.my_imp_symm {P Q : Prop} (hnpq : ¬P → Q) (hnq : ¬Q) : P :=
by_contradiction $ assume hnp, hnq $ hnpq hnp

example: (¬∀ x, p x) → ∃ x, ¬p x :=
not.my_imp_symm $ assume nx x, nx.my_imp_symm $ assume hnpx, ⟨x,hnpx⟩ -- Success!

So my questions are:

1. If I'm working classically what do I do if I need a theorem that requires decidability (such as not.imp_symm)? (Obviously reproving it as I did is ugly.)
2. Along the way I noticed that the above lemma is called using "dot notation" (namely nx.my_imp_symm). I assume this is similar to things like and.left, but I don't understand how the syntax works. Is it described somewhere?

[Joe]

You need local attribute [instance] classical.prop_decidable

[Luis O'Shea]

Thanks. I'm curious, do "normal" classical Lean scripts start with that line (local attribute [instance] classical.prop_decidable)? (Perhaps a more pointed version of my question is: if I'm a classical mathematician , should I start all my scripts with local attribute [instance] classical.prop_decidable?)

[Luis O'Shea]

Thanks to the above tip (and searching through mathlib) it seems I can also do open_locale classical (with a import tactic at the top). Is that the way to write classical math? (Note that I don't understand the implications of open_locale).

[Joe]

Yes. open_locale is for both notations and attributes.

[Joe]

Here is its documentation

[Joe]

This consists of two user-commands which allow you to declare notation and commands localized to a namespace.

• Declare notation which is localized to a namespace using:

localized "infix ` ⊹ `:60 := my_add" in my.add

• After this command it will be available in the same section/namespace/file, just as if you wrote local infix ⊹ :60 := my_add
• You can open it in other places. The following command will declare the notation again as local notation in that section/namespace/files:

open_locale my.add

• More generally, the following will declare all localized notation in the specified namespaces.

open_locale namespace1 namespace2 ...

• You can also declare other localized commands, like local attributes

localized "attribute [simp] le_refl" in le

• Warning 1: as a limitation on user commands, you cannot put open_locale directly after your imports. You have to write another command first (e.g. open, namespace, universe variables, noncomputable theory, run_cmd tactic.skip, ...).
• Warning 2: You have to fully specify the names used in localized notation, so that the localized notation also works when the appropriate namespaces are not opened.

[Joe]

So there is a line in the file tactic/localized.lean that makes open_locale work:

-- you can run `open_locale classical` to get the decidability of all propositions.
localized "attribute [instance, priority 9] classical.prop_decidable" in classical

[Luis O'Shea]

That's how I found it -- I searched mathlib for classical.prop_decidable and one of the first hits is the comment above (namely "you can run open_locale classical to get the decidability of all propositions.").

[Luis O'Shea]

Beyond that I find the documentation for open_locale a bit obscure (being a beginner at Lean). Is it fair to summarize this thread as: If you want to do classical math just put open_locale classical at the top of your files? (Or perhaps more conservatively, wait until you need it, then stick it at the top.)

[Joe]

Yes, you can do that.
The other use for open_locale is for notation.
You can define the notation for pi like this

localized "notation `π` := real.pi" in real

And when you want to use the notation, say open_locale real.

[Kevin Buzzard]

That (open_locale classical) is pretty much what I do. I also add noncomputable theory at the top sometimes

[Luis O'Shea]

I wonder whether I should start a new thread for my "dot notation" question? (It's orthogonal ...)

[Joe]

If you have a list l : list nat, l.length is the same as list.length l.

[Joe]

I don't know what else can be said about the dot notation.

[Joe]

For me it is just a way of avoiding writing the namespace.

[Bryan Gin-ge Chen]

It's discussed briefly in TPiL in section 3.3.1:

Lean provides another useful syntactic gadget. Given an expression e of an inductive type foo (possibly applied to some arguments), the notation e.bar is shorthand for foo.bar e. This provides a convenient way of accessing functions without opening a namespace.

There's also a little bit more about it in 9.1.

[Luis O'Shea]

I'm going to read through §3.3.1 and §9.1. In the meantime (while I figure out what degree of denseness I'm suffering from) here is a more concrete explanation of what I fund puzzling about the dot syntax. While I understand l.length, what I don't understand is that this works (it's just a minimal version of the above):

lemma not.my_imp_symm {P Q : Prop} (hnpq : ¬P → Q) (hnq : ¬Q) : P :=  sorry
variables (α : Type) (p q : α → Prop)
example (nx : ¬∃ x, ¬p x) (x : α) : p x := nx.my_imp_symm (λ h, ⟨x,h⟩) -- this is fine!

and yet if I do the obvious replacement of nx.my_imp_symm to not.my_imp_symm nx:

example (nx : ¬∃ x, ¬p x) (x : α) : p x := (not.my_imp_symm nx) (λ h, ⟨x,h⟩) -- this does not work!

then it (clearly) does not work.

[Luis O'Shea]

I'm going to read through §3.3.1 and §9.1. In the meantime (while I figure out what degree of denseness I'm suffering from) here is a more concrete explanation of what I fund puzzling about the dot syntax. While I understand l.length, what I don't understand is that this works (it's just a minimal version of the above):

lemma not.my_imp_symm {P Q : Prop} (hnpq : ¬P → Q) (hnq : ¬Q) : P :=  sorry
variables (α : Type) (p q : α → Prop)
example (nx : ¬∃ x, ¬p x) (x : α) : p x := nx.my_imp_symm (λ h, ⟨x,h⟩) -- this is fine!

and yet if I do the obvious replacement of nx.my_imp_symm to not.my_imp_symm nx:

example (nx : ¬∃ x, ¬p x) (x : α) : p x := (not.my_imp_symm nx) (λ h, ⟨x,h⟩) -- this does not work!

then it (clearly) does not work.

[Kevin Buzzard]

It doesn't work, but that's not because of a dot notation issue.

[Kevin Buzzard]

It doesn't work because the inputs are the wrong way around.

[Kevin Buzzard]

example (nx : ¬∃ x, ¬p x) (x : α) : p x := not.my_imp_symm (λ h, ⟨x,h⟩ : ¬ p x → ∃ x, ¬p x) nx

[Kevin Buzzard]

The idea is that if L has type list then L.blah will look at list.blah and then go through the inputs and find the first one of type list and replace it with L. This might not be the first explicit input to the function.

[Kevin Buzzard]

def list.silly (n : ℕ) (l : list ℕ) := 37

def L : list ℕ := [1,2,3]

#eval L.silly 5 -- 37

[Luis O'Shea]

Ah!

[Kevin Buzzard]

In your example, hnpq is a pi type, and it's hnq which has type not <something>.

[Kevin Buzzard]

If you can be bothered to search back a few months you'll find some thread where someone else explains pretty much the same thing to me ;-)

[Luis O'Shea]

Right -- I need lemma not_my_imp_symm {P Q : Prop} (hnq : ¬Q) (hnpq : ¬P → Q) : P := sorry (flipped order of arguments)

[Kevin Buzzard]

One wonders whether this sort of thing should be documented somehow.

[Kevin Buzzard]

PS

import tactic

lemma not.my_imp_symm {P Q : Prop} (hnpq : ¬P → Q) (hnq : ¬Q) : P := by finish

[Luis O'Shea]

Sadly, once you see what's going on it does seem very trivial.

[Luis O'Shea]

(Mind you I'm very grateful to have this explained to me!)

[Kevin Buzzard]

dot notation is trivial, but only once you've spent a fair amount of time figuring out what's going on ;-) I think a lot of the computer scientists figured this out a long time ago, but it took me a while.

[Kevin Buzzard]

For what it's worth, here is me wrestling with this stuff just under a year ago: https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/dot.20notation.20confusion/near/157341136

[Bryan Gin-ge Chen]

I think I finally "got" dot notation from reading your thread as well.

[Luis O'Shea]

I was chuffed when I recently used flip in a proof. This trick (dot syntax) is another sneaky way of reordering arguments (without resorting to lambdas or small lemmas).