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