## Stream: new members

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

#### Luis O'Shea (Jan 01 2020 at 22:27):

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 (Jan 01 2020 at 23:09):

You need local attribute [instance] classical.prop_decidable

#### Luis O'Shea (Jan 01 2020 at 23:35):

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 (Jan 01 2020 at 23:38):

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 (Jan 01 2020 at 23:45):

Yes. open_locale is for both notations and attributes.

#### Joe (Jan 01 2020 at 23:45):

Here is its documentation

#### Joe (Jan 01 2020 at 23:45):

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 (Jan 01 2020 at 23:50):

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 (Jan 01 2020 at 23:52):

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 (Jan 01 2020 at 23:55):

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 (Jan 01 2020 at 23:57):

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 (Jan 01 2020 at 23:58):

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

#### Luis O'Shea (Jan 02 2020 at 00:01):

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

#### Joe (Jan 02 2020 at 00:03):

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

#### Joe (Jan 02 2020 at 00:03):

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

#### Joe (Jan 02 2020 at 00:04):

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

#### Bryan Gin-ge Chen (Jan 02 2020 at 00:07):

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 (Jan 02 2020 at 02:00):

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 (Jan 02 2020 at 02:00):

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 (Jan 02 2020 at 02:02):

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

#### Kevin Buzzard (Jan 02 2020 at 02:07):

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

#### Kevin Buzzard (Jan 02 2020 at 02:07):

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

#### Kevin Buzzard (Jan 02 2020 at 02:08):

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 (Jan 02 2020 at 02:09):

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

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

#eval L.silly 5 -- 37


Ah!

#### Kevin Buzzard (Jan 02 2020 at 02:10):

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

#### Kevin Buzzard (Jan 02 2020 at 02:11):

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 (Jan 02 2020 at 02:11):

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

#### Kevin Buzzard (Jan 02 2020 at 02:11):

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

#### Kevin Buzzard (Jan 02 2020 at 02:12):

PS

import tactic

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


#### Luis O'Shea (Jan 02 2020 at 02:12):

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

#### Luis O'Shea (Jan 02 2020 at 02:12):

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

#### Kevin Buzzard (Jan 02 2020 at 02:12):

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 (Jan 02 2020 at 02:17):

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