Преобразование Coq в Идрис

Question

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

Answer 1

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

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

• intros - просто укажите переменные на LHS
• reflexivity - Refl
• apply- вызов функции напрямую
• simpl - Упрощение производится автоматически Идрисом
• 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с, однако это не всегда работает (например, когда replace делает большой кусок термина исчезнуть)
• destruct - если для одной переменной, попробуйте разделить в LHS, в противном случае используйте with сооружать
• induction - разделить в LHS и использовать рекурсивный вызов в rewrite или напрямую. Убедитесь, что хотя бы один из аргументов в рекурсии структурно меньше, иначе вы потерпите неудачу в совокупности и не сможете использовать результат в качестве леммы. Для более сложных выражений вы также можете попробовать SizeAccessible от Prelude.WellFounded,
• trivial - обычно сводится к расщеплению в LHS в максимально возможной степени и решению с Refls
• assert - лемма под where
• exists - зависимая пара (x ** prf)
• case - или case .. of или же with, Будь осторожен с case однако - не используйте это ни в чем, о чем вы позже захотите доказать, иначе вы застрянете rewrite (см. выпуск № 4001). Обходной путь должен сделать на высшем уровне (в настоящее время вы не можете обратиться к леммам в where/withсм. выпуск № 3991) помощники по сопоставлению с образцом.
• revert - "не вводить" переменную путем создания лямбды и последующего применения ее к указанной переменной

• 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