Selecting part of disjunction in a lemma

Stream: new members

[Ralf Stephan]

I tried selecting part of a disjunction with .1 in this code. The manuals describe the case if the goal is the disjunction but what if I need to match a disjunction that is the condition of a lemma?

import Mathlib
set_option autoImplicit false

lemma h {k p: ℚ} (hk: 0 < k): p ≥ k + 1 → p / (p - 1) ≤ (k + 1) / k := by
  intro hp
  conv at hk =>
    rw [ne_iff_lt_or_gt.mpr.1 hk]     -- <========
  rw [← one_add_div hk k 1]
  sorry

invalid field notation, type is not of the form (C ...) where C is a constant
  ne_iff_lt_or_gt.mpr
has type
  ?m.386 < ?m.387 ∨ ?m.386 > ?m.387 → ?m.386 ≠ ?m.387

I think the invalid field notation... means that it just can't find .1. My plan is to pick the left part of the disjunction to rewrite hk to k \ne 0, and then to use it to rewrite (k+1)/k to k/k + 1/k. Please help.

[Ralf Stephan]

Also, 0 < k as condition cannot be changed.

[Ruben Van de Velde]

So ne_iff_lt_or_gt.mpr has type ?m.61 < ?m.62 ∨ ?m.61 > ?m.62 → ?m.61 ≠ ?m.62. That is, it's an implication whose premise is an or. In English: if either a < b or b < a, a and b are not equal. That means you need to apply it to a value of type ?m.61 < ?m.62 ∨ ?m.61 > ?m.62. You can construct such a type either by giving a proof of the left hand side (Or.inl hk) or the right hand side (Or.inr hk), where l and r stand for left and right, respectively

[Ruben Van de Velde]

Now in either case , your conclusion is going to be an inequality, so you can't rewrite with it

[Ralf Stephan]

I meant I planned to use the (as 0 \ne k) rewritten hk to rewrite the right side of the goal (k + 1)/k to k/k + 1/k because ← one_add_div has 0 \ne k as condition. And by delegating to a sublemma that suddenly resolved. But no.

lemma h {k p: ℚ} (hk: 0 < k): p ≥ k + 1 → p / (p - 1) ≤ (k + 1) / k := by
  intro hp
  have hkk: 0 ≠ k := ne_iff_lt_or_gt.mpr (Or.inl hk)
  rw [← one_add_div hkk 1 k]

function expected at
  one_add_div ?m.493
term has type
  1 + ?m.435 / ?m.436 = (?m.436 + ?m.435) / ?m.436

But what does this error mean? I gave the needed condition hkk and what should be substituted for a and b in one_add_div.
It looks like I should much more write have with subgoals instead of immediate attempts to rewrite/apply because the glue mechanics is so delicate (and the error messages so ... hmm).

[Ruben Van de Velde]

function expected at means that you're passing more (explicit) arguments than one_add_div expects

[Ralf Stephan]

Many thanks. The final version will be in \R and look like this:

lemma H {k p: ℝ} (hk: k > 0): p ≥ k + 1 → p / (p - 1) ≤ (k + 1) / k := by
  have h_k_nonzero: k ≠ 0 := ne_iff_lt_or_gt.mpr (Or.inr hk)
  have h_p_gt_one: p > 1 := by sorry
  have h_p_ne_one: p - 1 ≠ 0 := by sorry
  have h₁: p / (p - 1) = 1 + 1 / (p - 1) := by
    rw [one_add_div h_p_ne_one, sub_add_cancel]
  rw [← one_add_div h_k_nonzero, h₁, add_le_add_iff_left,
    ge_iff_le, one_div_le_one_div, ← succ_le_succ_iff]
  sorry

When finished, this could be part of Ch.01, 4th proof of The Formal BOOK. It's a bit concerning that a big part of such formalizations have to deal with manipulations of simple conditions, like from k<0 to k \ne 0 or from p \ge k+1 to p > 1. Having something where one just states the conditions needed for all the rewrites and then invoking a tactic would substantially shrink proofs. Beginner's dreams.

[Daniel Weber]

If you're willing to use a stronger tactic then you can just intro; rw [div_le_div_iff] and then repeat linarith

[Ralf Stephan]

Can linarith somehow print what it finds, like simp? ?

[Daniel Weber]

No, as it doesn't work by directly looking for lemmas which can simplify the problem but by applying a linear programming algorithm. You can use set_option trace.linarith true to get more details, though

[Ruben Van de Velde]

It could apparently generate a linear_combination tactic call, but this needs some work