使用coq中的“function”和“program”简化依赖类型编程的生命

我试图在COQ中实现一个依赖类型的stlc评估器,使用 Program Fixpoint . 由于语言没有固定点运算符,我认为评估器应该终止,尽管终止条件不是结构化的。

在我的开发过程中,我发现一个头疼的原因是我不能同时跟踪太多的变量,并且模式匹配过于嵌套。

如果只是一个 Fixpoint 我可以使用策略来实现身体,但是当使用 程序固定点 或 Function 我就是不能。在这种情况下,有没有什么技巧可以使用策略来建立身体?

我被困在最后: https://gist.github.com/HuStmpHrrr/0d92e646916ae9ec7ced3ff21724ba2d