## Stream: new members

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

#### 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


#### 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


#### Kenny Lau (Aug 17 2020 at 12:45):

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

#### Rick Love (Aug 17 2020 at 13:32):

norm_num seems like something I need to use more

#### 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


#### 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?


#### 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


#### 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

#### 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.

#### Mario Carneiro (Aug 17 2020 at 15:33):

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

#### 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

#### Mario Carneiro (Aug 17 2020 at 15:38):

(never mind, I misread the statement)

#### Rick Love (Aug 17 2020 at 15:47):

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

cases g, linarith, linarith,


#### 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


#### Rick Love (Aug 17 2020 at 15:52):

Oh, I see. Thanks!

Last updated: May 10 2021 at 00:31 UTC