A gentle overview to the Coq proof assistant

Gallina

Coq relies first and foremost on Gallina, a purely functional language equipped with a particularly rich type system. To a very rough first approximation, you can think about the functional fragment of OCaml.

Inductive types

Gallina relies on a powerful tool to define data-types: so-called inductive types. Intuitively, an inductive type is defined by a finite set of constructors describing how values of this type can be built. They encompass the type constructors you may be familiar with, and more.

Sum types

Here are a simple enumerated types containing exactly four values, as well as the booleans as implemented in the standard library.

Inductive Suit : Type := Spades | Hearts | Diamonds | Clubs.
Inductive bool : Type := true | false.

We can pattern match on values of inductive types to start programming

Definition is_red (card : Suit) : bool :=
match card with
| Hearts | Diamonds => true
| _                 => false
end.

Definition is_pointy (card : Suit) : bool :=
match card with
| Spades | Diamonds => true
| _                 => false
end.

Patterns must always be exhaustive: here we use "_" as a wild card.

We can ask Coq to compute for us.

Compute (is_red Hearts).
= true
: bool

But we can also state our first "theorem": writing as an assertion what we expect to get as an answer.

This time we are provided with an interactive goal: a separate window displays our proof context and goal. In order to _prove_ this fact, we are going to use some mysterious commands that are not part of Gallina: tactics.

This proof is an example of a proof by simple reduction and reflexivity.

Example test_next_weekday:
  is_red Hearts = true.
is_red Hearts = true
Proof.
is_red Hearts = true
  simpl.       (* We reduce our goal by computation *)
true = true
  reflexivity. (* Equality between a term and itself *)
Qed.

The constructors of an inductive types provide the _only_ ways to construct elements of this type. We can exploit this fact to prove lemmas by case analysis.

Lemma pointy_and_red:
  forall (c : Suit),
    is_red c = true ->
    is_pointy c = true ->
    c = Diamonds.
forall c : Suit,
is_red c = true -> is_pointy c = true -> c = Diamonds
Proof.
forall c : Suit,
is_red c = true -> is_pointy c = true -> c = Diamonds
  intros c ISRED ISPOINTY. (* We introduce our hypotheses *)
c:Suit
ISRED:is_red c = true
ISPOINTY:is_pointy c = true
c = Diamonds
  destruct c. (* Case analysis on c *)
ISRED:is_red Spades = true
ISPOINTY:is_pointy Spades = true
Spades = Diamonds
ISRED:is_red Hearts = true
ISPOINTY:is_pointy Hearts = true
Hearts = Diamonds
ISRED:is_red Diamonds = true
ISPOINTY:is_pointy Diamonds = true
Diamonds = Diamonds
ISRED:is_red Clubs = true
ISPOINTY:is_pointy Clubs = true
Clubs = Diamonds
  -
ISRED:is_red Spades = true
ISPOINTY:is_pointy Spades = true
Spades = Diamonds simpl in *.
ISRED:false = true
ISPOINTY:true = true
Spades = Diamonds
    discriminate ISRED.
  -
ISRED:is_red Hearts = true
ISPOINTY:is_pointy Hearts = true
Hearts = Diamonds simpl in *.
ISRED:true = true
ISPOINTY:false = true
Hearts = Diamonds
    discriminate ISPOINTY.
  -
ISRED:is_red Diamonds = true
ISPOINTY:is_pointy Diamonds = true
Diamonds = Diamonds reflexivity.
  -
ISRED:is_red Clubs = true
ISPOINTY:is_pointy Clubs = true
Clubs = Diamonds simpl in *.
ISRED, ISPOINTY:false = true
Clubs = Diamonds
    discriminate ISPOINTY.
Qed.

We have been using tactics to prove our lemmas interactively. This may look a little bit mysterious. Tactics are part of a completely different language from Gallina, called [Ltac]. This language provide some primitive tactics, and a wild effectful, untyped, language to build new tactics! We won't discuss much how to write tactics in this introduction, but it allows for some extremely powerful proof automation.

It however begs a question: isn't this complex unsafe language ruining all our trust? Luckily, no. Tactics serve only one purpose: they build Gallina terms behind the scene. What guarantees the validity of the theorem is the [Qed] steps: it uses the trusted core of Coq to type check the term, without caring by which magical process it may have been built.

Actually, we can even check that I'm not lying: we can print the term that has been built. Discriminate leads to something a bit mysterious, but we can notice the pattern match corresponding to destruct, and the intros becoming binders.

Print pointy_and_red.
pointy_and_red = 
fun (c : Suit) (ISRED : is_red c = true)
  (ISPOINTY : is_pointy c = true) =>
match
  c as s
  return
    (is_red s = true ->
     is_pointy s = true -> s = Diamonds)
with
| Spades =>
    fun (ISRED0 : is_red Spades = true)
      (_ : is_pointy Spades = true) =>
    let H : False :=
      eq_ind false
        (fun e : bool =>
         match e with
         | true => False
         | false => True
         end) I true ISRED0 in
    False_ind (Spades = Diamonds) H
| Hearts =>
    fun (_ : is_red Hearts = true)
      (ISPOINTY0 : is_pointy Hearts = true) =>
    let H : False :=
      eq_ind false
        (fun e : bool =>
         match e with
         | true => False
         | false => True
         end) I true ISPOINTY0 in
    False_ind (Hearts = Diamonds) H
| Diamonds =>
    fun (_ : is_red Diamonds = true)
      (_ : is_pointy Diamonds = true) => eq_refl
| Clubs =>
    fun (_ : is_red Clubs = true)
      (ISPOINTY0 : is_pointy Clubs = true) =>
    let H : False :=
      eq_ind false
        (fun e : bool =>
         match e with
         | true => False
         | false => True
         end) I true ISPOINTY0 in
    False_ind (Clubs = Diamonds) H
end ISRED ISPOINTY
     : forall c : Suit,
       is_red c = true ->
       is_pointy c = true -> c = Diamonds

We will come back to proofs and tactics in greater details in a moment, let's focus on programming for now.

Polymorphism

Gallina supports full polymorphic types.

Inductive option (A : Type) : Type :=
| None
| Some : A -> option A.

Product types

Your usual polymorphic product type is just a particular inductive type. We introduce two

Inductive prod (A B : Type) : Type :=
| pair : A -> B -> prod A B.

Recursive types

So far, we have only manipulated base constructors. Recursive types are simply created by having recursive constructors.

Inductive nat : Type :=
| O 
| S : nat -> nat.

Now that we have a recursive type, we naturally want to write recursive functions!

Fixpoint sum (n m : nat) : nat :=
  match n with
  | O => m
  | S n => S (sum n m)
  end.
Infix "+" := sum.

When it comes to proving, implementation matters even more than in usual programming! The proofs of the following two statements will be radically different: 1. forall n, 0 + n = n 2. forall n, n + 0 = n Can you foresee why?

Lemma sum_n_O : forall n,
    O + n = n.
forall n : nat, O + n = n
Proof.
forall n : nat, O + n = n
  intros n.
n:nat
O + n = n
  simpl.
n:nat
n = n
  reflexivity.
Qed.

Lemma sum_O_n : forall n,
    n + O = n.
forall n : nat, n + O = n
Proof.
forall n : nat, n + O = n
  intros n.
n:nat
n + O = n
  simpl. (* Nothing happens! *)
n:nat
n + O = n
  Fail reflexivity. (* We cannot conclude by reflexivity *)
The command has indeed failed with message:
In environment
n : nat
Unable to unify "n" with "n + O".
n:nat
n + O = n
  (* We could try by case analysis *)
  destruct n as [| n].
O + O = O
n:nat
S n + O = S n
  reflexivity.
n:nat
S n + O = S n
  simpl.
n:nat
S (n + O) = S n
  f_equal. (* We eliminate the S *)
n:nat
n + O = n
  (* We are back to square one *)
  Undo 6.
n:nat
n + O = n
  (* We are going to proceed by induction *)
  induction n as [| n IH].
O + O = O
n:nat
IH:n + O = n
S n + O = S n
  -
O + O = O reflexivity. (* Base case *)
  -
n:nat
IH:n + O = n
S n + O = S n simpl.
n:nat
IH:n + O = n
S (n + O) = S n
    f_equal.
n:nat
IH:n + O = n
n + O = n
    apply IH.
Qed.

And since Paul taught us some Origami last week, let's play with lists and folds.

Inductive list (A : Type) : Type :=
| Nil : list A
| Cons : A -> list A -> list A.

A pretty cool detail: Coq provides great facilities to extend the grammar of the language. (Great as in extremely expressive, but hence can get tricky to use!)

Notation "'[]'" := Nil.
Notation "hd '::' tl" := (Cons hd tl).

Here's a trivial recursive version of the [length] of a list

Fixpoint length {A} (l : list A) : nat :=
  match l with
  | [] => O
  | _ :: tl => S (length tl)
  end.

And here is a version using [fold]

Fixpoint fold {A B} (f : A -> B -> B) (acc : B) (l: list A) :=
  match l with
  | [] => acc
  | x :: xs => f x (fold f acc xs)
  end.

Definition length' {A} : list A -> nat := fold (fun _ k => S k) O.

Can you prove that they are (extensionally) equal?

Lemma length_is_length' :
  forall {A} (l : list A),
    length l = length' l.
forall (A : Type) (l : list A), length l = length' l
Proof.
forall (A : Type) (l : list A), length l = length' l
  (* EXERCISE! You may want to use a tactic we have not seen yet: `rewrite` *)
Admitted.

Prop

We have defined so far several datatypes : nats, booleans, lists, ... Each of these were devised to intuitively represent collections of objects, each of which we care to distinguish. As such, they have all had the sort [Type]. We have then defined functions computing specific elements of these types, and even reasoned a bit about the specific elements these functions compute.

I have actaully lied slightly; there are a few cases we have gone off trail : when we have stated these properties. Indeed, we have pondered whether two terms were equal: let's check the type of such a foe.

Check (3 = 2).
3 = 2
     : Prop

The answer we get is [Prop], the sort of propositions. There are a few subtleties differentiating [Type] and [Prop], but for Today we will stick to a simple pragmatic idea: - we define in [Type] the collections of which we care about the particular elements, and whose functions we care about the computational content: that is what you would define in traditional programming languages - we define in [Prop] the properties, of which we only care if they are inhabited (i.e. they hold true) or if they are not inhabited (i.e. they are False).

Let's do a little bit of elementary logic to explore this.

What is our traditional notion of truth? It's the type that has a unique inhabitant:

Inductive True : Prop := I : True.

And of course what is False? The vaccuous type, that contains no inhabitant. As an inductive type, it has simply no constructors: it is impossible to build a value for this type.

Inductive False : Prop :=. 

Naturally, we can define the propositional combinators we are used to manipulate. For instance the conjunction of two propositions: notice that the constructor is the usual introduction rule.

Inductive and (A B : Prop) : Prop := conj : A -> B -> and A B.

EXERCISE! Can you define the disjunction?

End NotationConflict.

Let's prove that [and] is associative!

Theorem and_assoc : forall P Q R : Prop,
  P /\ (Q /\ R) -> (P /\ Q) /\ R.
forall P Q R : Prop, P /\ Q /\ R -> (P /\ Q) /\ R
Proof.
forall P Q R : Prop, P /\ Q /\ R -> (P /\ Q) /\ R
  intros P Q R H.
P, Q, R:Prop
H:P /\ Q /\ R
(P /\ Q) /\ R
  destruct H as [HP [HQ HR]].
P, Q, R:Prop
HP:P
HQ:Q
HR:R
(P /\ Q) /\ R
  split.
P, Q, R:Prop
HP:P
HQ:Q
HR:R
P /\ Q
P, Q, R:Prop
HP:P
HQ:Q
HR:R
R
  -
P, Q, R:Prop
HP:P
HQ:Q
HR:R
P /\ Q split.
P, Q, R:Prop
HP:P
HQ:Q
HR:R
P
P, Q, R:Prop
HP:P
HQ:Q
HR:R
Q
    +
P, Q, R:Prop
HP:P
HQ:Q
HR:R
P exact HP.
    +
P, Q, R:Prop
HP:P
HQ:Q
HR:R
Q exact HQ.
  -
P, Q, R:Prop
HP:P
HQ:Q
HR:R
R exact HR.
Qed.

EXERCISE! Can you write the proof without using any tactic, by programming it directly? You can simply print [and_assoc] to check a possible answer.

Note: Coq does not assume excluded middle by default, but it is compatible with it: it is up to the user to decide whether they want to prove things constructively or not.

Definition excluded_middle := forall P : Prop,
  P \/ ~ P.

By using functions into [Prop], we can define properties of the arguments of this function. For instance, here is the property of a function to be injective.

Definition injective {A B} (f : A -> B) :=
  forall x y : A, f x = f y -> x = y.

But since we do not care about the computational content, we even get an additional liberty: we can define such properties using inductive types. Here is the property of a natural number to be even

Inductive even : nat -> Prop :=
| evenO  : even 0
| evenSS : forall n, even n -> even (S (S n))
.

The latter style has an attracting aspect: as our inductive data-types came with induction principles, so do our inductive properties! Think for instance when you establish a property by induction on the type derivation of a term: you are not inducting over the term, nore the type, but over the proof of well-typedness of the term at a type.

Fixpoint double (n:nat) :=
  match n with
  | O => O
  | S n' => S (S (double n'))
  end.

Lemma even_double : forall n,
  even n -> exists k, n = double k.
forall n : nat, even n -> exists k : nat, n = double k
Proof.
forall n : nat, even n -> exists k : nat, n = double k
  (* Can you prove this result by induction on the evidence that [n] is [even]? *)
Admitted.

End Logic.

Pure expressions

Let's start by defining the abstract syntax of a little language of arithmetic expressions.

Inductive aexp : Type :=
  | ANum (n : nat)
  | APlus (a1 a2 : aexp)
  | AMinus (a1 a2 : aexp)
  | AMult (a1 a2 : aexp).

This mini-language is particularly simple: it is pure, in particular it can neither fail nor diverge. We can therefore easily represent its semantics directly as Gallina computations by implementing an interpreter.

Fixpoint aeval (a : aexp) : nat :=
  match a with
  | ANum n => n
  | APlus  a1 a2 => (aeval a1) + (aeval a2)
  | AMinus a1 a2 => (aeval a1) - (aeval a2)
  | AMult  a1 a2 => (aeval a1) * (aeval a2)
  end.

Let's get ambitious and prove a quite complex optimization: we can substitute "0 + e" by "e" in arithmetic expressions!

First, we need to program our optimization as a Gallina function.

Fixpoint optimize_0plus (a:aexp) : aexp :=
  match a with
  | ANum n => ANum n
  | APlus (ANum 0) e2 => optimize_0plus e2
  | APlus  e1 e2 => APlus  (optimize_0plus e1) (optimize_0plus e2)
  | AMinus e1 e2 => AMinus (optimize_0plus e1) (optimize_0plus e2)
  | AMult  e1 e2 => AMult  (optimize_0plus e1) (optimize_0plus e2)
  end.

Now we can state our theorem: any arithmetic expression has the same semantics before and after optimization.

Things are looking good for us: both the semantics and the optimization are defined by recursion on the structure of our expressions, we have a good chance of success by induction on this structure!

Theorem optimize_0plus_sound: forall a,
  aeval (optimize_0plus a) = aeval a.
forall a : aexp, aeval (optimize_0plus a) = aeval a
Proof.
forall a : aexp, aeval (optimize_0plus a) = aeval a
  intros a.
a:aexp
aeval (optimize_0plus a) = aeval a induction a.
n:nat
aeval (optimize_0plus (ANum n)) = aeval (ANum n)
a1, a2:aexp
IHa1:aeval (optimize_0plus a1) = aeval a1
IHa2:aeval (optimize_0plus a2) = aeval a2
aeval (optimize_0plus (APlus a1 a2)) =
aeval (APlus a1 a2)
a1, a2:aexp
IHa1:aeval (optimize_0plus a1) = aeval a1
IHa2:aeval (optimize_0plus a2) = aeval a2
aeval (optimize_0plus (AMinus a1 a2)) =
aeval (AMinus a1 a2)
a1, a2:aexp
IHa1:aeval (optimize_0plus a1) = aeval a1
IHa2:aeval (optimize_0plus a2) = aeval a2
aeval (optimize_0plus (AMult a1 a2)) =
aeval (AMult a1 a2)
  - (* ANum *)
n:nat
aeval (optimize_0plus (ANum n)) = aeval (ANum n) reflexivity.
  - (* APlus *)
a1, a2:aexp
IHa1:aeval (optimize_0plus a1) = aeval a1
IHa2:aeval (optimize_0plus a2) = aeval a2
aeval (optimize_0plus (APlus a1 a2)) =
aeval (APlus a1 a2) destruct a1 eqn:Ea1.
a1, a2:aexp
n:nat
Ea1:a1 = ANum n
IHa1:aeval (optimize_0plus (ANum n)) =
aeval (ANum n)
IHa2:aeval (optimize_0plus a2) = aeval a2
aeval (optimize_0plus (APlus (ANum n) a2)) =
aeval (APlus (ANum n) a2)
a1, a2, a3, a4:aexp
Ea1:a1 = APlus a3 a4
IHa1:aeval (optimize_0plus (APlus a3 a4)) =
aeval (APlus a3 a4)
IHa2:aeval (optimize_0plus a2) = aeval a2
aeval (optimize_0plus (APlus (APlus a3 a4) a2)) =
aeval (APlus (APlus a3 a4) a2)
a1, a2, a3, a4:aexp
Ea1:a1 = AMinus a3 a4
IHa1:aeval (optimize_0plus (AMinus a3 a4)) =
aeval (AMinus a3 a4)
IHa2:aeval (optimize_0plus a2) = aeval a2
aeval (optimize_0plus (APlus (AMinus a3 a4) a2)) =
aeval (APlus (AMinus a3 a4) a2)
a1, a2, a3, a4:aexp
Ea1:a1 = AMult a3 a4
IHa1:aeval (optimize_0plus (AMult a3 a4)) =
aeval (AMult a3 a4)
IHa2:aeval (optimize_0plus a2) = aeval a2
aeval (optimize_0plus (APlus (AMult a3 a4) a2)) =
aeval (APlus (AMult a3 a4) a2)
    + (* a1 = ANum n *)
a1, a2:aexp
n:nat
Ea1:a1 = ANum n
IHa1:aeval (optimize_0plus (ANum n)) =
aeval (ANum n)
IHa2:aeval (optimize_0plus a2) = aeval a2
aeval (optimize_0plus (APlus (ANum n) a2)) =
aeval (APlus (ANum n) a2) destruct n eqn:En.
a1, a2:aexp
n:nat
En:n = 0
Ea1:a1 = ANum 0
IHa1:aeval (optimize_0plus (ANum 0)) =
aeval (ANum 0)
IHa2:aeval (optimize_0plus a2) = aeval a2
aeval (optimize_0plus (APlus (ANum 0) a2)) =
aeval (APlus (ANum 0) a2)
a1, a2:aexp
n, n0:nat
En:n = S n0
Ea1:a1 = ANum (S n0)
IHa1:aeval (optimize_0plus (ANum (S n0))) =
aeval (ANum (S n0))
IHa2:aeval (optimize_0plus a2) = aeval a2
aeval (optimize_0plus (APlus (ANum (S n0)) a2)) =
aeval (APlus (ANum (S n0)) a2)
      * (* n = 0 *)
a1, a2:aexp
n:nat
En:n = 0
Ea1:a1 = ANum 0
IHa1:aeval (optimize_0plus (ANum 0)) =
aeval (ANum 0)
IHa2:aeval (optimize_0plus a2) = aeval a2
aeval (optimize_0plus (APlus (ANum 0) a2)) =
aeval (APlus (ANum 0) a2)  simpl.
a1, a2:aexp
n:nat
En:n = 0
Ea1:a1 = ANum 0
IHa1:aeval (optimize_0plus (ANum 0)) =
aeval (ANum 0)
IHa2:aeval (optimize_0plus a2) = aeval a2
aeval (optimize_0plus a2) = aeval a2 apply IHa2.
      * (* n <> 0 *)
a1, a2:aexp
n, n0:nat
En:n = S n0
Ea1:a1 = ANum (S n0)
IHa1:aeval (optimize_0plus (ANum (S n0))) =
aeval (ANum (S n0))
IHa2:aeval (optimize_0plus a2) = aeval a2
aeval (optimize_0plus (APlus (ANum (S n0)) a2)) =
aeval (APlus (ANum (S n0)) a2) simpl.
a1, a2:aexp
n, n0:nat
En:n = S n0
Ea1:a1 = ANum (S n0)
IHa1:aeval (optimize_0plus (ANum (S n0))) =
aeval (ANum (S n0))
IHa2:aeval (optimize_0plus a2) = aeval a2
S (n0 + aeval (optimize_0plus a2)) = S (n0 + aeval a2) rewrite IHa2.
a1, a2:aexp
n, n0:nat
En:n = S n0
Ea1:a1 = ANum (S n0)
IHa1:aeval (optimize_0plus (ANum (S n0))) =
aeval (ANum (S n0))
IHa2:aeval (optimize_0plus a2) = aeval a2
S (n0 + aeval a2) = S (n0 + aeval a2) reflexivity.
    + (* a1 = APlus a1_1 a1_2 *)
a1, a2, a3, a4:aexp
Ea1:a1 = APlus a3 a4
IHa1:aeval (optimize_0plus (APlus a3 a4)) =
aeval (APlus a3 a4)
IHa2:aeval (optimize_0plus a2) = aeval a2
aeval (optimize_0plus (APlus (APlus a3 a4) a2)) =
aeval (APlus (APlus a3 a4) a2)
      simpl.
a1, a2, a3, a4:aexp
Ea1:a1 = APlus a3 a4
IHa1:aeval (optimize_0plus (APlus a3 a4)) =
aeval (APlus a3 a4)
IHa2:aeval (optimize_0plus a2) = aeval a2
aeval
  match a3 with
  | ANum 0 => optimize_0plus a4
  | _ => APlus (optimize_0plus a3) (optimize_0plus a4)
  end + aeval (optimize_0plus a2) =
aeval a3 + aeval a4 + aeval a2 simpl in IHa1.
a1, a2, a3, a4:aexp
Ea1:a1 = APlus a3 a4
IHa1:aeval
  match a3 with
  | ANum 0 => optimize_0plus a4
  | _ =>
      APlus (optimize_0plus a3)
        (optimize_0plus a4)
  end = aeval a3 + aeval a4
IHa2:aeval (optimize_0plus a2) = aeval a2
aeval
  match a3 with
  | ANum 0 => optimize_0plus a4
  | _ => APlus (optimize_0plus a3) (optimize_0plus a4)
  end + aeval (optimize_0plus a2) =
aeval a3 + aeval a4 + aeval a2 rewrite IHa1.
a1, a2, a3, a4:aexp
Ea1:a1 = APlus a3 a4
IHa1:aeval
  match a3 with
  | ANum 0 => optimize_0plus a4
  | _ =>
      APlus (optimize_0plus a3)
        (optimize_0plus a4)
  end = aeval a3 + aeval a4
IHa2:aeval (optimize_0plus a2) = aeval a2
aeval a3 + aeval a4 + aeval (optimize_0plus a2) =
aeval a3 + aeval a4 + aeval a2
      rewrite IHa2.
a1, a2, a3, a4:aexp
Ea1:a1 = APlus a3 a4
IHa1:aeval
  match a3 with
  | ANum 0 => optimize_0plus a4
  | _ =>
      APlus (optimize_0plus a3)
        (optimize_0plus a4)
  end = aeval a3 + aeval a4
IHa2:aeval (optimize_0plus a2) = aeval a2
aeval a3 + aeval a4 + aeval a2 =
aeval a3 + aeval a4 + aeval a2 reflexivity.
    + (* a1 = AMinus a1_1 a1_2 *)
a1, a2, a3, a4:aexp
Ea1:a1 = AMinus a3 a4
IHa1:aeval (optimize_0plus (AMinus a3 a4)) =
aeval (AMinus a3 a4)
IHa2:aeval (optimize_0plus a2) = aeval a2
aeval (optimize_0plus (APlus (AMinus a3 a4) a2)) =
aeval (APlus (AMinus a3 a4) a2)
      simpl.
a1, a2, a3, a4:aexp
Ea1:a1 = AMinus a3 a4
IHa1:aeval (optimize_0plus (AMinus a3 a4)) =
aeval (AMinus a3 a4)
IHa2:aeval (optimize_0plus a2) = aeval a2
aeval (optimize_0plus a3) - aeval (optimize_0plus a4) +
aeval (optimize_0plus a2) =
aeval a3 - aeval a4 + aeval a2 simpl in IHa1.
a1, a2, a3, a4:aexp
Ea1:a1 = AMinus a3 a4
IHa1:aeval (optimize_0plus a3) -
aeval (optimize_0plus a4) = 
aeval a3 - aeval a4
IHa2:aeval (optimize_0plus a2) = aeval a2
aeval (optimize_0plus a3) - aeval (optimize_0plus a4) +
aeval (optimize_0plus a2) =
aeval a3 - aeval a4 + aeval a2 rewrite IHa1.
a1, a2, a3, a4:aexp
Ea1:a1 = AMinus a3 a4
IHa1:aeval (optimize_0plus a3) -
aeval (optimize_0plus a4) = 
aeval a3 - aeval a4
IHa2:aeval (optimize_0plus a2) = aeval a2
aeval a3 - aeval a4 + aeval (optimize_0plus a2) =
aeval a3 - aeval a4 + aeval a2
      rewrite IHa2.
a1, a2, a3, a4:aexp
Ea1:a1 = AMinus a3 a4
IHa1:aeval (optimize_0plus a3) -
aeval (optimize_0plus a4) = 
aeval a3 - aeval a4
IHa2:aeval (optimize_0plus a2) = aeval a2
aeval a3 - aeval a4 + aeval a2 =
aeval a3 - aeval a4 + aeval a2 reflexivity.
    + (* a1 = AMult a1_1 a1_2 *)
a1, a2, a3, a4:aexp
Ea1:a1 = AMult a3 a4
IHa1:aeval (optimize_0plus (AMult a3 a4)) =
aeval (AMult a3 a4)
IHa2:aeval (optimize_0plus a2) = aeval a2
aeval (optimize_0plus (APlus (AMult a3 a4) a2)) =
aeval (APlus (AMult a3 a4) a2)
      simpl.
a1, a2, a3, a4:aexp
Ea1:a1 = AMult a3 a4
IHa1:aeval (optimize_0plus (AMult a3 a4)) =
aeval (AMult a3 a4)
IHa2:aeval (optimize_0plus a2) = aeval a2
aeval (optimize_0plus a3) * aeval (optimize_0plus a4) +
aeval (optimize_0plus a2) =
aeval a3 * aeval a4 + aeval a2 simpl in IHa1.
a1, a2, a3, a4:aexp
Ea1:a1 = AMult a3 a4
IHa1:aeval (optimize_0plus a3) *
aeval (optimize_0plus a4) = 
aeval a3 * aeval a4
IHa2:aeval (optimize_0plus a2) = aeval a2
aeval (optimize_0plus a3) * aeval (optimize_0plus a4) +
aeval (optimize_0plus a2) =
aeval a3 * aeval a4 + aeval a2 rewrite IHa1.
a1, a2, a3, a4:aexp
Ea1:a1 = AMult a3 a4
IHa1:aeval (optimize_0plus a3) *
aeval (optimize_0plus a4) = 
aeval a3 * aeval a4
IHa2:aeval (optimize_0plus a2) = aeval a2
aeval a3 * aeval a4 + aeval (optimize_0plus a2) =
aeval a3 * aeval a4 + aeval a2
      rewrite IHa2.
a1, a2, a3, a4:aexp
Ea1:a1 = AMult a3 a4
IHa1:aeval (optimize_0plus a3) *
aeval (optimize_0plus a4) = 
aeval a3 * aeval a4
IHa2:aeval (optimize_0plus a2) = aeval a2
aeval a3 * aeval a4 + aeval a2 =
aeval a3 * aeval a4 + aeval a2 reflexivity.
  - (* AMinus *)
a1, a2:aexp
IHa1:aeval (optimize_0plus a1) = aeval a1
IHa2:aeval (optimize_0plus a2) = aeval a2
aeval (optimize_0plus (AMinus a1 a2)) =
aeval (AMinus a1 a2)
    simpl.
a1, a2:aexp
IHa1:aeval (optimize_0plus a1) = aeval a1
IHa2:aeval (optimize_0plus a2) = aeval a2
aeval (optimize_0plus a1) - aeval (optimize_0plus a2) =
aeval a1 - aeval a2 rewrite IHa1.
a1, a2:aexp
IHa1:aeval (optimize_0plus a1) = aeval a1
IHa2:aeval (optimize_0plus a2) = aeval a2
aeval a1 - aeval (optimize_0plus a2) =
aeval a1 - aeval a2 rewrite IHa2.
a1, a2:aexp
IHa1:aeval (optimize_0plus a1) = aeval a1
IHa2:aeval (optimize_0plus a2) = aeval a2
aeval a1 - aeval a2 = aeval a1 - aeval a2 reflexivity.
  - (* AMult *)
a1, a2:aexp
IHa1:aeval (optimize_0plus a1) = aeval a1
IHa2:aeval (optimize_0plus a2) = aeval a2
aeval (optimize_0plus (AMult a1 a2)) =
aeval (AMult a1 a2)
    simpl.
a1, a2:aexp
IHa1:aeval (optimize_0plus a1) = aeval a1
IHa2:aeval (optimize_0plus a2) = aeval a2
aeval (optimize_0plus a1) * aeval (optimize_0plus a2) =
aeval a1 * aeval a2 rewrite IHa1.
a1, a2:aexp
IHa1:aeval (optimize_0plus a1) = aeval a1
IHa2:aeval (optimize_0plus a2) = aeval a2
aeval a1 * aeval (optimize_0plus a2) =
aeval a1 * aeval a2 rewrite IHa2.
a1, a2:aexp
IHa1:aeval (optimize_0plus a1) = aeval a1
IHa2:aeval (optimize_0plus a2) = aeval a2
aeval a1 * aeval a2 = aeval a1 * aeval a2 reflexivity.
Qed.

Naturally, we don't have quite enough for a paper, this result is not too impressive. However it is already a good support to pause and think about what it means to prove such a result in Coq.

We have defined: - a syntax - a semantics - an optimization - a proof of soundness of the optimization.

In a way, what Coq provides us is the guarantee that all of these components are what they claim (in particular, that the proof _is_ a proof), but also that they _actually_ talk about one another. There is no ambiguity about what language a result talks about, things are properly specified. This raises majors questions about maintainability and evolution of formal language: if add a construction, or amend a semantic rule, then my proof will likely break. But it ensures that no bad interaction between two features that would have been checked sound separately on their own right could sneak in.

So what should you keep an eye for when wondering whether a claim of the flavor of "I've formalized my work in Coq"? - If the object they have formalized is the same as the object they claim to talk about. This is very much a process of modelization, it can be as crude and non-sensical as in any other context! - If the theorem they prove states something interesting. In particular if they don't constrain the scope of the result by adding assumptions. - Marginally if they don't use axioms or admit results, but this is a simpler problem.

Impure expressions

Let's add some states!

Inductive aexp : Type :=
  | ANum (n : nat)
  | AId (x : string)              (* <--- NEW *)
  | APlus (a1 a2 : aexp)
  | AMinus (a1 a2 : aexp)
  | AMult (a1 a2 : aexp).

Of course our semantics now need a notion of state to find the meaning of an identifier. Let's not be fancy Today, we'll use good old total maps.

Definition state : Type := string -> nat.

Fixpoint aeval (a : aexp) (s : state) : nat :=
  match a with
  | ANum n => n
  | AId x => s x
  | APlus  a1 a2 => (aeval a1 s) + (aeval a2 s)
  | AMinus a1 a2 => (aeval a1 s) - (aeval a2 s)
  | AMult  a1 a2 => (aeval a1 s) * (aeval a2 s)
  end.

Alright, let's now get serious: let's consider a Turing-complete language!

Inductive com : Type :=
  | CSkip
  | CAss (x : string) (a : aexp)
  | CSeq (c1 c2 : com)
  | CIf (b : aexp) (c1 c2 : com)
  | CWhile (b : aexp) (c : com).

And let's define a few fancy notations for convenience.

Bind Scope imp_scope with com.
Declaring a scope implicitly is deprecated; use in
advance an explicit "Declare Scope imp_scope.".
[undeclared-scope,deprecated]
Notation "'SKIP'" :=
   CSkip : imp_scope.
Notation "x '::=' a" :=
  (CAss x a) (at level 60) : imp_scope.
Notation "c1 ;; c2" :=
  (CSeq c1 c2) (at level 80, right associativity) : imp_scope.
Notation "'WHILE' b 'DO' c 'END'" :=
  (CWhile b c) (at level 80, right associativity) : imp_scope.
Notation "'TEST' c1 'THEN' c2 'ELSE' c3 'FI'" :=
  (CIf c1 c2 c3) (at level 80, right associativity) : imp_scope.
Open Scope imp_scope.
Open Scope string_scope.
Open Scope nat_scope.

We are of course tempted to jump in and define a new Fixpoint for the semantics of our commands.

We just need an update function on our states, and we shoudl be good

Definition update (s : state) x v : state :=
  fun y => if eqb x y then v else s y.

Notation "x '!->' v ';' s" := (update s x v)
                              (at level 100, v at next level, right associativity).

Fixpoint ceval_fun_no_while (c : com) (st : state) 
                          : state :=
  match c with
    | SKIP =>
        st
    | x ::= a1 =>
        (x !-> (aeval a1 st) ; st)
    | c1 ;; c2 =>
        let st' := ceval_fun_no_while c1 st in
        ceval_fun_no_while c2 st'
    | TEST b THEN c1 ELSE c2 FI =>
        if (aeval b st) =? 1
          then ceval_fun_no_while c1 st
          else ceval_fun_no_while c2 st
    | WHILE b DO c END =>
        st  (* bogus *)
  end.

As long as we don't worry about the loop, things of course go smoothly...

What if we just give it a shot?

Fail Fixpoint ceval_fun_hopeful_while (c : com) (st : state) 
  : state :=
  match c with
  | SKIP =>
    st
  | x ::= a1 =>
          (x !-> (aeval a1 st) ; st)
        | c1 ;; c2 =>
          let st' := ceval_fun_hopeful_while c1 st in
          ceval_fun_hopeful_while c2 st'
        | TEST b THEN c1 ELSE c2 FI =>
          if (aeval b st) =? 1
          then ceval_fun_hopeful_while c1 st
          else ceval_fun_hopeful_while c2 st
        | WHILE b DO c END =>
          if (aeval b st) =? 1
          then
            ceval_fun_hopeful_while (WHILE b DO c END) st
          else st
  end.
The command has indeed failed with message:
Cannot guess decreasing argument of fix.

This definition fails with the following message: Coq "Cannot guess decreasing argument of fix", and it seems to a concern.

Indeed while we are happy to live in this world where programming and proving conflates, it can only happen at the cost of programming in a constraint environment, where the logic corresponding to the type system is sound. As it turns out, diverging programs are sources of inconsistencies. Imagine the following imaginary recursive function:

[Fixpoint bad (u : unit) : P := bad u.]

OCaml will happily typecheck it parametrically in P. However if we read it under Curry Howard, we just found a proof for any proposition!!

Recursive functions in Coq are therefore severely restricted in Coq: they must all terminate. Coq has some structural criteria to prove it automatically by structural arguments, and provide facilities to manually provide a measure and prove the termination of our functions.

However here there is no hope: our interpreter indeed diverges for some inputs! We will hence switch gears and define a propositional semantics to Imp.

We will follow closely a style we can find in many semantic papers: a set of big-step reduction rules. It's not the most pleasant to parse, btu it really is not more complex.

For instance, the rule of sequence is exactly saying:

if [c1,st ->* st'] and [c2,st' ->* st'']

then [c1;c2,st ->* st'']

Inductive ceval : com -> state -> state -> Prop :=
  | E_Skip : forall st,
      st =[ SKIP ]=> st
  | E_Ass  : forall st a1 n x,
      aeval a1 st = n ->
      st =[ x ::= a1 ]=> (x !-> n ; st)
  | E_Seq : forall c1 c2 st st' st'',
      st  =[ c1 ]=> st'  ->
      st' =[ c2 ]=> st'' ->
      st  =[ c1 ;; c2 ]=> st''
  | E_IfTrue : forall st st' b c1 c2,
      aeval b st = 1 ->
      st =[ c1 ]=> st' ->
      st =[ TEST b THEN c1 ELSE c2 FI ]=> st'
  | E_IfFalse : forall st st' b c1 c2,
      aeval b st <> 1 ->
      st =[ c2 ]=> st' ->
      st =[ TEST b THEN c1 ELSE c2 FI ]=> st'
  | E_WhileFalse : forall b st c,
      aeval b st <> 1 ->
      st =[ WHILE b DO c END ]=> st
  | E_WhileTrue : forall st st' st'' b c,
      aeval b st = 1 ->
      st  =[ c ]=> st' ->
      st' =[ WHILE b DO c END ]=> st'' ->
      st  =[ WHILE b DO c END ]=> st''

  where "st =[ c ]=> st'" := (ceval c st st').

By moving from an interpreter to a propositional caracterisation of the semantics, we have gained a lot of freedom, at the cost of static guarantees.

We have not had to worry about any question of termination. But note that we have actually simply modeled _exclusively_ the finite executions: this is captured by the inductive interpretation of our rules. Only finite trees can be built, hence only finite computations are modeled.

But we actually got new perks. Is our semantics only partially defined? Easy, no one asked our rules to be total! (Actually divergence is precisely a source of partiality) Is our semantics non-deterministic? Easy, no one asked our rules to be deterministic!

But is our semantics deterministic btw? Exercise!

Theorem ceval_deterministic: forall c st st1 st2,
     st =[ c ]=> st1  ->
     st =[ c ]=> st2 ->
     st1 = st2.
forall (c : com) (st st1 st2 : state),
st =[ c ]=> st1 -> st =[ c ]=> st2 -> st1 = st2
Proof.
forall (c : com) (st st1 st2 : state),
st =[ c ]=> st1 -> st =[ c ]=> st2 -> st1 = st2
Admitted.

Of course we can prove properties of specific programs.

In particular, we can prove their functional correctness. Behold a colossal example.

Note: we could define lots of fancier notations and coercions to ease the pain of writing these programs.

Definition plus2 : com :=
  "X" ::= APlus (AId "X") (ANum 2).

Theorem plus2_spec : forall (st : state) (n : nat) (st' : state),
  st "X" = n ->
  st =[ plus2 ]=> st' ->
  st' "X" = n + 2.
forall (st : state) (n : nat) (st' : state),
st "X" = n -> st =[ plus2 ]=> st' -> st' "X" = n + 2
Proof.
forall (st : state) (n : nat) (st' : state),
st "X" = n -> st =[ plus2 ]=> st' -> st' "X" = n + 2
  intros st n st' HX Heval.
st:state
n:nat
st':state
HX:st "X" = n
Heval:st =[ plus2 ]=> st'
st' "X" = n + 2
  inversion Heval.
st:state
n:nat
st':state
HX:st "X" = n
Heval:st =[ plus2 ]=> st'
st0:state
a1:aexp
n0:nat
x:string
H3:aeval (APlus (AId "X") (ANum 2)) st = n0
H:x = "X"
H1:a1 = APlus (AId "X") (ANum 2)
H0:st0 = st
H2:("X" !-> n0; st) = st'
("X" !-> n0; st) "X" = n + 2 subst.
st:state
Heval:st =[ plus2
]=> ("X"
     !-> aeval (APlus (AId "X") (ANum 2)) st;
     st)
("X" !-> aeval (APlus (AId "X") (ANum 2)) st; st) "X" =
st "X" + 2 clear Heval.
st:state
("X" !-> aeval (APlus (AId "X") (ANum 2)) st; st) "X" =
st "X" + 2
  simpl.
st:state
("X" !-> st "X" + 2; st) "X" = st "X" + 2
  (* We need a lemma to conclude!
     We need to reason about a lookup to a variable we have just written to. 
     Let's do something forbidden and nest it in our proof.
   *)

  Set Nested Proofs Allowed.
st:state
("X" !-> st "X" + 2; st) "X" = st "X" + 2
  Lemma update_eq :
    forall st x v,
      (x !-> v; st) x = v.
forall (st : state) (x : string) (v : nat),
(x !-> v; st) x = v
  Proof.
forall (st : state) (x : string) (v : nat),
(x !-> v; st) x = v
    intros.
st:state
x:string
v:nat
(x !-> v; st) x = v
    unfold update.
st:state
x:string
v:nat
(if (x =? x)%string then v else st x) = v
    rewrite eqb_refl.
st:state
x:string
v:nat
v = v
    reflexivity.
  Qed.
st:state
("X" !-> st "X" + 2; st) "X" = st "X" + 2

  (* We can now invoke our freshly proved lemma *)
  apply update_eq.

Qed.

Or in a different style, we can prove that the following infinite loop indeed diverges (more specifically, we will state that it admits no finite derivation. It is strictly weaker, as the rules could simply be partial).

Definition loop : com :=
  WHILE ANum 1 DO
    SKIP
  END.

Theorem loop_never_stops : forall st st',
  ~(st =[ loop ]=> st').
forall st st' : state, ~ st =[ loop ]=> st'
Proof.
forall st st' : state, ~ st =[ loop ]=> st'
  intros st st' contra.
st, st':state
contra:st =[ loop ]=> st'
False unfold loop in contra.
st, st':state
contra:st =[ WHILE ANum 1 DO SKIP END ]=> st'
False
  remember (WHILE ANum 1 DO SKIP END) as loopdef
           eqn:Heqloopdef.
st, st':state
loopdef:com
Heqloopdef:loopdef = (WHILE ANum 1 DO SKIP END)
contra:st =[ loopdef ]=> st'
False
  (* Minimal setup to proceed by induction on the hypothetical derivation *)
Admitted.

From there, if you feel so enclined, you could define an alternate semantics to Imp, this time as the transitive closure of a small step semantics, and prove the equivalence of your new semantics with the previous one.

But if you are sufficiently on board to be motivated to do so, you might want to rather get a proper introduction by going through Software Foundation!

https://softwarefoundations.cis.upenn.edu/

If I have gauged right, we will not have reached this point in under an hour.

If I happen to be wildly incorrect, here is a non exhaustive list of aspects we have not discussed at all, let's discuss! - Extraction to OCaml/Haskel/ML - Type classes - Modules - Advance uses of LTac - Working with non-structural recursive functions - Coinduction - Using libraries, searching for exhisting theormes