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.

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.

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.

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.

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.

is_red Hearts = trueis_red Hearts = truereflexivity. (* Equality between a term and itself *) Qed.true = true

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.

forall c : Suit, is_red c = true -> is_pointy c = true -> c = Diamondsforall c : Suit, is_red c = true -> is_pointy c = true -> c = Diamondsc:SuitISRED:is_red c = trueISPOINTY:is_pointy c = truec = DiamondsISRED: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 = DiamondsISRED:is_red Spades = trueISPOINTY:is_pointy Spades = trueSpades = Diamondsdiscriminate ISRED.ISRED:false = trueISPOINTY:true = trueSpades = DiamondsISRED:is_red Hearts = trueISPOINTY:is_pointy Hearts = trueHearts = Diamondsdiscriminate ISPOINTY.ISRED:true = trueISPOINTY:false = trueHearts = Diamondsreflexivity.ISRED:is_red Diamonds = trueISPOINTY:is_pointy Diamonds = trueDiamonds = DiamondsISRED:is_red Clubs = trueISPOINTY:is_pointy Clubs = trueClubs = Diamondsdiscriminate ISPOINTY. Qed.ISRED, ISPOINTY:false = trueClubs = Diamonds

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.

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

Gallina supports full polymorphic types.

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

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

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?

forall n : nat, O + n = nforall n : nat, O + n = nn:natO + n = nreflexivity. Qed.n:natn = nforall n : nat, n + O = nforall n : nat, n + O = nn:natn + O = nn:natn + O = n(* We could try by case analysis *)n:natn + O = nO + O = On:natS n + O = S nn:natS n + O = S nn:natS (n + O) = S n(* We are back to square one *)n:natn + O = n(* We are going to proceed by induction *)n:natn + O = nO + O = On:natIH:n + O = nS n + O = S nreflexivity. (* Base case *)O + O = On:natIH:n + O = nS n + O = S nn:natIH:n + O = nS (n + O) = S napply IH. Qed.n:natIH:n + O = nn + O = n

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?

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.forall (A : Type) (l : list A), length l = length' l

```
```

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.

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!

forall P Q R : Prop, P /\ Q /\ R -> (P /\ Q) /\ Rforall P Q R : Prop, P /\ Q /\ R -> (P /\ Q) /\ RP, Q, R:PropH:P /\ Q /\ R(P /\ Q) /\ RP, Q, R:PropHP:PHQ:QHR:R(P /\ Q) /\ RP, Q, R:PropHP:PHQ:QHR:RP /\ QP, Q, R:PropHP:PHQ:QHR:RRP, Q, R:PropHP:PHQ:QHR:RP /\ QP, Q, R:PropHP:PHQ:QHR:RPP, Q, R:PropHP:PHQ:QHR:RQexact HP.P, Q, R:PropHP:PHQ:QHR:RPexact HQ.P, Q, R:PropHP:PHQ:QHR:RQexact HR. Qed.P, Q, R:PropHP:PHQ:QHR:RR

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.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.forall n : nat, even n -> exists k : nat, n = double k

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.

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!

forall a : aexp, aeval (optimize_0plus a) = aeval aforall a : aexp, aeval (optimize_0plus a) = aeval aa:aexpaeval (optimize_0plus a) = aeval an: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)reflexivity.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: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, 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: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)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)apply IHa2.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 a2a1, 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)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)reflexivity.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)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 = 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 a2a1, 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 a2a1, 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 a2reflexivity.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 a2a1, 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 = 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 a2a1, 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 a2a1, 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 a2reflexivity.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 a2a1, 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, 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 a2a1, 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 a2a1, 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 a2reflexivity.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 a2a1, 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 a1) - aeval (optimize_0plus a2) = aeval a1 - aeval a2a1, a2:aexpIHa1:aeval (optimize_0plus a1) = aeval a1IHa2:aeval (optimize_0plus a2) = aeval a2aeval a1 - aeval (optimize_0plus a2) = aeval a1 - aeval a2reflexivity.a1, a2:aexpIHa1:aeval (optimize_0plus a1) = aeval a1IHa2:aeval (optimize_0plus a2) = aeval a2aeval a1 - aeval a2 = aeval a1 - aeval a2a1, a2:aexpIHa1:aeval (optimize_0plus a1) = aeval a1IHa2:aeval (optimize_0plus a2) = aeval a2aeval (optimize_0plus (AMult a1 a2)) = aeval (AMult a1 a2)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 a2a1, a2:aexpIHa1:aeval (optimize_0plus a1) = aeval a1IHa2:aeval (optimize_0plus a2) = aeval a2aeval a1 * aeval (optimize_0plus a2) = aeval a1 * aeval a2reflexivity. Qed.a1, a2:aexpIHa1:aeval (optimize_0plus a1) = aeval a1IHa2:aeval (optimize_0plus a2) = aeval a2aeval a1 * aeval a2 = aeval a1 * aeval a2

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.

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.

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?

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!

forall (c : com) (st st1 st2 : state), st =[ c ]=> st1 -> st =[ c ]=> st2 -> st1 = st2Admitted.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).forall (st : state) (n : nat) (st' : state), st "X" = n -> st =[ plus2 ]=> st' -> st' "X" = n + 2forall (st : state) (n : nat) (st' : state), st "X" = n -> st =[ plus2 ]=> st' -> st' "X" = n + 2st:staten:natst':stateHX:st "X" = nHeval:st =[ plus2 ]=> st'st' "X" = n + 2st: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 + 2st:stateHeval:st =[ plus2 ]=> ("X" !-> aeval (APlus (AId "X") (ANum 2)) st; st)("X" !-> aeval (APlus (AId "X") (ANum 2)) st; st) "X" = st "X" + 2st:state("X" !-> aeval (APlus (AId "X") (ANum 2)) st; 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. *)st:state("X" !-> st "X" + 2; st) "X" = st "X" + 2st:state("X" !-> st "X" + 2; st) "X" = st "X" + 2forall (st : state) (x : string) (v : nat), (x !-> v; st) x = vforall (st : state) (x : string) (v : nat), (x !-> v; st) x = vst:statex:stringv:nat(x !-> v; st) x = vst:statex:stringv:nat(if (x =? x)%string then v else st x) = vreflexivity.st:statex:stringv:natv = v(* We can now invoke our freshly proved lemma *) apply update_eq. Qed.st:state("X" !-> st "X" + 2; st) "X" = st "X" + 2

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.forall st st' : state, ~ st =[ loop ]=> st'forall st st' : state, ~ st =[ loop ]=> st'st, st':statecontra:st =[ loop ]=> st'Falsest, st':statecontra:st =[ WHILE ANum 1 DO SKIP END ]=> st'False(* Minimal setup to proceed by induction on the hypothetical derivation *) Admitted.st, st':stateloopdef:comHeqloopdef:loopdef = (WHILE ANum 1 DO SKIP END)contra:st =[ loopdef ]=> st'False

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