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.


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


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


  • 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


  • 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


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


  • different ranges are provided


  • 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


  • one can use exchange sum and product

Property, Relation and Morphism

save script