@@ -60,7 +60,7 @@ On the contrary, as most recent functional programming languages (e.g OCaml), Co

...

@@ -60,7 +60,7 @@ On the contrary, as most recent functional programming languages (e.g OCaml), Co

The main type constructor is the *functional arrow*`->`.

The main type constructor is the *functional arrow*`->`.

Note that `A->B->C` is `A->(B->C)`.

Note that `A->B->C` is `A->(B->C)`.

First, simply-typed lambda-calculus : just take lambda-calculus plus a typing judgement `Γ ⊢ t:T` described by the rules below. Here Γ is a *typing context*, i.e. a finite list of variables associated with their respective types.

First, simply-typed lambda-calculus : just take lambda-calculus plus a typing judgment `Γ ⊢ t:T` described by the rules below. Here Γ is a *typing context*, i.e. a finite list of variables associated with their respective types.

- If `x:T` is in Γ then `Γ ⊢ x:T`

- If `x:T` is in Γ then `Γ ⊢ x:T`

- If `Γ+x:τ ⊢ t:σ` then `Γ ⊢ (λx.t):(τ→σ)`

- If `Γ+x:τ ⊢ t:σ` then `Γ ⊢ (λx.t):(τ→σ)`

...

@@ -114,7 +114,7 @@ Roughly, the typing rule for a product looks like :

...

@@ -114,7 +114,7 @@ Roughly, the typing rule for a product looks like :

- If `Γ ⊢ A:Type` and `Γ+x:A ⊢ B:Type` then `Γ ⊢ (forall x:A,B) : Type`

- If `Γ ⊢ A:Type` and `Γ+x:A ⊢ B:Type` then `Γ ⊢ (forall x:A,B) : Type`

In reality, one must take care of the indices of the `Type` universes : lthe rightmost index is the max of the two others. And this typing rule has a particular case for `Prop` that we will not detail here.

In reality, one must take care of the indices of the `Type` universes : the rightmost index is the max of the two others. And this typing rule has a particular case for `Prop` that we will not detail here.

We can now generalize the typing rules for functions and applications:

We can now generalize the typing rules for functions and applications:

...

@@ -168,11 +168,11 @@ A `let x:=t in u` behave almost like `((fun x=>u) t)`.

...

@@ -168,11 +168,11 @@ A `let x:=t in u` behave almost like `((fun x=>u) t)`.

Once again, a reduction rule (`ζ`, zeta) allows to discard this local abbreviation by replacing everywhere `x` by `t` in `u`.

Once again, a reduction rule (`ζ`, zeta) allows to discard this local abbreviation by replacing everywhere `x` by `t` in `u`.

## First data types : boolean and natural numbers.

## First data types : Boolean and natural numbers.

Coq provides a type `bool` and constants `true` and `false`.

Coq provides a type `bool` and constants `true` and `false`.

There is a construction `if ... then ... else ...`.

There is a construction `if ... then ... else ...`.

@@ -198,7 +198,7 @@ We will see later how to perform efficient arithmetical operations (binary encod

...

@@ -198,7 +198,7 @@ We will see later how to perform efficient arithmetical operations (binary encod

`Fixpoint` allows to reuse the function we are actually defining in itself !

`Fixpoint` allows to reuse the function we are actually defining in itself !

Before accepting a `Fixpoint`, Coq checks that this definition is syntactically decreasing. For that, a criterion of *stuctural decrease* is used, we will detail it later. In short, recursive calls must be done on *strict sub-terms*. Practically, this means using a construction `match ... with ... end` for accessing the previous integer (for instance).

Before accepting a `Fixpoint`, Coq checks that this definition is syntactically decreasing. For that, a criterion of *structural decrease* is used, we will detail it later. In short, recursive calls must be done on *strict sub-terms*. Practically, this means using a construction `match ... with ... end` for accessing the previous integer (for instance).