Облегчить жизнь в программировании с зависимой типизацией, используя `Function` и` Program` в Coq

Question

Я пытаюсь реализовать зависимый тип оценщика STLC в Coq, используя Program Fixpoint.Поскольку в языке нет оператора с фиксированной запятой, я думаю, что оценщик должен завершиться, хотя условие завершения не является структурным.слишком много переменных одновременно, и сопоставление с образцом слишком вложенное.

Если бы это было просто Fixpoint, я мог бы просто реализовать тело, используя тактику, но при использовании Program Fixpoint или Function, Я просто не могу.Есть ли какая-нибудь хитрость для построения тела с использованием тактики в этом случае?

Я застрял в самом конце: https://gist.github.com/HuStmpHrrr/0d92e646916ae9ec7ced3ff21724ba2d

Answer 1

При использовании Program вы можете просто оставить подчеркивание для тех частей вашего термина, которые вы хотите заполнить, используя пробный режим. Любые подчеркивания, которые могут быть выведены, будут автоматически заполнены, а остальные приведут к обязательствам. Например, вы можете написать все run в режиме проверки, написав Program Fixpoint run ... {measure ...} := _. Мера будет отображаться в качестве аргумента для run в контексте.