Chapter 2: Nat.trichotomous may not be powerful enough

Stream: Analysis I

[JJ]

Hello! I'm finishing up Chapter 2 and have hit a bit of a snag I could use some advice on. I'm not sure whether it's an inadequate mechanization of one of the proofs, or whether I'm holding it wrong (I'm new to proving things in Lean).

The definition of Nat.trichotomous as given is a < b ∨ a = b ∨ a > b, for (a b:Nat). If I'm not mistaken with how Lean ∨ works -- this seems not the same as the book's statement of trichotomy, which states that exactly one of a < b, a = b, a > b is true.

This poses a problem for me right now as I have a nice clean proof of Nat.decLe that depends on two ne_le_iff_gt : ¬a ≤ b ↔ a > b and ne_lt_iff_ge : ¬a < b ↔ a ≥ b lemmas I defined. I would like to prove both of these by cases given trichotomy -- but I can't. In each of the sorrys following I only have one component of the trichotomy, not that the other two are false.

lemma Nat.ne_le_iff_gt (a b : Nat) : ¬a ≤ b ↔ a > b := by
  have tri := by apply trichotomous a b
  rcases tri with lt | eq | gt
  . sorry
  . sorry
  . sorry

I don't know if this is intentional or not! Could use some advice regardless. Thanks!

[Aaron Liu]

That should probably be not_le_iff_gt (or what core calls it, docs#Nat.not_le)

[Aaron Liu]

same for the not_lt

[Aaron Liu]

what you have should be enough since you know ne_of_lt and not_lt_of_gt which would rule out the other two cases if you know any one of them

[Aaron Liu]

for example you know the ne_of_lt tells you that you can't be in both lt and eq cases simultaneously, so it allows you to rule out eq given lt and it allows you to rule out lt given eq

[JJ]

Oh yeah thanks! I missed that we defined those theorems earlier.

[JJ]

I see the theorem was updated with a note, thanks :thumbs_up: