Zulip Chat Archive

Stream: new members

Topic: How to apply eq_or_lt_of_le on a hypothesis


Shadman Sakib (Jun 08 2021 at 01:43):

import data.real.basic
import algebra.group.pi

set_option pp.beta true

def non_decreasing (f :   ) :=  x₁ x₂, x₁  x₂  f x₁  f x₂

def non_increasing (f :   ) :=  x₁ x₂, x₁  x₂  f x₁  f x₂

example (f :   ) : (non_decreasing f)   x y, x < y  f x  f y :=
begin
  split,
  intros hf x₁ x₂ h,
  apply hf,
  exact le_of_lt h,

  intros h x₁ y₁ hf,
  apply eq_or_lt_of_le at hf,

end

Shadman Sakib (Jun 08 2021 at 01:44):

I want to use the eq_or_lt_of_le term to rewrite my hypothesis x \le y as x = y or x < y, but I can't

Shadman Sakib (Jun 08 2021 at 01:49):

Is there a way to do this?

Adam Topaz (Jun 08 2021 at 01:50):

your code is not working for me. Are those all the imports?

Shadman Sakib (Jun 08 2021 at 01:52):

Sorry forgot the defs

Adam Topaz (Jun 08 2021 at 01:53):

import data.real.basic
import algebra.group.pi

set_option pp.beta true

def non_decreasing (f :   ) :=  x₁ x₂, x₁  x₂  f x₁  f x₂

def non_increasing (f :   ) :=  x₁ x₂, x₁  x₂  f x₁  f x₂

example (f :   ) : (non_decreasing f)   x y, x < y  f x  f y :=
begin
  split,
  intros hf x₁ x₂ h,
  apply hf,
  exact le_of_lt h,

  intros h x₁ y₁ hf,
  replace hf := eq_or_lt_of_le hf,

end

Shadman Sakib (Jun 08 2021 at 01:54):

Thanks!

Shadman Sakib (Jun 08 2021 at 01:54):

Now is there a way to split hf?

Adam Topaz (Jun 08 2021 at 01:54):

cases hf

Shadman Sakib (Jun 08 2021 at 01:54):

or is that through cases

Shadman Sakib (Jun 08 2021 at 01:54):

yeah

Shadman Sakib (Jun 08 2021 at 01:55):

okay thanks

Shadman Sakib (Jun 08 2021 at 01:55):

very trivial questions

Adam Topaz (Jun 08 2021 at 01:55):

It's good practice to use { .. } to break up your goals. Something like this:

import data.real.basic
import algebra.group.pi

set_option pp.beta true

def non_decreasing (f :   ) :=  x₁ x₂, x₁  x₂  f x₁  f x₂

def non_increasing (f :   ) :=  x₁ x₂, x₁  x₂  f x₁  f x₂

example (f :   ) : (non_decreasing f)   x y, x < y  f x  f y :=
begin
  split,
  { intros hf x₁ x₂ h,
    apply hf,
    exact le_of_lt h },
  { intros h x₁ y₁ hf,
    replace hf := eq_or_lt_of_le hf,
    sorry,
  }
end

Shadman Sakib (Jun 08 2021 at 01:57):

Okay

Shadman Sakib (Jun 08 2021 at 01:57):

Helps with organization

Shadman Sakib (Jun 08 2021 at 02:00):

General question: How come sorry makes it so that I don't have to prove x_1 = y_1 implies my goal? I only had to prove the x_1 < y_1 case

Adam Topaz (Jun 08 2021 at 02:01):

I'm not sure what you mean... sorry is just a placeholder for a proof that should be filled in later.

Bryan Gin-ge Chen (Jun 08 2021 at 02:02):

You haven't proved it until you've removed all the sorrys!

Adam Topaz (Jun 08 2021 at 02:02):

I think what must have happened is that you did cases hf which gives you two separate goals, and the sorry killed the first goal, and only the second goal was left.

Shadman Sakib (Jun 08 2021 at 02:03):

Ahh I see

Adam Topaz (Jun 08 2021 at 02:04):

again, it's good practice to introduce { ... } immediately after the cases hf since you created new goals.

Adam Topaz (Jun 08 2021 at 02:04):

example (f :   ) : (non_decreasing f)   x y, x < y  f x  f y :=
begin
  split,
  { intros hf x₁ x₂ h,
    apply hf,
    exact le_of_lt h },
  { intros h x₁ y₁ hf,
    replace hf := eq_or_lt_of_le hf,
    cases hf,
    { sorry },
    { sorry } }
end

Adam Topaz (Jun 08 2021 at 02:05):

So now the two sorry's are just placeholders for proofs that you still need to finish. And as you can see, there are two separate goals that need to be finished.

Shadman Sakib (Jun 08 2021 at 02:09):

Yeah, I see both now, thank you!


Last updated: Dec 20 2023 at 11:08 UTC