helm/software/matita/contribs/CoRN-Decl/algebra/Basics.ma

   1 (**************************************************************************)
   2 (*       ___                                                              *)
   3 (*      ||M||                                                             *)
   4 (*      ||A||       A project by Andrea Asperti                           *)
   5 (*      ||T||                                                             *)
   6 (*      ||I||       Developers:                                           *)
   7 (*      ||T||         The HELM team.                                      *)
   8 (*      ||A||         http://helm.cs.unibo.it                             *)
   9 (*      \   /                                                             *)
  10 (*       \ /        This file is distributed under the terms of the       *)
  11 (*        v         GNU General Public License Version 2                  *)
  12 (*                                                                        *)
  13 (**************************************************************************)
  14
  15 (* This file was automatically generated: do not edit *********************)
  16
  17 set "baseuri" "cic:/matita/CoRN-Decl/algebra/Basics".
  18
  19 (* $Id: Basics.v,v 1.7 2004/04/09 15:58:31 lcf Exp $ *)
  20
  21 (*#* printing alpha %\ensuremath{\alpha}% #&alpha;# *)
  22
  23 (*#* printing beta %\ensuremath{\beta}% #&beta;# *)
  24
  25 (*#* printing delta %\ensuremath{\delta}% #&delta;# *)
  26
  27 (*#* printing eps %\ensuremath{\varepsilon}% #&epsilon;# *)
  28
  29 (*#* printing phi %\ensuremath{\phi}% #&phi;# *)
  30
  31 (*#* printing eta %\ensuremath{\eta}% #&eta;# *)
  32
  33 (*#* printing omega %\ensuremath{\omega}% #&omega;# *)
  34
  35 (*#* printing nat %\ensuremath{\mathbb N}% #<b>N</b># *)
  36
  37 (*#* printing Z %\ensuremath{\mathbb Z}% #<b>Z</b># *)
  38
  39 (* INCLUDE
  40 Omega
  41 *)
  42
  43 (* INCLUDE
  44 Even
  45 *)
  46
  47 (* INCLUDE
  48 Max
  49 *)
  50
  51 (* INCLUDE
  52 Min
  53 *)
  54
  55 (* INCLUDE
  56 ListType
  57 *)
  58
  59 (*#* *Basics
  60 This is random stuff that should be in the Coq basic library.
  61 *)
  62
  63 inline cic:/CoRN/algebra/Basics/lt_le_dec.con.
  64
  65 inline cic:/CoRN/algebra/Basics/lt_z_two.con.
  66
  67 inline cic:/CoRN/algebra/Basics/le_pred.con.
  68
  69 inline cic:/CoRN/algebra/Basics/lt_mult_right.con.
  70
  71 inline cic:/CoRN/algebra/Basics/le_mult_right.con.
  72
  73 (*#* The power function does not exist in the standard library *)
  74
  75 inline cic:/CoRN/algebra/Basics/power.con.
  76
  77 (*#* Factorial function. Does not exist in Arith.
  78 Needed for special operations on polynomials. *)
  79
  80 inline cic:/CoRN/algebra/Basics/fac.con.
  81
  82 inline cic:/CoRN/algebra/Basics/nat_fac_gtzero.con.
  83
  84 (* needed for computational behavior of "Inversion" tactic *)
  85
  86 (* UNEXPORTED
  87 Transparent sym_eq.
  88 *)
  89
  90 (* UNEXPORTED
  91 Transparent f_equal.
  92 *)
  93
  94 (* Following only needed in finite, but tha's now obsolete
  95
  96 Lemma deMorgan_or_and: (A,B,X:Prop)((A\/B)->X)->(A->X)/\(B->X).
  97 Tauto.
  98 Qed.
  99
 100 Lemma deMorgan_and_or: (A,B,X:Prop)(A->X)/\(B->X)->(A\/B->X).
 101 Tauto.
 102 Qed.
 103
 104 Lemma deMorgan_ex_all:
 105   (A:Set)(P:A->Prop)(X:Prop)((Ex P)->X)->(a:A)(P a)->X.
 106 Intros. Apply H; Exists a; Assumption.
 107 Qed.
 108
 109 Lemma deMorgan_all_ex:
 110   (A:Set)(P:A->Prop)(X:Prop)((a:A)(P a)->X)->(Ex P)->X.
 111 Intros. Elim H0; Assumption.
 112 Qed.
 113
 114 Implicit Arguments Off.
 115
 116 Three lemmas for proving properties about definitions made with case
 117 distinction to a sumbool, i.e. [{A} + {B}].
 118
 119 Lemma sumbool_rec_or : (A,B:Prop)(S:Set)(l,r:S)(s:{A}+{B})
 120                   (sumbool_rec A B [_:{A}+{B}]S [x:A]l [x:B]r s) = l \/
 121                   (sumbool_rec A B [_:{A}+{B}]S [x:A]l [x:B]r s) = r.
 122 Intros. Elim s.
 123 Intros. Left. Reflexivity.
 124 Intros. Right. Reflexivity.
 125 Qed.
 126 *)
 127
 128 inline cic:/CoRN/algebra/Basics/not_r_sumbool_rec.con.
 129
 130 inline cic:/CoRN/algebra/Basics/not_l_sumbool_rec.con.
 131
 132 (* begin hide *)
 133
 134 (* UNEXPORTED
 135 Set Implicit Arguments.
 136 *)
 137
 138 (* UNEXPORTED
 139 Unset Strict Implicit.
 140 *)
 141
 142 (* end hide *)
 143
 144 (*#* **Some results about [Z]
 145
 146 We consider the injection [inject_nat] from [nat] to [Z] as a
 147 coercion. *)
 148
 149 (* begin hide *)
 150
 151 (* end hide *)
 152
 153 inline cic:/CoRN/algebra/Basics/POS_anti_convert.con.
 154
 155 inline cic:/CoRN/algebra/Basics/NEG_anti_convert.con.
 156
 157 inline cic:/CoRN/algebra/Basics/lt_O_positive_to_nat.con.
 158
 159 inline cic:/CoRN/algebra/Basics/anti_convert_pred_convert.con.
 160
 161 inline cic:/CoRN/algebra/Basics/p_is_some_anti_convert.con.
 162
 163 inline cic:/CoRN/algebra/Basics/convert_is_POS.con.
 164
 165 inline cic:/CoRN/algebra/Basics/min_convert_is_NEG.con.
 166
 167 inline cic:/CoRN/algebra/Basics/inject_nat_convert.con.
 168
 169 inline cic:/CoRN/algebra/Basics/Z_exh.con.
 170
 171 inline cic:/CoRN/algebra/Basics/nats_Z_ind.con.
 172
 173 inline cic:/CoRN/algebra/Basics/pred_succ_Z_ind.con.
 174
 175 inline cic:/CoRN/algebra/Basics/Zmult_minus_distr_r.con.
 176
 177 inline cic:/CoRN/algebra/Basics/Zodd_Zeven_min1.con.
 178
 179 (* begin hide *)
 180
 181 (* UNEXPORTED
 182 Set Implicit Arguments.
 183 *)
 184
 185 (* UNEXPORTED
 186 Unset Strict Implicit.
 187 *)
 188
 189 (* end hide *)
 190
 191 inline cic:/CoRN/algebra/Basics/caseZ_diff.con.
 192
 193 (* begin hide *)
 194
 195 (* UNEXPORTED
 196 Set Strict Implicit.
 197 *)
 198
 199 (* UNEXPORTED
 200 Unset Implicit Arguments.
 201 *)
 202
 203 (* end hide *)
 204
 205 inline cic:/CoRN/algebra/Basics/caseZ_diff_O.con.
 206
 207 inline cic:/CoRN/algebra/Basics/caseZ_diff_Pos.con.
 208
 209 inline cic:/CoRN/algebra/Basics/caseZ_diff_Neg.con.
 210
 211 inline cic:/CoRN/algebra/Basics/proper_caseZ_diff.con.
 212
 213 inline cic:/CoRN/algebra/Basics/diff_Z_ind.con.
 214
 215 inline cic:/CoRN/algebra/Basics/Zlt_reg_mult_l.con.
 216
 217 inline cic:/CoRN/algebra/Basics/Zlt_opp.con.
 218
 219 inline cic:/CoRN/algebra/Basics/Zlt_conv_mult_l.con.
 220
 221 inline cic:/CoRN/algebra/Basics/Zgt_not_eq.con.
 222
 223 inline cic:/CoRN/algebra/Basics/Zmult_absorb.con.
 224
 225 (* UNEXPORTED
 226 Section Well_foundedT.
 227 *)
 228
 229 inline cic:/CoRN/algebra/Basics/A.var.
 230
 231 inline cic:/CoRN/algebra/Basics/R.var.
 232
 233 (*#* The accessibility predicate is defined to be non-informative *)
 234
 235 inline cic:/CoRN/algebra/Basics/Acc.ind.
 236
 237 (* UNEXPORTED
 238 End Well_foundedT.
 239 *)
 240
 241 (* UNEXPORTED
 242 Section AccT.
 243 *)
 244
 245 inline cic:/CoRN/algebra/Basics/A.var.
 246
 247 inline cic:/CoRN/algebra/Basics/well_founded.con.
 248
 249 (* UNEXPORTED
 250 End AccT.
 251 *)
 252
 253 (* UNEXPORTED
 254 Implicit Arguments Acc [A].
 255 *)
 256
 257 (* UNEXPORTED
 258 Section IndT.
 259 *)
 260
 261 inline cic:/CoRN/algebra/Basics/A.var.
 262
 263 inline cic:/CoRN/algebra/Basics/R.var.
 264
 265 (* UNEXPORTED
 266 Section AccIter.
 267 *)
 268
 269 inline cic:/CoRN/algebra/Basics/P.var.
 270
 271 inline cic:/CoRN/algebra/Basics/F.var.
 272
 273 inline cic:/CoRN/algebra/Basics/Acc_inv.con.
 274
 275 inline cic:/CoRN/algebra/Basics/Acc_iter.con.
 276
 277 (* UNEXPORTED
 278 End AccIter.
 279 *)
 280
 281 inline cic:/CoRN/algebra/Basics/Rwf.var.
 282
 283 inline cic:/CoRN/algebra/Basics/well_founded_induction_type.con.
 284
 285 (* UNEXPORTED
 286 End IndT.
 287 *)
 288
 289 (* UNEXPORTED
 290 Section InductionT.
 291 *)
 292
 293 inline cic:/CoRN/algebra/Basics/A.var.
 294
 295 inline cic:/CoRN/algebra/Basics/f.var.
 296
 297 inline cic:/CoRN/algebra/Basics/ltof.con.
 298
 299 inline cic:/CoRN/algebra/Basics/well_founded_ltof.con.
 300
 301 inline cic:/CoRN/algebra/Basics/induction_ltof2T.con.
 302
 303 (* UNEXPORTED
 304 End InductionT.
 305 *)
 306
 307 (* UNEXPORTED
 308 Section InductionTT.
 309 *)
 310
 311 inline cic:/CoRN/algebra/Basics/lt_wf_rect.con.
 312
 313 (* UNEXPORTED
 314 End InductionTT.
 315 *)
 316