Elimination rules play an important role in computations over datatypes in proof assistants like Coq. In his paper “Elimination with a Motive”, Conor McBride argued that “we should exploit a hypothesis not in terms of its immediate consequences, but in terms of the leverage it exerts on an arbitrary goal: we should give elimination a motive.” In other words, proofs in a refinement setting (backwards reasoning) should use their goals to guide elimination.
Read more...
So you may have heard about this popular new programming language called Haskell. What’s Haskell? Haskell is a non-dependently typed programming language, sporting general recursion, type inference and built-in side-effects. It is true that dependent types are considered an essential component of modern, expressive type systems. However, giving up dependence can result in certain benefits for other aspects of software engineering, and in this article, we’d like to talk about the omissions that Haskell makes to support these changes.
Read more...
In Software Foundations, equality is defined in this way:
Even Coq’s equality relation is not built in. It has (roughly) the following inductive definition. :
Inductive eq0 {X:Type} : X -> X -> Prop :=
refl_equal0 : forall x, eq0 x x.
Why the roughly? Well, as it turns out, Coq defines equality a little differently (reformatted to match the Software Foundations presentation):
Inductive eq1 {X:Type} (x:X) : X -> Prop :=
refl_equal1 : eq1 x x.
What’s the difference? The trick is to look at the induction principles that Coq generates for each of these:
Read more...
I spent some of my plane ride yesterday working on Coq versions of the exercises in The HoTT book. I got as far as 1.6 (yeah, not very far, perhaps I should make a GitHub repo if other folks are interested in contributing skeletons. Don’t know what to do about the solutions though). All of these have been test solved.
You will need HoTT/coq in order to run this development; instructions on how to install it are here.
Read more...