Proof based on order of two integers

Stream: new members

[Bob Rubbens]

How to do a case analysis based on the order of two numbers? I've tried:

theorem myTheorem (x y : Int) : P x y := by
  let ord := compare x y
  cases ord with
  | lt => sorry
  | eq => sorry
  | gt => sorry

The problem here is that I don't get the additional assumption compare x y = .lt, and so on, in each of the subsequent proof states. How to proceed?

[Kenny Lau]

@Bob Rubbens case on lt_trichotomy instead

[Bob Rubbens]

I see, then I do need a more specific typeclass, right, LinearOrder. I wasn't using that yet but maybe it's okay. It certainly is a lot more readable than what I've come up with:

  let y := compare self.start other.start
  have hy : y = .lt ∨ y = .gt ∨ y = .eq := by cases y <;> simp
  cases hy with
  | inl hy => sorry
  | inr hy =>
    cases hy with
    | inl => sorry
    | inr => sorry

I guess the shortcoming with my earlier example is that the ord variable is not mentioned in the goal, nor in any of the assumptions of the proof state. So distinguishing its case does not augment the proof in any way, and I think cases throws the thing you're casing on away by default. In total that more or less explains the situation I got into above.

[Weiyi Wang]

What is your concern about LinearOrder? It certainly should be on the type where you expect you can cases on </=/>

[Aaron Liu]

Bob Rubbens said:

and I think cases throws the thing you're casing on away by default. In total that more or less explains the situation I got into above.

You can tell it to not do that by doing cases h : ord with

[Bob Rubbens]

You can tell it to not do that by doing cases h : ord with

That's the missing link! Thanks.

What is your concern about LinearOrder?

I was thinking of making my file not depend on mathlib, to keep it small and self-contained, and just using Ord everywhere. But on second thought it's not so important.

Now the only thing left to understand why my ord variable is replaced in one case, but not in the other. Is that because in the first case it's present in the goal, but not in the second?

theorem myTheorem (P : Int → Int → Prop) (x y : Int) : P x y := by
  let ord := compare x y
  have hord : ord = .lt ∨ ord = .gt ∨ ord = .eq := by cases ord <;> simp -- ord is replaced
  cases ord -- ord is not replaced...?
  sorry
  sorry
  sorry

[Kenny Lau]

Bob Rubbens said:

not depend on mathlib

Int.lt_trichotomy is in core

[Bob Rubbens]

Perfect!! Many thanks.