如何将Coq源代码转换为Idris代码,有哪些有用的指导方针(例如它们的类型系统有多相似,如何翻译证明等)?据我所知,Idris的内置策略库很少但可扩展,因此我想这应该是可能的,只需进行一些额外的工作。
如何将Coq源代码转换为Idris代码,有哪些有用的指导方针(例如它们的类型系统有多相似,如何翻译证明等)?据我所知,Idris的内置策略库很少但可扩展,因此我想这应该是可能的,只需进行一些额外的工作。
我最近翻译了一部分Software Foundations,并进行了{P|N|Z}Arith的部分移植,在此过程中我发现了一些观察结果:
总体上讲,目前不太建议使用Idris Tactics(以它们的 Pruvloj
/Elab.Reflection
形式),这种方法有点脆弱,并且当出现问题时很难调试。最好使用所谓的“Agda风格”,尽可能依赖模式匹配。以下是一些简单Coq策略的粗略等价:
intros
- just mention variables on the LHSreflexivity
- Refl
apply
- calling the function directlysimpl
- simplification is done automatically by Idrisunfold
- also done automatically for yousymmetry
- sym
congruence
/f_equal
- cong
split
- split in LHSrewrite
- 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 rewrite
s, 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
constructinduction
- 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 Refl
sassert
- 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 variableinversion
- 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