将Coq转换为Idris

Question

将Coq源转换为Idris的一些有用的指导方针是什么(例如，它们的类型系统有多相似，以及如何翻译这些证据)？据我所知，Idris的内置战术库是最小的，但也是可以扩展的，所以我认为，通过一些额外的工作，这应该是可能的。

Answer 1

我最近翻译了软件基础的一部分，并做了{P=N，Z}Arith的部分端口，我在这个过程中做了一些观察：

通常，目前并不推荐使用Idris策略(以它们的Pruvloj/Elab.Reflection形式)，这个工具有点脆弱，在出了问题时很难调试。最好使用所谓的"Agda风格“，在可能的情况下依靠模式匹配。以下是一些简单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构造。遗憾的是，Idris大部分时间都无法推断出P，因此它变得有点笨重。另一种选择是将类型提取到一个引理中并使用rewrite，但是这并不总是有效的(例如，当replace使一个词的一大部分消失时)
• destruct -如果在单个变量上，尝试在LHS中拆分，否则使用with构造。
• induction -在LHS中拆分并在rewrite或直接中使用递归调用。确保递归中至少有一个参数在结构上更小，否则就会失败，不能将结果用作引理。对于更复杂的表达式，您也可以尝试使用SizeAccessible从Prelude.WellFounded。
• trivial -通常意味着尽可能多地在LHS中拆分，并使用Refl来解决。
• assert - where下的一个引理
• exists依赖对(x ** prf)
• case --不是case .. of就是with。但是，对case要小心--不要在以后想证明的任何事情中使用它，否则您将被困在rewrite上(参见第4001期)。解决办法是制作顶级(目前您不能参考where/with下的引理，请参阅第3991期)模式匹配助手。
• revert -通过创建lambda“取消”变量，然后将其应用于所述变量。
• inversion -手动定义和使用关于构造函数的平凡引理： -内射性，与cong/sym FooInj相同: Foo a= Foo b -> a=b FooInj ->l= Refl