Goal g>0, h: g>1

Stream: new members

[Rick Love]

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

[Ruben Van de Velde]

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

[Kenny Lau]

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

[Rick Love]

norm_num seems like something I need to use more

[Kenny Lau]

import data.real.basic

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

[Rick Love]

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?

[Ruben Van de Velde]

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

[Kenny Lau]

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

[Rick Love]

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.

[Mario Carneiro]

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

[Mario Carneiro]

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

[Mario Carneiro]

(never mind, I misread the statement)

[Rick Love]

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

cases g, linarith, linarith,

[Mario Carneiro]

linarith should be able to do this without the cases

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

[Rick Love]

Oh, I see. Thanks!