help naming?

Stream: Is there code for X?

[Scott Morrison]

Can someone suggest a name for this mouthful:

theorem foo [LinearOrder α] {a b c : α} (w : min a b = c) (h : c < a) : b = c := by
  rw [min_eq_iff] at w
  rcases w with ⟨rfl, -⟩ | ⟨rfl, -⟩
  · exfalso; apply lt_irrefl a; exact h
  · rfl

(Or what the canonical proof is?)

To #xy, I have some fact of the form w : min a b = c, and would like to "upgrade" it to b = c, by creating a side-goal c < a that I plan on dispatching before continuing on with the new fact.

[Yaël Dillies]

I would instead prove

lemma min_lt_left [LinearOrder α] {a b : α} : min a b < a ↔ b < a := by simp

[Scott Morrison]

I'm not sure how I would then use that in my #xy.

[Yaël Dillies]

Here's a Lean 3 demo (because that's what I have open

variables {α : Type*} [linear_order α] {a b c : α}

lemma min_lt_left : min a b < a ↔ b < a := by simp

example (hc : min a b = c) : true :=
begin
  rw [min_eq_right] at hc,
  swap,
  refine (min_lt_left.1 _).le,
  rw hc,
  sorry,
  /-
  α:  Type u_1
  _inst_1 : linear_order α
  a b c : α
  hc : min a b = c
  ⊢ c < a
  -/
  sorry,
  /-
  α : Type u_1
  _inst_1 : linear_order α
  a b c : α
  hc : b = c
  ⊢ true
  -/
end

[Yaël Dillies]

If you don't mind the slight obfuscation, you can get it down to one-line:

example (hc : min a b = c) : true :=
begin
  rw min_eq_right (min_lt_left.1 $ hc.trans_lt _).le at hc,
  sorry,
  sorry,
end

... except for the fact that rw won't rewrite hc with a term containing itself. Has that changed in Lean 4?

[Scott Morrison]

Hmm, that seems like a lot of rw and refine compared to what I want:

theorem foo [LinearOrder α] {a b c : α} (w : min a b = c) (h : c < a) : b = c := by
  rw [min_eq_iff] at w
  rcases w with ⟨rfl, -⟩ | ⟨rfl, -⟩
  · exfalso; apply lt_irrefl a; exact h
  · rfl

example [LinearOrder α] {a b c : α} (w : min a b = c) : b = c := by
  replace w := foo w ?_
  -- Now I can use the stronger result
  exact w
  -- But I have to prove the inequality at some point:
  · guard_target = c < a
    sorry

[Yaël Dillies]

Maybe, but I don't think we want your lemma in mathlib. There's a reason why we never have lemmas that assume an equality with one side being a free variable.

[Scott Morrison]

What is that reason?

[Eric Wieser]

Usually, because the caller could just rw by it first

[Eric Wieser]

An example of a lemma that mathlib wouldn't have ismul_distrib_of_eq_add (a b c ab) (hab : a + b = ab) : ab * c = a * c + b * c, because the caller should just rw hab first.

[Eric Wieser]

The exceptions to the rule are usually congr lemmas or places where dependent types make that rw unpleasant

[Yaël Dillies]

... and lemmas used by tactics (eg norm_num)

[Yaël Dillies]

If we included your particular lemma, then we would also have to include many more for completeness. And I don't think the following is so offputting (my first version was pedagogical, not optimal):

example (hc : min a b = c) : true :=
begin
  rw min_eq_right (min_lt_left.1 _).le at hc,
  sorry,
  refine hc.trans_lt _,
  sorry,
end

[Eric Wieser]

@Yaël Dillies, I'm finding your #mwe's hard to follow due to the use of : true

[Yaël Dillies]

Why? My point was to show that I neither needed to act on the goal nor to have the hypothesis c < a laying around to do what Scott wanted.

[Yury G. Kudryashov]

@Scott Morrison Do you have an #mwe for your #xy?

[Scott Morrison]

@Yury G. Kudryashov, for a #mwe, I think what I have above:

import Mathlib.Order.MinMax

theorem foo [LinearOrder α] {a b c : α} (w : min a b = c) (h : c < a) : b = c := by
  rw [min_eq_iff] at w
  rcases w with ⟨rfl, -⟩ | ⟨rfl, -⟩
  · exfalso; apply lt_irrefl a; exact h
  · rfl

example [LinearOrder α] {a b c : α} (w : min a b = c) : b = c := by
  replace w := foo w ?_
  -- Now I can use the stronger result:
  exact w
  -- But I have to prove the inequality at some point:
  · guard_target = c < a
    sorry

The desiderata is:

• at the line that is currently replace w := foo w ?_ I want something that is:
  • short,
  • ideally readably indicates what the new state will be
• after that line, we have
  • b = c in the context
  • a side goal of c < a
  • I don't particularly mind the order of the goals, although would slightly prefer (unlike the #mwe) the side goal to come first.

Maybe it's also clearer if you just imagine c = 0 in all of this.

[Scott Morrison]

As for the actual #xy, I'm not sure I can usefully minimise it right now, but the place this came up was on branch#edit_distance, at this line.

I have a hypothesis that looks like

w : min (Cost.insert y + levenshtein (x :: xs) ys) (Cost.substitute x y + levenshtein xs ys) = 0

and at this point in the proof the reasoning should be:

• "Clearly Cost.insert y is positive, and levenshtein is non-negative
• so the first alternative can't be the minimum, and
• we can conclude Cost.substitute x y + levenshtein xs ys = 0.

[Yury G. Kudryashov]

What are the types?

[Yury G. Kudryashov]

Does docs#min_eq_iff help?

[Yury G. Kudryashov]

Also, if you live in NNReal or Nat, then we have docs#min_eq_bot

[Yury G. Kudryashov]

Looking at the code, did you consider adding a requirement that the codomain is a docs#CanonicallyOrderedAddMonoid ?

[tsuki hao]

is there code for theorem my_lemma : ∀ x y ε : ℝ , 0 < ε → ε ≤ 1 → ∣ x ∣ < ε → ∣ y ∣ < ε → ∣ x * y ∣ < ε :=
sorry

[Yury G. Kudryashov]

docs#mul_lt_of_lt_of_le_one_of_nonneg

[Yury G. Kudryashov]

(after rewriting abs_mul)

[Yury G. Kudryashov]

The assumption on y can be weakend to |y| ≤ 1