## Stream: new members

### Topic: An example involving Ch.2 and NNG

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

#### Kenny Lau (Mar 16 2020 at 23:15):

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

#### Debendro Mookerjee (Mar 16 2020 at 23:22):

Thanks, it works now

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

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

#### Reid Barton (Mar 16 2020 at 23:44):

Or just use hp hadn directly wherever you need it

#### Reid Barton (Mar 16 2020 at 23:45):

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

#### 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
term
has type
dvd a n
but is expected to have type
dvd p n


Ah, well, yeah

#### Reid Barton (Mar 16 2020 at 23:58):

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

#### Debendro Mookerjee (Mar 17 2020 at 00:02):

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

type mismatch at application
term
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


#### Debendro Mookerjee (Mar 17 2020 at 00:03):

So what is dedup and how is it used?

#### Kenny Lau (Mar 17 2020 at 00:03):

It means you have two variables with the same name p

#### Reid Barton (Mar 17 2020 at 00:04):

You've done something wrong earlier.

#### Debendro Mookerjee (Mar 17 2020 at 00:04):

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

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

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

end


#### Reid Barton (Mar 17 2020 at 00:10):

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

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

#### Reid Barton (Mar 17 2020 at 00:11):

What are you trying to prove in English?

(deleted)

#### Kevin Buzzard (Mar 17 2020 at 00:15):

but 1 is a factor of n

#### Kevin Buzzard (Mar 17 2020 at 00:16):

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

#### Reid Barton (Mar 17 2020 at 00:16):

It's not what your practice statement says anyways.

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

Wait really?

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

end


Oh wow...

#### Kevin Buzzard (Mar 17 2020 at 00:52):

Your hypothesis hp says "if the fixed number $p$ you chose at the beginning divides $n$, then also assume that $p^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.

#### jack (Mar 17 2020 at 08:50):

Hi there, I m stuck again :rolling_on_the_floor_laughing:

#### jack (Mar 17 2020 at 08:51):

theorem Equivalence1 (A B : Prop) :
(A → B) → (¬ A ∨ B) :=
-- classical should be used
assume h,
assume b: B, b
) $assume b : B, b  I m getting into a circle. #### Johan Commelin (Mar 17 2020 at 09:13): Hint: false.elim #### Johan Commelin (Mar 17 2020 at 09:14): You should remove the second block of or.cases_on h _ _ #### jack (Mar 17 2020 at 09:15): #check @false.elim gives me Π {C : Sort u_1}, false → C. Is it pi-calculus? #### 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). #### Marc Huisinga (Mar 17 2020 at 09:16): this is known as the principle of explosion, "from falsehood, anything follows" #### 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. #### 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! #### 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.

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

#### jack (Mar 17 2020 at 09:22):

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

thank you!

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

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

#### Kevin Buzzard (Mar 17 2020 at 13:05):

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

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