Преобразование Coq в Idris

Какими будут полезные рекомендации по преобразованию источника Coq в Idris (например, насколько похожи их системы типов и что можно сделать для перевода доказательств)? Из того, что я собираю, встроенная библиотека тактики Идриса минимальна, но расширяется, поэтому я полагаю, что с некоторой дополнительной работой это должно быть возможно.

Ответ 1

Недавно я перевел фрагмент Software Foundations и сделал частичный порт {P | N | Z} Arith, некоторые наблюдения, которые я сделал в процессе:

Обычно использование тактики Idris (в форме Pruvloj/Elab.Reflection) на данный момент не рекомендуется, этот объект несколько хрупкий и довольно трудно отлаживать, когда что-то идет не так. Лучше использовать так называемый "стиль Агды", полагаясь, если это возможно, на соответствие шаблону. Вот несколько грубых эквивалентов для более простой тактики Coq:

intros - просто укажите переменные на LHS
reflexivity - Refl
apply - вызов функции напрямую
simpl - упрощение выполняется автоматически Idris
unfold - также автоматически выполняется для вас
symmetry - sym
congruence/f_equal - cong
split - разделение на LHS
rewrite - rewrite ... in
rewrite <- - rewrite sym $ ... in
rewrite in - чтобы переписать внутри того, что у вас есть в качестве параметра, вы можете использовать конструкцию replace {P=\x=>...} equation term. К сожалению, Идрис не может вывести P большую часть времени, поэтому это становится немного громоздким. Другой вариант состоит в том, чтобы извлечь тип в лемму и использовать rewrite s, однако это не всегда будет работать (например, когда replace удаляет большую часть термина)
destruct - если в одной переменной попробуйте расщепление в LHS, в противном случае используйте конструкцию with
induction - разделение на LHS и использование рекурсивного вызова в rewrite или непосредственно. Убедитесь, что по крайней мере один из аргументов в рекурсии структурно меньше, или вы терпите тотальность и не сможете использовать результат в качестве леммы. Для более сложных выражений вы также можете попробовать SizeAccessible из Prelude.WellFounded.
trivial - как правило, как можно больше расщепляется в LHS и решает с помощью Refl s
assert - лемма под where
exists - зависимая пара (x ** prf)
case - либо case .. of, либо with. Однако будьте осторожны с case - не используйте его во всем, о чем вы позже захотите узнать, иначе вы застрянете на rewrite (см. вопрос № 4001). Обходным путем является создание верхнего уровня (в настоящее время вы не можете ссылаться на леммы в where/with, см. issue # 3991).
revert - "unintroduce" переменную, сделав лямбду и затем применив ее к указанной переменной

inversion - вручную определить и использовать тривиальные леммы о конструкторах:

-- injectivity, used same as `cong`/`sym`
FooInj : Foo a = Foo b -> a = b
FooInj Refl = Refl

-- disjointness, this sits in scope and is invoked when using `uninhabited`/`absurd`
Uninhabited (Foo = Bar) where   
  uninhabited Refl impossible