Lesson 4

Introduction to finite sets
Finite graph in SSR
Proving Kosaraju's algorithm

Finite sets

In SSR, they are sets over a finite type T

a set encapsulates an indicator function {ffun T -> bool}

sets share the collective predicate _ \in _ with lists

Definition x0 : 'I_10 := inZp 0.
Definition x1 : 'I_10 := inZp 1.
Definition x2 : 'I_10 := inZp 2.
Definition x3 : 'I_10 := inZp 3.
Definition x4 : 'I_10 := inZp 4.
Definition x5 : 'I_10 := inZp 5.
Definition x6 : 'I_10 := inZp 6.
Definition x7 : 'I_10 := inZp 7.
Definition x8 : 'I_10 := inZp 8.
Definition x9 : 'I_10 := inZp 9.

Definition zs : {set 'I_10} := set0.

Lemma zs0 : x0 \notin zs.
Proof.
rewrite inE.
by [].
Qed.

Definition alls : {set 'I_10} := setT.

Lemma alls0 : x0 \in alls.
Proof.
rewrite inE.
by [].
Qed.

Lemma disjoint_az : [disjoint zs & alls].
Proof.
apply/pred0P.
move=> x.
rewrite /=.
rewrite !inE.
by [].
Qed.

Definition odds := [set x : 'I_10 | odd x].

Lemma odds5 : x5 \in odds.
Proof.
rewrite inE.
by [].
Qed.

Definition evens := x0 |: (x2 |: (x4 |: (x6 |: (x8 |: zs)))).

Lemma oddUeven :  odds :|: evens = alls.
Proof.
apply/setP.
move=> i.
rewrite !inE.
rewrite /=.
case: i.
rewrite /=.
case => //.
by do 9 (case => //).
Qed.

Lemma oddIeven :  odds :&: evens = zs.
Proof.
apply/setP.
move=> i.
rewrite !inE.
by case i; do 10 (case => //).
Qed.

Path

path r x p : r relation, x is an element, p is a list (x :: p) is a path starting at x and ending at (last x p) of r related element

Graph

a graph is manipulated either by its adjacency relation or its adjacency function
the functions grel and rgraph let you change representation

Depth-First Search

defs f n x v : returns the nodes visited by a dfs at depth n avoiding the nodes in v

Connection

boolean relation that indicates if two nodes are connected

Kosaraju's algorithm

2 dfs traversals
one to build a post-fixed stack
one on the reverse graph to collect the components

save script

load script