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