Understanding assume

Stream: new members

[Daniel Keys]

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]

Because -> is right associative. The first argument of theorem ex2 is a function from p to r or s.

[Moses Schönfinkel]

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]

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]

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]

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

[Mario Carneiro]

You can prove it by cases on whether p is true or false

[Daniel Keys]

How to get started in that case?

[Mario Carneiro]

begin by_cases p,

[Mario Carneiro]

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

local attribute [instance] classical.prop_decidable

[Daniel Keys]

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

[Kevin Buzzard]

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]

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

[Kevin Buzzard]

oh sure

[Kevin Buzzard]

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]

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

[Daniel Keys]

@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]

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

[Kevin Buzzard]

¬p ∧ ¬q → ¬(p ∨ q) is of the form X -> Y with X=¬p ∧ ¬q and Y=¬(p ∨ q). Do you understand that?

[Kevin Buzzard]

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

[Kevin Buzzard]

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]

@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]

sure it works after the intros!

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Joe]

@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]

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

[Daniel Keys]

@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]

Yes you can do that

[Kevin Buzzard]

Do you have mathlib installed? What happens if you type import tactic.linarith at the beginning of your file?

[Daniel Keys]

What does that do? Why install mathlib?

[Cerek Hillen (he) (W2'20)]

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

e.g. i'm using it for data.set.basic which just defines sets and their properties

[Kevin Buzzard]

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]

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]

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]

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]

@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]

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

[Daniel Keys]

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

[Kevin Buzzard]

Try the exercises in Theorem Proving In Lean

[Kevin Buzzard]

Or the natural number game

[Daniel Keys]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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]

@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]

@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]

@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]

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]

The tactic version of lambda is intros

[Mario Carneiro]

The dollar sign is just a trick for reducing parentheses. f $ g x y is the same as f (g x y)

[Daniel Keys]

So how do you write it with begin...end? I probably just need to see that once.

[Mario Carneiro]

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]

Thanks a lot! This will get me going.

[Mario Carneiro]

protip: use ```lean ... ``` to fence lean code

[Daniel Keys]

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]

They're explained in the natural number game

[Patrick Massot]

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

[Daniel Keys]

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