To play this document inside your browser use ALT-N and ALT-P. If you get stack overflow errors, try to use Google Chrome or Chromium with the command line option --js-flags="--harmony-tailcalls".

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.

Roadmap for lessons 3 and 4

  • finite types
  • big operators

Lesson 3

  • The math-comp library gives some support for finite types.
  • 'I_n is the the set of natural numbers smaller than n.
  • a : 'I_n is composed of a value m and a proof that m < n.

  • Example : oid modifies the proof part with an equivalent one.

Note

  • nat_of_ord is a coercion (see H)
  • 'I_0 is an empty type

Equality

  • Every finite type is also an equality type.
  • For 'I_n, only the value matters

An optimic map from nat to ordinal : inord

  • If the expected type has shape 'I_n.+1
  • Takes a natural number as input and return an element of 'I_n.+1
  • The same number if it is small enough, otherwise 0.

Sequence

  • a finite type can be seen as a sequence
  • enum T gives this sequence.
  • it is duplicate free.
  • it relates to the cardinal of a finite type

Boolean theory of finite types.

  • for finite type, boolean reflection can be extended to quantifiers
  • getting closer to classical logic!

Selecting an element

  • pick selects an element that has a given property
  • pickP triggers the reflection

Building finite types

  • SSR automatically discovers the pair of two finite types is finite
  • For functions there is an explicit construction ffun x => body

Installing the finite type structure for an arbitrary type

  • When you have a type that you know is finite, you need some work to make it recognized.

  • Solution: exhibit an injection into a finite type.

  • The lemma monster_ord_can means that there is an injection from forest_monster into a known finite type. This gives a host of structure bridges to eqType, choiceType, countType, finiteType.

Big operators

  • Big operators provide a library to manipulate iterations in math-comp
  • this is an encapsulation of the fold function

Notation

  • iteration is provided by the \big notation
  • the basic operation is on list
  • special notations are introduced for usual case (\sum, \prod, \bigcap ..)

Range

  • different ranges are provided

Filtering

  • it is possible to filter elements from the range

Switching range

  • it is possible to change representation (big_nth, big_mkord).

Big operators and equality

  • one can exchange function and/or predicate

Monoid structure

  • one can use associativity to reorganize the bigop

Abelian Monoid structure

  • one can use communitativity to massage the bigop

Distributivity

  • one can exchange sum and product

Property, Relation and Morphism