Zulip Chat Archive

Stream: new members

Topic: stuck


Shadman Sakib (Jun 13 2021 at 20:57):

import data.real.basic

def fn_ub (f :   ) (a : ) : Prop :=  x, f x  a
def fn_lb (f :   ) (a : ) : Prop :=  x, a  f x

def fn_has_ub (f :   ) :=  a, fn_ub f a
def fn_has_lb (f :   ) :=  a, fn_lb f a

variable f :   

example : ¬ fn_has_ub (λ x, x) :=
begin
  intros fnub,
  cases fnub with a fnuba,
  unfold fn_ub at fnuba,

end

Shadman Sakib (Jun 13 2021 at 20:58):

I'm not sure how to affirm the x as a variable, since it is within a universal statement

Yakov Pechersky (Jun 13 2021 at 21:03):

specialize fnuba (a + 1)

Kevin Buzzard (Jun 13 2021 at 21:56):

The term fnuba is a term of type "for all..." so it is literally a function (which takes a number as input, and outputs a proof!). You could also do have h := fnuba (a+1).

Shadman Sakib (Jun 14 2021 at 20:11):

import data.real.basic

-- BEGIN
theorem not_monotone_iff {f :   }:
  ¬ monotone f   x y, x  y  f x > f y :=
by { rw monotone, push_neg }

example : ¬ monotone (λ x : , -x) :=
begin
  rw monotone,
  intros hab,

end
-- END

Shadman Sakib (Jun 14 2021 at 20:11):

How do I introduce a new hypothesis that says a <= b -> -b <= a

Shadman Sakib (Jun 14 2021 at 20:11):

Since a and b are not introduced

Heather Macbeth (Jun 14 2021 at 20:13):

Do you know a counterexample, that would disprove this? (That is, with actual numbers, like a = 7 and b = 17, or something.)

Heather Macbeth (Jun 14 2021 at 20:13):

Try finding the counterexample on paper and then applying hab to that counterexample.

Patrick Massot (Jun 14 2021 at 20:15):

Maybe Shadman is confused by the implicit binders

Patrick Massot (Jun 14 2021 at 20:17):

You can state something like

have key : (1 : )  2,
sorry,

and then specialize hab key (there is a faster way of course, but this should be clearer)

Shadman Sakib (Jun 14 2021 at 20:25):

Thank you! It worked.

Shadman Sakib (Jun 14 2021 at 20:26):

Another question when dealing with partial orders, I want to apply two hypotheses with exact to show the goal but I am not sure how.

Shadman Sakib (Jun 14 2021 at 20:26):

import tactic

-- BEGIN
variables {α : Type*} [partial_order α]
variables a b : α

example : a < b  a  b  a  b :=
begin
  rw lt_iff_le_not_le,
  split,
  { rintros h₀, h₁⟩,
    split,
    { exact h₀,},
    {
      sorry,
    }
  },
  {
    sorry,
  }
end
-- END

Heather Macbeth (Jun 14 2021 at 20:27):

There are two unproved pieces here -- which part are you asking for help on?

Heather Macbeth (Jun 14 2021 at 20:31):

You might like to read the instructions at the following link: #mwe which will help you ask more focused questions. For example, here you could have asked instead how to prove:

import tactic

-- BEGIN
variables {α : Type*} [partial_order α]
variables a b : α

example (h₀ : a  b) (h₁ : ¬b  a) :
  a  b :=
begin
  sorry
end

(which is the goal state after all the work you show towards the first sorry).

Shadman Sakib (Jun 14 2021 at 20:31):

The first sorry

Heather Macbeth (Jun 14 2021 at 20:33):

OK! So, you need to prove that ¬b ≤ a implies a ≠ b. Do you know how to prove its contrapositive, that a = b implies b ≤ a?

Shadman Sakib (Jun 14 2021 at 20:36):

Ahh yes we would use rw after contraposing h\1.

Shadman Sakib (Jun 14 2021 at 20:36):

More than one way to do it, Thank you!


Last updated: Dec 20 2023 at 11:08 UTC