将Coq转换为Idris [英] Converting Coq to Idris

问题描述

将Coq来源转换为Idris的有用指南是什么（例如，它们的类型系统有多相似，如何翻译证明？）？据我所知，Idris的内置战术库极少但可扩展，因此我认为应该可以做一些额外的工作。

What would be some useful guidelines for converting Coq source to Idris (e.g. how similar are their type systems and what can be made of translating the proofs)? From what I gather, Idris' built-in library of tactics is minimal yet extendable, so I suppose with some extra work this should be possible.

推荐答案

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

I've recently translated a chunk of Software Foundations and did a partial port of {P|N|Z}Arith, some observations I've made in the process:

通常使用Idris战术（在他们的 Pruvloj / Elab.Reflection 形式）目前尚不推荐，此功能有些脆弱，出现问题时很难调试。最好使用所谓的 Agda样式，并尽可能使用模式匹配。以下是一些较为简单的Coq策略的大致等效项：

Generally using Idris tactics (in their Pruvloj/Elab.Reflection form) is not really recommended at the moment, this facility is somewhat fragile, and pretty hard to debug when something goes wrong. It's better to use the so-called "Agda style", relying on pattern matching where possible. Here are some rough equivalences for simpler Coq tactics:

• intros -仅提及变量在LHS上


• 自反性- Refl


• 应用-直接调用函数


• simpl -简化由Idris自动完成


• 展开-也为您自动完成


• 对称- sym


• 同余 / f_equal - cong


• split -在LHS中拆分


• 重写-重写...在


• 重写<--重写sym $ ... in


• 重写-要在内部将某些内容作为参数重写，可以使用 replace {P = \x => ...}方程项的构造。可悲的是，伊德里斯大部分时间都无法推断 P ，因此这变得有些笨重。另一种选择是将类型提取到引理中并使用 rewrite s，但这并不总是可行的（例如，当 replace 使一个词的大部分消失）


• 破坏-如果是单个变量，请尝试在LHS中拆分，否则使用 with 构造


• 归纳-在LHS中拆分并使用递归调用重写或直接调用。确保递归中的至少一个参数在结构上较小，否则您将无法通过合计并不能将结果用作引理。对于更复杂的表达式，您还可以尝试从 Prelude.WellFounded 中的 SizeAccessible 。


• 平凡的-通常等于在LHS中尽可能多地拆分，并使用 Refl s
$ b解决$ b
• 断言-其中
下的引理

• 存在-依赖对（x ** prf）


• case -的情况。或 with 。但是，在使用 case 时要小心-不要在以后要证明其用途的任何东西中使用它，否则，您将陷入 rewrite （请参见问题＃4001 ）。一种解决方法是将其设为顶层（当前，您不能在 / / 和下引用引理，请参见< a href = https://github.com/idris-lang/Idris-dev/issues/3991 rel = noreferrer>问题＃3991 ）模式匹配助手。


• 还原-通过创建lambda并随后将其应用于所述变量来引入变量



• inversion -手动定义并使用关于构造函数的琐碎引理：

• intros - just mention variables on the LHS
• reflexivity - Refl
• apply- calling the function directly
• simpl - simplification is done automatically by Idris
• unfold - also done automatically for you
• symmetry - sym
• congruence/f_equal - cong
• split - split in LHS
• rewrite - rewrite ... in
• rewrite <- - rewrite sym $ ... in
• rewrite in - to rewrite inside something you have as a parameter you can use the replace {P=\x=>...} equation term construct. Sadly Idris is not able to infer P most of the time, so this becomes a bit bulky. Another option is to extract the type into a lemma and use rewrites, however this won't always work (e.g., when replace makes a large chunk of a term disappear)
• destruct - if on a single variable, try splitting in LHS, otherwise use the with construct
• induction - split in LHS and use a recursive call in a rewrite or directly. Make sure that at least one of arguments in recursion is structurally smaller, or you'll fail totality and won't be able to use the result as a lemma. For more complex expressions you can also try SizeAccessible from Prelude.WellFounded.
• trivial - usually amounts to splitting in LHS as much as possible and solving with Refls
• assert - a lemma under where
• exists - dependent pair (x ** prf)
• case - either case .. of or with. Be careful with case however - don't use it in anything you will later want to prove things about, otherwise you'll get stuck on rewrite (see issue #4001). A workaround is to make top-level (currently you can't refer to lemmas under where/with, see issue #3991) pattern-matching helpers.
• revert - "unintroduce" a variable by making a lambda and later applying it to said variable

• inversion - manually define and use trivial lemmas about constructors:

-- 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   

这篇关于将Coq转换为Idris的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！