## Stream: Coq users

### Topic: Searching a lemma

#### Julin Shaji (Feb 21 2024 at 09:28):

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.

#### Pierre Roux (Feb 21 2024 at 09:29):

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.

#### Julin Shaji (Feb 21 2024 at 09:34):

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.
``````

#### Pierre Roux (Feb 21 2024 at 09:37):

That's better. Then just figure out what `<`, `<=` and `~` are with `Set Printing All` or `Locate "_ < _",... and do a `Search` with the result.

#### Julin Shaji (Feb 21 2024 at 09:43):

Thanks!

I did `Search not lt le.` and found it.

#### Julin Shaji (Feb 21 2024 at 09:44):

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.
``````

#### Julin Shaji (Feb 21 2024 at 09:45):

I guess ` by rewrite -(PeanoNat.Nat.nlt_ge a b).` is more appropriate instead of the line with `iffLR`.

#### Julin Shaji (Feb 21 2024 at 09:46):

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

#### Meven Lennon-Bertrand (Feb 21 2024 at 09:48):

Or `by lia`?

#### Julin Shaji (Feb 21 2024 at 09:49):

Huh..?
Oh yeah.. :face_palm:

#### Cyril Cohen (Feb 21 2024 at 15:09):

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`.

#### Ana de Almeida Borges (Feb 22 2024 at 14:00):

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.

#### Ana de Almeida Borges (Feb 22 2024 at 14:03):

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.

#### Julin Shaji (Feb 22 2024 at 16:53):

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.

#### Julin Shaji (Feb 22 2024 at 16:55):

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

#### Meven Lennon-Bertrand (Feb 22 2024 at 16:58):

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`

#### Ana de Almeida Borges (Feb 23 2024 at 17:02):

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