I’m writing proofs about Coq functions that frequently contain non-reducable terms constructed of a series of let ... := ... in expressions, as well as anonymous fixpoints and functions. If I want to reduce these terms, I have to extract, say, each anonymous fixpoint as its own object, write a subproof about what it evaluates to for a generic input, and then rewrite the result. I would really like to write a tactic that automatically extracts all of these anonymous bits from goals and hypotheses so that I don’t have a large number of big and manual remember sentences in my proofs.
It looks like the Search vernacular does have this capability, but I can’t seem to recreate it with a match goal ... Ltac expression. Any leads I can look at to write something like this?
n: nat
(* maybe this actually can be reduced... but this is an oversimplication of the terms I'm dealing with *)
H: (x, y) = (true, let thing1 := ... in (fix loop n := ...) n)
(* Would be nice to automatically generate: *)
loop : nat -> whatever
H0 : loop (fix loop n := ...)