---

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

Property, Relation and Morphism

---