An example involving Ch.2 and NNG

Stream: new members

[Debendro Mookerjee]

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]

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

[Debendro Mookerjee]

Thanks, it works now

[Debendro Mookerjee]

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]

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]

Or just use hp hadn directly wherever you need it

[Reid Barton]

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

[Debendro Mookerjee]

@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

[Reid Barton]

Ah, well, yeah

[Reid Barton]

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

[Debendro Mookerjee]

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

[Debendro Mookerjee]

So what is dedup and how is it used?

[Kenny Lau]

It means you have two variables with the same name p

[Reid Barton]

You've done something wrong earlier.

[Debendro Mookerjee]

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

[Bryan Gin-ge Chen]

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

[Debendro Mookerjee]

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

[Reid Barton]

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

[Kevin Buzzard]

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]

What are you trying to prove in English?

[Debendro Mookerjee]

(deleted)

[Kevin Buzzard]

but 1 is a factor of n

[Kevin Buzzard]

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

[Reid Barton]

It's not what your practice statement says anyways.

[Kevin Buzzard]

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

[Debendro Mookerjee]

Wait really?

[Debendro Mookerjee]

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

[Debendro Mookerjee]

Oh wow...

[Kevin Buzzard]

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]

Hi there, I m stuck again :rolling_on_the_floor_laughing:

[jack]

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

[jack]

Maybe equivalence2 is simpler.

[Johan Commelin]

If you use

```lean
code goes here
```

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

[jack]

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

[jack]

Still SO difficult ...

[Johan Commelin]

Hint: or.cases_on

[jack]

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

[Marc Huisinga]

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

[jack]

100% correct!

[Marc Huisinga]

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

[jack]

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.

[Johan Commelin]

Hint: false.elim

[Johan Commelin]

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

[jack]

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

[Marc Huisinga]

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]

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

[Johan Commelin]

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]

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]

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]

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]

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

[Marc Huisinga]

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

[jack]

Thank you @Kevin Buzzard

[jack]

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

[Johan Commelin]

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

[Johan Commelin]

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

[jack]

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

[Johan Commelin]

What do you mean?

[Johan Commelin]

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

[Johan Commelin]

I prefer tactic mode.

[jack]

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

[jack]

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

[Johan Commelin]

It is called "function composition"

[Johan Commelin]

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

[jack]

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

[Johan Commelin]

Nope

[Johan Commelin]

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

[jack]

Amazing!

[jack]

h : A → B
⊢ ¬A ∨ B

May I have some hint please?

[Kenny Lau]

case on whether A is true or false

[jack]

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

[Kenny Lau]

use classical.em

[jack]

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

[jack]

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

[jack]

Thanks a lot @Kenny Lau

[Kevin Buzzard]

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

[Kevin Buzzard]

Same proof but bundled up into a more compact form.

[Kevin Buzzard]

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.

[Anas Himmi]

what does the $ sign mean?

[jack]

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

[Kevin Buzzard]

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

[Anas Himmi]

thank you!

[Kevin Buzzard]

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

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]

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

[Anas Himmi]

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