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.

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

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!

Have you tried using evidence in proofs?

More specifically, induction on evidence.

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.

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: Jun 15 2024 at 05:01 UTC