14

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

4

1 回答 1

8

我最近翻译了一大块软件基础并做了部分移植{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构造。遗憾的是，伊德里斯大部分时间都无法推断P，所以这变得有点笨重。另一种选择是将类型提取到引理中并使用rewrites，但这并不总是有效（例如，当replace使大部分术语消失时）
  • destruct- 如果在单个变量上，尝试在 LHS 中拆分，否则使用with构造
  • induction- 在 LHS 中拆分并在 arewrite或直接使用递归调用。确保递归中的至少一个参数在结构上更小，否则您将完全失败并且无法将结果用作引理。对于更复杂的表达式，您也可以尝试SizeAccessiblefrom Prelude.WellFounded。
  • trivial- 通常等于尽可能在 LHS 中拆分并用Refls求解
  • assert- 下的引理where
  • exists- 依赖对(x ** prf)
  • case- 要么case .. of要么with。但是要小心case- 不要在以后想要证明的任何事情中使用它，否则你会被卡住rewrite（参见问题 #4001）。一种解决方法是制作顶级（目前您不能在where/下引用引理with，请参阅问题 #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
于 2017-10-02T14:59:24.710 回答