Zulip Chat Archive

Stream: new members

Topic: An example involving Ch.2 and NNG


view this post on Zulip Debendro Mookerjee (Mar 16 2020 at 23:13):

In chapter 2 in Theorem Proving in Lean, we learn about definitions, so to try it out I made this definition:
def dvd (m n: ℕ): Prop := ∃ k, n = m * k
In the Natural Number Game, we learn about tactics like rw,etc. So I was wondering how to rewrite a goal with a definition. I have this statement in my tatic state:
hbleft : n = a * b. Clearly we see that a divides n. But when I say rw dvd at hbleft Lean rejects this as a valid piece of code. So I can I apply dvd to the statement hbleft to show a divides n?

view this post on Zulip Kenny Lau (Mar 16 2020 at 23:15):

have hadn : dvd a n := \<_, hbleft\>

view this post on Zulip Debendro Mookerjee (Mar 16 2020 at 23:22):

Thanks, it works now

view this post on Zulip Debendro Mookerjee (Mar 16 2020 at 23:31):

Also in the natural number game we could use the rw tactic to invoke previous theorems; does that same thing work for conditional sentences that I assume to be true? For instance I have a conditional sentence hp : dvd p n → q and in my tactic state I have hadn : dvd a n Can I use my hpto rewrite hadn. I tried rw hp at hadn and apply hp at hadn but Lean stated that code was not valid. How to I use hp to simplify hadn?

view this post on Zulip Reid Barton (Mar 16 2020 at 23:44):

You can only rw with an equality or an iff. An implication is just a function, so you can apply it, but there is no such thing as apply at. Here, you could write replace hadn := hp hadn

view this post on Zulip Reid Barton (Mar 16 2020 at 23:44):

Or just use hp hadn directly wherever you need it

view this post on Zulip Reid Barton (Mar 16 2020 at 23:45):

Or have hq : q, { apply hp, exact hadn }, or many other variations.

view this post on Zulip Debendro Mookerjee (Mar 16 2020 at 23:57):

@Reid Barton I used have hq : q, { apply hp, exact hadn }, and replace hadn := hp hadn but got this error:

type mismatch at application
  hp hadn
term
  hadn
has type
  dvd a n
but is expected to have type
  dvd p n

view this post on Zulip Reid Barton (Mar 16 2020 at 23:58):

Ah, well, yeah

view this post on Zulip Reid Barton (Mar 16 2020 at 23:58):

I missed that it was a trick question. a is not p.

view this post on Zulip Debendro Mookerjee (Mar 17 2020 at 00:02):

But when I replace a with p I get the error:

type mismatch at application
  hp hadn
term
  hadn
has type
  dvd p n
but is expected to have type
  dvd p n
types contain aliased name(s): p
remark: the tactic `dedup` can be used to rename aliases

view this post on Zulip Debendro Mookerjee (Mar 17 2020 at 00:03):

So what is dedup and how is it used?

view this post on Zulip Kenny Lau (Mar 17 2020 at 00:03):

It means you have two variables with the same name p

view this post on Zulip Reid Barton (Mar 17 2020 at 00:04):

You've done something wrong earlier.

view this post on Zulip Debendro Mookerjee (Mar 17 2020 at 00:04):

But if I use difference variable names a and p I still get the Type Mismatch

view this post on Zulip Bryan Gin-ge Chen (Mar 17 2020 at 00:05):

Please post your code. It's very hard to help without seeing what you're working with.

view this post on Zulip Debendro Mookerjee (Mar 17 2020 at 00:07):

def composite (d : ℕ): Prop:= ¬ prime d

theorem composite_fact (c: ℕ) : composite c ↔ ∃ (a b: ℕ), c = a*b ∧ a ≤ b := sorry

Main part:

theorem practice (n p : ℕ) (hn : n > 1) (hp : dvd p n → p*p >  n) : ¬ composite  n :=
begin
  intro h,
  rw composite_fact at h,
  cases h with p ha,
  cases ha with b hb,

  have hbleft: n = p*b, from and.left hb,
  have hbright: p ≤ b, from and.right hb,

  have hadn : dvd p n,

  rw dvd,
  use b,
  rw hbleft,

  replace hadn := hp hadn,

end

view this post on Zulip Reid Barton (Mar 17 2020 at 00:10):

This proof, and possibly statement, doesn't make sense

view this post on Zulip Kevin Buzzard (Mar 17 2020 at 00:10):

please can you post exactly one code block containing all imports and opens, so people can just cut and paste to see your problem.

view this post on Zulip Reid Barton (Mar 17 2020 at 00:11):

What are you trying to prove in English?

view this post on Zulip Debendro Mookerjee (Mar 17 2020 at 00:15):

(deleted)

view this post on Zulip Kevin Buzzard (Mar 17 2020 at 00:15):

but 1 is a factor of n

view this post on Zulip Kevin Buzzard (Mar 17 2020 at 00:16):

just because it's called p doesn't make it prime :-)

view this post on Zulip Reid Barton (Mar 17 2020 at 00:16):

It's not what your practice statement says anyways.

view this post on Zulip Kevin Buzzard (Mar 17 2020 at 00:16):

Unrelated: if you put ```lean at the top of where you quote your code, then it comes out in neat colours

view this post on Zulip Debendro Mookerjee (Mar 17 2020 at 00:37):

Wait really?

view this post on Zulip Debendro Mookerjee (Mar 17 2020 at 00:37):

theorem practice (n p : ) (hn : n > 1) (hp : dvd p n  p*p >  n) : ¬ composite  n :=
begin
  intro h,
  rw composite_fact at h,
  cases h with p ha,
  cases ha with b hb,

  have hbleft: n = p*b, from and.left hb,
  have hbright: p  b, from and.right hb,

  have hadn : dvd p n,

  rw dvd,
  use b,
  rw hbleft,

  replace hadn := hp hadn,

end

view this post on Zulip Debendro Mookerjee (Mar 17 2020 at 00:38):

Oh wow...

view this post on Zulip Kevin Buzzard (Mar 17 2020 at 00:52):

Your hypothesis hp says "if the fixed number pp you chose at the beginning divides nn, then also assume that p2>np^2>n. So for example practice 7 5 says "if 7>1, and if the statement 'if 5 divides 7 then 5^2>7' is true (which it is, because 5 doesn't divide 7) then 7 is not composite". In particular practice 7 5 is false so you can't prove practice in general. You need to learn to work basic logic before you can get to Hungerford.

view this post on Zulip jack (Mar 17 2020 at 08:50):

Hi there, I m stuck again :rolling_on_the_floor_laughing:

view this post on Zulip jack (Mar 17 2020 at 08:51):

theorem Equivalence1 (A B : Prop) :
(A  B)  (¬ A  B) :=
-- classical should be used
assume h,
--classical.by_contradiction $
--assume h1,
_

theorem Equivalence2 (A B : Prop) :
(¬ A  B)  (A  B) :=
assume h,
assume a,
_

view this post on Zulip jack (Mar 17 2020 at 08:52):

Maybe equivalence2 is simpler.

view this post on Zulip Johan Commelin (Mar 17 2020 at 08:53):

If you use

```lean
code goes here
```

for your codeblocks, you even get fancy colors (-;

view this post on Zulip jack (Mar 17 2020 at 08:54):

This is not the homework, but I would like to challenge myself.

view this post on Zulip jack (Mar 17 2020 at 08:55):

Still SO difficult ...

view this post on Zulip Johan Commelin (Mar 17 2020 at 08:56):

Hint: or.cases_on

view this post on Zulip jack (Mar 17 2020 at 08:58):

#check @or.cases_on seems similar to or.elim... actually I see no difference between them.

view this post on Zulip Marc Huisinga (Mar 17 2020 at 08:59):

it is!

for the first one, i'd try using (classical.em A).elim instead, maybe you had the law of excluded middle in class to motivate things like by_contradiction

view this post on Zulip jack (Mar 17 2020 at 09:01):

100% correct!

view this post on Zulip Marc Huisinga (Mar 17 2020 at 09:06):

(note that (classical.em A).elim is just or.elim (classical.em A), i should perhaps be careful with using notation that might not have been introduced yet)

view this post on Zulip jack (Mar 17 2020 at 09:12):

theorem Equivalence2 (A B : Prop) :
(¬ A  B)  (A  B) :=
assume h,
assume a,
or.cases_on h
(assume na ,
or.cases_on h (
assume na,
_
) $
assume b: B, b
) $ assume b : B, b

I m getting into a circle.

view this post on Zulip Johan Commelin (Mar 17 2020 at 09:13):

Hint: false.elim

view this post on Zulip Johan Commelin (Mar 17 2020 at 09:14):

You should remove the second block of or.cases_on h _ _

view this post on Zulip jack (Mar 17 2020 at 09:15):

#check @false.elim gives me Π {C : Sort u_1}, false → C. Is it pi-calculus?

view this post on Zulip Marc Huisinga (Mar 17 2020 at 09:15):

think about the proof you'd write on paper. you've got ¬ A ∨ B and A. in the first case, where you've got ¬ A, you've got a contradiction on your hands that allows you to get false, and thus prove anything (with false.elim).

view this post on Zulip Marc Huisinga (Mar 17 2020 at 09:16):

this is known as the principle of explosion, "from falsehood, anything follows"

view this post on Zulip Johan Commelin (Mar 17 2020 at 09:17):

jack said:

#check @false.elim gives me Π {C : Sort u_1}, false → C. Is it pi-calculus?

I don't know anything about calculus, but this is telling you that if you can find a contradiction (i.e., proof of false), then you can prove everything.

view this post on Zulip jack (Mar 17 2020 at 09:18):

OK got you. After adding a false.elim I 've got a A and \not A, then I can get a false \not A A. Cheers!

view this post on Zulip jack (Mar 17 2020 at 09:21):

My proves seems like this:

theorem Equivalence2 (A B : Prop) :
(¬ A  B)  (A  B) :=
assume h,
assume a,
or.cases_on h
(
assume na,
false.elim $
na a
) $ assume b : B, b

I'm wondering if I can use $ to remove the parentheses.

view this post on Zulip Kevin Buzzard (Mar 17 2020 at 09:22):

jack said:

#check @false.elim gives me Π {C : Sort u_1}, false → C. Is it pi-calculus?

Pi is the name of the types, lambda is the name of the terms. λ a, b has type Π A, B

view this post on Zulip jack (Mar 17 2020 at 09:22):

or.elim is a 3-parameter operator, where comes the problem.

view this post on Zulip Marc Huisinga (Mar 17 2020 at 09:22):

i don't think so, $ won't allow you to eliminate all parentheses, only the ones at the end. the proof looks good!

view this post on Zulip jack (Mar 17 2020 at 09:22):

Thank you @Kevin Buzzard

view this post on Zulip jack (Mar 17 2020 at 09:23):

Thanks to all of you :grinning_face_with_smiling_eyes: I have only 50% left.

view this post on Zulip Johan Commelin (Mar 17 2020 at 09:26):

@jack If you wanna golf: assume b : B, b is the same as id

view this post on Zulip Johan Commelin (Mar 17 2020 at 09:27):

theorem Equivalence2 (A B : Prop) :
(¬ A  B)  (A  B) :=
assume h a, h.cases_on (false.elim  absurd a) id

view this post on Zulip jack (Mar 17 2020 at 09:29):

Do you invent this language @Johan Commelin ? Or do you use it every day?

view this post on Zulip Johan Commelin (Mar 17 2020 at 09:30):

What do you mean?

view this post on Zulip Johan Commelin (Mar 17 2020 at 09:30):

I use Lean pretty much every day. But I usually don't write my proofs like this.

view this post on Zulip Johan Commelin (Mar 17 2020 at 09:30):

I prefer tactic mode.

view this post on Zulip jack (Mar 17 2020 at 09:31):

Maybe I'll learn to use it at the end of this semester.

view this post on Zulip jack (Mar 17 2020 at 09:34):

Could you please explain a little more? Never seen this in the class.

view this post on Zulip Johan Commelin (Mar 17 2020 at 09:35):

It is called "function composition"

view this post on Zulip Johan Commelin (Mar 17 2020 at 09:35):

f ∘ g = \lambda x, f (g x)

view this post on Zulip jack (Mar 17 2020 at 09:37):

Does it mean false.elim ∘ absurd a is the same as false.elim (absurd a)?

view this post on Zulip Johan Commelin (Mar 17 2020 at 09:37):

Nope

view this post on Zulip Johan Commelin (Mar 17 2020 at 09:38):

It's the same as assume blabla, false.elim (absurd a blabla)

view this post on Zulip jack (Mar 17 2020 at 09:41):

Amazing!

view this post on Zulip jack (Mar 17 2020 at 10:00):

h : A  B
 ¬A  B

May I have some hint please?

view this post on Zulip Kenny Lau (Mar 17 2020 at 10:01):

case on whether A is true or false

view this post on Zulip jack (Mar 17 2020 at 10:05):

Do you mean or.cases_on? Which only works with a ... \or ... but there isn't.

view this post on Zulip Kenny Lau (Mar 17 2020 at 10:13):

use classical.em

view this post on Zulip jack (Mar 17 2020 at 10:34):

theorem Equivalence1 (A B : Prop) :
(A  B)  (¬ A  B) :=
-- classical should be used
assume h,
have h1 : A  ¬ A, from classical.em A,
h1.cases_on
(assume a : A,
 or.intro_right _ $ h a
) $
 assume na : ¬ A,
 or.intro_left _ na

view this post on Zulip jack (Mar 17 2020 at 10:35):

Finally I made it :tada: There must be some fancy syntax which could simplify the prove.

view this post on Zulip jack (Mar 17 2020 at 10:35):

Thanks a lot @Kenny Lau

view this post on Zulip Kevin Buzzard (Mar 17 2020 at 11:48):

theorem Equivalence1 (A B : Prop) : (A  B)  (¬ A  B) :=
λ h, (classical.em A).elim (λ a, or.intro_right _ $ h a) $ or.intro_left _

view this post on Zulip Kevin Buzzard (Mar 17 2020 at 11:49):

Same proof but bundled up into a more compact form.

view this post on Zulip Kevin Buzzard (Mar 17 2020 at 11:51):

import tactic

run_cmd tactic.skip -- working around open_locale bug

open_locale classical

theorem Equivalence1 (A B : Prop) : (A  B)  (¬ A  B) :=
begin
  intro hAB,
  by_cases A,
  { right,
    apply hAB,
    assumption
  },
  { left,
    assumption
  }
end

Same proof but in tactic mode.

view this post on Zulip Anas Himmi (Mar 17 2020 at 11:54):

what does the $ sign mean?

view this post on Zulip jack (Mar 17 2020 at 12:31):

It means saving some paratheses, e.g. foo $ a b c <-> foo (a b c)

view this post on Zulip Kevin Buzzard (Mar 17 2020 at 12:44):

theorem Equivalence1 (A B : Prop) : (A  B)  (¬ A  B) :=
λ h, (classical.em A).elim (λ a, or.intro_right _ (h a)) (or.intro_left _)

$-free version

view this post on Zulip Anas Himmi (Mar 17 2020 at 13:04):

thank you!

view this post on Zulip Kevin Buzzard (Mar 17 2020 at 13:04):

@anas himmi you can work out what most things mean in Lean if you know how. For example, if you realise that $ is notation then #print notation $ is the next step. It tells you _ $:1 _:0 := #1 #0 which is a rather encrypted way of saying that f $ g means f g except that the binding power of $ is 1, which is very low.

view this post on Zulip Kevin Buzzard (Mar 17 2020 at 13:05):

This means that the composition happens last, saving you from having to write the brackets (which have super-high binding power). I wrote a blog post about binding power in Lean here.

view this post on Zulip Kevin Buzzard (Mar 17 2020 at 13:05):

You can compare with #print notation + and so on.

view this post on Zulip Anas Himmi (Mar 17 2020 at 13:06):

i tested it out before asking but didn't understand the notation. now i see it better


Last updated: May 10 2021 at 19:16 UTC