## Stream: new members

### Topic: apply to hypothesis

#### Rick Love (Aug 15 2020 at 21:50):

How do you apply to an hypothesis.

I know how to rewrite, etc. But I can't figure out how to work with a hypothesis (especially when using contradiction when the goal is false).

#### Adam Topaz (Aug 15 2020 at 21:56):

I'm not really sure what you're trying to do, but, from a logical point of view, you can't use the tactic apply on a hypothesis.

#### Kenny Lau (Aug 15 2020 at 21:57):

specialize

#### Adam Topaz (Aug 15 2020 at 21:58):

Yeah, that's probably what you're trying to do.

#### Adam Topaz (Aug 15 2020 at 21:58):

That will replace (i.e. specialize) some variables in the hypothesis with specific values.

#### Kenny Lau (Aug 15 2020 at 21:59):

would help to include goal state

#### Anatole Dedecker (Aug 15 2020 at 22:00):

Or maybe you want to go the other way around : if hpq : p -> q and hp : p you can get hq : q just by writing have hq := hpq hp ("applying" hpq to hp)

#### Kenny Lau (Aug 15 2020 at 22:01):

use hpq and hp and hq

#### Rick Love (Aug 15 2020 at 22:05):

Here is what I am working on:

theorem gcd_then_not_one_left_01 (a b : ℕ):
gcd a b > 1 ->
a > 1 :=
begin
intros,
generalize hgcd : gcd a b = g,
by_contra hcont,
push_neg at hcont,
cases g with g,
{
revert a_1,
rw hgcd,
simp,
},

-- Probably need to use one of:
-- eq_zero_of_gcd_eq_zero_left
-- gcd_pos_of_pos_left

sorry,
end


image.png

#### Kenny Lau (Aug 15 2020 at 22:07):

and what do you want to apply to what hypothesis?

#### Rick Love (Aug 15 2020 at 22:08):

So I was trying to use gcd_pos_of_pos_left on a_1

#### Rick Love (Aug 15 2020 at 22:09):

theorem gcd_pos_of_pos_left {m : ℕ} (n : ℕ) (mpos : 0 < m) : 0 < gcd m n :=
pos_of_dvd_of_pos (gcd_dvd_left m n) mpos


#### Rick Love (Aug 15 2020 at 22:10):

It's not exactly the same (but I can figure out how to adjust the 1 to the 0)

#### Adam Topaz (Aug 15 2020 at 22:12):

You can't deduce p from a proof of q and a proof of p -> q.

#### Adam Topaz (Aug 15 2020 at 22:12):

It sounds like that's what you're trying to do

#### Adam Topaz (Aug 15 2020 at 22:12):

Unless I'm misunderstanding

#### Adam Topaz (Aug 15 2020 at 22:15):

For the lemma you're trying to prove, I would use the fact that gcd(a,b) divides a, and the fact that, for two natural numbers m and n, if m is positive and n divides n then n is positive

#### Adam Topaz (Aug 15 2020 at 22:15):

Wait, that's false, everything divides 0

#### Rick Love (Aug 15 2020 at 22:17):

Well, I can deal with the gcd 0,0 = 0 case. I'm having trouble with the rest of it.

#### Adam Topaz (Aug 15 2020 at 22:17):

How is gcd defined? What's the gcd of 0 and 1?

(deleted)

(deleted)

#### Rick Love (Aug 15 2020 at 22:18):

yes, gcd of 0, n = 0 I believe

#### Adam Topaz (Aug 15 2020 at 22:19):

Ok, then use the fact that the gcd of a and b divides a*b

#### Rick Love (Aug 15 2020 at 22:19):

There is also these:

theorem eq_zero_of_gcd_eq_zero_left {m n : ℕ} (H : gcd m n = 0) : m = 0 :=
or.elim (eq_zero_or_pos m) id
(assume H1 : 0 < m, absurd (eq.symm H) (ne_of_lt (gcd_pos_of_pos_left _ H1)))

theorem eq_zero_of_gcd_eq_zero_right {m n : ℕ} (H : gcd m n = 0) : n = 0 :=
by rw gcd_comm at H; exact eq_zero_of_gcd_eq_zero_left H


#### Adam Topaz (Aug 15 2020 at 22:20):

Oh then it's easy, there should be a lemma saying that a natural is positive if and only if it's not 0

#### Reid Barton (Aug 15 2020 at 22:20):

The gcd of 0 and n is n

#### Adam Topaz (Aug 15 2020 at 22:20):

Yeah it's the sum of the ideals

#### Adam Topaz (Aug 15 2020 at 22:21):

I can't think of these things without thinking of ideals in Z

#### Adam Topaz (Aug 15 2020 at 22:25):

Anyway docs#nat.pos_of_ne_zero

#### Adam Topaz (Aug 15 2020 at 22:26):

Jeez, my brain is not working right now

#### Rick Love (Aug 15 2020 at 22:30):

Oh nice, I needed that earlier on another problem.

#### Rick Love (Aug 15 2020 at 22:34):

Ok, so this is another problem I have. I have a hyp: hcont : a ≤ 1

But I only care about the a = 1 case in order to reach my goal. The a=0 case is a contradiction. So how do I assume a = 1 and ignore the other case?

#### Kevin Buzzard (Aug 15 2020 at 22:35):

Why not prove a \ne 0 next

#### Rick Love (Aug 15 2020 at 22:35):

i.e. in general how do I ignore cases that are contradictions, but continue on cases that proceed to the goal?

#### Kevin Buzzard (Aug 15 2020 at 22:35):

You can't ignore cases

#### Adam Topaz (Aug 15 2020 at 22:35):

I don't know, but you can just start the proof by applying nat.pos_of_ne_zero,

#### Kevin Buzzard (Aug 15 2020 at 22:36):

It's your job to prove the contradictions, not just assert that they're contradictions so you don't have to deal with them

#### Rick Love (Aug 15 2020 at 22:38):

Ok, so how would you set up cases so that one branch ends with a contradiction (proving that the case is invalid), but the other case is successful?

#### Mario Carneiro (Aug 15 2020 at 22:38):

Assuming you prove a contradiction, the contradiction tactic will close the goal

#### Adam Topaz (Aug 15 2020 at 22:38):

If you start by applying nat.pos_of_ne_zero, that reduces to proving the gcd is nonzero, then use contradiction and one of the lemmas above to contradict the fact that a is nonzero

#### Rick Love (Aug 15 2020 at 22:42):

Well, it won't directly:

invalid apply tactic, failed to unify
a > 1
with
?m_1 > 0
state:
a b : ℕ,
a_1 : a.gcd b > 1
⊢ a > 1


#backticks

#### Mario Carneiro (Aug 15 2020 at 22:43):

the message says that you tried to apply something that proves ? > 0

#### Mario Carneiro (Aug 15 2020 at 22:43):

you need a > 1

#### Mario Carneiro (Aug 15 2020 at 22:45):

I suppose you did what adam said and applied nat.pos_of_ne_zero. That will prove a > 0 from a != 0, but what you need is a > 1

#### Rick Love (Aug 15 2020 at 22:46):

But even then:

theorem gcd_then_not_one_left_02 (a b : ℕ):
gcd a b > 1 ->
a > 1 :=
begin
intros,
cases le_or_gt a 1 with a,{
apply nat.pos_of_ne_zero,
},
end

invalid apply tactic, failed to unify
a > 1
with
?m_1 > 0
state:
case or.inl
a b : ℕ,
a_1 : a.gcd b > 1,
a : a ≤ 1
⊢ a > 1


#### Mario Carneiro (Aug 15 2020 at 22:46):

#mwe, don't forget the imports

#### Rick Love (Aug 15 2020 at 22:47):

Nevermind, I did the wrong case

#### Rick Love (Aug 15 2020 at 22:48):

Ok, so I can create a new hypothesis, but my goal is unchanged...

#### Adam Topaz (Aug 15 2020 at 22:50):

Oh sorry, I misread your original lemma. But once you prove that a is nonzero, you can use divisibility by the gcd to prove that it's >1

#### Mario Carneiro (Aug 15 2020 at 22:56):

Here's an easy set up:

import data.nat.gcd
open nat

theorem gcd_then_not_one_left_02 (a b : ℕ) (h : gcd a b > 1) : a > 1 :=
begin
rcases a with _|_|a,
{ -- a is zero, prove a contradiction
sorry },
{ -- a is one, interesting case
sorry },
{ exact dec_trivial } -- a + 2 > 1
end


#### Rick Love (Aug 15 2020 at 22:59):

Thanks! That's helpful. My main goal is to learn helpful patterns.

#### Rick Love (Aug 15 2020 at 23:01):

How does this work?

exact dec_trivial


#### Mario Carneiro (Aug 15 2020 at 23:03):

Lean knows a decision procedure for natural number less than (among many other things), and this procedure can determine that a + 2 > 1 is true before evaluating a, so it is true for all a. This technique only works in limited circumstances but it's nice when it works

#### Adam Topaz (Aug 15 2020 at 23:05):

That's some rcases voodoo too...

#### Mario Carneiro (Aug 15 2020 at 23:05):

Perhaps a more useful way to close that last case is { simp [succ_eq_add_one] }

#### Rick Love (Aug 15 2020 at 23:05):

Ok, I usually try: simp, cc, ring which sometimes work

#### Mario Carneiro (Aug 15 2020 at 23:05):

rcases is awesome

#### Rick Love (Aug 15 2020 at 23:05):

Yeah, cc works in this case

#### Adam Topaz (Aug 15 2020 at 23:07):

What's exactly going on with this rcases?

#### Mario Carneiro (Aug 15 2020 at 23:07):

it's best to use tactics only when you know why they work though; the strategy of trying everything that works runs out of steam once you get to larger scale

#### Mario Carneiro (Aug 15 2020 at 23:07):

The rcases splits the nat into three cases, 0,1,a+2

#### Mario Carneiro (Aug 15 2020 at 23:07):

because nat is an inductive type

#### Mario Carneiro (Aug 15 2020 at 23:08):

that's the easiest way to handle this sort of argument where you want to say that a = 0 or a = 1 or a > 1

#### Rick Love (Aug 15 2020 at 23:08):

Ok, so I'm still trying to figure out the contradiction:

So the first case is a clear contradiction in the goal:

        -- a is zero, prove a contradiction
b : ℕ,
h : 0.gcd b > 1
⊢ 0 > 1


#### Mario Carneiro (Aug 15 2020 at 23:08):

it's not clear to me. why is it clear to you?

#### Mario Carneiro (Aug 15 2020 at 23:09):

oh you mean the goal is a contradiction

#### Rick Love (Aug 15 2020 at 23:09):

Well I mean 0 > 1 is not true... oh so is this just false

#### Mario Carneiro (Aug 15 2020 at 23:09):

the goal doesn't really matter

#### Mario Carneiro (Aug 15 2020 at 23:09):

because you are proving a contradiction in this case

#### Mario Carneiro (Aug 15 2020 at 23:10):

the question is why 0.gcd b > 1 is false

#### Rick Love (Aug 15 2020 at 23:10):

Ok, so it would be the same if I started with exfalso to get rid of that.

Ah, I see

#### Mario Carneiro (Aug 15 2020 at 23:11):

you can use exfalso if it helps cognitively, but it's usually not needed

#### Rick Love (Aug 15 2020 at 23:13):

Yeah, I'm still fuzzy on how to fulfill the false goal. Usually I try to create contradictory hypothesis and revert them and then use 'simp' and that sometimes works.

What is the correct way to complete it?

#### Mario Carneiro (Aug 15 2020 at 23:17):

I would first try to figure out what gcd 0 b is

#### Mario Carneiro (Aug 15 2020 at 23:17):

that seems like the sort of thing that would have a simp lemma

#### Rick Love (Aug 15 2020 at 23:19):

Well, I think it has two cases: gcd 0 0 = 0, gcd 0 d = d,

#### Adam Topaz (Aug 15 2020 at 23:25):

Your lemma is false. gcd 0 10 > 1 but 0 is not > 1.

#### Adam Topaz (Aug 15 2020 at 23:32):

You can prove that gcd a b > 1 implies that a>1 or b>1

#### Adam Topaz (Aug 15 2020 at 23:33):

Or you can add an assumption that a is nonzero to begin with.

#### Mario Carneiro (Aug 15 2020 at 23:33):

@Rick Love those two cases look the same to me

#### Mario Carneiro (Aug 15 2020 at 23:34):

Don't look at the definition of gcd, look at the API

#### Mario Carneiro (Aug 15 2020 at 23:34):

that would be the theorems in data.nat.gcd

#### Rick Love (Aug 15 2020 at 23:46):

Your lemma is false. gcd 0 10 > 1 but 0 is not > 1.

Good catch. I tried working with nat+, but it seems akward so I keep forgetting to include the assumptions

#### Adam Topaz (Aug 15 2020 at 23:47):

pnat are the "actual" natural numbers anyway. (I can already feel the angry responses.)

#### Rick Love (Aug 15 2020 at 23:47):

Or you can add an assumption that a is nonzero to begin with.

What is the best way to write an assumption?

I just put a > 1 -> b > 1 -> ... at the beginning usually, but is there a better way?

#### Adam Topaz (Aug 15 2020 at 23:49):

Use something like Mario wrote, adding the hypotheses before the colon. But make it >0 :smiling_face:

#### Rick Love (Aug 15 2020 at 23:51):

Ah, I see so each assumption would get it's own (hn:...)

#### Adam Topaz (Aug 15 2020 at 23:53):

Note that if you used pnats instead of Nats, Mario's rcases trick probably would not work as is.

#### Adam Topaz (Aug 15 2020 at 23:54):

But if you add in the hypotheses on the nats, it should be ok.

#### Patrick Massot (Aug 15 2020 at 23:59):

Rick, did you try to do the Lean tutorial or read Mathematics in Lean? I looks like you still have some basic stuff to learn.

#### Rick Love (Aug 16 2020 at 00:37):

Patrick Massot said:

Rick, did you try to do the Lean tutorial or read Mathematics in Lean? I looks like you still have some basic stuff to learn.

Yeah, I've read alot and done some tutorials, but there is a difference between a spoonfed walkthrough and actually trying to create your own objectives and learning which patterns are actually useful.

#### Rick Love (Aug 16 2020 at 00:38):

But haven't done those tutorials, so I'll work on those also since I can see they go beyond the other resources and I'll probably retain more than Mathematics in Lean

#### Rick Love (Aug 16 2020 at 00:44):

Thanks @Patrick Massot after getting the tutorial repo and scanning through the exercises, I can see there are many things covered that I have questions about.

Last updated: May 13 2021 at 21:12 UTC