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 *********************)
19 (* $Id: Basics.v,v 1.7 2004/04/09 15:58:31 lcf Exp $ *)
21 (*#* printing alpha %\ensuremath{\alpha}% #α# *)
23 (*#* printing beta %\ensuremath{\beta}% #β# *)
25 (*#* printing delta %\ensuremath{\delta}% #δ# *)
27 (*#* printing eps %\ensuremath{\varepsilon}% #ε# *)
29 (*#* printing phi %\ensuremath{\phi}% #φ# *)
31 (*#* printing eta %\ensuremath{\eta}% #η# *)
33 (*#* printing omega %\ensuremath{\omega}% #ω# *)
35 (*#* printing nat %\ensuremath{\mathbb N}% #<b>N</b># *)
37 (*#* printing Z %\ensuremath{\mathbb Z}% #<b>Z</b># *)
39 include "algebra/ListType.ma".
42 This is random stuff that should be in the Coq basic library.
45 inline procedural "cic:/CoRN/algebra/Basics/lt_le_dec.con" as lemma.
47 inline procedural "cic:/CoRN/algebra/Basics/lt_z_two.con" as lemma.
49 inline procedural "cic:/CoRN/algebra/Basics/le_pred.con" as lemma.
51 inline procedural "cic:/CoRN/algebra/Basics/lt_mult_right.con" as lemma.
53 inline procedural "cic:/CoRN/algebra/Basics/le_mult_right.con" as lemma.
55 (*#* The power function does not exist in the standard library *)
57 inline procedural "cic:/CoRN/algebra/Basics/power.con" as definition.
59 (*#* Factorial function. Does not exist in Arith.
60 Needed for special operations on polynomials. *)
62 inline procedural "cic:/CoRN/algebra/Basics/fac.con" as definition.
64 inline procedural "cic:/CoRN/algebra/Basics/nat_fac_gtzero.con" as lemma.
66 (* needed for computational behavior of "Inversion" tactic *)
77 Notation Pair := (pair (B:=_)).
81 Notation Proj1 := (proj1 (B:=_)).
85 Notation Proj2 := (proj2 (B:=_)).
88 (* Following only needed in finite, but tha's now obsolete
90 Lemma deMorgan_or_and: (A,B,X:Prop)((A\/B)->X)->(A->X)/\(B->X).
94 Lemma deMorgan_and_or: (A,B,X:Prop)(A->X)/\(B->X)->(A\/B->X).
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.
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.
108 Implicit Arguments Off.
110 Three lemmas for proving properties about definitions made with case
111 distinction to a sumbool, i.e. [{A} + {B}].
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.
117 Intros. Left. Reflexivity.
118 Intros. Right. Reflexivity.
122 inline procedural "cic:/CoRN/algebra/Basics/not_r_sumbool_rec.con" as lemma.
124 inline procedural "cic:/CoRN/algebra/Basics/not_l_sumbool_rec.con" as lemma.
129 Set Implicit Arguments.
133 Unset Strict Implicit.
138 (*#* **Some results about [Z]
140 We consider the injection [inject_nat] from [nat] to [Z] as a
146 cic:/Coq/ZArith/BinInt/Z_of_nat.con
151 inline procedural "cic:/CoRN/algebra/Basics/POS_anti_convert.con" as lemma.
153 inline procedural "cic:/CoRN/algebra/Basics/NEG_anti_convert.con" as lemma.
155 inline procedural "cic:/CoRN/algebra/Basics/lt_O_positive_to_nat.con" as lemma.
157 inline procedural "cic:/CoRN/algebra/Basics/anti_convert_pred_convert.con" as lemma.
159 inline procedural "cic:/CoRN/algebra/Basics/p_is_some_anti_convert.con" as lemma.
161 inline procedural "cic:/CoRN/algebra/Basics/convert_is_POS.con" as lemma.
163 inline procedural "cic:/CoRN/algebra/Basics/min_convert_is_NEG.con" as lemma.
165 inline procedural "cic:/CoRN/algebra/Basics/inject_nat_convert.con" as lemma.
167 inline procedural "cic:/CoRN/algebra/Basics/Z_exh.con" as lemma.
169 inline procedural "cic:/CoRN/algebra/Basics/nats_Z_ind.con" as lemma.
171 inline procedural "cic:/CoRN/algebra/Basics/pred_succ_Z_ind.con" as lemma.
173 inline procedural "cic:/CoRN/algebra/Basics/Zmult_minus_distr_r.con" as lemma.
175 inline procedural "cic:/CoRN/algebra/Basics/Zodd_Zeven_min1.con" as lemma.
180 Set Implicit Arguments.
184 Unset Strict Implicit.
189 inline procedural "cic:/CoRN/algebra/Basics/caseZ_diff.con" as definition.
198 Unset Implicit Arguments.
203 inline procedural "cic:/CoRN/algebra/Basics/caseZ_diff_O.con" as lemma.
205 inline procedural "cic:/CoRN/algebra/Basics/caseZ_diff_Pos.con" as lemma.
207 inline procedural "cic:/CoRN/algebra/Basics/caseZ_diff_Neg.con" as lemma.
209 inline procedural "cic:/CoRN/algebra/Basics/proper_caseZ_diff.con" as lemma.
211 inline procedural "cic:/CoRN/algebra/Basics/diff_Z_ind.con" as lemma.
213 inline procedural "cic:/CoRN/algebra/Basics/Zlt_reg_mult_l.con" as lemma.
215 inline procedural "cic:/CoRN/algebra/Basics/Zlt_opp.con" as lemma.
217 inline procedural "cic:/CoRN/algebra/Basics/Zlt_conv_mult_l.con" as lemma.
219 inline procedural "cic:/CoRN/algebra/Basics/Zgt_not_eq.con" as lemma.
221 inline procedural "cic:/CoRN/algebra/Basics/Zmult_absorb.con" as lemma.
224 Section Well_foundedT
228 cic:/CoRN/algebra/Basics/Well_foundedT/A.var
232 cic:/CoRN/algebra/Basics/Well_foundedT/R.var
235 (*#* The accessibility predicate is defined to be non-informative *)
237 inline procedural "cic:/CoRN/algebra/Basics/Acc.ind".
248 cic:/CoRN/algebra/Basics/AccT/A.var
251 inline procedural "cic:/CoRN/algebra/Basics/well_founded.con" as definition.
258 Implicit Arguments Acc [A].
266 cic:/CoRN/algebra/Basics/IndT/A.var
270 cic:/CoRN/algebra/Basics/IndT/R.var
278 cic:/CoRN/algebra/Basics/IndT/AccIter/P.var
282 cic:/CoRN/algebra/Basics/IndT/AccIter/F.var
285 inline procedural "cic:/CoRN/algebra/Basics/Acc_inv.con" as lemma.
287 inline procedural "cic:/CoRN/algebra/Basics/Acc_iter.con" as definition.
294 cic:/CoRN/algebra/Basics/IndT/Rwf.var
297 inline procedural "cic:/CoRN/algebra/Basics/well_founded_induction_type.con" as theorem.
308 cic:/CoRN/algebra/Basics/InductionT/A.var
312 cic:/CoRN/algebra/Basics/InductionT/f.var
315 inline procedural "cic:/CoRN/algebra/Basics/ltof.con" as definition.
317 inline procedural "cic:/CoRN/algebra/Basics/well_founded_ltof.con" as theorem.
319 inline procedural "cic:/CoRN/algebra/Basics/induction_ltof2T.con" as theorem.
329 inline procedural "cic:/CoRN/algebra/Basics/lt_wf_rect.con" as lemma.