Coq provides two ways to finish definitions
Defined. The former is meant for “proofs” and makes the definition opaque while the later is meant for “definitions” and leaves the definition transparent. While the “proof” and “definition” dicotomy initially makes a lot of sense to users, but as users start to use dependent types more and more, they realize that the distinction is quite arbitrary, in which case, should we abandon
Qed? In this post, I argue that yes abandoning
Qedis a perfectly sensible thing to do.
You can now watch my thesis defense on computational reflection in intensional type theory. Some minor hicups during the talk but otherwise gives a very high-level overview of MirrorCore and Rtac at the time (2014).
During my post-doc at UCSD I’ve been working on verifying cyber-physical systems in the VeriDrone project. Cyber-physical systems are just systems that interact with the real world (think quadcopters, cars, planes, hydro-electric dams, and robots). The interesting thing about verifying cyber-physical systems in Coq is that they require a lot of reasoning about continuous mathematics, real numbers, differential equations, and all that. Coq does a great job at all of the discrete reasoning that we do (see my previous blog post on embedding logics in Coq) but at the end of all the nice theory, problems often boil down to mundane reasoning about real arithmetic. In this post I’m going to discuss a plugin that I wrote to call SMT solvers from Coq.
In this post I’m going to discuss Rtac the reflective tactic language that I developed as a central piece of my dissertation. The results there show how reflective tactics can be a game-changer in the ability to build very efficient automation. For comparison, the automation that I’m going to write in this post is a monoidal cancellation procedure and at the end of the post we’ll see that it scales substantially better than Ltac, e.g. on larger problems it is almost 2 orders of magnitude faster than Ltac.
Coq inductive data types are required to be strictly positive. In this article, I’ll discuss a bit about what this means, and I’ll show a simple technique to approximate an inductive data type. While not the paragon of computational efficiency, the technique that I describe here makes it possible to build inductive data types compositionally (though it only supports data-types with finite branching). In addition, it may serve as a less mathematical introduction to some of the concepts in fixpoints.
Coq comes with a powerful, built-in logic (Gallina) with features such as inductive and dependent types, recursion, etc. However, most uses of Coq don’t study its theory, but rather use it as a foundation to reason about something else. A few examples come to mind:
Computational reflection is a technique for extending proof assistants with efficient, domain-specific automation. There are a lot of interesting ideas in computational reflection but in this blog post I’m just going to cover a simple example, proving evenness of large constants. This example is purposefully extremely simple, and computational reflection is certainly capable of doing a lot more, but the very key pieces are here.