1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| The HELM team. *)
8 (* ||A|| http://helm.cs.unibo.it *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU General Public License Version 2 *)
13 (**************************************************************************)
15 (* This file was automatically generated: do not edit *********************)
17 set "baseuri" "cic:/matita/CoRN-Decl/algebra/Basics".
19 include "CoRN_notation.ma".
21 (* $Id: Basics.v,v 1.7 2004/04/09 15:58:31 lcf Exp $ *)
23 (*#* printing alpha %\ensuremath{\alpha}% #α# *)
25 (*#* printing beta %\ensuremath{\beta}% #β# *)
27 (*#* printing delta %\ensuremath{\delta}% #δ# *)
29 (*#* printing eps %\ensuremath{\varepsilon}% #ε# *)
31 (*#* printing phi %\ensuremath{\phi}% #φ# *)
33 (*#* printing eta %\ensuremath{\eta}% #η# *)
35 (*#* printing omega %\ensuremath{\omega}% #ω# *)
37 (*#* printing nat %\ensuremath{\mathbb N}% #<b>N</b># *)
39 (*#* printing Z %\ensuremath{\mathbb Z}% #<b>Z</b># *)
41 include "algebra/ListType.ma".
44 This is random stuff that should be in the Coq basic library.
47 inline "cic:/CoRN/algebra/Basics/lt_le_dec.con".
49 inline "cic:/CoRN/algebra/Basics/lt_z_two.con".
51 inline "cic:/CoRN/algebra/Basics/le_pred.con".
53 inline "cic:/CoRN/algebra/Basics/lt_mult_right.con".
55 inline "cic:/CoRN/algebra/Basics/le_mult_right.con".
57 (*#* The power function does not exist in the standard library *)
59 inline "cic:/CoRN/algebra/Basics/power.con".
61 (*#* Factorial function. Does not exist in Arith.
62 Needed for special operations on polynomials. *)
64 inline "cic:/CoRN/algebra/Basics/fac.con".
66 inline "cic:/CoRN/algebra/Basics/nat_fac_gtzero.con".
68 (* needed for computational behavior of "Inversion" tactic *)
78 (* Following only needed in finite, but tha's now obsolete
80 Lemma deMorgan_or_and: (A,B,X:Prop)((A\/B)->X)->(A->X)/\(B->X).
84 Lemma deMorgan_and_or: (A,B,X:Prop)(A->X)/\(B->X)->(A\/B->X).
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.
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.
98 Implicit Arguments Off.
100 Three lemmas for proving properties about definitions made with case
101 distinction to a sumbool, i.e. [{A} + {B}].
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.
107 Intros. Left. Reflexivity.
108 Intros. Right. Reflexivity.
112 inline "cic:/CoRN/algebra/Basics/not_r_sumbool_rec.con".
114 inline "cic:/CoRN/algebra/Basics/not_l_sumbool_rec.con".
119 Set Implicit Arguments.
123 Unset Strict Implicit.
128 (*#* **Some results about [Z]
130 We consider the injection [inject_nat] from [nat] to [Z] as a
135 coercion "cic:/matita/CoRN-Decl/algebra/Basics/Z_of_nat.con" 0 (* compounds *).
139 inline "cic:/CoRN/algebra/Basics/POS_anti_convert.con".
141 inline "cic:/CoRN/algebra/Basics/NEG_anti_convert.con".
143 inline "cic:/CoRN/algebra/Basics/lt_O_positive_to_nat.con".
145 inline "cic:/CoRN/algebra/Basics/anti_convert_pred_convert.con".
147 inline "cic:/CoRN/algebra/Basics/p_is_some_anti_convert.con".
149 inline "cic:/CoRN/algebra/Basics/convert_is_POS.con".
151 inline "cic:/CoRN/algebra/Basics/min_convert_is_NEG.con".
153 inline "cic:/CoRN/algebra/Basics/inject_nat_convert.con".
155 inline "cic:/CoRN/algebra/Basics/Z_exh.con".
157 inline "cic:/CoRN/algebra/Basics/nats_Z_ind.con".
159 inline "cic:/CoRN/algebra/Basics/pred_succ_Z_ind.con".
161 inline "cic:/CoRN/algebra/Basics/Zmult_minus_distr_r.con".
163 inline "cic:/CoRN/algebra/Basics/Zodd_Zeven_min1.con".
168 Set Implicit Arguments.
172 Unset Strict Implicit.
177 inline "cic:/CoRN/algebra/Basics/caseZ_diff.con".
186 Unset Implicit Arguments.
191 inline "cic:/CoRN/algebra/Basics/caseZ_diff_O.con".
193 inline "cic:/CoRN/algebra/Basics/caseZ_diff_Pos.con".
195 inline "cic:/CoRN/algebra/Basics/caseZ_diff_Neg.con".
197 inline "cic:/CoRN/algebra/Basics/proper_caseZ_diff.con".
199 inline "cic:/CoRN/algebra/Basics/diff_Z_ind.con".
201 inline "cic:/CoRN/algebra/Basics/Zlt_reg_mult_l.con".
203 inline "cic:/CoRN/algebra/Basics/Zlt_opp.con".
205 inline "cic:/CoRN/algebra/Basics/Zlt_conv_mult_l.con".
207 inline "cic:/CoRN/algebra/Basics/Zgt_not_eq.con".
209 inline "cic:/CoRN/algebra/Basics/Zmult_absorb.con".
212 Section Well_foundedT.
215 inline "cic:/CoRN/algebra/Basics/A.var".
217 inline "cic:/CoRN/algebra/Basics/R.var".
219 (*#* The accessibility predicate is defined to be non-informative *)
221 inline "cic:/CoRN/algebra/Basics/Acc.ind".
231 inline "cic:/CoRN/algebra/Basics/A.var".
233 inline "cic:/CoRN/algebra/Basics/well_founded.con".
240 Implicit Arguments Acc [A].
247 inline "cic:/CoRN/algebra/Basics/A.var".
249 inline "cic:/CoRN/algebra/Basics/R.var".
255 inline "cic:/CoRN/algebra/Basics/P.var".
257 inline "cic:/CoRN/algebra/Basics/F.var".
259 inline "cic:/CoRN/algebra/Basics/Acc_inv.con".
261 inline "cic:/CoRN/algebra/Basics/Acc_iter.con".
267 inline "cic:/CoRN/algebra/Basics/Rwf.var".
269 inline "cic:/CoRN/algebra/Basics/well_founded_induction_type.con".
279 inline "cic:/CoRN/algebra/Basics/A.var".
281 inline "cic:/CoRN/algebra/Basics/f.var".
283 inline "cic:/CoRN/algebra/Basics/ltof.con".
285 inline "cic:/CoRN/algebra/Basics/well_founded_ltof.con".
287 inline "cic:/CoRN/algebra/Basics/induction_ltof2T.con".
297 inline "cic:/CoRN/algebra/Basics/lt_wf_rect.con".