My first proofs in Coq

Lately I’ve been spending some time working on Mike Nahas’s tutorial, for the Coq theorem prover.

Here’s a quick summary of what I’ve learned:

Coq is structured into 3 languages:
– Vernacular language – manages definitions, e.g. commands “Theorem”, “Proof”, “Qed”.
– Tactics language – the commands we use to do the proofs themselves, e.g. intros, pose, destruct, exact, etc.
– Gallina language – where we specify what we want to prove, e.g. (forall A B : Prop, A /\ B -> B).

Here’s the first proof I’ve managed to do myself:

Theorem my_first_proof : (forall A B : Prop, A /\ B -> B).
Proof.
  intros A B.     (* These are the Props *)
  intros A_and_B. (* This is A and B from the Gallina definition above *)
  destruct A_and_B as [proof_A proof_B].
  (* At this point we've destructed A_and_B innto proof_A : A and proof_B : B *)
  exact proof_B.  (* This is exactly proof_B *)
Qed.

And here’s how that looks in CoqIDE:

Here’s my second proof, which uses the pose tactic to do a rename:

Theorem my_second_proof : (forall A B : Prop, A -> (A -> B) -> B).
Proof.
  intros A B.     (* These are the Props *)
  intros proof_A. (* This is the proof of A *)
  intros A_imp_B. (* This is A -> B)
  pose (proof_B := A_imp_B proof_A).
  (* At this point, proof_B is actually the combination of A -> B and A, which is B *)
  exact proof_B.  (* And is exactly what we needed. We could've also just do  exact (A_imp_B proof_A). instead *)
Qed.

Proving conditionals:

Theorem my_third_proof : (forall A B : Prop, A -> A \/ B).
Proof.
  intros A B.
  intros proof_A.
  pose (proof_A_or_B := or_introl proof_A : A \/ B).
  exact proof_A_or_B.
Qed.

We had to use the built-in or_introl proof for the type “or”. Note that “Inductive” allows us to create a new type. In addition, we had to explicitly set the type of the proof_A_or_B.

Finally, let’s define our week days, have a function that calculates the next day and prove that after Monday comes Tuesday:

Inductive Day : Set :=
  | Mon : Day
  | Tue : Day
  | Wed : Day
  | Thu : Day
  | Fri : Day
  | Sat : Day
  | Sun : Day.

Definition Next (day : Day) : Day :=
  match day with
    | Mon => Tue
    | Tue => Wed
    | Wed => Thu
    | Thu => Fri
    | Fri => Sat
    | Sat => Sun
    | Sun => Mon
  end.

Eval compute in Next Mon.

Theorem after_monday_simple : ((Next Mon) = Tue).
Proof.
  simpl.         (* Evaluate (Next Mon) which is Tue as we've seen above *)
  exact eq_refl. (* This is exactly reflexivity on equality. *)

  (* Could also just use reflexivity here, but note that reflexivity does simpl implicitly *)
  (* reflexivity. (* Tue = Tue is proven by reflexivity *) *)
Qed.

Theorem after_monday : (forall A : Day, A = Mon -> Next A = Tue).
Proof.
  intros A.
  intros A_eq_Mon.
  rewrite A_eq_Mon. (* Instead of trying to prove Next A = Tue, try to prove Next Mon = Tue *)
  simpl.
  constructor.      (* Since reflexivity does simpl implicitly, it makes more sense to use this instead *)
Qed.

And some interesting discussion on #coq @ freenode:

 <bor0> how many tactic commands are there like in total? 😀
 <johnw> 191 in Coq 8.5
 <bor0> wow, that's a lot. and I've only got introduced to about 10 or so
 <johnw> you don't need to know all of them, by any means
 <johnw> some are the more basic tactics from which other tactics are built up
 <johnw> think of it like a standard tactic library
 <johnw> that's the beauty of all this: almost everything is just about types and finding inhabitants of types

Fun stuff, right? 🙂