If you want to combine syntactic and interactive construction of functions, the standard advice I give these days is to use Equations (with _
for what you want to build with tactics), which is nowadays part of the Coq Platform. See a simple use example.
1 Like