Can you use rcases with a hypothesis without clearing it?

Stream: new members

[Mitchell Lee]

Hello! In chapter 6 of Mathematics in Lean, there's an example involving this structure:

structure StandardTwoSimplex where
  x : ℝ
  y : ℝ
  z : ℝ
  x_nonneg : 0 ≤ x
  y_nonneg : 0 ≤ y
  z_nonneg : 0 ≤ z
  sum_eq : x + y + z = 1

One of the problems is to write a function to take the weighted average of two elements of the standard two-simplex given a parameter lambda between 0 and 1. This is what I have:

def weightedAverage (lambda : Real) (lambda_nonneg : 0 ≤ lambda) (lambda_le : lambda ≤ 1)
    (a b : StandardTwoSimplex) : StandardTwoSimplex := by
  have : 1 - lambda ≥ 0 := by linarith
  exact {
    x := lambda * a.x + (1 - lambda) * b.x,
    y := lambda * a.y + (1 - lambda) * b.y,
    z := lambda * a.z + (1 - lambda) * b.z,
    x_nonneg := by cases a; cases b; positivity,
    y_nonneg := by cases a; cases b; positivity,
    z_nonneg := by cases a; cases b; positivity,
    sum_eq := by linear_combination (lambda * a.sum_eq + (1 - lambda) * b.sum_eq) }

This works, but it is slightly unsatisfying. I use cases a; cases b; in order to add a.x_nonneg (etc.) to the list of hypotheses so that the positivity tactic can use them. I would like to be able to move the cases a and cases b before the exact so that those lines do not have to be repeated three times. Unfortunately, doing so would clear the hypotheses a and b and make it impossible to refer to a.x(etc.). Is there a way around this?

[Eric Wieser]

You can use cases id a, but that probably gives the wrong hypotheses

[Mitchell Lee]

Yeah, it doesn't work, unfortunately. I get the following state:

case mk
  lambda : ℝ
  lambda_nonneg : 0 ≤ lambda
  lambda_le : lambda ≤ 1
  a b : StandardTwoSimplex
  this : 1 - lambda ≥ 0
  x✝ y✝ z✝ : ℝ
  x_nonneg✝ : 0 ≤ x✝
  y_nonneg✝ : 0 ≤ y✝
  z_nonneg✝ : 0 ≤ z✝
  sum_eq✝ : x✝ + y✝ + z✝ = 1
  ⊢ StandardTwoSimplex

So the hypotheses don't say anything about a.x, a.y, a.z. I do like the "cases id" trick though.

[Richard Copley]

How do you feel about:

  have ⟨ax, ay, az, _, _, _, as⟩ := a
  have ⟨bx, by', bz, _, _, _, bs⟩ := b

?

[Eric Wieser]

The non-beginner solution to your original question is:

open Qq
@[positivity StandardTwoSimplex.x _]
def xPos : Mathlib.Meta.Positivity.PositivityExt where eval {u α} _ _ e := do
  match u, α, e with
  | 0, ~q(ℝ), ~q(StandardTwoSimplex.x $s) =>
    assertInstancesCommute
    pure <| .nonnegative q(StandardTwoSimplex.x_nonneg $s)
  | _, _, _ => failure

@[positivity StandardTwoSimplex.y _]
def yPos : Mathlib.Meta.Positivity.PositivityExt where eval {u α} _ _ e := do
  match u, α, e with
  | 0, ~q(ℝ), ~q(StandardTwoSimplex.y $s) =>
    assertInstancesCommute
    pure <| .nonnegative q(StandardTwoSimplex.y_nonneg $s)
  | _, _, _ => failure

@[positivity StandardTwoSimplex.z _]
def zPos : Mathlib.Meta.Positivity.PositivityExt where eval {u α} _ _ e := do
  match u, α, e with
  | 0, ~q(ℝ), ~q(StandardTwoSimplex.z $s) =>
    assertInstancesCommute
    pure <| .nonnegative q(StandardTwoSimplex.z_nonneg $s)
  | _, _, _ => failure

which means you can just drop the cases entirely!

[Mitchell Lee]

Thanks for the replies. I hope that one day I will understand the non-beginner solution.

I have noticed that

  have := a.x
  have := a.y
  have := a.z
  have := a.x_nonneg
  have := a.y_nonneg
  have := a.z_nonneg
  have := a.sum_eq

gives exactly the proof state I want, with this✝²: 0 ≤ a.x in the hypothesis list, even if I permute the seven lines or put an underscore before one or more of the := signs. However,

have ⟨_,_,_,_,_,_,_⟩ := a

does not. It gives x_nonneg✝: 0 ≤ x✝ instead. To be honest, I do not quite understand this.

[Mitchell Lee]

The simplest I have so far now is this:

def weightedAverage (lambda : Real) (lambda_nonneg : 0 ≤ lambda) (lambda_le : lambda ≤ 1)
    (a b : StandardTwoSimplex) : StandardTwoSimplex := by
  have : 1 - lambda ≥ 0 := by linarith
  have := a.x_nonneg; have := a.y_nonneg; have := a.z_nonneg
  have := b.x_nonneg; have := b.y_nonneg; have := b.z_nonneg
  exact {
    x := lambda * a.x + (1 - lambda) * b.x,
    y := lambda * a.y + (1 - lambda) * b.y,
    z := lambda * a.z + (1 - lambda) * b.z,
    x_nonneg := by positivity,
    y_nonneg := by positivity,
    z_nonneg := by positivity,
    sum_eq := by linear_combination (lambda * a.sum_eq + (1 - lambda) * b.sum_eq) }

Maybe it's not reasonable to expect anything better.

[Eric Wieser]

That looks pretty reasonable to me

[Eric Wieser]

You could probably inline the haves before the positivity, since each one only needs the haves for one variable at a time

[Mitchell Lee]

I guess technically this is actually longer than my original solution

[Mitchell Lee]

Yeah, you're right; inlining them would make it more readable