Stream: math-comp users

Topic: ssrint


view this post on Zulip Marie Kerjean (Feb 18 2021 at 20:45):

How do I handle x : int for which I know that 0 <= x as an element of type nat ? I'm sure it's obvious but for a reason I can't find it in ssrint.

view this post on Zulip Pierre-Yves Strub (Feb 18 2021 at 20:45):

What do you mean. That you want to get a nat from x?

view this post on Zulip Pierre-Yves Strub (Feb 18 2021 at 20:46):

In that case, case: x le0x => // x _ will do it.

view this post on Zulip Marie Kerjean (Feb 18 2021 at 20:55):

Thanks ! So Znat is here for a whole other purpose ?

view this post on Zulip Pierre-Yves Strub (Feb 18 2021 at 21:12):

Well, Znat is transparent enough s.t. the above tactic works when le0x : x \is a Znat

view this post on Zulip Pierre-Yves Strub (Feb 18 2021 at 21:16):

And if you want to use ZnatP, you can do that: case/ZnatP: le0x => [n {x}->].

view this post on Zulip Cyril Cohen (Feb 18 2021 at 21:20):

And if you are not inside a proof you can use `|x|%N instead

view this post on Zulip Marie Kerjean (Feb 18 2021 at 21:36):

Pierre-Yves Strub said:

In that case, case: x le0x => // x _ will do it.

Is there a way to do that do that x : nat is not opaque ?

view this post on Zulip Cyril Cohen (Feb 18 2021 at 21:44):

Yes: `|x|%N

view this post on Zulip Marie Kerjean (Feb 18 2021 at 22:03):

Thanks ! For the record I was trying to get out an ugly mixture between Rfloor Rtoint and nat, using the floor of a positive real as a nat, but I did not manage at the end : https://github.com/math-comp/analysis/blob/8f51f8711e896f99859a9856597d1ce377ecb0bd/theories/banach_steinhaus.v#L144.


Last updated: Jan 29 2023 at 18:03 UTC