# Zulip Chat Archive

## 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:

- 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.) - 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

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

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

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

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

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

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).

Last updated: Dec 20 2023 at 11:08 UTC