helm/coq-contribs/SUBSETS/st_nat.v

   1 Require Export st_logic.
   2
   3 Section Nat_Sets.
   4
   5    Section natural_numbers.
   6
   7       Definition N: Set := (List One).
   8
   9       Definition zero: N := (empty One).
  10
  11       Definition succ: N -> N := [n](fr One n tt).
  12
  13       Definition natrec: (P:N->Set) (P zero) ->
  14                          ((n:N) (P n) -> (P (succ n))) -> (n:N)(P n).
  15       Intros.
  16       MElim 'n 'listrec.
  17       MElim 's 'onerec.
  18       MApply '(H0 l).
  19       Defined.
  20
  21       Definition NatFam: (P:N->Type) (P zero) ->
  22                          ((n:N) (P n) -> (P (succ n))) -> (n:N)(P n).
  23       Intros.
  24       MElim 'n 'ListFam.
  25       MElim 's 'OneFam.
  26       MApply '(X0 l).
  27       Defined.
  28
  29       Definition one: N := (succ zero).
  30 (*
  31 Definition two:N := (succ one).
  32 *)
  33    End natural_numbers.
  34 (*
  35 Section sequences.
  36
  37 Definition ListS := [S:Set](N -> (List S)).
  38
  39 Definition BooleS: Set := N -> Boole.
  40
  41 Definition NS := N -> N.
  42
  43 Definition trues:BooleS := [_]true.
  44
  45 End sequences.
  46 *)
  47 End Nat_Sets.
  48
  49 Section Nat_Functions.
  50 (*
  51 Section bounded_iteration.
  52
  53 Variable S:Set; e:S; f:S->S->S.
  54
  55 Definition bs_iter: (N -> S) -> N -> S := [s](natrec [_]S e [m](f (s m))).
  56
  57 Definition rbs_iter: (N -> S) -> N -> S := [s;n](bs_iter s (succ n)).
  58
  59 End bounded_iteration.
  60
  61 Section nat_boolean_eq.
  62
  63 Variable S:Set.
  64
  65 Definition n_id: N -> N -> Boole := (natrec [_]N->Boole (natrec [_]Boole true [_;_]false)
  66                                     [_;pm'](natrec [_]Boole false [n';_](pm' n'))).
  67
  68 Definition ifeq: N -> N -> S -> S -> S := [m,n;a;b](ite [_]S b a (n_id m n)).
  69
  70 Definition ifz: N -> S -> S -> S := [n;a;b](natrec [_]S a [_;_]b n).
  71
  72 End nat_boolean_eq.
  73 *)
  74    Section less_equal.
  75
  76       Definition b_le: N -> N -> Boole := (natrec [_]N->Boole [n]true [m';p](natrec [_]Boole false [n';_](p n'))).
  77
  78       Definition LE: N -> N -> Set := [m,n](Id Boole (b_le m n) true).
  79
  80       Definition GT: N -> N -> Set := [m,n](Id Boole (b_le m n) false).
  81
  82    End less_equal.
  83
  84 End Nat_Functions.
  85
  86 Section Nat_Hints.
  87
  88    Section nat_fold.
  89
  90       Theorem succ_fold: (n:N; P:N->Set) (P (succ n)) -> (P (fr One n tt)).
  91       Intros.
  92       Assumption.
  93       Qed.
  94 (*
  95 Theorem LE_fold: (m,n:N; P:Set->Set) (P (LE m n)) -> (P (Id Boole (b_le m n) true)).
  96 Intros.
  97 Assumption.
  98 Qed.
  99 *)
 100    End nat_fold.
 101
 102 End Nat_Hints.
 103
 104 Section Nat_Results.
 105
 106    Section nat_indipendence.
 107
 108       Theorem n_p4: (n:N) (Id N zero (succ n)) -> Empty.
 109       Intros.
 110       MApply '(list_p4 One n tt).
 111       Qed.
 112
 113       Theorem n_false: (n:N; P:Set) (Id N zero (succ n)) -> P.
 114       Intros.
 115       MCut 'Empty.
 116       MApply '(n_p4 n).
 117       MElim 'H0 'efq.
 118       Qed.
 119
 120    End nat_indipendence.
 121
 122    Section b_le_results.
 123
 124       Theorem le_wf: (n:N) (LE zero n).
 125       Intros.
 126       Unfold LE.
 127       MApply 'id_r.
 128       Qed.
 129
 130       Theorem le_comp_succ: (m,n:N) (LE m n) -> (LE (succ m) (succ n)).
 131       Intros.
 132       Assumption.
 133       Qed.
 134 (*
 135 Theorem le_ssucc: (m,n:N) (LE (succ m) (succ n)) -> (LE m n).
 136 Intros.
 137 Assumption.
 138 Qed.
 139 *)
 140       Theorem le_false: (n:N; P:Set) (LE (succ n) zero) -> P.
 141       Intros n P.
 142       Unfold LE.
 143       MSimpl.
 144       Intros.
 145       MCut 'Empty.
 146       MApply 'boole_p4.
 147       MElim 'H0 'efq.
 148       Qed.
 149
 150       Theorem le_r: (n:N) (LE n n).
 151       Intros.
 152       MElim 'n 'natrec.
 153       MApply 'le_wf.
 154       Qed.
 155
 156       Theorem le_succ: (n:N) (LE n (succ n)).
 157       Intros.
 158       MElim 'n 'natrec.
 159       MApply 'le_wf.
 160       Qed.
 161
 162       Theorem le_zero: (n:N) (LE n zero) -> (Id N n zero).
 163       Intros n.
 164       MElim 'n 'natrec.
 165       MApply '(le_false n0).
 166       Qed.
 167
 168       Theorem le_trans: (b,c,a:N) (LE a b) -> (LE b c) -> (LE a c).
 169       Intros b.
 170       Elim b using natrec.
 171       Intros c a.
 172       MElim 'a 'natrec.
 173       MApply '(le_false n).
 174       Intros b' H c.
 175       Elim c using natrec.
 176       Intros.
 177       MApply '(le_false b').
 178       Intros c' H' a.
 179       MElim 'a 'natrec.
 180       MApply 'le_comp_succ.
 181       MCut '(LE n b').
 182       MCut '(LE b' c').
 183       MApply '(H c' n).
 184       Qed.
 185
 186       Theorem gt_wf: (n:N) (GT (succ n) zero).
 187       Intros.
 188       Unfold GT.
 189       MApply 'id_r.
 190       Qed.
 191
 192       Theorem gt_comp_succ: (m,n:N) (GT m n) -> (GT (succ m) (succ n)).
 193       Intros.
 194       Assumption.
 195       Qed.
 196
 197       Theorem gt_false: (n:N; P:Set) (GT zero n) -> P.
 198       Intros n P.
 199       Unfold GT.
 200       MSimpl.
 201       Intros.
 202       MCut 'Empty.
 203       MApply 'boole_p4.
 204       MElim 'H0 'efq.
 205       Qed.
 206
 207       Theorem le_gt: (m,n:N) (LE (succ n) m) -> (GT m n).
 208       Intros m.
 209       Elim m using natrec.
 210       Intros.
 211       MApply '(le_false n).
 212       Intros m' H n.
 213       Elim n using natrec.
 214       Intros.
 215       MApply 'gt_wf.
 216       Intros n' H1 H2.
 217       MApply 'gt_comp_succ.
 218       MApply '(H n').
 219       Qed.
 220
 221       Theorem gt_le: (m,n:N) (GT m n) -> (LE (succ n) m).
 222       Intros m.
 223       Elim m using natrec.
 224       Intros.
 225       MApply '(gt_false n).
 226       Intros m' H n.
 227       MElim 'n natrec.
 228       MApply 'le_comp_succ.
 229       MApply 'le_wf.
 230       MApply 'le_comp_succ.
 231       MApply '(H n0).
 232       Qed.
 233
 234       Theorem le_gt_trans: (b,c,a:N) (LE b a) -> (GT b c) -> (GT a c).
 235       Intros.
 236       MApply 'le_gt.
 237       MApply '(le_trans b).
 238       MApply 'gt_le.
 239       Qed.
 240
 241       Theorem boole_di: (b:Boole) (LOr (Id Boole b true) (Id Boole b false)).
 242       Intros.
 243       MElim 'b 'ite.
 244       MApply 'in_r.
 245       MApply 'in_l.
 246       Qed.
 247
 248       Theorem le_di: (m,n:N) (LOr (LE m n) (GT m n)).
 249       Intros.
 250       Unfold LE GT.
 251       MApply '(boole_di (b_le m n)).
 252       Qed.
 253 (*
 254 Theorem ble_trip: (m,n:N; P:N->Set) ((n:N) (LE n m) -> (P n)) -> ((n:N) (GT n m) -> (P n)) -> (P n).
 255 Intros.
 256 MApply '(or_e (LE n m) (GT n m)).
 257 MApply '(H n).
 258 MApply '(H0 n).
 259 MApply 'ble_tri.
 260 Qed.
 261 *)
 262    End b_le_results.
 263
 264 End Nat_Results.