Coq: определение родного языка, чтобы избежать дублирования - PullRequest
Новая
       69

Coq: определение родного языка, чтобы избежать дублирования

0 голосов
/ 04 июля 2018

В настоящее время я работаю над доказательствами, где снова и снова пишу такой код: 

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?

1 Ответ

0 голосов
/ 05 июля 2018

Вы правы, что Ltac не приспособлен для этой задачи. На данный момент нет способа автоматизировать такие задачи в Coq, но для этого разрабатываются некоторые инструменты. См. Например Template Coq или Coq-Elpi . Большинство из этих инструментов находятся в состоянии перед выпуском.

В качестве альтернативы я бы предложил создать ваши собственные файлы .v из более абстрактного описания типов, написав генератор файлов на выбранном вами языке.

...