I have made a basic theory of finite sets in Coq.
Syntax of Finite Sets (fsets)
An fset_expr can be
the empty set, an add operation,
a filter (set comprehension) of another set,
a cup (union) of two sets,
or a cap (intersection) of two sets.
Inductive fset_expr { A : Set } : Set :=
| fset_expr_empty : fset_expr
| fset_expr_add : fset_expr -> A -> fset_expr
| fset_expr_filter : fset_expr -> (A -> bool) -> fset_expr
| fset_expr_cup : fset_expr -> fset_expr -> fset_expr
| fset_expr_cap : fset_expr -> fset_expr -> fset_expr.
Semantics of Set Membership
in_fset s a means that the s : fset_expr contains the member a.
Inductive in_fset { A : Set } : fset_expr (A:=A) -> A -> Prop :=
| in_fset_add : forall x a, in_fset (fset_expr_add x a) a
| in_fset_added : forall x a0 a1, in_fset x a0 -> in_fset (fset_expr_add x a1) a0
| in_fset_cup_l : forall x y a, in_fset x a -> in_fset (fset_expr_cup x y) a
| in_fset_cup_r : forall x y a, in_fset y a -> in_fset (fset_expr_cup x y) a
| in_fset_cap : forall x y a, in_fset x a -> in_fset y a -> in_fset (fset_expr_cap x y) a
| in_fset_filter : forall x f a, in_fset x a -> (f a = true) -> in_fset (fset_expr_filter x f) a.
Subsets and Set Equality
Definition is_empty_fset {A : Set} (s : fset_expr (A:=A)) :=
forall a, ~(in_fset s a).
Definition subset_fset {A : Set} (x y : fset_expr (A:=A)) :=
forall a, in_fset x a -> in_fset y a.
Definition eq_fset {A : Set} (x y : fset_expr (A:=A)) :=
subset_fset x y /\ subset_fset y x.
Cardinality
This is where complications occured. I defined cardinality_fset s n which is supposed to mean that the finite set s : fset_expr contains n : nat elements.
Inductive cardinality_fset { A : Set } : fset_expr (A:=A) -> nat -> Prop :=
| cardinality_fset_empty : cardinality_fset fset_expr_empty 0
| cardinality_fset_add : forall s n a,
~(in_fset s a) ->
cardinality_fset s n ->
cardinality_fset (fset_expr_add s a) (S n)
| cardinality_fset_trans :
forall x y n,
eq_fset x y ->
cardinality_fset x n ->
cardinality_fset y n.
Problem
I could not prove that cardinality is well defined, i.e. every congruence class of fset_expr under relation eq_fset has a unique cardinality. Is it possible?
forall s : fset_expr (A:=A), exists n, (cardinality_fset s n /\ forall s' n', eq_fset s s' -> cardinality_fset s' n' -> n' = n).
