Require Export Standard.

Section Fin_Definitions.

   Section finite_sets.
   
      Definition Fin: N -> Set := (NatFam [_]Set Empty [_](LOr One)).
      
(* Constructors: first element, next element *)      
      Definition ffe: (n:N) (Fin (succ n)).
      Intros.
      MApply '(in_l One (Fin n) tt).
      Defined.

      Definition fne: (n:N) (Fin n) -> (Fin (succ n)).
      Intros.
      MApply '(in_r One (Fin n)).
      Defined.

(* Eliminator *)
      Definition finrec: (n:N; P:(Fin (succ n))->Set) (P (ffe n)) -> ((a:(Fin n))(P (fne n a))) -> (p:(Fin (succ n))) (P p).
      Intros.   
      MElim 'p '(when One (Fin n)).
      MElim 's 'onerec.
      MApply '(H0 t).
      Defined.

(* Predecessor *)       
      Definition fpe: (n:N) (Fin (succ (succ n))) -> (Fin (succ n)).
      Intros.
      MElim 'H '(finrec (succ n)).
      MApply '(ffe n).
      Defined.

(* Injection of (Fin (succ n)) in N *)      
      Definition fn: (n:N) (Fin (succ n)) -> N := (natrec [m](Fin (succ m))->N [_]zero [m;p](finrec (succ m) [_]N zero [a](succ (p a)))).
(*
      Intros n.
      Elim n using natrec.
      Intros.
      Exact zero.
      Intros.
      Apply H.
      Apply fpe.
      Apply H0.
*)
      
(* Surjection of N in (Fin (succ n)): (ffe n) returned if m >= n *)     
      Definition nf: (n,m:N) (Fin (succ n)) := (natrec [m]N->(Fin (succ m)) [_](ffe zero) [n';p](natrec [_](Fin (succ (succ n'))) (ffe (succ n')) [m';p'](fne (succ n') (p m')))).

(* Left injection of (Fin m) -> (Fin (add m n)) *)
      Definition fil: (m,n:N) (Fin m) -> (Fin (add m n)) := 
                      (natrec [m](n:N) (Fin m) -> (Fin (add m n))
                      [n](efq [_](Fin (add zero n)))
                      [m';_](natrec [n](Fin (succ m')) -> (Fin (add (succ m') n))
                      [a]a [n';_;a](nf (add (succ m') n') (fn m' a)))).
            
(* Right injection of (Fin n) -> (Fin (add m n)) *)	    
      Definition fir: (m,n:N) (Fin n) -> (Fin (add m n)) :=
                      [m](natrec [n](Fin n) -> (Fin (add m n))
                      (efq [_](Fin m))
                      [n';_;a](nf (add m n') (add (fn n' a) m))).

   End finite_sets.

   Section explicit_finite_domain_functions.      
      
      Definition xfdf_list: (S:Set; n:N) ((Fin n) -> S) -> (List S) := [S](natrec [m]((Fin m)->S)->(List S) [_](empty S) [m;p;f](fr S (p [k](f (fne m k))) (f (ffe m)))).   
      
      Definition xfdf_add': (S:Set; m:N) ((Fin (succ m))->S) -> (n:N) ((Fin (succ n))->S) -> (Fin (add_three (succ m) n one)) -> S :=
                            [S;m;v;n;w;a](ite [_]S (w (nf n (sub (fn (add (succ m) n) a) (succ m))))
                            (v (nf m (fn (add (succ m) n) a)))
                            (b_le (fn (add (succ m) n) a) m)). 

      Definition xfdf_add: (S:Set; m:N) ((Fin m)->S) -> (n:N) ((Fin n)->S) -> (Fin (add m n)) -> S :=
                           [S](natrec [m]((Fin m)->S) -> (n:N) ((Fin n)->S) -> (Fin (add m n)) -> S
                           [_](natrec [n]((Fin n)->S) -> (Fin (add zero n)) -> S
                           [w]w [n';_;w;a](w (nf n' (fn (add zero n') a))))
                           [m';_;v](natrec [n]((Fin n)->S) -> (Fin (add (succ m') n)) -> S
                           [_]v [n';_](xfdf_add' S m' v n'))).

   End explicit_finite_domain_functions.
   
   Section finite_domain_functions.
   
      Definition FDF: Set -> Set := [S](Sigma N [n](Fin n)->S).
   
      Definition fdf_i: (S:Set; n:N) ((Fin n)->S) -> (FDF S) := [S](pair N [n](Fin n)->S).
   
      Definition fdf_e: (S:Set; P:(FDF S)->Set) ((n:N; f:(Fin n)->S) (P (fdf_i S n f))) -> (v:(FDF S))(P v) :=
                        [S:Set](psplit N [n](Fin n)->S).

      Definition fdf_n: (S:Set) (FDF S) -> N := [S](fdf_e S [_]N [a;_]a).
      
      Definition fdf_f: (S:Set; v:(FDF S)) (Fin (fdf_n S v)) -> S := [S](fdf_e S [p](Fin (fdf_n S p))->S [_;p]p).

      Definition fdf_empty: (S:Set) (FDF S) := [S](fdf_i S zero (efq [_]S)).
   
      Definition fdf_fr: (S:Set) (FDF S) -> S -> (FDF S) := [S;v;a](fdf_i S (succ (fdf_n S v)) (when One (Fin (fdf_n S v)) [_]S [_]a (fdf_f S v))).
(*
      Definition lfdf: (S:Set) (List S) -> (FDF S) := [S](listrec S [_](FDF S) (fdf_empty S) [_](fdf_fr S)).
*)   
      Definition fdfl: (S:Set) (FDF S) -> (List S) := [S](fdf_e S [_](List S) (xfdf_list S)).

      Definition fdf_add: (S:Set) (FDF S) -> (FDF S) -> (FDF S) := [S;v;w](fdf_i S (add (fdf_n S v) (fdf_n S w)) (xfdf_add S (fdf_n S v) (fdf_f S v) (fdf_n S w) (fdf_f S w))).

   End finite_domain_functions.

End Fin_Definitions.

Section Fin_Results.

   Section fin_results.

(* Immediate result used for reference
      Theorem fpe_fne: (n:N; a:(Fin (succ n))) (Id (Fin (succ n)) (fpe n (fne (succ n) a)) a).
*)
      Theorem fne_ini: (n:N; a,b:(Fin n)) (Id (Fin (succ n)) (fne n a) (fne n b)) -> (Id (Fin n) a b).
      Intros n.
      Elim n using natrec.
      Intros.
      MElim a efq.
      Intros.
      MApply '(id_repl (Fin (succ n0)) a (fpe n0 (fne (succ n0) a))).
      MApply '(id_repl (Fin (succ n0)) b (fpe n0 (fne (succ n0) b))).
      MApply '(id_comp (Fin (succ (succ n0))) (Fin (succ n0)) (fpe n0)).
      Qed.

      Theorem fn_le: (n:N; a:(Fin (succ n))) (LE (fn n a) n).
      Intros n.
      Elim n using natrec; Intros.
      MApply 'le_r.
      MElim 'a '(finrec (succ n0)).
      MApply 'le_wf.
      MApply 'le_comp_succ.
      MApply '(H a0).
      Qed.

      Theorem nfn': (n:N; a:(Fin (succ n)); m:N) (LE m n) -> (Id (Fin (succ n)) (nf n m) a) -> (Id N (fn n a) m).
      Intros n.
      Elim n using natrec.
      Intros; Simpl.
      MApply 'id_comm.
      MApply '(le_zero m).      
      Intros n' H a m.
      Elim a using (finrec (succ n')).   
      MElim 'm 'natrec.
      MCut 'Empty.
      Unfold fne in H2.
      MApply '(lor_p4 One (Fin (succ n')) tt (nf n' n0)).
      MElim 'H3 'efq.
      Intros a'.
      Elim m using natrec.
      Simpl.
      Intros.
      MCut 'Empty.
      MApply '(lor_p4 One (Fin (succ n')) tt a').
      MElim 'H2 'efq.      
      Intros.
      Simpl.
      MApply '(id_comp N).
      Change (Id N (fn n' a') n0).
      MApply '(H a' n0).
      Simpl in H2.
      Change (Id (Fin (succ (succ n'))) (fne (succ n') (nf n' n0)) (fne (succ n') a')) in H2.
      MApply 'fne_ini.
      Qed.

      Theorem nfn: (n:N; m:N) (LE m n) -> (Id N (fn n (nf n m)) m).
      Intros.
      MApply 'nfn'.
      Qed.
          
      Theorem fnf_fne: (n:N; a:(Fin n)) (Id (Fin (succ n)) (nf n (fn n (fne n a))) (fne n a)).
      Intros n.
      Elim n using natrec; Intros.
      MElim 'a 'efq.
      Elim a using (finrec n0); Intros.
      MElim 'n0 'natrec.
      MSimpl.
      MApply '(id_comp (Fin (succ n0))).
      MApply '(H a0).
      Qed.

      Theorem fnf: (n:N; a:(Fin (succ n))) (Id (Fin (succ n)) (nf n (fn n a)) a).
      Intros.
      Elim a using (finrec n); Intros.
      MElim 'n 'natrec.      
      MApply 'fnf_fne.
      Qed.

   End fin_results.

   Section xfdf_results.   
      
      Theorem xfdfl_lin: (S:Set; n:N; a:(Fin n); v:(Fin n)->S) (LIn S (v a) (xfdf_list S n v)).
      Intros S n.
      Elim n using natrec; Intros.
      MElim a efq.
      MSimpl.
      MApply 'lin_fr_i.
      MElim 'a '(finrec n0).
      MApply 'in_r.
      MApply 'in_l.
      MApply '(H a0 [k:(Fin n0)](v (fne n0 k))).
      Qed.
            
      Theorem xfdfa_fil: (S:Set; m:N; a:(Fin m); v:(Fin m)->S; n:N; w:(Fin n)->S) (Id S (xfdf_add S m v n w (fil m n a)) (v a)).
      Intros S m.
      Elim m using natrec.
      Intros a.
      Elim a using efq.
      Intros m' H a v n.
      Elim n using natrec.
      Intros.
      MApply 'id_r.
      Intros n' H0 w.
      Simpl.
      MCut '(LE (fn m' a) (add (succ m') n')).
      MApply '(le_trans m').
      MApply 'fn_le.
      MApply '(id_repl N (add (succ m') n') (add_three m' n' one)).
      MApply 'id_comm.
      MApply '(add_succ m' n').
      MApply '(le_add m' (succ n')).      
      Unfold xfdf_add'.      
      MApply '(id_repl Boole (b_le (fn (add (succ m') n') (nf (add (succ m') n') (fn m' a))) m') true).
      MApply 'id_comm.
      Fold (LE (fn (add (succ m') n') (nf (add (succ m') n') (fn m' a))) m').
      MApply '(id_repl N (fn (add (succ m') n') (nf (add (succ m') n') (fn m' a))) (fn m' a)).
      MApply 'id_comm.
      MApply 'nfn.
      MApply 'fn_le.
      Simpl.
      MApply '(id_comp (Fin (succ m'))).
      MApply '(id_repl N (fn (add (succ m') n') (nf (add (succ m') n') (fn m' a))) (fn m' a)).
      MApply 'id_comm.
      MApply 'nfn.
      MApply 'fnf.
      Qed.

      Theorem xfdfa_fir: (S:Set; m:N; v:(Fin m)->S; n:N; a:(Fin n); w:(Fin n)->S) (Id S (xfdf_add S m v n w (fir m n a)) (w a)).
      Intros S m.
      Elim m using natrec.
      Intros v n.
      Elim n using natrec.
      Intros a.
      Elim a using efq.
      Intros n' H a w.
      MSimpl.
      MApply '(id_comp (Fin (succ n'))).
      MApply '(id_repl N (fn (add zero n') (nf (add zero n') (fn n' a))) (fn n' a)).
      MApply 'id_comm.
      MApply 'nfn.
      MApply '(le_trans n').
      MApply 'fn_le.
      MApply '(id_repl N (add zero n') n').
      MApply '(add_comm n' zero).
      MApply 'le_r.
      MApply 'fnf.
      Intros m' H v n.
      Elim n using natrec.
      Intros a.
      Elim a using efq.
      Intros n' H' a w.
      (MSimpl; Apply succ_fold). (**)
      MCut '(LE (succ (add (fn n' a) m')) (add (succ m') n')).
      MApply '(id_repl N (add (succ m') n') (succ (add m' n'))).
      MApply 'id_comm.
      MApply 'add_succ.
      MApply 'le_comp_succ.
      MApply '(id_repl N (add m' n') (add n' m')).
      MApply 'add_comm.
      MApply 'le_comp_add.
      MApply 'fn_le.
      Unfold xfdf_add'.
      MApply '(id_repl Boole (b_le (fn (add (succ m') n') (nf (add (succ m') n') (succ (add (fn n' a) m')))) m') false).
      MApply 'id_comm.
      Fold (GT (fn (add (succ m') n') (nf (add (succ m') n') (succ (add (fn n' a) m')))) m').
      MApply 'le_gt.      
      MApply '(id_repl N (fn (add (succ m') n') (nf (add (succ m') n') (succ (add (fn n' a) m')))) (succ (add (fn n' a) m'))).
      MApply 'id_comm.
      MApply 'nfn.
      MApply 'le_comp_succ.
      MApply '(id_repl N (add (fn n' a) m') (add m' (fn n' a))).
      MApply 'add_comm.
      MApply 'le_add.
      MSimpl.
      MApply 'pred_fold.
      MApply '(id_comp (Fin (succ n'))).
      MApply '(id_repl N (sub (pred (fn (add (succ m') n') (nf (add (succ m') n') (succ (add (fn n' a) m'))))) m') (fn n' a)).
      MApply 'id_comm.
      MApply 'add_sub_e.
      MApply 'succ_pred_e.
      MApply '(id_repl N (add m' (fn n' a)) (add (fn n' a) m')).
      MApply 'add_comm.
      MApply 'nfn.
      MApply 'fnf.
      Qed.

   End xfdf_results.

End Fin_Results.