In order to understand things clearly and to learn Coq proof assistant at the same time, I’ve decided to do some proves while reading the TAPL book.

The code is on the GitHub.

For the excercises I want to use the ssreflect proof language instead of ltac. I’ll keep solutions to each chapter in a separate file. We’ll always work in the following context:

Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.
From Coq Require Import ssreflect.

I’ll start with the operational semantics of boolean expressions. Here is the definition in Coq:

Inductive term : Type :=
| T_true
| T_false
| T_cond (cond t1 t2 : term).

Let’s introduce a custom grammar entry for expressiveness.

Declare Custom Entry term.

Notation "[ e ]" := e (e custom term at level 2).
Notation "( x )" := x (in custom term, x at level 2).

Notation "'true'"  := (T_true)  (in custom term at level 0).
Notation "'false'" := (T_false) (in custom term at level 0).

Notation "'if' cond 'then' t1 'else' t2" :=
  (T_cond cond t1 t2) (in custom term at level 2).

Notation "x" := x (in custom term at level 0, x constr at level 0).

We can check that it works as expected:

Check [ true ].
Check fun cond t1 t2 => [ if cond then t1 else t2 ].
Unset Printing Notations.
Check fun cond t1 t2 => [ if cond then t1 else t2 ].
Set Printing Notations.

The ==> notation represents an evaluation relation on terms: “t evaluates to t' in one step” (as per p.35)

Reserved Notation "t ==> t'" (at level 50).

This relation is defined by three inference rules:

Inductive eval_step : term -> term -> Prop :=
| E_IfTrue  : forall t1 t2, [ if true  then t1 else t2 ] ==> t1
| E_IfFalse : forall t1 t2, [ if false then t1 else t2 ] ==> t2
| E_If : forall c c' t1 t2, c ==> c' -> [ if c then t1 else t2] ==> [ if c' then t1 else t2 ]
where "e ==> e'" := (eval_step e e').

Definition: an instance of an inference rule is obtained by consistently replace each metavariable by the same term in the rule’s conclusion and all its premises (if any).

The example instance of the E_IfTrue rule:

Theorem ex_inst_e_iftrue :
  [ if true then true else (if false then false else false) ] ==> [ true ].
Proof. by apply: E_IfTrue. Qed.

Definition: The one-step evaluation relation ==> is the smallest binary relation on terms satisfying the three rules in eval_step. When the pair (t, t') is in the evaluation relation, we say that “the evaluation statement (or judgment) t ==> t' is derivable”.

Let’s show an example of a derivable evaluation statememt. We’ll use these 3 abbreviations (they are taken from the book as is):

The proof is by construction of a derivation “tree”:

Module Ex_3_5_3.
  Definition s := [ if true  then false else false ].
  Definition t := [ if s     then true  else true  ].
  Definition u := [ if false then true  else true  ].

  Theorem ex :
    [ if t then false else false ] ==> [ if u then false else false ].
  Proof.
    apply: E_If.
    (*                             t ==> u
       [ if s then true else true  ] ==> [ if false then true else true  ] *)
    apply: E_If.
    (*                                 s ==> [ false ]
       [ if true then false else false ] ==> [ false ] *)
    exact: E_IfTrue.

    Restart.

    by do 2! apply: E_If; exact: E_IfTrue.
  Qed.
End Ex_3_5_3.

Theorem [Determinacy of one-step evaluation]: if t ==> t' and t ==> t'', then t' = t''.

Theorem eval_step_is_det :
  forall t t' t'' : term,
    (t ==> t') /\ (t ==> t'') -> t' = t''.
  Proof.
  (* I haven’t came up with a proof yet *)
  Abort.

It would be much easier to define the one-step evaluation as a function instead:

Fixpoint one_step (t : term) : term :=
match t with
| T_cond T_true t1 t2 => t1
| T_cond T_false t1 t2 => t2
| T_cond cond t1 t2 => T_cond (one_step cond) t1 t2
| t => t
end.

A separate notation for our fixpoint-definition:

Notation "t ==>> t'" := (one_step t = t') (at level 50).

Now, it is much simplier to proove it:

Theorem one_step_is_det t t' t'':
  t ==>> t' /\ t ==>> t'' -> t' = t''.
Proof.
  move=> [] H1 H2.
  rewrite -H1 -H2.
  done.

  Restart.

  (* Idiomatic proof *)
  by move=> [] ->.
Qed.

Let’s define a notion of the “normal form”.

Definition nf t := t ==>> t.

Theorem 3.5.7: Every value is in normal form.

The proof is trivial:

Theorem vnf : nf [[ true ]] /\ nf [[ false ]].
Proof. by []. Qed.

Theorem 3.5.8: If t is in normal form, then t is a value.

Summary Link to heading

TODO