--- /dev/null
+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.
+
projects / helm.git / blobdiff