helm/software/matita/contribs/procedural/CoRN/algebra/Basics.mma

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