apply to hypothesis

Stream: new members

[Rick Love]

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]

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]

specialize

[Adam Topaz]

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

[Adam Topaz]

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

[Kenny Lau]

would help to include goal state

[Anatole Dedecker]

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]

use hpq and hp and hq

[Rick Love]

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]

and what do you want to apply to what hypothesis?

[Rick Love]

So I was trying to use gcd_pos_of_pos_left on a_1

[Rick Love]

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]

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

[Adam Topaz]

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

[Adam Topaz]

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

[Adam Topaz]

Unless I'm misunderstanding

[Adam Topaz]

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]

Wait, that's false, everything divides 0

[Rick Love]

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

[Adam Topaz]

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

[Adam Topaz]

(deleted)

[Adam Topaz]

(deleted)

[Rick Love]

yes, gcd of 0, n = 0 I believe

[Adam Topaz]

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

[Rick Love]

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]

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]

The gcd of 0 and n is n

[Adam Topaz]

Yeah it's the sum of the ideals

[Adam Topaz]

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

[Adam Topaz]

Anyway docs#nat.pos_of_ne_zero

[Adam Topaz]

Jeez, my brain is not working right now

[Rick Love]

Oh nice, I needed that earlier on another problem.

[Rick Love]

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]

Why not prove a \ne 0 next

[Rick Love]

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

[Kevin Buzzard]

You can't ignore cases

[Adam Topaz]

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

[Kevin Buzzard]

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]

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]

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

[Adam Topaz]

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]

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

[Mario Carneiro]

#backticks

[Mario Carneiro]

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

[Mario Carneiro]

you need a > 1

[Mario Carneiro]

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]

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]

#mwe, don't forget the imports

[Rick Love]

Nevermind, I did the wrong case

[Rick Love]

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

[Adam Topaz]

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]

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]

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

[Rick Love]

How does this work?

exact dec_trivial

[Mario Carneiro]

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]

That's some rcases voodoo too...

[Mario Carneiro]

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

[Rick Love]

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

[Mario Carneiro]

rcases is awesome

[Rick Love]

Yeah, cc works in this case

[Adam Topaz]

What's exactly going on with this rcases?

[Mario Carneiro]

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]

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

[Mario Carneiro]

because nat is an inductive type

[Mario Carneiro]

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]

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]

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

[Mario Carneiro]

oh you mean the goal is a contradiction

[Rick Love]

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

[Mario Carneiro]

the goal doesn't really matter

[Mario Carneiro]

because you are proving a contradiction in this case

[Mario Carneiro]

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

[Rick Love]

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

Ah, I see

[Mario Carneiro]

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

[Rick Love]

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]

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

[Mario Carneiro]

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

[Rick Love]

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

[Adam Topaz]

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

[Adam Topaz]

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

[Adam Topaz]

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

[Mario Carneiro]

@Rick Love those two cases look the same to me

[Mario Carneiro]

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

[Mario Carneiro]

that would be the theorems in data.nat.gcd

[Rick Love]

Adam Topaz said:

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]

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

[Rick Love]

Adam Topaz said:

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]

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

[Rick Love]

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

[Adam Topaz]

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

[Adam Topaz]

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

[Patrick Massot]

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]

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]

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]

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.