Stream: Coq users

Topic: ulep?

Shea Levy (Oct 23 2020 at 10:17):

Does the standard library have a proof of "uniqueness of le proofs", i.e. $\forall n m (p_1 p_2 : n \le m), p_1 = p_2$?

Shea Levy (Oct 23 2020 at 10:20):

Or some other library (without axioms)?

Maxime Dénès (Oct 23 2020 at 10:46):

you mean le on natural numbers?

Maxime Dénès (Oct 23 2020 at 10:47):

in mathcomp, the order is defined as a boolean relation, so you can use a generic axiom-free proof of uniqueness for such relations

Emilio Jesús Gallego Arias (Oct 23 2020 at 11:02):

IIANM also math-comp includes a proof for the standard library https://github.com/math-comp/math-comp/blob/2b97a257956d307e7cb9ad7d4920fb5db969b69b/mathcomp/ssreflect/ssrnat.v#L464

Jakob Botsch Nielsen (Oct 23 2020 at 13:42):

Note that the proof of this is very short, at least with Equations:
https://github.com/MetaCoq/metacoq/blob/abc736f20020156e520e7ca4ef0557ce5f8b7db0/pcuic/theories/PCUICWcbvEval.v#L693-L699

Last updated: Oct 03 2023 at 20:01 UTC