将Coq转换为Idris

Question

将Coq源转换为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大多数时间进行推断，因此这变得有些笨重。另一种选择是将类型提取到引理中并使用rewrites，但这并不总是有效（例如，当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 -通过创建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