Finite Sets
(* FINITE SETS *)
(* by Venanzio Capretta *)
(* Coq version 6.2.3 *)
(* Definition of the finite sets of the form *)
(* (Finite n) = {0,1, ..., n-1} . *)
Require Export Arith.
Require Export Compare_dec.
Require Export Type_Constructions.
Require Export Non_dep_eq.
Implicit Arguments On.
(* The empty set. *)
Inductive
empty : Set := .
(* You can always construct a function from the empty set to any set. *)
Definition
from_empty : (A:Set)empty -> A :=
[A : Set](empty_rec [e]A).
(* Definition of finite sets. *)
Fixpoint
Finite [n : nat] : Set :=
Cases n of
O => empty
| (S n') => unit + (Finite n')
end.
(* We define an injection function that allows to write *)
(* (fin_inj n m) for the m-th element of (Finite n). *)
Fixpoint
fin_inj [n, m : nat] : (gt n m) -> (Finite n) :=
<[n:nat](gt n m) -> (Finite n)>
Cases n of
O => [p : (gt O m)](False_rec (Finite O) (lt_n_O m p))
| (S n') => <[m:nat](gt (S n') m) -> (Finite (S n'))>
Cases m of
O => [_ : (gt (S n') O)](inl ? ? tt)
| (S m') => [p : (gt (S n') (S m'))]
(inr ? ? (fin_inj (gt_S_n m' n' p)))
end
end.
(* We can extract the index from an element of a finite type. *)
Fixpoint
fin_extr [n : nat] : (Finite n) -> nat :=
<[n:nat](Finite n) -> nat>
Cases n of
O => (from_empty nat)
| (S n') => [i : (Finite (S n'))]
Cases i of
(inl _) => O
| (inr j) => (S (fin_extr j))
end
end.
Lemma
fin_extr_gt : (n : nat)(i : (Finite n))(gt n (fin_extr i)).
Lemma
fin_extr_injection : (n : nat)(i1, i2 : (Finite n))
(fin_extr i1) = (fin_extr i2)
-> i1 = i2.
Lemma
fin_extr_eq : (n, m : nat)(p : (gt n m))
(fin_extr (fin_inj p)) = m.
Lemma
fin_section :
(n : nat)(i : (Finite n))
(fin_inj (fin_extr_gt i)) = i.
Lemma
fin_unicity :
(n : nat)(m : nat)(p1, p2 : (gt n m))
(fin_inj p1) = (fin_inj p2).
Section Finite_n.
Variable n : nat.
(* Now on we work on (Finite n). *)
(* Since gt is decidable, we can use (Finite n) as a subtype of nat. *)
Lemma
gt_decidable : (m : nat){(gt n m)}+{~(gt n m)}.
(*
To be able to use the decidability of gt as a decision procedure
we need gt_decidable to be Transparent. So we have to give the commands
Transparent le_lt_dec.
Transparent le_gt_dec.
Transparent gt_decidable.
(also the other decidability results used in gt_decidable must be
trasparent).
But we don't want le_lt_dec and le_gt_dec to be trasparent.
The only other solution that I know is to give directly the
definition of gt_decidable without using le_lt_dec and le_gt_dec.
I did this by copying the result of the command
Eval Compute in gt_decidable.
*)
Definition
gt_dec : (m : nat){(gt n m)}+{~(gt n m)} :=
[m:nat]
<[_:{(le n m)}+{(le (S m) n)}]
{(le (S m) n)}+{((le (S m) n)->False)}>
Cases
(Fix F{F/1 : (n0,m0:nat){(le n0 m0)}+{(le (S m0) n0)} :=
[n0:nat]
<[n1:nat](m0:nat){(le n1 m0)}+{(le (S m0) n1)}>
Cases n0 of
O =>
[m0:nat]
(left (le (0) m0) (le (S m0) (0))
(le_O_n m0))
| (S n1) =>
[m0:nat]
(Fix F0{F0/1 : (n2:nat)
{(le (S n1) n2)}
+{(le (S n2) (S n1))} :=
[n2:nat]
<[n3:nat]
{(le (S n1) n3)}
+{(le (S n3) (S n1))}>
Cases n2 of
O =>
(right
(le (S n1) (0))
(le (1) (S n1))
(lt_O_Sn n1))
| (S n3) =>
<[_:{(le n1 n3)}
+{(le (S n3) n1)}]
{(le (S n1) (S n3))}
+{(le (S (S n3))
(S n1))}>
Cases (F n1 n3) of
(left y) =>
(left
(le (
S n1)
(
S n3))
(le
(
S (S n3))
(
S n1))
(le_n_S n1
n3 y))
| (right y) =>
(right
(le (
S n1)
(
S n3))
(le
(
S (S n3))
(
S n1))
(lt_n_S n3
n1 y))
end
end} m0)
end} n m)
of
(left H) =>
(right (le (S m) n) (le (S m) n)->False
(le_not_gt n m H))
| (right g) => (left (le (S m) n) (le (S m) n)->False g)
end.
(* The following associate to a natural number m the set (Finite n) *)
(* if and only if m<n. Otherwise it gives the default value unit. *)
(* At the same time we define an immersion function that associates *)
(* to m an element of (nat_type m). *)
(* Note that we use the type (sigTS Set [A:Set]A), that can be *)
(* thought of as the disjoint union of all Sets. *)
Definition
nat_type_el : nat -> (sigTS Set [A:Set]A) :=
[m : nat]
Cases (gt_dec m) of
(left p) => (existTS Set [A:Set]A (Finite n) (fin_inj p))
| (right _) => (existTS Set [A:Set]A unit tt )
end.
Definition
nat_type : nat -> Set :=
[m : nat](projTS1 (nat_type_el m)).
(* For any m:nat we associate an element of (nat_type m). *)
Definition
nat_inj : (m:nat)(nat_type m) :=
[m : nat](projTS2 (nat_type_el m)).
(* This allow us, when we want to index elements of (Finite n) on the *)
(* natural numbers, to give just the index m and let Coq synthetize *)
(* the proof of (gt n m). *)
(* Definition of a successor function for finite sets. *)
Definition
fin_succ : (Finite n) -> (Finite (S n)) :=
[i : (Finite n)]
(fin_inj (gt_n_S n (fin_extr i) (fin_extr_gt i))).
(* fin_succ behaves well with respect to fin_inj. *)
Lemma
fin_succ_inj :
(m : nat)(p : (gt (S n) (S m)))
(fin_succ (fin_inj (gt_S_n m n p))) =
(fin_inj p).
(* The following is equivalent to saying that (Finite O) is empty. *)
Definition
empty_finite_O : (S : Set)(Finite O) -> S :=
[S : Set][i : (Finite O)]
(False_rec S (lt_n_O (fin_extr i) (fin_extr_gt i))).
End Finite_n.
Infix 4 "}-" nat_inj.
(* We now want to define a recursion principle for finite sets. *)
(* The O element of a non-empty finite set. *)
Definition
fin_zero : (n : nat)(Finite (S n)) :=
[n](fin_inj (gt_Sn_O n)).
Implicit Arguments Off.
Definition
fin_rec' :
(P : (n:nat)(Finite n) -> Set)
((n:nat)(P (S n) (fin_zero n))) ->
((n,m:nat)(p:(gt n m))
(P n (fin_inj p)) ->
(P (S n) (fin_inj (gt_n_S n m p)))) ->
(n,m:nat)(p:(gt n m))(P n (fin_inj p)).
Definition
fin_rec :
(P : (n:nat)(Finite n) -> Set)
((n:nat)(P (S n) (fin_inj (gt_Sn_O n)))) ->
((n:nat)(i:(Finite n))
(P n i) -> (P (S n) (fin_succ i))) ->
(n:nat)(i:(Finite n))(P n i).
Implicit Arguments On.
(* Elements of a finite set obtained from equal natural numbers are equal. *)
Theorem
fun_inj_eq : (n, m1, m2 : nat)(p1 : (gt n m1))(p2 : (gt n m2))m1=m2
-> (fin_inj p1) = (fin_inj p2).
Implicit Arguments Off.
25/02/99, 14:36