LeanGrow project

Stream: metaprogramming / tactics

[Yves Jäckle]

Hello!
I wanted to share the current state of the project I've been working on: LeanGrow
The name "grow" comes from the fact that I initially intended it to be a suggestion tool similar to apply? or rw?, but it has since become the target to make this a full proof search tactic, such as Aesop, Canonical and Grind. This is still a work in progress. Some parts work, others don't. I've written a small report on the approach I've taken, which can be found on the repo. It's now public for potential future collaborators to see :wink:

[Kiran]

this is super cool! I really enjoyed reading the writeup and as someone unfamiliar with the internals of proof search implementations, the data structures were fun to read about!

One thing that wasn't clear from the writeup that I was curious about was how does this implementation of leangrow differ from existing tools such as grind and aesop? Also was the design of leangrow comparable to similar search strategies in other theorem provers? Isabelle/HOL, etc.

[Yves Jäckle]

In guess that in essence the implementation of the core search procedure is similar to that of Aesop in the sense that it isn't really based on higher order logic, but uses simple tree like data-structures to keep track of backward and forward steps that are taken to form the term that constitutes the proof. So the difference in the core search procedure is in the implementation details. Other then that Aesop allows for white-box automation, whereas grow won't. I'm not too familiar with grind, as it's still in development. However, as far as I know, grind has much more clever machinery to handle rewrites and case disjunctions, for example. I guess that the key feature of grow (if I get it to work) is the approach taken to select the forward and backward steps to be taken at each step ?
There are a lot of proof search and premise selection tools out there, and I guess that those that come closest are those based on naive Bayes. However I hope that the use of the generalization procedure described in section 3.2 of the report, its combinations with the use of set-tires, and their use for scoring, is original.