Improving Search in Rocq
Master Project

Project Description

In this project, you improve the search function in Rocq.

The search function in Rocq does not unfold constants. This often leads to relevant constants not being shown when searching.

For instance, suppose a constant “injective” is defined in Rocq, to mean forall x y, f x = f y -> x = y. Searching for the pattern (?f ?x = ?f ?y -> ?x = ?y) does not show results mentioning the constant “injective”, since the definition of “injective” is not unfolded during search.

In this project, you extend the search function of Rocq to do unfolding, for a more complete search.

Project Goals

In this project, you

• investigate the feasibility of intertwining unfolding with searching,
• study performance implications
• develop recommendations for the future developement of Rocq regarding searching.

Contacts for the Project

• Benedikt Ahrens (TU Delft)