Stream: Coq users

Topic: Searching a lemma


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

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

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

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

view this post on Zulip Julin Shaji (Feb 21 2024 at 09:43):

Thanks!

I did Search not lt le. and found it.

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

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

view this post on Zulip Julin Shaji (Feb 21 2024 at 09:46):

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

view this post on Zulip Meven Lennon-Bertrand (Feb 21 2024 at 09:48):

Or by lia?

view this post on Zulip Julin Shaji (Feb 21 2024 at 09:49):

Huh..?
Oh yeah.. :face_palm:

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

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

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

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

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

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

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