将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 $ c时) $ c>使一个词的大部分消失)
-
破坏
-如果是单个变量,请尝试在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 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 thereplace {P=\x=>...} equation term
construct. Sadly Idris is not able to inferP
most of the time, so this becomes a bit bulky. Another option is to extract the type into a lemma and userewrite
s, however this won't always work (e.g., whenreplace
makes a large chunk of a term disappear)destruct
- if on a single variable, try splitting in LHS, otherwise use thewith
constructinduction
- split in LHS and use a recursive call in arewrite
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 trySizeAccessible
fromPrelude.WellFounded
.trivial
- usually amounts to splitting in LHS as much as possible and solving withRefl
sassert
- a lemma underwhere
exists
- dependent pair(x ** prf)
case
- eithercase .. of
orwith
. Be careful withcase
however - don't use it in anything you will later want to prove things about, otherwise you'll get stuck onrewrite
(see issue #4001). A workaround is to make top-level (currently you can't refer to lemmas underwhere
/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
这篇关于将Coq转换为Idris的文章就介绍到这了,希望我们推荐的答案对大家有所帮助,也希望大家多多支持IT屋!