Zulip Chat Archive

Stream: new members

Topic: apply to hypothesis


view this post on Zulip 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).

view this post on Zulip 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.

view this post on Zulip Kenny Lau (Aug 15 2020 at 21:57):

specialize

view this post on Zulip Adam Topaz (Aug 15 2020 at 21:58):

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

view this post on Zulip Adam Topaz (Aug 15 2020 at 21:58):

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

view this post on Zulip Kenny Lau (Aug 15 2020 at 21:59):

would help to include goal state

view this post on Zulip 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)

view this post on Zulip Kenny Lau (Aug 15 2020 at 22:01):

use hpq and hp and hq

view this post on Zulip 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

view this post on Zulip Kenny Lau (Aug 15 2020 at 22:07):

and what do you want to apply to what hypothesis?

view this post on Zulip Rick Love (Aug 15 2020 at 22:08):

So I was trying to use gcd_pos_of_pos_left on a_1

view this post on Zulip 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

view this post on Zulip 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)

view this post on Zulip Adam Topaz (Aug 15 2020 at 22:12):

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

view this post on Zulip Adam Topaz (Aug 15 2020 at 22:12):

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

view this post on Zulip Adam Topaz (Aug 15 2020 at 22:12):

Unless I'm misunderstanding

view this post on Zulip 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

view this post on Zulip Adam Topaz (Aug 15 2020 at 22:15):

Wait, that's false, everything divides 0

view this post on Zulip 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.

view this post on Zulip Adam Topaz (Aug 15 2020 at 22:17):

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

view this post on Zulip Adam Topaz (Aug 15 2020 at 22:18):

(deleted)

view this post on Zulip Adam Topaz (Aug 15 2020 at 22:18):

(deleted)

view this post on Zulip Rick Love (Aug 15 2020 at 22:18):

yes, gcd of 0, n = 0 I believe

view this post on Zulip Adam Topaz (Aug 15 2020 at 22:19):

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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Reid Barton (Aug 15 2020 at 22:20):

The gcd of 0 and n is n

view this post on Zulip Adam Topaz (Aug 15 2020 at 22:20):

Yeah it's the sum of the ideals

view this post on Zulip Adam Topaz (Aug 15 2020 at 22:21):

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

view this post on Zulip Adam Topaz (Aug 15 2020 at 22:25):

Anyway docs#nat.pos_of_ne_zero

view this post on Zulip Adam Topaz (Aug 15 2020 at 22:26):

Jeez, my brain is not working right now

view this post on Zulip Rick Love (Aug 15 2020 at 22:30):

Oh nice, I needed that earlier on another problem.

view this post on Zulip 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?

view this post on Zulip Kevin Buzzard (Aug 15 2020 at 22:35):

Why not prove a \ne 0 next

view this post on Zulip 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?

view this post on Zulip Kevin Buzzard (Aug 15 2020 at 22:35):

You can't ignore cases

view this post on Zulip 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,

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip Mario Carneiro (Aug 15 2020 at 22:38):

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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Aug 15 2020 at 22:42):

#backticks

view this post on Zulip Mario Carneiro (Aug 15 2020 at 22:43):

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

view this post on Zulip Mario Carneiro (Aug 15 2020 at 22:43):

you need a > 1

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Aug 15 2020 at 22:46):

#mwe, don't forget the imports

view this post on Zulip Rick Love (Aug 15 2020 at 22:47):

Nevermind, I did the wrong case

view this post on Zulip Rick Love (Aug 15 2020 at 22:48):

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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Rick Love (Aug 15 2020 at 22:59):

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

view this post on Zulip Rick Love (Aug 15 2020 at 23:01):

How does this work?

exact dec_trivial

view this post on Zulip 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

view this post on Zulip Adam Topaz (Aug 15 2020 at 23:05):

That's some rcases voodoo too...

view this post on Zulip Mario Carneiro (Aug 15 2020 at 23:05):

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

view this post on Zulip Rick Love (Aug 15 2020 at 23:05):

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

view this post on Zulip Mario Carneiro (Aug 15 2020 at 23:05):

rcases is awesome

view this post on Zulip Rick Love (Aug 15 2020 at 23:05):

Yeah, cc works in this case

view this post on Zulip Adam Topaz (Aug 15 2020 at 23:07):

What's exactly going on with this rcases?

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Aug 15 2020 at 23:07):

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

view this post on Zulip Mario Carneiro (Aug 15 2020 at 23:07):

because nat is an inductive type

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Aug 15 2020 at 23:08):

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

view this post on Zulip Mario Carneiro (Aug 15 2020 at 23:09):

oh you mean the goal is a contradiction

view this post on Zulip Rick Love (Aug 15 2020 at 23:09):

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

view this post on Zulip Mario Carneiro (Aug 15 2020 at 23:09):

the goal doesn't really matter

view this post on Zulip Mario Carneiro (Aug 15 2020 at 23:09):

because you are proving a contradiction in this case

view this post on Zulip Mario Carneiro (Aug 15 2020 at 23:10):

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

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Aug 15 2020 at 23:11):

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

view this post on Zulip 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?

view this post on Zulip Mario Carneiro (Aug 15 2020 at 23:17):

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

view this post on Zulip Mario Carneiro (Aug 15 2020 at 23:17):

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

view this post on Zulip Rick Love (Aug 15 2020 at 23:19):

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

view this post on Zulip Adam Topaz (Aug 15 2020 at 23:25):

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

view this post on Zulip Adam Topaz (Aug 15 2020 at 23:32):

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

view this post on Zulip Adam Topaz (Aug 15 2020 at 23:33):

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

view this post on Zulip Mario Carneiro (Aug 15 2020 at 23:33):

@Rick Love those two cases look the same to me

view this post on Zulip Mario Carneiro (Aug 15 2020 at 23:34):

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

view this post on Zulip Mario Carneiro (Aug 15 2020 at 23:34):

that would be the theorems in data.nat.gcd

view this post on Zulip Rick Love (Aug 15 2020 at 23:46):

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

view this post on Zulip Adam Topaz (Aug 15 2020 at 23:47):

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

view this post on Zulip Rick Love (Aug 15 2020 at 23:47):

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?

view this post on Zulip 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:

view this post on Zulip Rick Love (Aug 15 2020 at 23:51):

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

view this post on Zulip 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.

view this post on Zulip Adam Topaz (Aug 15 2020 at 23:54):

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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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