Zulip Chat Archive

Stream: new members

Topic: Goal g>0, h: g>1


view this post on Zulip Rick Love (Aug 17 2020 at 12:02):

Is there a simple way to apply a comparison that is more strict than the required goal:

invalid apply tactic, failed to unify
  g > 0
with
  g > 1

view this post on Zulip Ruben Van de Velde (Aug 17 2020 at 12:13):

Some options:

import data.real.basic

example (g : ) (h: g > 1) : g > 0 :=
by linarith

example (g : ) (h: g > 1) : g > 0 :=
begin
  transitivity (1 : ),
  exact h,
  norm_num
end

example (g : ) (h: g > 1) : g > 0 :=
calc g > 1 : h
... > 0 : by norm_num

view this post on Zulip Kenny Lau (Aug 17 2020 at 12:45):

apply has a strict meaning that isn't "use this fact somehow"

view this post on Zulip Rick Love (Aug 17 2020 at 13:32):

norm_num seems like something I need to use more

view this post on Zulip Kenny Lau (Aug 17 2020 at 13:40):

import data.real.basic

example (g : ) (h : 1 < g) : 0 < g := -- please use < and ≤ instead of > and ≥
lt_trans zero_lt_one h

view this post on Zulip Rick Love (Aug 17 2020 at 13:43):

Kenny Lau said:

import data.real.basic

example (g : ) (h : 1 < g) : 0 < g := -- please use < and ≤ instead of > and ≥
lt_trans zero_lt_one h
````
Yeah, I'm going to go through and make that consistent. Are they definitionally equivalent?

view this post on Zulip Ruben Van de Velde (Aug 17 2020 at 13:46):

This works, but should perhaps be avoided if you want a readable proof:

import data.real.basic

example (g : ) (h : g > 1) : g > 0 :=
lt_trans zero_lt_one h

view this post on Zulip Kenny Lau (Aug 17 2020 at 13:47):

Rick Love said:

Kenny Lau said:

import data.real.basic

example (g : ) (h : 1 < g) : 0 < g := -- please use < and ≤ instead of > and ≥
lt_trans zero_lt_one h

Yeah, I'm going to go through and make that consistent. Are they definitionally equivalent?

Yeah

view this post on Zulip Rick Love (Aug 17 2020 at 13:49):

Ruben Van de Velde said:

This works, but should perhaps be avoided if you want a readable proof:

import data.real.basic

example (g : ) (h : g > 1) : g > 0 :=
lt_trans zero_lt_one h

Right, I'm a software engineer so used to keeping my variables on the left and values on the right. I just have to form the habit.

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

Ah, but the key is to think of h as a variable too

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

that's the curry howard isomorphism in action, hypotheses are just like variables in a type because propositions are types

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

(never mind, I misread the statement)

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

To answer my own question (in the context of needing a tactic):

cases g, linarith, linarith,

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

linarith should be able to do this without the cases

example (g : ) (h : g > 1) : g > 0 :=
by linarith

view this post on Zulip Rick Love (Aug 17 2020 at 15:52):

Oh, I see. Thanks!


Last updated: May 10 2021 at 00:31 UTC