Stream: Coq users

Topic: n <= m

Rafael Garcia Leiva (Aug 05 2020 at 16:13):

Hi,

Still learning Coq. Can somebody help me to prove the following Lemma?

Lemma equivalence (n m : nat):
n <= m <-> (n < m \/ n = m).

Many thanks in advance.

Daniel Sousa (Aug 05 2020 at 16:50):

Sure! What progress have you been able to do so far? Where are you stuck?

Rafael Garcia Leiva (Aug 05 2020 at 18:30):

Hi,

I have checked the standard library with:

SearchPattern (nat -> nat -> bool).
Search Nat.leb.

and

Locate "_ <= _".
Search Nat.le.

but it seems this property is not included.

Also, I have tried:

Proof.
split.
intros.
firstorder.

and

Proof.
split.
intros.
left.
auto.

Now I am reading about proofs by induction.

Many thanks!

Yishuai Li (Aug 05 2020 at 20:26):

Have you tried using evidence in proofs?

Yishuai Li (Aug 05 2020 at 20:29):

More specifically, induction on evidence.

Rafael Garcia Leiva (Aug 06 2020 at 08:01):

Hi,

I have managed to prove it with:

Lemma equivalence (n m : nat):
n <= m <-> (n < m \/ n = m).
Proof.
split.
intros.
induction H.
right.
reflexivity.
left.
assert (m < S m).
auto.
firstorder.
intros.
destruct H as [H1 | H2].
induction H1.
auto.
auto.
induction H2.
auto.
Qed.

But probably there is an easier way :)

Thanks for the links.

Enrico Tassi (Aug 10 2020 at 08:13):

Side note: in the Mathematical Components library we found that a different definition of leq works better. In particular one can define leq as a program rather than as a (functional) relation. See https://math-comp.github.io/htmldoc/mathcomp.ssreflect.ssrnat.html for the file about arithmetic (search for Definition leq) and here you can find a more extensive doc about this formalization style: https://math-comp.github.io/mcb/

Last updated: Oct 05 2023 at 02:01 UTC