How to be bad at coq if you know idris

Relating to coq proofs if your frame of reference is idris.

I wanted to expand my reptoire and know more proof systems, so I took this weekend to learn coq.

I’m not as passable in it as idris yet, but there were some parts of its metaphor that I don’t feel got as good a treatment in its documentation as they might. I was helped in the late evening by:

• Vilem — https://twitter.com/buggymcbugfix

and

• Bob Atkey — https://twitter.com/bentnib

In figuring out how contradictions work in coq.

My first bad proof is here (note: this can be simplified and improved a lot… it’s the result of me banging my head into coq for a weekend to learn to use it passably).

https://gist.github.com/prozacchiwawa/95738434f2b9e24bf1c4b5c0d2097431

It’s a proof that for basic structural definitions of less than and div_2 on nat that for some number p less than r, p div 2 is less than r. It’s a fairly simple proof set, but enough to need to stretch one’s legs a bit and use the basic facilities of a proof assistant:

• Ability to fulfill obligations.
• Ability to dismiss obligations that are impossible (using dependencies between proofs).
• Ability to apply induction.

I’m writing this as a cheat sheet to try to match the search terms others (or me) might use when searching for specific tricks in coq.

Consider this function:

Fixpoint nat_lt (a : nat) (b : nat) : bool :=
  match b with
  | 0 => false
  | (S b1) =>
      match a with
      | 0 => true
      | (S a1) => nat_lt a1 b1
      end
  end.

Syntactically it’s mostly ocaml, but uses fat arrows (FP languages love not being consistent on that). And ends match expressions with end.

Every ‘statement’ in coq ends in a period. It’s more evident when you’re in proof mode and the statements are tactics.

This is a basic proof:

Lemma zero_zero_lt : nat_lt 0 0 = false.                             Proof.
  reflexivity.
Qed.

‘reflexivity’ is a tactic and tactics are interpreted in order and change some implicit state:

• The bound variables held by the prover.
• A stack of state machines that provide the next goal.

This isn’t visible in the source file, we’re relying on knowing what each tactic does to the state to know what’s permitted next. I recommend using coqide for this reason … it’s actually much better and more necessary than TLA+ toolbox, although it’d be nice if it wasn’t. You can use idris as a proof assistant entirely using the compiler and holes, and I prefer that tbh. Implicit in the IDE is the current expression. What you observe in its diagnostic windows is the state at the current statement, and it has controls to advance or retract.

There are good resources for coq if you look for them, but the style of proofs tends not to be similar to what you’d do in idris. Some documentation feels a bit more familiar than others, and I’d recommend

Coq Tactic Index

Which is a good brief intro to many common tactics in understandable language.

There were a few things I ran into that I didn’t feel had great explanations after the initial success of just producing valid coq with trivial proofs. The first was dismissing impossible goals.

Consider this with some annotation:

Lemma two_lt_n_means_1_lt_n (n : nat) (p : nat_lt 2 n = true) : nat_lt 1 n = true.
Proof.
  intros.
  case_eq n. (* push n = 0 and n = S n0 as variant proof goals *)
  eintros. (* bind H: n = 0 and n: 0 *)
  rewrite H in p. (* H is a hypothesis bound above, n = 0 *)
  (* any_lt_zero x -> nat_lt (S x) 0 = false *)
  rewrite (any_lt_zero 1) in p.
  (* if any proof in scope is a contradiction, dismiss this goal. *)
  discriminate.
  intros.
  case_eq n0.
  intros. (* bind n0 = 0 *)
  rewrite H in p.
  rewrite H0 in p.
  simpl in p.
  discriminate.
  intros.
  simpl.
  reflexivity.
Qed.

In idris, every name that’s accessible at the type level is in scope when constructing proofs since types aren’t runtime values. In coq, you have to use the ‘intros’ tactic to cause a binding that coq is capable of providing into the actual namespace. Some tactics affect how these are pulled in and named but I didn’t need them for my test.

I used ‘discriminate’ in many places to dismiss impossible goals. This tactic search the bindings for a proof that contains an obvious contradiction (such as (true = false) or (S 0) = 0. This is equivalent to idris’ impossible, but it will allow the goal to be retired if any proof you hold matches. If you’re within striking distance in a proof, you can use the ‘simpl’ tactic with ‘in’ to do as much substitution and simplification as possible in the proof. Note that the proof state is only affected in the current proof goal; when it’s retired, the modifications to the proof are reverted as well. The ‘inversion’ tactic can also do something similar regarding inductive types but I was able to get by using one tactic consistently.

A simple example might be like this:

consider the tactic above where we do:

rewrite (any_lt_zero 1) in p.

p is provided as a proof parameter, and was previously:

p : nat_lt 2 0 = true

But gets transformed to:

p : false = true

Because we have a binding with this obvious contradiction,

discriminate.

Can dismiss this goal and go on to the next, it looks like going from this:

2 goals
n : nat
p : false = true
H : n = 0
______________________________________(1/2)
nat_lt 1 0 = true
______________________________________(2/2)
forall n0 : nat, n = S n0 -> nat_lt 1 (S n0) = true

to this:

1 goal
n : nat
p : nat_lt 2 n = true
______________________________________(1/1)
forall n0 : nat, n = S n0 -> nat_lt 1 (S n0) = true

It took more time than I’d like to figure out how to do induction in proofs, and the simple answer was to declare the proof with the Fixpoint keyword instead of Lemma (which is similar to ocaml’s ‘let rec’ binding). At the end of the proof (usually in the complex case at the end) you’ll either ‘rewrite’ with a recursive use of the proof, or use the ‘apply tactic’ to provide a solution. coq will keep track of whether it understands how the induction terminates, and complain in an understandable way if it’s wrong. Coq is more sophisticated than idris about how it detects whether the recursion terminates, so I was able to trust it when it couldn’t detect how to terminate it. When you’ve used rewrites to produce a genuinely smaller input and used ‘apply’ to fulfill the current goal, coq will either allow the final Qed or reject it.