将 Coq 转换为 Idris

Question

对于将 Coq 源代码转换为 Idris 有哪些有用的指导原则（例如，它们的类型系统有多相似以及如何翻译证明）？据我所知，Idris 的内置战术库很小但可扩展，所以我想通过一些额外的工作应该可以做到这一点。

Answer 1

我最近翻译了Software Foundations 的一部分，并做了{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，所以这变得有点笨重。另一种选择是将类型提取到引理中并使用rewrites，但这并不总是有效（例如，当replace 使大部分术语消失时）
• destruct - 如果在单个变量上，尝试在 LHS 中拆分，否则使用 with 构造
• induction - 在 LHS 中拆分并在 rewrite 中或直接使用递归调用。确保递归中的至少一个参数在结构上更小，否则您将完全失败并且无法将结果用作引理。对于更复杂的表达式，您还可以尝试 SizeAccessible from Prelude.WellFounded。
• trivial - 通常相当于在 LHS 中尽可能多地拆分并使用 Refls 解决
• assert - where 下的引理
• exists - 依赖对 (x ** prf)
• case - case .. of 或 with。但是要小心case - 不要在以后想要证明的任何事情中使用它，否则你会卡在rewrite 上（请参阅issue #4001）。一种解决方法是制作顶级（目前您不能在where/with 下引用引理，请参阅issue #3991）模式匹配助手。
• revert - 通过制作 lambda 并随后将其应用于所述变量来“取消引入”变量

• 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