About the usage of SearchAbout and SearchPattern

[jaewooklee93]

For proving pigeonhole_principle, I used the theorem S n < S m -> n < m.

However, the problem is that I don't know how I can find that theorem using SearchPattern. My first try was SearchPattern (S _ < S _ -> _ < _), however, it didn't give any useful information. It only showed

Coq < SearchPattern (S _ < S _ -> _ < _).

Warning: query commands should not be inserted in scripts

So I tried again with SearchPattern (S _ <= S _ -> _ <= _). At this time, I got the following result.

Coq < SearchPattern (S _ <= S _ -> _ <= _).

Warning: query commands should not be inserted in scripts
le_S_n: forall n m : nat, S n <= S m -> n <= m
Le.le_S_n: forall n m : nat, S n <= S m -> n <= m
Sn_le_Sm__n_le_m: forall n m : nat, S n <= S m -> n <= m

Thus, I just guessed that I could use Lt.lt_S_n for my purpose, since Le.le_S_n gave such result. That guess was found to be correct. After I had known the name if theorem, I could find its content with using SearchAbout.

Coq < SearchAbout "lt_S_n".

Warning: query commands should not be inserted in scripts
Lt.lt_S_n: forall n m : nat, S n < S m -> n < m

On the other hand, when I used SearchAbout instead of SearchPattern to look for the theorem related to <=, it gave

Coq < SearchAbout le.

Warning: query commands should not be inserted in scripts
Between.between_le:
  forall (P : nat -> Prop) (k l : nat), Between.between P k l -> k <= l
Between.between_Sk_l:
  forall (P : nat -> Prop) (k l : nat),
  Between.between P k l -> S k <= l -> Between.between P (S k) l
Between.between_restr:
  forall (P : nat -> Prop) (k l m : nat),
  k <= l -> l <= m -> Between.between P k m ->
...

(1000 lines of incomprehensible search results)

So I think that SearchAbout is almost useless if I deal with built-in objects like plus, mult or le, since it brings us bunch of theorems we don't need as well. Is it right?

In conclusion, my questions are,

1. In both of homework and exams, can we use all theorems which can be found by SearchAbout or SearchPattern, such as le_S_n, Le.le_S_n and Sn_le_Sm__n_le_m. Or, is there the most preferable one among them?
2. What is the proper way to find the theorem S n < S m -> n < m using SearchPattern in one-shot?
3. Can we use SearchAbout to search for theorems related to built-in objects? Since SearchPattern needs the exact pattern of theorem, it is sometimes harder to use than SearchAbout.

[jaewooklee93]

My question 1 is related to this phenomenon.

I'm curious about what happens if I have proved Sn_le_Sm__n_le_m of Assignment05_32.v with using le_S_n, which is exactly the same proposition. However, it doesn't work and show the error message.

(* Assignment05_32.v *)
Theorem Sn_le_Sm__n_le_m : forall n m,
  S n <= S m -> n <= m.
Proof. 
  apply le_S_n.
Qed.

Error: Impossible to unify "forall n m : nat, S n <= S m -> n <= m" with
 "forall n m : nat, S n <= S m -> n <= m".

However, when I have copied that proof into Assignment06_08.v, it works. Thus, I have two different cases, one which I can use le_S_n and another which I cannot use le_S_n, but I don't know the difference.

[fortunist]

2. I found the way using SearchAbout (Peano.lt (S ) (S ) -> Peano.lt ). Though I cannot explain why it does not work without Require Export "Prop".......

Addition : It was because that we cannot use Search, SearchAbout, SearchPattern properly without the code Require String. Open Scope string_scope. in induction.v.

By the way, I think the reason why SearchAbout lt. cannot find Lt.lt_Sn is that the definition of lt was redefined in Prop.v. SearchPattern (S < S -> < _). find Lt.lt_S_n well without redefining lt.

The library Lt use the definition of lt in Init/Peano.v.Coq cannot distinguish our lt and Init/Peano.v's lt when searching. However, with the equivalence of both definitions, we can apply Lt.lt_S_n to the new definition, I presume.

[jaewooklee93]

@fortunist Oh, it really works. Thank you. I guess the reason for that is Prop.v indirectly includes Induction.v and Induction.v imports lots of functions from the standard library. By the way, since SearchAbout lt doesn't work but SearchAbout Peano.lt works, the problem may be due to the overlapped namespaces or scopes.

[fortunist]

Oh, you commented when I was editing my comment for addition... Thank you.

[jaewooklee93]

@fortunist We arrived at the same conclusion :) Then it seems that it's better to avoid using lt. Well, we can always substitute lt with le, using unfold lt.

[fortunist]

1 - related phenomenon. The one defintion of le in Assignment0500.v and the other of Init/Peano.v are not equiavalent. Results of Print le. and Print Peano.le. have a little difference. It seems the difference makes restriction on applying initial theorems in Assignment05*.v.

3. SearchAbout is truly more powerful than SearchPattern. Just change a word SearchPattern to SearchAbout, and more results will appear. SearchAbout find the following all patterns in environmental definitions' argument types and return types. For example, compare the results of SearchAbout ( <= ) and SearchPattern( <= ).

Now that I've written, it seems you already know these now... Anyway I'm commenting to confirm my considerations.

[jaewooklee93]

@fortunist 1: Yeah, that seems the reason for all problems. Also, I want to point out that even if we have exactly the same definition for both of le and Peano.le, we cannot use the previous theorems. Maybe Coq has hidden serial numbers for differentiating each definition for the same name.

3: I only read the tutorial from Coq official website, so I didn't know that I also could use SearchAbout to match patterns, instead of SearchPattern. Thank you for letting me know. However, I think the fact that SearchAbout is giving us more results, doesn't directly mean that SearchAbout is more powerful. Because it gives too many results for le that even we cannot read them all.

When I compared the results of SearchAbout (_ <= _) and SearchPattern (_ <= _), I found that SearchAbout gave every theorem which contains (_ <= _), whereas SearchPattern only shows the theorems, whose conclusion contain (_ <= _). so seaching with SearchPattern is somewhat more selective and I think SeachPattern can be useful to find exactly what we want.