Zulip Chat Archive

Stream: new members

Topic: Understanding assume


view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Jan 18 2020 at 23:08):

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

view this post on Zulip Daniel Keys (Jan 18 2020 at 23:09):

How to get started in that case?

view this post on Zulip Mario Carneiro (Jan 18 2020 at 23:09):

begin by_cases p,

view this post on Zulip 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

view this post on Zulip Daniel Keys (Jan 18 2020 at 23:11):

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

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip Kevin Buzzard (Jan 18 2020 at 23:17):

oh sure

view this post on Zulip 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?

view this post on Zulip Mario Carneiro (Jan 18 2020 at 23:30):

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

view this post on Zulip 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.

view this post on Zulip Kevin Buzzard (Jan 18 2020 at 23:42):

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

view this post on Zulip 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?

view this post on Zulip Kevin Buzzard (Jan 18 2020 at 23:43):

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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Jan 18 2020 at 23:55):

sure it works after the intros!

view this post on Zulip Kevin Buzzard (Jan 18 2020 at 23:56):

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

view this post on Zulip Kevin Buzzard (Jan 18 2020 at 23:56):

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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Joe (Jan 18 2020 at 23:59):

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

view this post on Zulip 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.

view this post on Zulip Kevin Buzzard (Jan 19 2020 at 00:22):

Yes you can do that

view this post on Zulip 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?

view this post on Zulip Daniel Keys (Jan 19 2020 at 00:26):

What does that do? Why install mathlib?

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Kevin Buzzard (Jan 19 2020 at 01:01):

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

view this post on Zulip Daniel Keys (Jan 19 2020 at 01:01):

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

view this post on Zulip Kevin Buzzard (Jan 19 2020 at 01:01):

Try the exercises in Theorem Proving In Lean

view this post on Zulip Kevin Buzzard (Jan 19 2020 at 01:02):

Or the natural number game

view this post on Zulip 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.

view this post on Zulip Kevin Buzzard (Jan 19 2020 at 01:03):

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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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)

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Jan 19 2020 at 08:24):

The tactic version of lambda is intros

view this post on Zulip 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)

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Daniel Keys (Jan 19 2020 at 08:28):

Thanks a lot! This will get me going.

view this post on Zulip Mario Carneiro (Jan 19 2020 at 08:28):

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

view this post on Zulip 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?

view this post on Zulip Kevin Buzzard (Jan 19 2020 at 08:44):

They're explained in the natural number game

view this post on Zulip Patrick Massot (Jan 19 2020 at 09:01):

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

view this post on Zulip 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