Hello, I'm playing with easycrypt, but is there any reason for `res < 2`

to be defined (Int module) while `res > 2`

is not defined? It is to avoid duplicating the rules for the two versions?

Ok, I guess the fact that `=>`

already exists is also in favor of not using =>

This topic was moved here from #Coq users > Easycrypt by Karl Palmskog.

Hi @Leo Colisson , I guess indeed EasyCrypt follows the conventions of math-comp, where `x > y`

is just sugar for `y < x`

, so indeed, only `_ < _`

is "primitive".

If you're interested in Easycrypt, then the Formosa zulip will probably give you a more detailed answer.

If you'd like to do cryptographic proofs in Coq, you could try our https://github.com/SSProve/ssprove

Thanks a lot @Bas Spitters . I was actually not aware of ssprove, I'll get it a try. @Emilio Jesús Gallego Arias Regarding `x > y`

, as far as I tried it would not even compile as I would get a typing issue saying that `>`

is not defined for integers, while `<`

is (which is part of my confusion). But I guess it's just something to know about ^^ (unless I missed something)

It's been a while since I used EC indeed, you can try the Formosa Zulip or ping @Pierre-Yves Strub who may be able to point out what the right forum is.

Last updated: Jun 05 2023 at 09:01 UTC