В настоящее время я работаю над доказательствами, где снова и снова пишу такой код:
Lemma eq_T: forall (x y : T), {x = y} + {x <> y}
with eq_trait: forall (x y : trait), {x = y} + {x <> y}
with eq_pi: forall (x y : pi), {x = y} + {x <> y}.
Proof.
decide equality; auto with ott_coq_equality arith.
decide equality; auto with ott_coq_equality arith.
decide equality; auto with ott_coq_equality arith.
Defined
Hint Resolve eq_T : ott_coq_equality.
Hint Resolve eq_trait : ott_coq_equality.
Hint Resolve eq_pi : ott_coq_equality.
То есть у меня есть некоторое количество взаимно индуктивных типов, и я одновременно получаю равенство для всех из них.
Что я хотел бы сделать, так это написать макрос, в котором я могу написать
MutualDeriveEquality T, pi, trait
и он будет генерировать механические команды выше, так что я могу использовать это для различных групп взаимно индуктивных типов.
Я не очень разбираюсь в LTac, но я не уверен, что он применим здесь, так как я не просто автоматизирую генерацию проверочных терминов, но и определяю значения на местном языке. (Хотя я могу быть совершенно не прав).
Что мне интересно, так это то, что есть способ определить «народный макрос», который может автоматизировать это? Или это то, что можно сделать с помощью LTac? Или это единственный способ написать плагин Coq в OCaml?