Stream: Coq users

Topic: ulep?


view this post on Zulip Shea Levy (Oct 23 2020 at 10:17):

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

view this post on Zulip Shea Levy (Oct 23 2020 at 10:20):

Or some other library (without axioms)?

view this post on Zulip Maxime Dénès (Oct 23 2020 at 10:46):

you mean le on natural numbers?

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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: Jan 29 2023 at 01:02 UTC