helm/coq-contribs/SUBSETS/xt_fin.v

   1 Require Export Standard.
   2
   3 Section Fin_Definitions.
   4
   5    Section finite_sets.
   6
   7       Definition Fin: N -> Set := (NatFam [_]Set Empty [_](LOr One)).
   8
   9 (* Constructors: first element, next element *)
  10       Definition ffe: (n:N) (Fin (succ n)).
  11       Intros.
  12       MApply '(in_l One (Fin n) tt).
  13       Defined.
  14
  15       Definition fne: (n:N) (Fin n) -> (Fin (succ n)).
  16       Intros.
  17       MApply '(in_r One (Fin n)).
  18       Defined.
  19
  20 (* Eliminator *)
  21       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).
  22       Intros.
  23       MElim 'p '(when One (Fin n)).
  24       MElim 's 'onerec.
  25       MApply '(H0 t).
  26       Defined.
  27
  28 (* Predecessor *)
  29       Definition fpe: (n:N) (Fin (succ (succ n))) -> (Fin (succ n)).
  30       Intros.
  31       MElim 'H '(finrec (succ n)).
  32       MApply '(ffe n).
  33       Defined.
  34
  35 (* Injection of (Fin (succ n)) in N *)
  36       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)))).
  37 (*
  38       Intros n.
  39       Elim n using natrec.
  40       Intros.
  41       Exact zero.
  42       Intros.
  43       Apply H.
  44       Apply fpe.
  45       Apply H0.
  46 *)
  47
  48 (* Surjection of N in (Fin (succ n)): (ffe n) returned if m >= n *)
  49       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')))).
  50
  51 (* Left injection of (Fin m) -> (Fin (add m n)) *)
  52       Definition fil: (m,n:N) (Fin m) -> (Fin (add m n)) :=
  53                       (natrec [m](n:N) (Fin m) -> (Fin (add m n))
  54                       [n](efq [_](Fin (add zero n)))
  55                       [m';_](natrec [n](Fin (succ m')) -> (Fin (add (succ m') n))
  56                       [a]a [n';_;a](nf (add (succ m') n') (fn m' a)))).
  57
  58 (* Right injection of (Fin n) -> (Fin (add m n)) *)
  59       Definition fir: (m,n:N) (Fin n) -> (Fin (add m n)) :=
  60                       [m](natrec [n](Fin n) -> (Fin (add m n))
  61                       (efq [_](Fin m))
  62                       [n';_;a](nf (add m n') (add (fn n' a) m))).
  63
  64    End finite_sets.
  65
  66    Section explicit_finite_domain_functions.
  67
  68       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)))).
  69
  70       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 :=
  71                             [S;m;v;n;w;a](ite [_]S (w (nf n (sub (fn (add (succ m) n) a) (succ m))))
  72                             (v (nf m (fn (add (succ m) n) a)))
  73                             (b_le (fn (add (succ m) n) a) m)).
  74
  75       Definition xfdf_add: (S:Set; m:N) ((Fin m)->S) -> (n:N) ((Fin n)->S) -> (Fin (add m n)) -> S :=
  76                            [S](natrec [m]((Fin m)->S) -> (n:N) ((Fin n)->S) -> (Fin (add m n)) -> S
  77                            [_](natrec [n]((Fin n)->S) -> (Fin (add zero n)) -> S
  78                            [w]w [n';_;w;a](w (nf n' (fn (add zero n') a))))
  79                            [m';_;v](natrec [n]((Fin n)->S) -> (Fin (add (succ m') n)) -> S
  80                            [_]v [n';_](xfdf_add' S m' v n'))).
  81
  82    End explicit_finite_domain_functions.
  83
  84    Section finite_domain_functions.
  85
  86       Definition FDF: Set -> Set := [S](Sigma N [n](Fin n)->S).
  87
  88       Definition fdf_i: (S:Set; n:N) ((Fin n)->S) -> (FDF S) := [S](pair N [n](Fin n)->S).
  89
  90       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) :=
  91                         [S:Set](psplit N [n](Fin n)->S).
  92
  93       Definition fdf_n: (S:Set) (FDF S) -> N := [S](fdf_e S [_]N [a;_]a).
  94
  95       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).
  96
  97       Definition fdf_empty: (S:Set) (FDF S) := [S](fdf_i S zero (efq [_]S)).
  98
  99       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))).
 100 (*
 101       Definition lfdf: (S:Set) (List S) -> (FDF S) := [S](listrec S [_](FDF S) (fdf_empty S) [_](fdf_fr S)).
 102 *)
 103       Definition fdfl: (S:Set) (FDF S) -> (List S) := [S](fdf_e S [_](List S) (xfdf_list S)).
 104
 105       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))).
 106
 107    End finite_domain_functions.
 108
 109 End Fin_Definitions.
 110
 111 Section Fin_Results.
 112
 113    Section fin_results.
 114
 115 (* Immediate result used for reference
 116       Theorem fpe_fne: (n:N; a:(Fin (succ n))) (Id (Fin (succ n)) (fpe n (fne (succ n) a)) a).
 117 *)
 118       Theorem fne_ini: (n:N; a,b:(Fin n)) (Id (Fin (succ n)) (fne n a) (fne n b)) -> (Id (Fin n) a b).
 119       Intros n.
 120       Elim n using natrec.
 121       Intros.
 122       MElim a efq.
 123       Intros.
 124       MApply '(id_repl (Fin (succ n0)) a (fpe n0 (fne (succ n0) a))).
 125       MApply '(id_repl (Fin (succ n0)) b (fpe n0 (fne (succ n0) b))).
 126       MApply '(id_comp (Fin (succ (succ n0))) (Fin (succ n0)) (fpe n0)).
 127       Qed.
 128
 129       Theorem fn_le: (n:N; a:(Fin (succ n))) (LE (fn n a) n).
 130       Intros n.
 131       Elim n using natrec; Intros.
 132       MApply 'le_r.
 133       MElim 'a '(finrec (succ n0)).
 134       MApply 'le_wf.
 135       MApply 'le_comp_succ.
 136       MApply '(H a0).
 137       Qed.
 138
 139       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).
 140       Intros n.
 141       Elim n using natrec.
 142       Intros; Simpl.
 143       MApply 'id_comm.
 144       MApply '(le_zero m).
 145       Intros n' H a m.
 146       Elim a using (finrec (succ n')).
 147       MElim 'm 'natrec.
 148       MCut 'Empty.
 149       Unfold fne in H2.
 150       MApply '(lor_p4 One (Fin (succ n')) tt (nf n' n0)).
 151       MElim 'H3 'efq.
 152       Intros a'.
 153       Elim m using natrec.
 154       Simpl.
 155       Intros.
 156       MCut 'Empty.
 157       MApply '(lor_p4 One (Fin (succ n')) tt a').
 158       MElim 'H2 'efq.
 159       Intros.
 160       Simpl.
 161       MApply '(id_comp N).
 162       Change (Id N (fn n' a') n0).
 163       MApply '(H a' n0).
 164       Simpl in H2.
 165       Change (Id (Fin (succ (succ n'))) (fne (succ n') (nf n' n0)) (fne (succ n') a')) in H2.
 166       MApply 'fne_ini.
 167       Qed.
 168
 169       Theorem nfn: (n:N; m:N) (LE m n) -> (Id N (fn n (nf n m)) m).
 170       Intros.
 171       MApply 'nfn'.
 172       Qed.
 173
 174       Theorem fnf_fne: (n:N; a:(Fin n)) (Id (Fin (succ n)) (nf n (fn n (fne n a))) (fne n a)).
 175       Intros n.
 176       Elim n using natrec; Intros.
 177       MElim 'a 'efq.
 178       Elim a using (finrec n0); Intros.
 179       MElim 'n0 'natrec.
 180       MSimpl.
 181       MApply '(id_comp (Fin (succ n0))).
 182       MApply '(H a0).
 183       Qed.
 184
 185       Theorem fnf: (n:N; a:(Fin (succ n))) (Id (Fin (succ n)) (nf n (fn n a)) a).
 186       Intros.
 187       Elim a using (finrec n); Intros.
 188       MElim 'n 'natrec.
 189       MApply 'fnf_fne.
 190       Qed.
 191
 192    End fin_results.
 193
 194    Section xfdf_results.
 195
 196       Theorem xfdfl_lin: (S:Set; n:N; a:(Fin n); v:(Fin n)->S) (LIn S (v a) (xfdf_list S n v)).
 197       Intros S n.
 198       Elim n using natrec; Intros.
 199       MElim a efq.
 200       MSimpl.
 201       MApply 'lin_fr_i.
 202       MElim 'a '(finrec n0).
 203       MApply 'in_r.
 204       MApply 'in_l.
 205       MApply '(H a0 [k:(Fin n0)](v (fne n0 k))).
 206       Qed.
 207
 208       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)).
 209       Intros S m.
 210       Elim m using natrec.
 211       Intros a.
 212       Elim a using efq.
 213       Intros m' H a v n.
 214       Elim n using natrec.
 215       Intros.
 216       MApply 'id_r.
 217       Intros n' H0 w.
 218       Simpl.
 219       MCut '(LE (fn m' a) (add (succ m') n')).
 220       MApply '(le_trans m').
 221       MApply 'fn_le.
 222       MApply '(id_repl N (add (succ m') n') (add_three m' n' one)).
 223       MApply 'id_comm.
 224       MApply '(add_succ m' n').
 225       MApply '(le_add m' (succ n')).
 226       Unfold xfdf_add'.
 227       MApply '(id_repl Boole (b_le (fn (add (succ m') n') (nf (add (succ m') n') (fn m' a))) m') true).
 228       MApply 'id_comm.
 229       Fold (LE (fn (add (succ m') n') (nf (add (succ m') n') (fn m' a))) m').
 230       MApply '(id_repl N (fn (add (succ m') n') (nf (add (succ m') n') (fn m' a))) (fn m' a)).
 231       MApply 'id_comm.
 232       MApply 'nfn.
 233       MApply 'fn_le.
 234       Simpl.
 235       MApply '(id_comp (Fin (succ m'))).
 236       MApply '(id_repl N (fn (add (succ m') n') (nf (add (succ m') n') (fn m' a))) (fn m' a)).
 237       MApply 'id_comm.
 238       MApply 'nfn.
 239       MApply 'fnf.
 240       Qed.
 241
 242       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)).
 243       Intros S m.
 244       Elim m using natrec.
 245       Intros v n.
 246       Elim n using natrec.
 247       Intros a.
 248       Elim a using efq.
 249       Intros n' H a w.
 250       MSimpl.
 251       MApply '(id_comp (Fin (succ n'))).
 252       MApply '(id_repl N (fn (add zero n') (nf (add zero n') (fn n' a))) (fn n' a)).
 253       MApply 'id_comm.
 254       MApply 'nfn.
 255       MApply '(le_trans n').
 256       MApply 'fn_le.
 257       MApply '(id_repl N (add zero n') n').
 258       MApply '(add_comm n' zero).
 259       MApply 'le_r.
 260       MApply 'fnf.
 261       Intros m' H v n.
 262       Elim n using natrec.
 263       Intros a.
 264       Elim a using efq.
 265       Intros n' H' a w.
 266       (MSimpl; Apply succ_fold). (**)
 267       MCut '(LE (succ (add (fn n' a) m')) (add (succ m') n')).
 268       MApply '(id_repl N (add (succ m') n') (succ (add m' n'))).
 269       MApply 'id_comm.
 270       MApply 'add_succ.
 271       MApply 'le_comp_succ.
 272       MApply '(id_repl N (add m' n') (add n' m')).
 273       MApply 'add_comm.
 274       MApply 'le_comp_add.
 275       MApply 'fn_le.
 276       Unfold xfdf_add'.
 277       MApply '(id_repl Boole (b_le (fn (add (succ m') n') (nf (add (succ m') n') (succ (add (fn n' a) m')))) m') false).
 278       MApply 'id_comm.
 279       Fold (GT (fn (add (succ m') n') (nf (add (succ m') n') (succ (add (fn n' a) m')))) m').
 280       MApply 'le_gt.
 281       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'))).
 282       MApply 'id_comm.
 283       MApply 'nfn.
 284       MApply 'le_comp_succ.
 285       MApply '(id_repl N (add (fn n' a) m') (add m' (fn n' a))).
 286       MApply 'add_comm.
 287       MApply 'le_add.
 288       MSimpl.
 289       MApply 'pred_fold.
 290       MApply '(id_comp (Fin (succ n'))).
 291       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)).
 292       MApply 'id_comm.
 293       MApply 'add_sub_e.
 294       MApply 'succ_pred_e.
 295       MApply '(id_repl N (add m' (fn n' a)) (add (fn n' a) m')).
 296       MApply 'add_comm.
 297       MApply 'nfn.
 298       MApply 'fnf.
 299       Qed.
 300
 301    End xfdf_results.
 302
 303 End Fin_Results.
 304