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 $ *)
inline "cic:/CoRN/algebra/CLogic/CProp.con".
(* UNEXPORTED
-Section Basics.
+Section Basics
*)
(*#* ** Basics
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".
*)
(* 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".
(* 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 *)
(*
*)
(* 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
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
%\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".
inline "cic:/CoRN/algebra/CLogic/Cequiv.con".
(* UNEXPORTED
-End CRelation_Definition.
+End CRelation_Definition
*)
(* UNEXPORTED
-Section TRelation_Definition.
+Section TRelation_Definition
*)
(*#* ** [Prop]-valued Relations
%\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".
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]
inline "cic:/CoRN/algebra/CLogic/to_Ceven.con".
(* UNEXPORTED
-End le_odd.
+End le_odd
*)
(* UNEXPORTED
-Section Misc.
+Section Misc
*)
(*#* **Miscellaneous
inline "cic:/CoRN/algebra/CLogic/not_l_sum_rec.con".
(* UNEXPORTED
-End Misc.
+End Misc
*)
(*#* **Results about the natural numbers
*)
(* UNEXPORTED
-Section Odd_and_Even.
+Section Odd_and_Even
*)
(*#*
inline "cic:/CoRN/algebra/CLogic/even_or_odd_plus_gt.con".
(* UNEXPORTED
-End Odd_and_Even.
+End Odd_and_Even
*)
(* UNEXPORTED
*)
(* UNEXPORTED
-Section Natural_Numbers.
+Section Natural_Numbers
*)
(*#* **Algebraic Properties
%\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)]
inline "cic:/CoRN/algebra/CLogic/weird_mon_covers.con".
(* UNEXPORTED
-End Natural_Numbers.
+End Natural_Numbers
*)
(*#*
inline "cic:/CoRN/algebra/CLogic/kseq_prop.con".
(* UNEXPORTED
-Section Predicates_to_CProp.
+Section Predicates_to_CProp
*)
(*#* **Logical Properties
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
inline "cic:/CoRN/algebra/CLogic/four_ind.con".
(* UNEXPORTED
-End Predicates_to_Prop.
+End Predicates_to_Prop
*)
(*#* **Integers
inline "cic:/CoRN/algebra/CLogic/Zmult_Sm_Sn.con".
+(* NOTATION
+Notation ProjT1 := (proj1_sigT _ _).
+*)
+
+(* NOTATION
+Notation ProjT2 := (proj2_sigT _ _).
+*)
+