将Coq转换为Idris

Question

将Coq转换为Idris

coqidris

13

如何将Coq源代码转换为Idris代码，有哪些有用的指导方针（例如它们的类型系统有多相似，如何翻译证明等）？据我所知，Idris的内置策略库很少但可扩展，因此我想这应该是可能的，只需进行一些额外的工作。

- Arets Paeglis

1

我很想通过Idris学习“软件基础”。这似乎是一个不错的学习方式。有6个赞和4颗星。有人可以提供反馈吗？许多新手都想知道。 - user1198582

1

这也许与本题无关，但我猜您可能想找一种既能进行证明又能进行编程的语言。您还可以直接使用 Coq 来进行编程，使用 (相当新的) Coq.io 库。该库向 Coq 添加了 IO 和并发原语，并采用某些技术对它们进行认证。完全披露：我是 Coq.io 的主要作者之一。 - Clarus

1个回答

网页内容由stack overflow 提供, 点击上面的

可以查看英文原文，
原文链接

- Alexander Gryzlov · Accepted Answer

我最近翻译了一部分Software Foundations，并进行了{P|N|Z}Arith的部分移植，在此过程中我发现了一些观察结果:

总体上讲，目前不太建议使用Idris Tactics（以它们的 Pruvloj/Elab.Reflection形式），这种方法有点脆弱，并且当出现问题时很难调试。最好使用所谓的“Agda风格”，尽可能依赖模式匹配。以下是一些简单Coq策略的粗略等价：

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