Order on `fin n.succ`

Stream: Is there code for X?

[Michael Stoll]

I'm having problems finding a good proof of the following.

example {n : ℕ} {a b : fin n.succ} (h : a ≤ b) (ha : a = n) (hb : b ≠ n) : false

I somehow can't find a statement of the form example {n : ℕ} {a : fin n.succ} : a ≤ n.
There is docs#fin.is_le, but this coerces a to a natural number.
There is docs#fin.le_last, but then I need to convert between n : fin n.succ and fin.last n, which are apparently not defeq.

[Michael Stoll]

Hm, there is docs#fin.coe_nat_eq_last, which would deal with this latter issue.

[Michael Stoll]

So my proof is now

by { rw ha at h,
     exact hb (le_antisymm (le_of_le_of_eq (fin.le_last b) (fin.coe_nat_eq_last n).symm) h),}

but I have the feeling that there should be a simpler one.

[Michael Stoll]

Next question:

example  {n : ℕ} {a : fin n.succ} (h : a  ≠ 0) : a.pred h < a

There is docs#order.pred_lt, but this requires a [no_min_order α] instance. (For natural numbers, there is docs#nat.pred_lt, but this is not directly applicable either.)

[Yaël Dillies]

docs#order.pred_lt_of_not_is_min for the statement about docs#order.pred. There should be some lemma relating it to docs#fin.pred.

[Michael Stoll]

I just noticed that a.pred h is a of type fin n and not fin n.succ, so there is an additional coercion involved, which makes applying docs#order.pred_lt_of_not_is_min not completely straightforward...

[Michael Stoll]

Is there a "better" pred here that takes values in the same fin _?

[Eric Rodriguez]

file#order/succ_pred/fin file#data/fin/succ_pred

[Eric Rodriguez]

so in some ways it's order.pred

[Eric Rodriguez]

we don't seem to have docs#is_min_iff_eq_zero for canonically ordered blah blahs though

[Eric Rodriguez]

oh we do but it overuses defeq, yuck

import data.fin.succ_pred

example  {n : ℕ} {a : fin n.succ} (h : a ≠ 0) : order.pred a < a :=
order.pred_lt_of_not_is_min $ not_is_min_iff_ne_bot.mpr h

[Michael Stoll]

[Yes, this is where I'm stuck now.] No longer, thanks.

[Michael Stoll]

Another question: Is there a version of fin.find that looks for the largest index of an entry satisfying a property?

[Yaël Dillies]

Related: docs#nat.find_greatest

[Michael Stoll]

OK, perhaps I can use that. But it is getting late...

[Junyan Xu]

It seems what you want is in an open PR: you may use top_le_iff if you have last n.succ instead of n.
By the way, you shouldn't usually leave a substitutable equality like ha : a = n among the hypotheses.

[Kevin Buzzard]

There's zify to change slightly annoying questions about naturals to less annoying questions about integers which are >= 0. Maybe we need an nify tactic to change annoying questions about fin n to less annoying questions about nat? I feel like the answer to the first question in this thread should be nify, linarith

[Kevin Buzzard]

The idea is that nify changes the local context to a b : nat, a < n.succ, b < n.succ, a <= b, ...

[Kevin Buzzard]

Oh, maybe this is problematic because the tactic doesn't know that the coercion from nat to fin n.succ and back sends n to n

[Kevin Buzzard]

But that's also linarith

[Michael Stoll]

Junyan Xu said:

By the way, you shouldn't usually leave a substitutable equality like ha : a = n among the hypotheses.

The example was extracted from the middle of a proof, I guess just before doing rw ha...