lesson7

To play this document inside your browser use ALT-N and ALT-P.

You can save your edits inside your browser and load them back (edits are also saved when you close the window). Finally you can download the file for offline editing.

Lesson 7: summary

generic notations and theories
interfaces
parametrizing theories
the BigOp library (the theories of fold)

Let's start with a lie and then make it true:

Coq is an object oriented programming language.

Generic notations and theories

Polymorphism != overloading.

Example: the == computable equality

Polymorphism

Overloading : looking inside types

Object oriented flavor

Overloading may fail, polymorphism never

Type inference

We call eqType an interface. With some approximation eqType is defined as follows:


Module Equality.

Structure type : Type := Pack {
  sort : Type;
  op : sort -> sort -> bool;
  axiom : ∀x y, reflect (x = y) (op x y)
}.


End Equality

(notes)

This slide corresponds to section 5.4 of the Mathematical Components book

Interfaces

Mathematical Components defines a hierarchy of interfaces. They group notations and theorems.

Let's use the theory of eqType

Interfaces do apply to registered, concrete examples such as bool or nat. They can also apply to variables, as long as their type is rich (eqType is richer than Type).

(notes)

This slide corresponds to section 5.5 and 7 of the Mathematical Components book

Theories over an interface

Interfaces can be used to parametrize an entire theory

Others interfaces

(notes)

This slide corresponds to section 5.6 of the Mathematical Components book

Generic theories: the BigOp library

The BigOp library is the canonical example of a generic theory. It it about the fold iterator we studied in lesson 1, and the many uses it can have.

Most of the lemmas require the operation to be a monoid, some others to be a commutative monoid.

Searching for bigop

Primer for bigop

Section Primer.

Variable n: nat.
Variable f : 'I_n -> nat.
Variable g : nat -> nat.

Check \big[addn/0]_(i <- [::1; 4; 5] | odd i) g i.

Check \big[addn/0]_(i : 'I_n | odd i) f i.

Definition oddIn := [pred i | odd (i : 'I_n)].

Check \big[addn/0]_(i in oddIn) f i.

Goal \sum_(i in oddIn) i = \sum_(i < n | odd i) i.
Proof.
by [].
Qed.

Check \big[addn/0]_(0 <= i < n | odd i) g i.

Goal \sum_(0 <= i < n | odd i) g i = \sum_(i < n | odd i) g i.
Proof.
Check big_mkord.
rewrite big_mkord.
by [].

Goal \sum_(0 <= i < n |odd i) i.*2 = \sum_(0 <= i < n|odd i) (i + i).
Proof.
Fail rewrite addnn.
About eq_bigr.
apply: eq_bigr.
move=> i Hi.
by rewrite addnn.

Goal \sum_(0 <= i < n |odd i) i.*2 = \sum_(0 <= i < n | odd i) (i + i).
Proof.
About eq_bigr.
rewrite (eq_bigr (fun i => i + i)) //.
move=> i Hi.
by rewrite addnn.

Goal (\sum_(i < n|odd i) i).*2 = \sum_(i < n |odd i) i.*2.
Proof.
About  big_morph.
Fail rewrite big_morph.
rewrite (big_morph _ (_ : {morph double : x y / x + y}) (_ : 0.*2 = 0)).
- by [].
- move=> x y; exact: doubleD.
by [].

End Primer.

(notes)

This slide corresponds to section 5.7 of the Mathematical Components book

Sum up

Coq is an object oriented language ;-)
in the Mathematical Components library xxType is an interface (eg eqType for types with an equality test). Notations and theorems are linked to interfaces. Interfaces are organized in hierarchies (we just saw a picture, how it works can be found in the book).