Built with Alectryon, running Coq+SerAPI v8.12.0+0.12.0. Coq sources are in this panel; goals and messages will appear in the other. Bubbles () indicate interactive fragments: hover for details, tap to reveal contents. Use Ctrl+↑ Ctrl+↓ to navigate, Ctrl+🖱️ to focus.

Disclaimer 1: This crash introduction to Coq has stolen a lot of snippets of code from the excellent Software Foundation series of books: https://softwarefoundations.cis.upenn.edu/ If you are interested in learning more about Coq, you should definitely check it out!

Disclaimer 2: this file is not meant to constitute a self-contained quality tutorial for a reader that would stumble upon it, it was written as support material for a presentation touring informally the Coq proof assistant.

# A gentle overview to the Coq proof assistant

## Coq: a functional programming language

### 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:SuitISRED:is_red c = trueISPOINTY:is_pointy c = truec = Diamonds
destruct c. (* Case analysis on c *)ISRED:is_red Spades = trueISPOINTY:is_pointy Spades = trueSpades = DiamondsISRED:is_red Hearts = trueISPOINTY:is_pointy Hearts = trueHearts = DiamondsISRED:is_red Diamonds = trueISPOINTY:is_pointy Diamonds = trueDiamonds = DiamondsISRED:is_red Clubs = trueISPOINTY:is_pointy Clubs = trueClubs = Diamonds
discriminate ISRED.
-ISRED:is_red Hearts = trueISPOINTY:is_pointy Hearts = trueHearts = Diamonds simpl in *.ISRED:true = trueISPOINTY:false = trueHearts = Diamonds
discriminate ISPOINTY.
-ISRED:is_red Diamonds = trueISPOINTY:is_pointy Diamonds = trueDiamonds = Diamonds reflexivity.
-ISRED:is_red Clubs = trueISPOINTY:is_pointy Clubs = trueClubs = Diamonds simpl in *.ISRED, ISPOINTY:false = trueClubs = 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
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
| 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:natO + n = n
simpl.n:natn = 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:natn + O = n
simpl. (* Nothing happens! *)n:natn + 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:natn + O = n
(* We could try by case analysis *)
destruct n as [| n].O + O = On:natS n + O = S n
reflexivity.n:natS n + O = S n
simpl.n:natS (n + O) = S n
f_equal. (* We eliminate the S *)n:natn + O = n
(* We are back to square one *)
Undo 6.n:natn + O = n
(* We are going to proceed by induction *)
induction n as [| n IH].O + O = On:natIH:n + O = nS n + O = S n
-O + O = O reflexivity. (* Base case *)
-n:natIH:n + O = nS n + O = S n simpl.n:natIH:n + O = nS (n + O) = S n
f_equal.n:natIH:n + O = nn + 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` *)
```
```

## Coq: expressing mathematical statements

### 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:PropH:P /\ Q /\ R(P /\ Q) /\ R
destruct H as [HP [HQ HR]].P, Q, R:PropHP:PHQ:QHR:R(P /\ Q) /\ R
split.P, Q, R:PropHP:PHQ:QHR:RP /\ QP, Q, R:PropHP:PHQ:QHR:RR
-P, Q, R:PropHP:PHQ:QHR:RP /\ Q split.P, Q, R:PropHP:PHQ:QHR:RPP, Q, R:PropHP:PHQ:QHR:RQ
+P, Q, R:PropHP:PHQ:QHR:RP exact HP.
+P, Q, R:PropHP:PHQ:QHR:RQ exact HQ.
-P, Q, R:PropHP:PHQ:QHR:RR 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]? *)

End Logic.```

## Coq: reasoning about programming languages

Coq can be used to formalize most mathematics. But for us in particular, an interesting domain of application is the formalization of the semantics of programming languages.

### 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:aexpaeval (optimize_0plus a) = aeval a induction a.n:nataeval (optimize_0plus (ANum n)) = aeval (ANum n)a1, a2:aexpIHa1:aeval (optimize_0plus a1) = aeval a1IHa2:aeval (optimize_0plus a2) = aeval a2aeval (optimize_0plus (APlus a1 a2)) =
aeval (APlus a1 a2)a1, a2:aexpIHa1:aeval (optimize_0plus a1) = aeval a1IHa2:aeval (optimize_0plus a2) = aeval a2aeval (optimize_0plus (AMinus a1 a2)) =
aeval (AMinus a1 a2)a1, a2:aexpIHa1:aeval (optimize_0plus a1) = aeval a1IHa2:aeval (optimize_0plus a2) = aeval a2aeval (optimize_0plus (AMult a1 a2)) =
aeval (AMult a1 a2)
- (* ANum *)n:nataeval (optimize_0plus (ANum n)) = aeval (ANum n) reflexivity.
- (* APlus *)a1, a2:aexpIHa1:aeval (optimize_0plus a1) = aeval a1IHa2:aeval (optimize_0plus a2) = aeval a2aeval (optimize_0plus (APlus a1 a2)) =
aeval (APlus a1 a2) destruct a1 eqn:Ea1.a1, a2:aexpn:natEa1:a1 = ANum nIHa1:aeval (optimize_0plus (ANum n)) =
aeval (ANum n)IHa2:aeval (optimize_0plus a2) = aeval a2aeval (optimize_0plus (APlus (ANum n) a2)) =
aeval (APlus (ANum n) a2)a1, a2, a3, a4:aexpEa1:a1 = APlus a3 a4IHa1:aeval (optimize_0plus (APlus a3 a4)) =
aeval (APlus a3 a4)IHa2:aeval (optimize_0plus a2) = aeval a2aeval (optimize_0plus (APlus (APlus a3 a4) a2)) =
aeval (APlus (APlus a3 a4) a2)a1, a2, a3, a4:aexpEa1:a1 = AMinus a3 a4IHa1:aeval (optimize_0plus (AMinus a3 a4)) =
aeval (AMinus a3 a4)IHa2:aeval (optimize_0plus a2) = aeval a2aeval (optimize_0plus (APlus (AMinus a3 a4) a2)) =
aeval (APlus (AMinus a3 a4) a2)a1, a2, a3, a4:aexpEa1:a1 = AMult a3 a4IHa1:aeval (optimize_0plus (AMult a3 a4)) =
aeval (AMult a3 a4)IHa2:aeval (optimize_0plus a2) = aeval a2aeval (optimize_0plus (APlus (AMult a3 a4) a2)) =
aeval (APlus (AMult a3 a4) a2)
+ (* a1 = ANum n *)a1, a2:aexpn:natEa1:a1 = ANum nIHa1:aeval (optimize_0plus (ANum n)) =
aeval (ANum n)IHa2:aeval (optimize_0plus a2) = aeval a2aeval (optimize_0plus (APlus (ANum n) a2)) =
aeval (APlus (ANum n) a2) destruct n eqn:En.a1, a2:aexpn:natEn:n = 0Ea1:a1 = ANum 0IHa1:aeval (optimize_0plus (ANum 0)) =
aeval (ANum 0)IHa2:aeval (optimize_0plus a2) = aeval a2aeval (optimize_0plus (APlus (ANum 0) a2)) =
aeval (APlus (ANum 0) a2)a1, a2:aexpn, n0:natEn:n = S n0Ea1:a1 = ANum (S n0)IHa1:aeval (optimize_0plus (ANum (S n0))) =
aeval (ANum (S n0))IHa2:aeval (optimize_0plus a2) = aeval a2aeval (optimize_0plus (APlus (ANum (S n0)) a2)) =
aeval (APlus (ANum (S n0)) a2)
* (* n = 0 *)a1, a2:aexpn:natEn:n = 0Ea1:a1 = ANum 0IHa1:aeval (optimize_0plus (ANum 0)) =
aeval (ANum 0)IHa2:aeval (optimize_0plus a2) = aeval a2aeval (optimize_0plus (APlus (ANum 0) a2)) =
aeval (APlus (ANum 0) a2)  simpl.a1, a2:aexpn:natEn:n = 0Ea1:a1 = ANum 0IHa1:aeval (optimize_0plus (ANum 0)) =
aeval (ANum 0)IHa2:aeval (optimize_0plus a2) = aeval a2aeval (optimize_0plus a2) = aeval a2 apply IHa2.
* (* n <> 0 *)a1, a2:aexpn, n0:natEn:n = S n0Ea1:a1 = ANum (S n0)IHa1:aeval (optimize_0plus (ANum (S n0))) =
aeval (ANum (S n0))IHa2:aeval (optimize_0plus a2) = aeval a2aeval (optimize_0plus (APlus (ANum (S n0)) a2)) =
aeval (APlus (ANum (S n0)) a2) simpl.a1, a2:aexpn, n0:natEn:n = S n0Ea1:a1 = ANum (S n0)IHa1:aeval (optimize_0plus (ANum (S n0))) =
aeval (ANum (S n0))IHa2:aeval (optimize_0plus a2) = aeval a2S (n0 + aeval (optimize_0plus a2)) = S (n0 + aeval a2) rewrite IHa2.a1, a2:aexpn, n0:natEn:n = S n0Ea1:a1 = ANum (S n0)IHa1:aeval (optimize_0plus (ANum (S n0))) =
aeval (ANum (S n0))IHa2:aeval (optimize_0plus a2) = aeval a2S (n0 + aeval a2) = S (n0 + aeval a2) reflexivity.
+ (* a1 = APlus a1_1 a1_2 *)a1, a2, a3, a4:aexpEa1:a1 = APlus a3 a4IHa1:aeval (optimize_0plus (APlus a3 a4)) =
aeval (APlus a3 a4)IHa2:aeval (optimize_0plus a2) = aeval a2aeval (optimize_0plus (APlus (APlus a3 a4) a2)) =
aeval (APlus (APlus a3 a4) a2)
simpl.a1, a2, a3, a4:aexpEa1:a1 = APlus a3 a4IHa1:aeval (optimize_0plus (APlus a3 a4)) =
aeval (APlus a3 a4)IHa2:aeval (optimize_0plus a2) = aeval a2aeval
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:aexpEa1:a1 = APlus a3 a4IHa1:aeval
match a3 with
| ANum 0 => optimize_0plus a4
| _ =>
APlus (optimize_0plus a3)
(optimize_0plus a4)
end = aeval a3 + aeval a4IHa2:aeval (optimize_0plus a2) = aeval a2aeval
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:aexpEa1:a1 = APlus a3 a4IHa1:aeval
match a3 with
| ANum 0 => optimize_0plus a4
| _ =>
APlus (optimize_0plus a3)
(optimize_0plus a4)
end = aeval a3 + aeval a4IHa2:aeval (optimize_0plus a2) = aeval a2aeval a3 + aeval a4 + aeval (optimize_0plus a2) =
aeval a3 + aeval a4 + aeval a2
rewrite IHa2.a1, a2, a3, a4:aexpEa1:a1 = APlus a3 a4IHa1:aeval
match a3 with
| ANum 0 => optimize_0plus a4
| _ =>
APlus (optimize_0plus a3)
(optimize_0plus a4)
end = aeval a3 + aeval a4IHa2:aeval (optimize_0plus a2) = aeval a2aeval a3 + aeval a4 + aeval a2 =
aeval a3 + aeval a4 + aeval a2 reflexivity.
+ (* a1 = AMinus a1_1 a1_2 *)a1, a2, a3, a4:aexpEa1:a1 = AMinus a3 a4IHa1:aeval (optimize_0plus (AMinus a3 a4)) =
aeval (AMinus a3 a4)IHa2:aeval (optimize_0plus a2) = aeval a2aeval (optimize_0plus (APlus (AMinus a3 a4) a2)) =
aeval (APlus (AMinus a3 a4) a2)
simpl.a1, a2, a3, a4:aexpEa1:a1 = AMinus a3 a4IHa1:aeval (optimize_0plus (AMinus a3 a4)) =
aeval (AMinus a3 a4)IHa2:aeval (optimize_0plus a2) = aeval a2aeval (optimize_0plus a3) - aeval (optimize_0plus a4) +
aeval (optimize_0plus a2) =
aeval a3 - aeval a4 + aeval a2 simpl in IHa1.a1, a2, a3, a4:aexpEa1:a1 = AMinus a3 a4IHa1:aeval (optimize_0plus a3) -
aeval (optimize_0plus a4) =
aeval a3 - aeval a4IHa2:aeval (optimize_0plus a2) = aeval a2aeval (optimize_0plus a3) - aeval (optimize_0plus a4) +
aeval (optimize_0plus a2) =
aeval a3 - aeval a4 + aeval a2 rewrite IHa1.a1, a2, a3, a4:aexpEa1:a1 = AMinus a3 a4IHa1:aeval (optimize_0plus a3) -
aeval (optimize_0plus a4) =
aeval a3 - aeval a4IHa2:aeval (optimize_0plus a2) = aeval a2aeval a3 - aeval a4 + aeval (optimize_0plus a2) =
aeval a3 - aeval a4 + aeval a2
rewrite IHa2.a1, a2, a3, a4:aexpEa1:a1 = AMinus a3 a4IHa1:aeval (optimize_0plus a3) -
aeval (optimize_0plus a4) =
aeval a3 - aeval a4IHa2:aeval (optimize_0plus a2) = aeval a2aeval a3 - aeval a4 + aeval a2 =
aeval a3 - aeval a4 + aeval a2 reflexivity.
+ (* a1 = AMult a1_1 a1_2 *)a1, a2, a3, a4:aexpEa1:a1 = AMult a3 a4IHa1:aeval (optimize_0plus (AMult a3 a4)) =
aeval (AMult a3 a4)IHa2:aeval (optimize_0plus a2) = aeval a2aeval (optimize_0plus (APlus (AMult a3 a4) a2)) =
aeval (APlus (AMult a3 a4) a2)
simpl.a1, a2, a3, a4:aexpEa1:a1 = AMult a3 a4IHa1:aeval (optimize_0plus (AMult a3 a4)) =
aeval (AMult a3 a4)IHa2:aeval (optimize_0plus a2) = aeval a2aeval (optimize_0plus a3) * aeval (optimize_0plus a4) +
aeval (optimize_0plus a2) =
aeval a3 * aeval a4 + aeval a2 simpl in IHa1.a1, a2, a3, a4:aexpEa1:a1 = AMult a3 a4IHa1:aeval (optimize_0plus a3) *
aeval (optimize_0plus a4) =
aeval a3 * aeval a4IHa2:aeval (optimize_0plus a2) = aeval a2aeval (optimize_0plus a3) * aeval (optimize_0plus a4) +
aeval (optimize_0plus a2) =
aeval a3 * aeval a4 + aeval a2 rewrite IHa1.a1, a2, a3, a4:aexpEa1:a1 = AMult a3 a4IHa1:aeval (optimize_0plus a3) *
aeval (optimize_0plus a4) =
aeval a3 * aeval a4IHa2:aeval (optimize_0plus a2) = aeval a2aeval a3 * aeval a4 + aeval (optimize_0plus a2) =
aeval a3 * aeval a4 + aeval a2
rewrite IHa2.a1, a2, a3, a4:aexpEa1:a1 = AMult a3 a4IHa1:aeval (optimize_0plus a3) *
aeval (optimize_0plus a4) =
aeval a3 * aeval a4IHa2:aeval (optimize_0plus a2) = aeval a2aeval a3 * aeval a4 + aeval a2 =
aeval a3 * aeval a4 + aeval a2 reflexivity.
- (* AMinus *)a1, a2:aexpIHa1:aeval (optimize_0plus a1) = aeval a1IHa2:aeval (optimize_0plus a2) = aeval a2aeval (optimize_0plus (AMinus a1 a2)) =
aeval (AMinus a1 a2)
simpl.a1, a2:aexpIHa1:aeval (optimize_0plus a1) = aeval a1IHa2:aeval (optimize_0plus a2) = aeval a2aeval (optimize_0plus a1) - aeval (optimize_0plus a2) =
aeval a1 - aeval a2 rewrite IHa1.a1, a2:aexpIHa1:aeval (optimize_0plus a1) = aeval a1IHa2:aeval (optimize_0plus a2) = aeval a2aeval a1 - aeval (optimize_0plus a2) =
aeval a1 - aeval a2 rewrite IHa2.a1, a2:aexpIHa1:aeval (optimize_0plus a1) = aeval a1IHa2:aeval (optimize_0plus a2) = aeval a2aeval a1 - aeval a2 = aeval a1 - aeval a2 reflexivity.
- (* AMult *)a1, a2:aexpIHa1:aeval (optimize_0plus a1) = aeval a1IHa2:aeval (optimize_0plus a2) = aeval a2aeval (optimize_0plus (AMult a1 a2)) =
aeval (AMult a1 a2)
simpl.a1, a2:aexpIHa1:aeval (optimize_0plus a1) = aeval a1IHa2:aeval (optimize_0plus a2) = aeval a2aeval (optimize_0plus a1) * aeval (optimize_0plus a2) =
aeval a1 * aeval a2 rewrite IHa1.a1, a2:aexpIHa1:aeval (optimize_0plus a1) = aeval a1IHa2:aeval (optimize_0plus a2) = aeval a2aeval a1 * aeval (optimize_0plus a2) =
aeval a1 * aeval a2 rewrite IHa2.a1, a2:aexpIHa1:aeval (optimize_0plus a1) = aeval a1IHa2:aeval (optimize_0plus a2) = aeval a2aeval 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

```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:

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

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:staten:natst':stateHX:st "X" = nHeval:st =[ plus2 ]=> st'st' "X" = n + 2
inversion Heval.st:staten:natst':stateHX:st "X" = nHeval:st =[ plus2 ]=> st'st0:statea1:aexpn0:natx:stringH3:aeval (APlus (AId "X") (ANum 2)) st = n0H:x = "X"H1:a1 = APlus (AId "X") (ANum 2)H0:st0 = stH2:("X" !-> n0; st) = st'("X" !-> n0; st) "X" = n + 2 subst.st:stateHeval: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:statex:stringv:nat(x !-> v; st) x = v
unfold update.st:statex:stringv:nat(if (x =? x)%string then v else st x) = v
rewrite eqb_refl.st:statex:stringv:natv = 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':statecontra:st =[ loop ]=> st'False unfold loop in contra.st, st':statecontra:st =[ WHILE ANum 1 DO SKIP END ]=> st'False
remember (WHILE ANum 1 DO SKIP END) as loopdef
eqn:Heqloopdef.st, st':stateloopdef:comHeqloopdef:loopdef = (WHILE ANum 1 DO SKIP END)contra:st =[ loopdef ]=> st'False
(* Minimal setup to proceed by induction on the hypothetical derivation *)