lesson3

Lesson 3 (of 4)

Finite types

Objective of this course

Understand the benefits and usage of finite types.

formation principle
A special case: ordinals
New tools : finite functions and finite set theory
Moving even closer to classical logic : choice and extensionality

Formation principle

For a finite type, you can enumerate the elements

The enumeration is a simple piece of data (based on sequences)

The enumeration gives some computation principle
Elements of a finite type can be indexed

The simplest finite types: ordinal numbers

Initial segments of natural numbers

Building blocks or yardsticks for other finite types
Usable as plain integers, thanks to coercions

Finite type constructions

In the rest of this talk I will use the following pattern to verify that I have a finite type.

New finite types can be built from existing ones

ordinal types are the usual examples of basic finite types
unit (with one element)
bool (with two elements)
cartesian product
disjoint sum
subtype
function type

Building a finite type from scratch

An example: building an enumerated type, show that is finite

Exhibit an injection into another finite type.

The lemma cp_can means that there is an injection from card_point into a known finite type

A succession of helper theorem to add qualities

equality is decidable eqType
there is a canonical way to choose witnesses choiceType
the elements can be enumerated countType
the type card_point is finite.

Tools about finiteness

More classical logic

Quantifications of decidable predicates become decidable.
Need to use special notations

Proofs about quantified statements.

Finite functions

Function whose domain is a finite type

A finite type when the type for values is finite
A special notation for functions from ordinals

Set theory over finite types

obviously finite sets over a finite type are finite
obviously the type of these sets is finite

Finite types and big operators

Big operators are the natural tool to compute repeatedly over all elements of a finite type
Elements are picked in the fixed order given by the enumeration.

Finite graphs

Finite graphs are build on a finite type of nodes

Three approaches

Use a function to list all targets of edges

The graph of a relation

The graph of a function

Definition mg := [:: (0,1); (1,0); (1,2); (3,3)].
Definition mgr : rel 'I_4 :=
   fun x y : 'I_4 => (val x, val y) \in mg.
Check rgraph mgr.
Check dfs_path (rgraph mgr) [::] ord0.
Lemma graph_proof : dfs_path (rgraph mgr) [::] ord0 (Ordinal (isT : 2 < 4)).
Search dfs_path.
Search _ (grel (rgraph _)).
have pp : path (grel (rgraph mgr)) ord0 [:: Ordinal (isT : 1 < 4); Ordinal (isT : 2 < 4)].
  rewrite /=. rewrite andbT; apply/andP; split.
    rewrite mem_enum. by [].
  rewrite mem_enum. by [].
apply: (DfsPath pp).
  by [].
rewrite disjoint_sym.
apply: disjoint0.

Parameters (z : T) (g : T -> seq T).
Hypothesis xny : x != y.
Hypothesis xnz : x != z.
Hypothesis ynz : y != z.
Hypothesis g_xyz :
  (g x == [::y]) && (g y == [:: x; z]).

Lemma graph_proof2 : dfs_path g [::] x z.
Proof.
have pp: path (grel g) x [::y;z].
  rewrite /= andbT.
  move/andP: g_xyz => [/eqP -> /eqP ->].
  rewrite !inE. rewrite !eqxx. rewrite orbT. by [].
apply (DfsPath pp).
  rewrite /=. by [].
rewrite disjoint_sym. rewrite disjoint0.
by [].
Qed.

Exercises

Exercises taken from Map Spring School (thanks to L. Rideau)

State and prove the following statements

E union F = (E minus F) union (F minus E) union (E inter F)