leanprover-community
Add ProofMode.SynthInstance
Based on #107
Add a custom version of synthInstance for the proof mode that can create and instantiate mvars. It is implemented as a simple backtracking search, reusing the standard instance infrastructure. This version of synthInstance should be used for the IPM proof mode classes, marked with the attribute ipm_class. This search only backtracks on instances marked with ipm_backtrack.
Also some other small refactorings:
- Allow iexists to take multiple arguments
- Fix handling of created goals in iexists
- Use the Goals structure more consistently
- Add some more error messages
- Generalize AsEmpValid over the direction similar to the Rocq version
Cool! Looks really good.
I tidied some of the proofmode names, and I added a top-level #ipm_synth command for debugging IPM synthesis (similar to the #synth command in Lean). I'll let you have the final word on whether or not to keep it, I implemented it just so I could understand your algorithm a little better myself.
Would you also be able to (briefly) document the differences ipm_backtrack, ipm_class, regular typeclasses, the in/out params versus your .in and .out etc? It would be good to have all of this in plain English so that someone extending the proofmode knows what to do. I think a good standard here would be just enough documentation so that someone could understand why everything in instances.lean is stated the way it is.
Thanks for the feedback!
I added a top-level #ipm_synth command for debugging IPM synthesis (similar to the #synth command in Lean). I'll let you have the final word on whether or not to keep it, I implemented it just so I could understand your algorithm a little better myself.
This is a good idea. I tweaked the implementation and added some tests using the #ipm_synth command.
Would you also be able to (briefly) document the differences ipm_backtrack, ipm_class, regular typeclasses, the in/out params versus your .in and .out etc? It would be good to have all of this in plain English so that someone extending the proofmode knows what to do. I think a good standard here would be just enough documentation so that someone could understand why everything in instances.lean is stated the way it is.
I added some documentation to SynthInstance.lean. Please have a look and let me know if you have any feedback.