Is there a lemma like this predefined in coq?

```
forall a b: nat,
~(a < b) -> b <= a.
```

I imported `Lia`

and then tried

```
Search (~(_ < _) -> _).
```

But couldn't spot it.

You should give a minimal example (with Requires) otherwise we don't even know what `<`

or `<=`

are. And if by "predefined in Coq", you mean in the prelude (the only thing loaded without any Require), the answer is likely no.

By predefined, I meant in some standard library that comes with Coq. I figured since it's an inequality, lia might be having something.

This is what I have been trying:

```
Require Import ssreflect Lia.
Goal forall (a b: nat),
~(a < b) -> b <= a.
Proof.
```

That's better. Then just figure out what `<`

, `<=`

and `~`

are with `Set Printing All`

or `Locate "_ < _",... and do a `

Search` with the result.

Thanks!

I did `Search not lt le.`

and found it.

Although I'm not sure if the proof I made is in the style of ssreflect:

```
Goal forall (a b: nat),
~(a < b) -> b <= a.
Proof.
move => a b H.
exact: iffLR (PeanoNat.Nat.nlt_ge a b) H.
Qed.
```

I guess ` by rewrite -(PeanoNat.Nat.nlt_ge a b).`

is more appropriate instead of the line with `iffLR`

.

Or even just ` by rewrite -PeanoNat.Nat.nlt_ge.`

!

Or `by lia`

?

Huh..?

Oh yeah.. :face_palm:

Julin Shaji said:

Although I'm not sure if the proof I made is in the style of ssreflect:

`Goal forall (a b: nat), ~(a < b) -> b <= a. Proof. move => a b H. exact: iffLR (PeanoNat.Nat.nlt_ge a b) H. Qed.`

I guess `by lia`

is best. And if you encounter a case where lia does not work and want to do it the ssreflect style, you nee to use boolean negations, load `ssreflect ssrfun ssrbool ssrnat eqtype`

, and do `by case: leqP`

.

Pierre Roux said:

That's better. Then just figure out what

`<`

,`<=`

and`~`

are with`Set Printing All`

or`Locate "_ < _",... and do a`

Search` with the result.

You can also `Search (_ < _).`

and similarly with the other notations, there is no need to figure out the name behind the notation.

Julin Shaji said:

I imported

`Lia`

and then tried`Search (~(_ < _) -> _).`

But couldn't spot it.

Yeah, a good rule-of-thumb for when searching doesn't work is to be less specific; there is often a relevant lemma even when it is not in the format we imagined. `Search not lt le.`

is indeed a way of being less specific.

Ana de Almeida Borges said:

Pierre Roux said:

That's better. Then just figure out what

`<`

,`<=`

and`~`

are with`Set Printing All`

or`Locate "_ < _",... and do a`

Search` with the result.You can also

`Search (_ < _).`

and similarly with the other notations, there is no need to figure out the name behind the notation.

Oh.. I had been doing `Locate`

and then using its output for `Search`

. Thanks for mentioning this.

But I guess Locate-Search combo would be unavoidable when there are multiple interpretations for the same notation?

I believe there is a risk with partial application, in the sense that `Search (_ < _)`

will not find lemmas where `lt`

is not fully applied, say `well_founded lt`

Julin Shaji said:

But I guess Locate-Search combo would be unavoidable when there are multiple interpretations for the same notation?

I don't think so, in the sense that at every point Coq has an opinion about which interpretation corresponds to which notation, and `Search`

will use that one. So `Search (_ < _)`

will interpret it in the default way and `Search (_ < _)%some_scope`

will interpret it in that scope.

Last updated: Jun 13 2024 at 19:02 UTC