X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2FCoRN-Decl%2Falgebra%2FCLogic.ma;h=b1d55aa9a128539923569d558862e807c43bb618;hb=db235934efa41a0f38e79747f6db4f468367410b;hp=17207594629ddb9faf9ee4c7436ff3ffc8e174eb;hpb=7a8f91f8aa2d6ba24bf6b3093866f759ee16e690;p=helm.git diff --git a/helm/software/matita/contribs/CoRN-Decl/algebra/CLogic.ma b/helm/software/matita/contribs/CoRN-Decl/algebra/CLogic.ma index 172075946..b1d55aa9a 100644 --- a/helm/software/matita/contribs/CoRN-Decl/algebra/CLogic.ma +++ b/helm/software/matita/contribs/CoRN-Decl/algebra/CLogic.ma @@ -16,7 +16,7 @@ set "baseuri" "cic:/matita/CoRN-Decl/algebra/CLogic". -include "CoRN_notation.ma". +include "CoRN.ma". (* $Id: CLogic.v,v 1.10 2004/04/09 15:58:31 lcf Exp $ *) @@ -81,7 +81,7 @@ version. inline "cic:/CoRN/algebra/CLogic/CProp.con". (* UNEXPORTED -Section Basics. +Section Basics *) (*#* ** Basics @@ -125,6 +125,10 @@ inline "cic:/CoRN/algebra/CLogic/COr.ind". Some lemmas to make it possible to use [Step] when reasoning with biimplications.*) +(* NOTATION +Infix "IFF" := Iff (at level 60, right associativity). +*) + inline "cic:/CoRN/algebra/CLogic/Iff_left.con". inline "cic:/CoRN/algebra/CLogic/Iff_right.con". @@ -150,11 +154,19 @@ Hint Resolve Iff_trans Iff_sym Iff_refl Iff_right Iff_left Iff_imp_imp : algebra *) (* UNEXPORTED -End Basics. +End Basics *) (* begin hide *) +(* NOTATION +Infix "or" := COr (at level 85, right associativity). +*) + +(* NOTATION +Infix "and" := CAnd (at level 80, right associativity). +*) + (* end hide *) inline "cic:/CoRN/algebra/CLogic/not_r_cor_rect.con". @@ -163,6 +175,17 @@ inline "cic:/CoRN/algebra/CLogic/not_l_cor_rect.con". (* begin hide *) +(* NOTATION +Notation "{ x : A | P }" := (sigT (fun x : A => P):CProp) + (at level 0, x at level 99) : type_scope. +*) + +(* NOTATION +Notation "{ x : A | P | Q }" := + (sig2T A (fun x : A => P) (fun x : A => Q)) (at level 0, x at level 99) : + type_scope. +*) + (* end hide *) (* @@ -187,23 +210,23 @@ Hint Resolve CI CAnd_intro Cinleft Cinright existT exist2T: core. *) (* UNEXPORTED -Section Choice. +Section Choice *) (* **Choice Let [P] be a predicate on $\NN^2$#N times N#. *) -inline "cic:/CoRN/algebra/CLogic/P.var". +alias id "P" = "cic:/CoRN/algebra/CLogic/Choice/P.var". inline "cic:/CoRN/algebra/CLogic/choice.con". (* UNEXPORTED -End Choice. +End Choice *) (* UNEXPORTED -Section Logical_Remarks. +Section Logical_Remarks *) (*#* We prove a few logical results which are helpful to have as lemmas @@ -215,11 +238,11 @@ inline "cic:/CoRN/algebra/CLogic/CNot_Not_or.con". inline "cic:/CoRN/algebra/CLogic/CdeMorgan_ex_all.con". (* UNEXPORTED -End Logical_Remarks. +End Logical_Remarks *) (* UNEXPORTED -Section CRelation_Definition. +Section CRelation_Definition *) (*#* ** [CProp]-valued Relations @@ -229,11 +252,11 @@ Similar to Relations.v in Coq's standard library. %\end{convention}% *) -inline "cic:/CoRN/algebra/CLogic/A.var". +alias id "A" = "cic:/CoRN/algebra/CLogic/CRelation_Definition/A.var". inline "cic:/CoRN/algebra/CLogic/Crelation.con". -inline "cic:/CoRN/algebra/CLogic/R.var". +alias id "R" = "cic:/CoRN/algebra/CLogic/CRelation_Definition/R.var". inline "cic:/CoRN/algebra/CLogic/Creflexive.con". @@ -244,11 +267,11 @@ inline "cic:/CoRN/algebra/CLogic/Csymmetric.con". inline "cic:/CoRN/algebra/CLogic/Cequiv.con". (* UNEXPORTED -End CRelation_Definition. +End CRelation_Definition *) (* UNEXPORTED -Section TRelation_Definition. +Section TRelation_Definition *) (*#* ** [Prop]-valued Relations @@ -258,11 +281,11 @@ Analogous. %\end{convention}% *) -inline "cic:/CoRN/algebra/CLogic/A.var". +alias id "A" = "cic:/CoRN/algebra/CLogic/TRelation_Definition/A.var". inline "cic:/CoRN/algebra/CLogic/Trelation.con". -inline "cic:/CoRN/algebra/CLogic/R.var". +alias id "R" = "cic:/CoRN/algebra/CLogic/TRelation_Definition/R.var". inline "cic:/CoRN/algebra/CLogic/Treflexive.con". @@ -273,13 +296,13 @@ inline "cic:/CoRN/algebra/CLogic/Tsymmetric.con". inline "cic:/CoRN/algebra/CLogic/Tequiv.con". (* UNEXPORTED -End TRelation_Definition. +End TRelation_Definition *) inline "cic:/CoRN/algebra/CLogic/eqs.ind". (* UNEXPORTED -Section le_odd. +Section le_odd *) (*#* ** The relation [le], [lt], [odd] and [even] in [CProp] @@ -326,11 +349,11 @@ inline "cic:/CoRN/algebra/CLogic/to_Codd.con". inline "cic:/CoRN/algebra/CLogic/to_Ceven.con". (* UNEXPORTED -End le_odd. +End le_odd *) (* UNEXPORTED -Section Misc. +Section Misc *) (*#* **Miscellaneous @@ -349,7 +372,7 @@ inline "cic:/CoRN/algebra/CLogic/not_r_sum_rec.con". inline "cic:/CoRN/algebra/CLogic/not_l_sum_rec.con". (* UNEXPORTED -End Misc. +End Misc *) (*#* **Results about the natural numbers @@ -374,7 +397,7 @@ Implicit Arguments nat_less_n_pred' [n]. *) (* UNEXPORTED -Section Odd_and_Even. +Section Odd_and_Even *) (*#* @@ -393,7 +416,7 @@ inline "cic:/CoRN/algebra/CLogic/even_or_odd_plus.con". inline "cic:/CoRN/algebra/CLogic/even_or_odd_plus_gt.con". (* UNEXPORTED -End Odd_and_Even. +End Odd_and_Even *) (* UNEXPORTED @@ -405,7 +428,7 @@ Hint Resolve toCle: core. *) (* UNEXPORTED -Section Natural_Numbers. +Section Natural_Numbers *) (*#* **Algebraic Properties @@ -444,7 +467,7 @@ inline "cic:/CoRN/algebra/CLogic/plus_pred_pred_plus.con". %\end{convention}% *) -inline "cic:/CoRN/algebra/CLogic/h.var". +alias id "h" = "cic:/CoRN/algebra/CLogic/Natural_Numbers/h.var". (*#* First we characterize monotonicity by a local condition: if [h(n) < h(n+1)] @@ -476,7 +499,7 @@ inline "cic:/CoRN/algebra/CLogic/mon_fun_covers.con". inline "cic:/CoRN/algebra/CLogic/weird_mon_covers.con". (* UNEXPORTED -End Natural_Numbers. +End Natural_Numbers *) (*#* @@ -486,7 +509,7 @@ Useful for the Fundamental Theorem of Algebra. inline "cic:/CoRN/algebra/CLogic/kseq_prop.con". (* UNEXPORTED -Section Predicates_to_CProp. +Section Predicates_to_CProp *) (*#* **Logical Properties @@ -516,11 +539,11 @@ inline "cic:/CoRN/algebra/CLogic/finite_or_elim.con". inline "cic:/CoRN/algebra/CLogic/str_finite_or_elim.con". (* UNEXPORTED -End Predicates_to_CProp. +End Predicates_to_CProp *) (* UNEXPORTED -Section Predicates_to_Prop. +Section Predicates_to_Prop *) (*#* Finally, analogous results for [Prop]-valued predicates are presented for @@ -536,7 +559,7 @@ inline "cic:/CoRN/algebra/CLogic/nat_complete_double_ind.con". inline "cic:/CoRN/algebra/CLogic/four_ind.con". (* UNEXPORTED -End Predicates_to_Prop. +End Predicates_to_Prop *) (*#* **Integers @@ -590,3 +613,11 @@ inline "cic:/CoRN/algebra/CLogic/Zgt_mult_reg_absorb_l.con". inline "cic:/CoRN/algebra/CLogic/Zmult_Sm_Sn.con". +(* NOTATION +Notation ProjT1 := (proj1_sigT _ _). +*) + +(* NOTATION +Notation ProjT2 := (proj2_sigT _ _). +*) +