## Roadmap for lessons 3 and 4

• finite types
• big operators
• playing with graph

## Lesson 3

• The SSR 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

## 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

## Booleans

• for finite type, boolean reflection can be extended to quantifiers

## 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

## Big operators

provide a library to manipulate iterations in SSR 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 reorder the bigop

## Abelian Monoid structure

• one can use communitativity to massage the bigop

## Distributivity

• one can use exchange sum and product