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.
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:
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
- 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
If you love us? You can donate to us via Paypal or buy me a coffee so we can maintain and grow! Thank you!
Donate Us With