fin.pred_above

Stream: general

[Scott Morrison]

We currently have a function fin.pred_above p i h, which sends fin (n+1) to fin n, by subtracting one if p < i.

It's set up to take a proof that h : p \ne i. This seems really strange to me --- more natural would be to have a total function, which just sends both p and p+1 to p.

Would anyone object if I tried to make this change? (Or know what would go horribly wrong elsewhere?)

[Johan Commelin]

I've also noticed this. I think this is a good idea. But I guess you need to think about n = 0.

[Scott Morrison]

Indeed. But I think that is only a matter of choosing between a hypothesis 0 < n, or sending fin (n+2) to fin (n+1).

[Scott Morrison]

My inclination is to use the former, to avoid DTT hell.

[Johan Commelin]

yup, agreed

[Scott Morrison]

In either case it's still a "total function".

[Johan Commelin]

We could even consider using [fact (0 < n)]

[Scott Morrison]

It looks like pred_above is not actually used much, so I might just go for it.

[Scott Morrison]

I think a better approach is to have p : fin n, and i : fin (n+1), and then subtract one if p < i. That ensures both that n \ne 0, and that subtraction actually occurs somewhere.

[Yakov Pechersky]

The one downside to this is that you lose the "injectivity" of fin.pred_above.

[Yakov Pechersky]

And if one was to change fin.pred_above, what about fin.succ_above?

[Floris van Doorn]

I agree that this should be made total (at the very least, the total version should exist).

You don't really lose the "injectivity", it will still hold under the assumptions that your input is not equal to i, and these inequalities must also appear in any current statement of "injectivity".

[Scott Morrison]

As far as I can see, fin.succ_above is already as it should be.

[Scott Morrison]

I got hung up last night on some lemmas about insert_nth and remove_nth that used pred_above, but I think I see how to handle them now.

[Yury G. Kudryashov]

What exactly do you suggest to do with n = 0?

[Scott Morrison]

I've made a PR now, as #6125. To handle n = 0, the change I've made is that p : fin n while i : fin (n + 1), and p.pred_above i produces something in fin n. Notice in particular that the original pred_above allowed p : fin (n+1). (This is fine if we insist p \ne i, but not if we want a total function, and this is also what causes the problem at n = 0.)

[Kevin Buzzard]

5^3*7^2