# Zulip Chat Archive

## Stream: new members

### Topic: Understanding assume

#### Daniel Keys (Jan 18 2020 at 22:47):

New to functional languages. Want to understand how `assume`

works in Lean. Why is it OK to have `theorem ex1 : ¬(p ∧ ¬q) → (p → q) := begin assume h : ¬(p ∧ ¬q), assume hp : p`

but not for example `theorem ex2 : (p → r ∨ s) → ((p → r) ∨ (p → s)) := begin assume rs : r ∨ s`

?

#### Moses Schönfinkel (Jan 18 2020 at 22:52):

Because -> is right associative. The first argument of `theorem ex2`

is a function from `p`

to `r or s`

.

#### Moses Schönfinkel (Jan 18 2020 at 22:53):

Also note that in `theorem ex1`

, your `h`

is of type `(p and not q) -> false`

, that is, a function type. You're then left with `p -> s`

, where associativity plays no part. You can therefore further assume `p`

. Note that the parentheses around `(p -> q)`

are redundant.

#### Kevin Buzzard (Jan 18 2020 at 23:03):

Surely the analogue of what works in ex1 is `assume prs : (p → r ∨ s)`

? That's the left hand side of the implication. Both goals are of the form `P -> Q`

and you want to start with `assume hP : P`

.

#### Daniel Keys (Jan 18 2020 at 23:04):

So is there any assumption that can be made to help in `theorem ex2`

? I wanted to get started like `assume hp : p`

, like @Kevin Buzzard suggests, but it just doesn't work. I get an error message.

#### Mario Carneiro (Jan 18 2020 at 23:08):

You can't prove that theorem in constructive logic, meaning that the straightforward "follow your nose" approach doesn't work

#### Mario Carneiro (Jan 18 2020 at 23:08):

You can prove it by cases on whether `p`

is true or false

#### Daniel Keys (Jan 18 2020 at 23:09):

How to get started in that case?

#### Mario Carneiro (Jan 18 2020 at 23:09):

`begin by_cases p,`

#### Mario Carneiro (Jan 18 2020 at 23:10):

if it complains about decidable something then write this at the top of your file:

local attribute [instance] classical.prop_decidable

#### Daniel Keys (Jan 18 2020 at 23:11):

Right, it does say `by_cases tactic failed, type of given expression is not decidable`

.

#### Kevin Buzzard (Jan 18 2020 at 23:15):

I said `P`

not `p`

. You have some super-complex goals with lots and lots of p's and q's and and's and r's, but ultimately it is of the form P -> Q with P and Q slightly less complicated expressions. Your job is to figure out what P and Q are, and then assume hP of type P.

#### Daniel Keys (Jan 18 2020 at 23:17):

@Kevin Buzzard Sorry, I noticed that too late. That is actually something I can already get from `intro`

, right?

#### Kevin Buzzard (Jan 18 2020 at 23:17):

oh sure

#### Kevin Buzzard (Jan 18 2020 at 23:25):

if it complains about decidable something then write this at the top of your file:

local attribute [instance] classical.prop_decidable

Isn't something like

local attribute [instance, priority 10] classical.prop_decidable

better? But isn't `open_locale classical`

even better?

#### Mario Carneiro (Jan 18 2020 at 23:30):

Yes, but I don't know if daniel is using mathlib

#### Daniel Keys (Jan 18 2020 at 23:41):

@Moses Schönfinkel Your response is too high-level for a newbie like me. Is there any way to elaborate a bit? For another example, I can do `theorem T3L : ¬p ∧ ¬q → ¬(p ∨ q) := assume right: p ∨ q`

but can't do `assume right : ((p → r) ∨ (p → s)) `

in that `ex2`

.

#### Kevin Buzzard (Jan 18 2020 at 23:42):

Are you really sure you can do `assume right: p ∨ q`

?

#### Kevin Buzzard (Jan 18 2020 at 23:43):

`¬p ∧ ¬q → ¬(p ∨ q)`

is of the form `X -> Y`

with `X=¬p ∧ ¬q`

and `Y=¬(p ∨ q)`

. Do you understand that?

#### Kevin Buzzard (Jan 18 2020 at 23:43):

So the only possible thing you can assume is a proof of `X`

#### Kevin Buzzard (Jan 18 2020 at 23:44):

ex2 is also of the form X -> Y and you have to figure out what X and Y are, and then assume you have a proof of X, and your goal will be to prove Y. But first you need to figure out what X and Y are.

#### Daniel Keys (Jan 18 2020 at 23:45):

@Kevin Buzzard I sure can. I have that working.

theorem T3L : ¬p ∧ ¬q → ¬(p ∨ q) := begin intros notP_and_notQ, assume rhs : p ∨ q, { cases rhs with hp hq, { exact notP_and_notQ.left hp }, { exact notP_and_notQ.right hq } } end #check T3L p q

#### Kevin Buzzard (Jan 18 2020 at 23:55):

sure it works after the intros!

#### Kevin Buzzard (Jan 18 2020 at 23:56):

After the intros, the goal is `(p ∨ q) -> false`

#### Kevin Buzzard (Jan 18 2020 at 23:56):

so you can assume a proof of `(p ∨ q)`

#### Kevin Buzzard (Jan 18 2020 at 23:58):

If your goal is X -> Y then you can assume a proof of X. That's the rule.

#### Joe (Jan 18 2020 at 23:59):

@Daniel Keys

You want to prove `((p → r) ∨ (p → s))`

in `ex2`

, so it just doesn't make any sense to assume it. Else there would be nothing left to prove.

#### Joe (Jan 18 2020 at 23:59):

I'm not sure why you find this confusing...

#### Daniel Keys (Jan 19 2020 at 00:20):

@Joe You're right, that part is not confusing. What I struggle with is something around these lines: to prove a statement, sometimes you need to go several routes. For example, you can have cases that split in "if p is true, this follows" and "if p is not true, this follows". So in my mind it seems like I should be able to "assume p" and reach a conclusion, then "assume not p" and reach the other. That is kind of where I struggle now.

#### Kevin Buzzard (Jan 19 2020 at 00:22):

Yes you can do that

#### Kevin Buzzard (Jan 19 2020 at 00:24):

Do you have mathlib installed? What happens if you type `import tactic.linarith`

at the beginning of your file?

#### Daniel Keys (Jan 19 2020 at 00:26):

What does that do? Why install mathlib?

#### Cerek Hillen (he) (W2'20) (Jan 19 2020 at 00:36):

fellow newbie so take this with a grain of salt: mathlib is the accompanying library that defines a bunch of common mathematical concepts for use in other proofs

#### Cerek Hillen (he) (W2'20) (Jan 19 2020 at 00:37):

e.g. i'm using it for `data.set.basic`

which just defines sets and their properties

#### Kevin Buzzard (Jan 19 2020 at 00:44):

Mathlib offers more tactic tools for you to be able to argue like a mathematician would, for example here's a proof of Q given that `P -> Q`

and `¬ P → Q`

, but using a tactic from mathlib:

import tactic variables (P Q : Prop) open_locale classical example (hP : P → Q) (hnP : ¬ P → Q) : Q := begin by_cases h : P, { apply hP, assumption }, { apply hnP, assumption } end

Without mathlib you have to write some more intimidating stuff like Mario's `local attribute [instance] classical.prop_decidable`

above.

#### Kevin Buzzard (Jan 19 2020 at 00:46):

Your underlying problem with `assume`

is that you're assuming it means a vague all-purpose "assume" which we use in normal English. In Lean `assume`

has one, extremely precise, meaning -- it can only be used on goals of the form `X -> Y`

and it can only be used to assume that `X`

is true.

#### Kevin Buzzard (Jan 19 2020 at 00:48):

I proved `Q`

above by saying "Assume `P`

is true -- then use `hP`

; now assume it's false and use `hnP`

instead". But the Lean translation of *that* kind of "assume" is `by_cases`

, at least if you have mathlib. If you only have core Lean then it will look uglier.

#### Kevin Buzzard (Jan 19 2020 at 00:49):

variables (P Q : Prop) example (hP : P → Q) (hnP : ¬ P → Q) : Q := begin have H : P ∨ ¬ P := classical.em P, cases H, { apply hP, assumption }, { apply hnP, assumption } end

`classical.em`

is the classical law of the excluded middle.

#### Daniel Keys (Jan 19 2020 at 00:59):

@Kevin Buzzard OK then, so the way to introduce other assumptions (is it goals?) is by `have`

? But what was confusing was that I could still use `assume hp:p`

in the very first example I posted. It seems like an extra.

#### Kevin Buzzard (Jan 19 2020 at 01:01):

I can only repeat what I've said before about exactly what assume does

#### Daniel Keys (Jan 19 2020 at 01:01):

That's fine, thank you! I need more homework.

#### Kevin Buzzard (Jan 19 2020 at 01:01):

Try the exercises in Theorem Proving In Lean

#### Kevin Buzzard (Jan 19 2020 at 01:02):

Or the natural number game

#### Daniel Keys (Jan 19 2020 at 01:02):

Well, I did all of those in chapter 3 except for the classical stuff (7 problems) where I got totally stuck.

#### Kevin Buzzard (Jan 19 2020 at 01:03):

Well maybe you could ask some very precise questions about things you were stuck on

#### Kevin Buzzard (Jan 19 2020 at 01:04):

A precise question in the form of some working lean code which people can just cut and paste without having to figure out variables or whatever is usually what goes down best here

#### Daniel Keys (Jan 19 2020 at 01:04):

@Kevin Buzzard I can. Here is this, I need help! `theorem T1 : (p → r ∨ s) → ((p → r) ∨ (p → s)) := sorry`

. The first one in the classical problems in ch.3

#### Joe (Jan 19 2020 at 03:03):

@Daniel Keys

theorem T1 {p q r s : Prop} : (p → r ∨ s) → ((p → r) ∨ (p → s)) := λ h, classical.by_cases (λ hp : p, or.elim (h hp) (λ hr, or.inl $ λ hp, hr) $ λ hs, or.inr $ λ hp, hs) (λ hp : ¬p, or.inl $ λ hp', absurd hp' hp)

#### Daniel Keys (Jan 19 2020 at 08:11):

@Joe @Kevin Buzzard So that brings me exactly to what I fail to understand in these proofs. All of a sudden you have `hr`

and `hs`

, or the even more cryptic `$ λ hp'`

coming up in your `lambda`

terms. How can you produce these and work with them if the only hypothesis is `(p → r ∨ s)`

? Where from does LEAN know what `hp'`

is? Maybe it is my unwillingness to work with `lambda`

. While I'll be looking into it, can one get what you wrote in a framework like this:

theorem T1 : (p → r ∨ s) → ((p → r) ∨ (p → s)) := begin intros prs, cases (em p) with hp hnp, { ... }, { ... } end

which is easier to read, to help my understanding?

#### Mario Carneiro (Jan 19 2020 at 08:24):

lambda is a binder, meaning that it introduces a new name. So when you see `λ hp'`

, you should expect that the name `hp'`

has not been previously used

#### Mario Carneiro (Jan 19 2020 at 08:24):

The tactic version of lambda is `intros`

#### Mario Carneiro (Jan 19 2020 at 08:25):

The dollar sign is just a trick for reducing parentheses. `f $ g x y`

is the same as `f (g x y)`

#### Daniel Keys (Jan 19 2020 at 08:27):

So how do you write it with `begin...end`

? I probably just need to see that once.

#### Mario Carneiro (Jan 19 2020 at 08:28):

variables p q r s : Prop open classical theorem T1 : (p → r ∨ s) → ((p → r) ∨ (p → s)) := begin intros prs, cases (em p) with hp hnp, { cases prs hp with hr hs, { left, intro, exact hr }, { right, intro, exact hs } }, { left, intro, contradiction } end

#### Daniel Keys (Jan 19 2020 at 08:28):

Thanks a lot! This will get me going.

#### Mario Carneiro (Jan 19 2020 at 08:28):

protip: use ` ```lean ... ``` `

to fence lean code

#### Daniel Keys (Jan 19 2020 at 08:43):

I can see what the `left`

and `right`

terms do in the above, but I don't remember having seen that in the manual. Is it there somewhere?

#### Kevin Buzzard (Jan 19 2020 at 08:44):

They're explained in the natural number game

#### Patrick Massot (Jan 19 2020 at 09:01):

https://leanprover.github.io/theorem_proving_in_lean/tactics.html?highlight=left#more-tactics

#### Daniel Keys (Jan 19 2020 at 09:02):

OK, I see. I only got to the end of chapter 3.

Last updated: May 13 2021 at 18:26 UTC