Adding a query to search for symbols ?

[NotBad4U]

Hi everyone,

Starting to work on large files with several symbols, I often feel the necessity to search for definitions and lemma during a prove that can sometimes be located in other files or previously defined in the same file. Coq has Search commands to help you out. I think it could be interesting to have something similar in LambdaPi.

For a quick overview of the Search in Coq, the simplest way to search is to search by name.

Coq < Search "len".
length: forall A : Type, list A -> nat

Another thing you can do is to search for patterns with holes _:

Search (S _ <= _).
le_S_n: forall n m : nat, S n <= S m -> n <= m
le_n_S: forall n m : nat, n <= m -> S n <= S m

I think we can imagine a query similar to Search Coq command that could have the behavior:

opaque symbol notnotI p : Prf p → Prf (not (not p)) ≔
begin
   admitted
end;

search "not";
// output in term: symbol notnotI : Π p: U, Prf p → Prf (not (not p));

search ( _  ∧ _ ).
// output in term:
// symbol andI : Π p: U, Π q: U, Prf p → Prf q → Prf (p ∧ q);
// symbol andD1 : Π p: U, Π q: U, Prf (p ∧ q) → Prf p;
// symbol andD2 : Π p: U, Π q: U, Prf (p ∧ q) → Prf q;

I am ready to develop this feature if you think that it is interesting to add this :smiley:. I will need that you indicate me where I should look to implement this feature.

[fblanqui]

Hi @NotBad4U . This is definitively something we are interested in, and we would be very happy to get a PR on this! I know that @sacerdot started to implement some algorithm for type-based search, which is complementary to what you propose, but it could be useful to get his comment first and see what can be shared/reused.

[sacerdot]

The secondo part of @NotBad4U proposal is an instance of type-based search. I have a small implementation waiting for some love (integration, etc.) and an undergraduate student (supposed to be) working on that. At the end of April I also have planned a STMS to visit Frederic and complete the thing (and more) in case the student did not deliver yet. The aim of the STMS is more ambitious (dealing also with encodings, etc.). If you need it urgently I can force the student to rush something in.

(e.g. of design issues not to be rushed: is Search supposed to be working only on required files (easy) or on any previously compiled file (hard))

[NotBad4U]

Hi @sacerdot and @fblanqui! Thanks your answer.

I have a small implementation waiting for some love (integration, etc.) ...

Could we start the work on the first instance proposed and add later the search by pattern when the type-based search feature is done?

If you need it urgently I can force the student to rush something in.

To give more context, I am a fresh Ph.D. student at Inria Nancy that work on a reliable reconstruction of TLAPS proofs generated by the SMT solver veriT in LambdaPi, so I daily use LambdaPi for now. But I don't think there is a necessity to rush something.

Search supposed to be working only on required files (easy) or on any previously compiled file (hard)

I think we should focus directly "previously compiled file (hard)". In my case, most of my searches are for lemmas declared in other files. Could you explain to me why this is considered as harder? Is it because of the module system?

[fblanqui]

This issue will be solved when https://github.com/Deducteam/lambdapi/pull/982 will be merged.