X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2FCoRN-Decl%2Falgebra%2FBasics.ma;h=32766572392cc0cc54d1dd59deeeeb53c06a8ca1;hb=e880d6eab5e1700f4a625ddcd7d0fa8f0cce2dcc;hp=8794b52cc732184ca9aa34ed827c8b4fb2d37a54;hpb=3199f2a8428b5d19a3a803c1b03d9f90e4120f74;p=helm.git diff --git a/helm/software/matita/contribs/CoRN-Decl/algebra/Basics.ma b/helm/software/matita/contribs/CoRN-Decl/algebra/Basics.ma index 8794b52cc..327665723 100644 --- a/helm/software/matita/contribs/CoRN-Decl/algebra/Basics.ma +++ b/helm/software/matita/contribs/CoRN-Decl/algebra/Basics.ma @@ -16,6 +16,8 @@ set "baseuri" "cic:/matita/CoRN-Decl/algebra/Basics". +include "CoRN.ma". + (* $Id: Basics.v,v 1.7 2004/04/09 15:58:31 lcf Exp $ *) (*#* printing alpha %\ensuremath{\alpha}% #α# *) @@ -36,50 +38,32 @@ set "baseuri" "cic:/matita/CoRN-Decl/algebra/Basics". (*#* printing Z %\ensuremath{\mathbb Z}% #Z# *) -(* INCLUDE -Omega -*) - -(* INCLUDE -Even -*) - -(* INCLUDE -Max -*) - -(* INCLUDE -Min -*) - -(* INCLUDE -ListType -*) +include "algebra/ListType.ma". (*#* *Basics This is random stuff that should be in the Coq basic library. *) -inline cic:/CoRN/algebra/Basics/lt_le_dec.con. +inline "cic:/CoRN/algebra/Basics/lt_le_dec.con". -inline cic:/CoRN/algebra/Basics/lt_z_two.con. +inline "cic:/CoRN/algebra/Basics/lt_z_two.con". -inline cic:/CoRN/algebra/Basics/le_pred.con. +inline "cic:/CoRN/algebra/Basics/le_pred.con". -inline cic:/CoRN/algebra/Basics/lt_mult_right.con. +inline "cic:/CoRN/algebra/Basics/lt_mult_right.con". -inline cic:/CoRN/algebra/Basics/le_mult_right.con. +inline "cic:/CoRN/algebra/Basics/le_mult_right.con". (*#* The power function does not exist in the standard library *) -inline cic:/CoRN/algebra/Basics/power.con. +inline "cic:/CoRN/algebra/Basics/power.con". (*#* Factorial function. Does not exist in Arith. Needed for special operations on polynomials. *) -inline cic:/CoRN/algebra/Basics/fac.con. +inline "cic:/CoRN/algebra/Basics/fac.con". -inline cic:/CoRN/algebra/Basics/nat_fac_gtzero.con. +inline "cic:/CoRN/algebra/Basics/nat_fac_gtzero.con". (* needed for computational behavior of "Inversion" tactic *) @@ -91,6 +75,18 @@ Transparent sym_eq. Transparent f_equal. *) +(* NOTATION +Notation Pair := (pair (B:=_)). +*) + +(* NOTATION +Notation Proj1 := (proj1 (B:=_)). +*) + +(* NOTATION +Notation Proj2 := (proj2 (B:=_)). +*) + (* Following only needed in finite, but tha's now obsolete Lemma deMorgan_or_and: (A,B,X:Prop)((A\/B)->X)->(A->X)/\(B->X). @@ -125,9 +121,9 @@ Intros. Right. Reflexivity. Qed. *) -inline cic:/CoRN/algebra/Basics/not_r_sumbool_rec.con. +inline "cic:/CoRN/algebra/Basics/not_r_sumbool_rec.con". -inline cic:/CoRN/algebra/Basics/not_l_sumbool_rec.con. +inline "cic:/CoRN/algebra/Basics/not_l_sumbool_rec.con". (* begin hide *) @@ -148,33 +144,35 @@ coercion. *) (* begin hide *) +coercion cic:/Coq/ZArith/BinInt/Z_of_nat.con 0 (* compounds *). + (* end hide *) -inline cic:/CoRN/algebra/Basics/POS_anti_convert.con. +inline "cic:/CoRN/algebra/Basics/POS_anti_convert.con". -inline cic:/CoRN/algebra/Basics/NEG_anti_convert.con. +inline "cic:/CoRN/algebra/Basics/NEG_anti_convert.con". -inline cic:/CoRN/algebra/Basics/lt_O_positive_to_nat.con. +inline "cic:/CoRN/algebra/Basics/lt_O_positive_to_nat.con". -inline cic:/CoRN/algebra/Basics/anti_convert_pred_convert.con. +inline "cic:/CoRN/algebra/Basics/anti_convert_pred_convert.con". -inline cic:/CoRN/algebra/Basics/p_is_some_anti_convert.con. +inline "cic:/CoRN/algebra/Basics/p_is_some_anti_convert.con". -inline cic:/CoRN/algebra/Basics/convert_is_POS.con. +inline "cic:/CoRN/algebra/Basics/convert_is_POS.con". -inline cic:/CoRN/algebra/Basics/min_convert_is_NEG.con. +inline "cic:/CoRN/algebra/Basics/min_convert_is_NEG.con". -inline cic:/CoRN/algebra/Basics/inject_nat_convert.con. +inline "cic:/CoRN/algebra/Basics/inject_nat_convert.con". -inline cic:/CoRN/algebra/Basics/Z_exh.con. +inline "cic:/CoRN/algebra/Basics/Z_exh.con". -inline cic:/CoRN/algebra/Basics/nats_Z_ind.con. +inline "cic:/CoRN/algebra/Basics/nats_Z_ind.con". -inline cic:/CoRN/algebra/Basics/pred_succ_Z_ind.con. +inline "cic:/CoRN/algebra/Basics/pred_succ_Z_ind.con". -inline cic:/CoRN/algebra/Basics/Zmult_minus_distr_r.con. +inline "cic:/CoRN/algebra/Basics/Zmult_minus_distr_r.con". -inline cic:/CoRN/algebra/Basics/Zodd_Zeven_min1.con. +inline "cic:/CoRN/algebra/Basics/Zodd_Zeven_min1.con". (* begin hide *) @@ -188,7 +186,7 @@ Unset Strict Implicit. (* end hide *) -inline cic:/CoRN/algebra/Basics/caseZ_diff.con. +inline "cic:/CoRN/algebra/Basics/caseZ_diff.con". (* begin hide *) @@ -202,52 +200,52 @@ Unset Implicit Arguments. (* end hide *) -inline cic:/CoRN/algebra/Basics/caseZ_diff_O.con. +inline "cic:/CoRN/algebra/Basics/caseZ_diff_O.con". -inline cic:/CoRN/algebra/Basics/caseZ_diff_Pos.con. +inline "cic:/CoRN/algebra/Basics/caseZ_diff_Pos.con". -inline cic:/CoRN/algebra/Basics/caseZ_diff_Neg.con. +inline "cic:/CoRN/algebra/Basics/caseZ_diff_Neg.con". -inline cic:/CoRN/algebra/Basics/proper_caseZ_diff.con. +inline "cic:/CoRN/algebra/Basics/proper_caseZ_diff.con". -inline cic:/CoRN/algebra/Basics/diff_Z_ind.con. +inline "cic:/CoRN/algebra/Basics/diff_Z_ind.con". -inline cic:/CoRN/algebra/Basics/Zlt_reg_mult_l.con. +inline "cic:/CoRN/algebra/Basics/Zlt_reg_mult_l.con". -inline cic:/CoRN/algebra/Basics/Zlt_opp.con. +inline "cic:/CoRN/algebra/Basics/Zlt_opp.con". -inline cic:/CoRN/algebra/Basics/Zlt_conv_mult_l.con. +inline "cic:/CoRN/algebra/Basics/Zlt_conv_mult_l.con". -inline cic:/CoRN/algebra/Basics/Zgt_not_eq.con. +inline "cic:/CoRN/algebra/Basics/Zgt_not_eq.con". -inline cic:/CoRN/algebra/Basics/Zmult_absorb.con. +inline "cic:/CoRN/algebra/Basics/Zmult_absorb.con". (* UNEXPORTED -Section Well_foundedT. +Section Well_foundedT *) -inline cic:/CoRN/algebra/Basics/A.var. +alias id "A" = "cic:/CoRN/algebra/Basics/Well_foundedT/A.var". -inline cic:/CoRN/algebra/Basics/R.var. +alias id "R" = "cic:/CoRN/algebra/Basics/Well_foundedT/R.var". (*#* The accessibility predicate is defined to be non-informative *) -inline cic:/CoRN/algebra/Basics/Acc.ind. +inline "cic:/CoRN/algebra/Basics/Acc.ind". (* UNEXPORTED -End Well_foundedT. +End Well_foundedT *) (* UNEXPORTED -Section AccT. +Section AccT *) -inline cic:/CoRN/algebra/Basics/A.var. +alias id "A" = "cic:/CoRN/algebra/Basics/AccT/A.var". -inline cic:/CoRN/algebra/Basics/well_founded.con. +inline "cic:/CoRN/algebra/Basics/well_founded.con". (* UNEXPORTED -End AccT. +End AccT *) (* UNEXPORTED @@ -255,62 +253,62 @@ Implicit Arguments Acc [A]. *) (* UNEXPORTED -Section IndT. +Section IndT *) -inline cic:/CoRN/algebra/Basics/A.var. +alias id "A" = "cic:/CoRN/algebra/Basics/IndT/A.var". -inline cic:/CoRN/algebra/Basics/R.var. +alias id "R" = "cic:/CoRN/algebra/Basics/IndT/R.var". (* UNEXPORTED -Section AccIter. +Section AccIter *) -inline cic:/CoRN/algebra/Basics/P.var. +alias id "P" = "cic:/CoRN/algebra/Basics/IndT/AccIter/P.var". -inline cic:/CoRN/algebra/Basics/F.var. +alias id "F" = "cic:/CoRN/algebra/Basics/IndT/AccIter/F.var". -inline cic:/CoRN/algebra/Basics/Acc_inv.con. +inline "cic:/CoRN/algebra/Basics/Acc_inv.con". -inline cic:/CoRN/algebra/Basics/Acc_iter.con. +inline "cic:/CoRN/algebra/Basics/Acc_iter.con". (* UNEXPORTED -End AccIter. +End AccIter *) -inline cic:/CoRN/algebra/Basics/Rwf.var. +alias id "Rwf" = "cic:/CoRN/algebra/Basics/IndT/Rwf.var". -inline cic:/CoRN/algebra/Basics/well_founded_induction_type.con. +inline "cic:/CoRN/algebra/Basics/well_founded_induction_type.con". (* UNEXPORTED -End IndT. +End IndT *) (* UNEXPORTED -Section InductionT. +Section InductionT *) -inline cic:/CoRN/algebra/Basics/A.var. +alias id "A" = "cic:/CoRN/algebra/Basics/InductionT/A.var". -inline cic:/CoRN/algebra/Basics/f.var. +alias id "f" = "cic:/CoRN/algebra/Basics/InductionT/f.var". -inline cic:/CoRN/algebra/Basics/ltof.con. +inline "cic:/CoRN/algebra/Basics/ltof.con". -inline cic:/CoRN/algebra/Basics/well_founded_ltof.con. +inline "cic:/CoRN/algebra/Basics/well_founded_ltof.con". -inline cic:/CoRN/algebra/Basics/induction_ltof2T.con. +inline "cic:/CoRN/algebra/Basics/induction_ltof2T.con". (* UNEXPORTED -End InductionT. +End InductionT *) (* UNEXPORTED -Section InductionTT. +Section InductionTT *) -inline cic:/CoRN/algebra/Basics/lt_wf_rect.con. +inline "cic:/CoRN/algebra/Basics/lt_wf_rect.con". (* UNEXPORTED -End InductionTT. +End InductionTT *)