set "baseuri" "cic:/matita/CoRN-Decl/algebra/CLogic".
+include "CoRN.ma".
+
(* $Id: CLogic.v,v 1.10 2004/04/09 15:58:31 lcf Exp $ *)
(*#* printing Not %\ensuremath\neg% #~# *)
(*#* printing and %\ensuremath{\mathrel\wedge}% *)
-(* INCLUDE
-Compare_dec
-*)
-
-(* INCLUDE
-Basics
-*)
-
-(* INCLUDE
-ZArith
-*)
-
-(* INCLUDE
-ZArithRing
-*)
-
-(* INCLUDE
-Div2
-*)
-
-(* INCLUDE
-Wf_nat
-*)
+include "algebra/Basics.ma".
(*#* *Extending the Coq Logic
Because notions of apartness and order have computational meaning, we
version.
*)
-inline cic:/CoRN/algebra/CLogic/CProp.con.
+inline "cic:/CoRN/algebra/CLogic/CProp.con".
(* UNEXPORTED
-Section Basics.
+Section Basics
*)
(*#* ** Basics
and some basic connectives in [CProp].
*)
-inline cic:/CoRN/algebra/CLogic/Not.con.
+inline "cic:/CoRN/algebra/CLogic/Not.con".
-inline cic:/CoRN/algebra/CLogic/CAnd.ind.
+inline "cic:/CoRN/algebra/CLogic/CAnd.ind".
-inline cic:/CoRN/algebra/CLogic/Iff.con.
+inline "cic:/CoRN/algebra/CLogic/Iff.con".
-inline cic:/CoRN/algebra/CLogic/CFalse.ind.
+inline "cic:/CoRN/algebra/CLogic/CFalse.ind".
-inline cic:/CoRN/algebra/CLogic/CTrue.ind.
+inline "cic:/CoRN/algebra/CLogic/CTrue.ind".
-inline cic:/CoRN/algebra/CLogic/proj1_sigT.con.
+inline "cic:/CoRN/algebra/CLogic/proj1_sigT.con".
-inline cic:/CoRN/algebra/CLogic/proj2_sigT.con.
+inline "cic:/CoRN/algebra/CLogic/proj2_sigT.con".
-inline cic:/CoRN/algebra/CLogic/sig2T.ind.
+inline "cic:/CoRN/algebra/CLogic/sig2T.ind".
-inline cic:/CoRN/algebra/CLogic/proj1_sig2T.con.
+inline "cic:/CoRN/algebra/CLogic/proj1_sig2T.con".
-inline cic:/CoRN/algebra/CLogic/proj2a_sig2T.con.
+inline "cic:/CoRN/algebra/CLogic/proj2a_sig2T.con".
-inline cic:/CoRN/algebra/CLogic/proj2b_sig2T.con.
+inline "cic:/CoRN/algebra/CLogic/proj2b_sig2T.con".
-inline cic:/CoRN/algebra/CLogic/toCProp.ind.
+inline "cic:/CoRN/algebra/CLogic/toCProp.ind".
-inline cic:/CoRN/algebra/CLogic/toCProp_e.con.
+inline "cic:/CoRN/algebra/CLogic/toCProp_e.con".
-inline cic:/CoRN/algebra/CLogic/CNot.con.
+inline "cic:/CoRN/algebra/CLogic/CNot.con".
-inline cic:/CoRN/algebra/CLogic/Ccontrapos'.con.
+inline "cic:/CoRN/algebra/CLogic/Ccontrapos'.con".
-inline cic:/CoRN/algebra/CLogic/COr.ind.
+inline "cic:/CoRN/algebra/CLogic/COr.ind".
(*#*
Some lemmas to make it possible to use [Step] when reasoning with
biimplications.*)
-inline cic:/CoRN/algebra/CLogic/Iff_left.con.
+(* 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.
+inline "cic:/CoRN/algebra/CLogic/Iff_right.con".
-inline cic:/CoRN/algebra/CLogic/Iff_refl.con.
+inline "cic:/CoRN/algebra/CLogic/Iff_refl.con".
-inline cic:/CoRN/algebra/CLogic/Iff_sym.con.
+inline "cic:/CoRN/algebra/CLogic/Iff_sym.con".
-inline cic:/CoRN/algebra/CLogic/Iff_trans.con.
+inline "cic:/CoRN/algebra/CLogic/Iff_trans.con".
-inline cic:/CoRN/algebra/CLogic/Iff_imp_imp.con.
+inline "cic:/CoRN/algebra/CLogic/Iff_imp_imp.con".
(* UNEXPORTED
Declare Right Step Iff_right.
*)
(* 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.
+inline "cic:/CoRN/algebra/CLogic/not_r_cor_rect.con".
-inline cic:/CoRN/algebra/CLogic/not_l_cor_rect.con.
+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 *)
(*
*)
(* 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.
+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
when [A], [B] and [C] are non trivial.
*)
-inline cic:/CoRN/algebra/CLogic/CNot_Not_or.con.
+inline "cic:/CoRN/algebra/CLogic/CNot_Not_or.con".
-inline cic:/CoRN/algebra/CLogic/CdeMorgan_ex_all.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
%\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/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/Creflexive.con".
-inline cic:/CoRN/algebra/CLogic/Ctransitive.con.
+inline "cic:/CoRN/algebra/CLogic/Ctransitive.con".
-inline cic:/CoRN/algebra/CLogic/Csymmetric.con.
+inline "cic:/CoRN/algebra/CLogic/Csymmetric.con".
-inline cic:/CoRN/algebra/CLogic/Cequiv.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/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/Treflexive.con".
-inline cic:/CoRN/algebra/CLogic/Ttransitive.con.
+inline "cic:/CoRN/algebra/CLogic/Ttransitive.con".
-inline cic:/CoRN/algebra/CLogic/Tsymmetric.con.
+inline "cic:/CoRN/algebra/CLogic/Tsymmetric.con".
-inline cic:/CoRN/algebra/CLogic/Tequiv.con.
+inline "cic:/CoRN/algebra/CLogic/Tequiv.con".
(* UNEXPORTED
-End TRelation_Definition.
+End TRelation_Definition
*)
-inline cic:/CoRN/algebra/CLogic/eqs.ind.
+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/Cle.ind.
+inline "cic:/CoRN/algebra/CLogic/Cle.ind".
-inline cic:/CoRN/algebra/CLogic/Cnat_double_ind.con.
+inline "cic:/CoRN/algebra/CLogic/Cnat_double_ind.con".
-inline cic:/CoRN/algebra/CLogic/my_Cle_ind.con.
+inline "cic:/CoRN/algebra/CLogic/my_Cle_ind.con".
-inline cic:/CoRN/algebra/CLogic/Cle_n_S.con.
+inline "cic:/CoRN/algebra/CLogic/Cle_n_S.con".
-inline cic:/CoRN/algebra/CLogic/toCle.con.
+inline "cic:/CoRN/algebra/CLogic/toCle.con".
(* UNEXPORTED
Hint Resolve toCle.
*)
-inline cic:/CoRN/algebra/CLogic/Cle_to.con.
+inline "cic:/CoRN/algebra/CLogic/Cle_to.con".
-inline cic:/CoRN/algebra/CLogic/Clt.con.
+inline "cic:/CoRN/algebra/CLogic/Clt.con".
-inline cic:/CoRN/algebra/CLogic/toCProp_lt.con.
+inline "cic:/CoRN/algebra/CLogic/toCProp_lt.con".
-inline cic:/CoRN/algebra/CLogic/Clt_to.con.
+inline "cic:/CoRN/algebra/CLogic/Clt_to.con".
-inline cic:/CoRN/algebra/CLogic/Cle_le_S_eq.con.
+inline "cic:/CoRN/algebra/CLogic/Cle_le_S_eq.con".
-inline cic:/CoRN/algebra/CLogic/Cnat_total_order.con.
+inline "cic:/CoRN/algebra/CLogic/Cnat_total_order.con".
-inline cic:/CoRN/algebra/CLogic/Codd.ind.
+inline "cic:/CoRN/algebra/CLogic/Codd.ind".
-inline cic:/CoRN/algebra/CLogic/Codd_even_to.con.
+inline "cic:/CoRN/algebra/CLogic/Codd_even_to.con".
-inline cic:/CoRN/algebra/CLogic/Codd_to.con.
+inline "cic:/CoRN/algebra/CLogic/Codd_to.con".
-inline cic:/CoRN/algebra/CLogic/Ceven_to.con.
+inline "cic:/CoRN/algebra/CLogic/Ceven_to.con".
-inline cic:/CoRN/algebra/CLogic/to_Codd_even.con.
+inline "cic:/CoRN/algebra/CLogic/to_Codd_even.con".
-inline cic:/CoRN/algebra/CLogic/to_Codd.con.
+inline "cic:/CoRN/algebra/CLogic/to_Codd.con".
-inline cic:/CoRN/algebra/CLogic/to_Ceven.con.
+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/CZ_exh.con.
+inline "cic:/CoRN/algebra/CLogic/CZ_exh.con".
-inline cic:/CoRN/algebra/CLogic/Cnats_Z_ind.con.
+inline "cic:/CoRN/algebra/CLogic/Cnats_Z_ind.con".
-inline cic:/CoRN/algebra/CLogic/Cdiff_Z_ind.con.
+inline "cic:/CoRN/algebra/CLogic/Cdiff_Z_ind.con".
-inline cic:/CoRN/algebra/CLogic/Cpred_succ_Z_ind.con.
+inline "cic:/CoRN/algebra/CLogic/Cpred_succ_Z_ind.con".
-inline cic:/CoRN/algebra/CLogic/not_r_sum_rec.con.
+inline "cic:/CoRN/algebra/CLogic/not_r_sum_rec.con".
-inline cic:/CoRN/algebra/CLogic/not_l_sum_rec.con.
+inline "cic:/CoRN/algebra/CLogic/not_l_sum_rec.con".
(* UNEXPORTED
-End Misc.
+End Misc
*)
(*#* **Results about the natural numbers
setoid equality.
*)
-inline cic:/CoRN/algebra/CLogic/nat_less_n_pred.con.
+inline "cic:/CoRN/algebra/CLogic/nat_less_n_pred.con".
-inline cic:/CoRN/algebra/CLogic/nat_less_n_pred'.con.
+inline "cic:/CoRN/algebra/CLogic/nat_less_n_pred'.con".
(* UNEXPORTED
Implicit Arguments nat_less_n_pred [n].
*)
(* UNEXPORTED
-Section Odd_and_Even.
+Section Odd_and_Even
*)
(*#*
Next, we prove the usual results about sums of even and odd numbers:
*)
-inline cic:/CoRN/algebra/CLogic/even_plus_n_n.con.
+inline "cic:/CoRN/algebra/CLogic/even_plus_n_n.con".
-inline cic:/CoRN/algebra/CLogic/even_or_odd_plus.con.
+inline "cic:/CoRN/algebra/CLogic/even_or_odd_plus.con".
(*#* Finally, we prove that an arbitrary natural number can be written in some canonical way.
*)
-inline cic:/CoRN/algebra/CLogic/even_or_odd_plus_gt.con.
+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
definitions keeping conciseness.
*)
-inline cic:/CoRN/algebra/CLogic/Clt_le_weak.con.
+inline "cic:/CoRN/algebra/CLogic/Clt_le_weak.con".
-inline cic:/CoRN/algebra/CLogic/lt_5.con.
+inline "cic:/CoRN/algebra/CLogic/lt_5.con".
-inline cic:/CoRN/algebra/CLogic/lt_8.con.
+inline "cic:/CoRN/algebra/CLogic/lt_8.con".
-inline cic:/CoRN/algebra/CLogic/pred_lt.con.
+inline "cic:/CoRN/algebra/CLogic/pred_lt.con".
-inline cic:/CoRN/algebra/CLogic/lt_10.con.
+inline "cic:/CoRN/algebra/CLogic/lt_10.con".
-inline cic:/CoRN/algebra/CLogic/lt_pred'.con.
+inline "cic:/CoRN/algebra/CLogic/lt_pred'.con".
-inline cic:/CoRN/algebra/CLogic/le_1.con.
+inline "cic:/CoRN/algebra/CLogic/le_1.con".
-inline cic:/CoRN/algebra/CLogic/le_2.con.
+inline "cic:/CoRN/algebra/CLogic/le_2.con".
-inline cic:/CoRN/algebra/CLogic/plus_eq_one_imp_eq_zero.con.
+inline "cic:/CoRN/algebra/CLogic/plus_eq_one_imp_eq_zero.con".
-inline cic:/CoRN/algebra/CLogic/not_not_lt.con.
+inline "cic:/CoRN/algebra/CLogic/not_not_lt.con".
-inline cic:/CoRN/algebra/CLogic/plus_pred_pred_plus.con.
+inline "cic:/CoRN/algebra/CLogic/plus_pred_pred_plus.con".
(*#* We now prove some properties of functions on the natural numbers.
%\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)]
holds for weak monotonicity.
*)
-inline cic:/CoRN/algebra/CLogic/nat_local_mon_imp_mon.con.
+inline "cic:/CoRN/algebra/CLogic/nat_local_mon_imp_mon.con".
-inline cic:/CoRN/algebra/CLogic/nat_local_mon_imp_mon_le.con.
+inline "cic:/CoRN/algebra/CLogic/nat_local_mon_imp_mon_le.con".
(*#* A strictly increasing function is injective: *)
-inline cic:/CoRN/algebra/CLogic/nat_mon_imp_inj.con.
+inline "cic:/CoRN/algebra/CLogic/nat_mon_imp_inj.con".
(*#* And (not completely trivial) a function that preserves [lt] also preserves [le]. *)
-inline cic:/CoRN/algebra/CLogic/nat_mon_imp_mon'.con.
+inline "cic:/CoRN/algebra/CLogic/nat_mon_imp_mon'.con".
(*#*
The last lemmas in this section state that a monotonous function in the
These are useful for integration.
*)
-inline cic:/CoRN/algebra/CLogic/mon_fun_covers.con.
+inline "cic:/CoRN/algebra/CLogic/mon_fun_covers.con".
-inline cic:/CoRN/algebra/CLogic/weird_mon_covers.con.
+inline "cic:/CoRN/algebra/CLogic/weird_mon_covers.con".
(* UNEXPORTED
-End Natural_Numbers.
+End Natural_Numbers
*)
(*#*
Useful for the Fundamental Theorem of Algebra.
*)
-inline cic:/CoRN/algebra/CLogic/kseq_prop.con.
+inline "cic:/CoRN/algebra/CLogic/kseq_prop.con".
(* UNEXPORTED
-Section Predicates_to_CProp.
+Section Predicates_to_CProp
*)
(*#* **Logical Properties
results for [CProp]-valued predicates:
*)
-inline cic:/CoRN/algebra/CLogic/even_induction.con.
+inline "cic:/CoRN/algebra/CLogic/even_induction.con".
-inline cic:/CoRN/algebra/CLogic/odd_induction.con.
+inline "cic:/CoRN/algebra/CLogic/odd_induction.con".
-inline cic:/CoRN/algebra/CLogic/four_induction.con.
+inline "cic:/CoRN/algebra/CLogic/four_induction.con".
-inline cic:/CoRN/algebra/CLogic/nat_complete_double_induction.con.
+inline "cic:/CoRN/algebra/CLogic/nat_complete_double_induction.con".
-inline cic:/CoRN/algebra/CLogic/odd_double_ind.con.
+inline "cic:/CoRN/algebra/CLogic/odd_double_ind.con".
(*#* For subsetoid predicates in the natural numbers we can eliminate
disjunction (and existential quantification) as follows.
*)
-inline cic:/CoRN/algebra/CLogic/finite_or_elim.con.
+inline "cic:/CoRN/algebra/CLogic/finite_or_elim.con".
-inline cic:/CoRN/algebra/CLogic/str_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
completeness's sake.
*)
-inline cic:/CoRN/algebra/CLogic/even_ind.con.
+inline "cic:/CoRN/algebra/CLogic/even_ind.con".
-inline cic:/CoRN/algebra/CLogic/odd_ind.con.
+inline "cic:/CoRN/algebra/CLogic/odd_ind.con".
-inline cic:/CoRN/algebra/CLogic/nat_complete_double_ind.con.
+inline "cic:/CoRN/algebra/CLogic/nat_complete_double_ind.con".
-inline cic:/CoRN/algebra/CLogic/four_ind.con.
+inline "cic:/CoRN/algebra/CLogic/four_ind.con".
(* UNEXPORTED
-End Predicates_to_Prop.
+End Predicates_to_Prop
*)
(*#* **Integers
(* end hide *)
-inline cic:/CoRN/algebra/CLogic/Zlts.con.
+inline "cic:/CoRN/algebra/CLogic/Zlts.con".
-inline cic:/CoRN/algebra/CLogic/toCProp_Zlt.con.
+inline "cic:/CoRN/algebra/CLogic/toCProp_Zlt.con".
-inline cic:/CoRN/algebra/CLogic/CZlt_to.con.
+inline "cic:/CoRN/algebra/CLogic/CZlt_to.con".
-inline cic:/CoRN/algebra/CLogic/Zsgn_1.con.
+inline "cic:/CoRN/algebra/CLogic/Zsgn_1.con".
-inline cic:/CoRN/algebra/CLogic/Zsgn_2.con.
+inline "cic:/CoRN/algebra/CLogic/Zsgn_2.con".
-inline cic:/CoRN/algebra/CLogic/Zsgn_3.con.
+inline "cic:/CoRN/algebra/CLogic/Zsgn_3.con".
(*#* The following have unusual names, in line with the series of lemmata in
fast_integers.v.
*)
-inline cic:/CoRN/algebra/CLogic/ZL4'.con.
+inline "cic:/CoRN/algebra/CLogic/ZL4'.con".
+
+inline "cic:/CoRN/algebra/CLogic/ZL9.con".
-inline cic:/CoRN/algebra/CLogic/ZL9.con.
+inline "cic:/CoRN/algebra/CLogic/Zsgn_4.con".
-inline cic:/CoRN/algebra/CLogic/Zsgn_4.con.
+inline "cic:/CoRN/algebra/CLogic/Zsgn_5.con".
-inline cic:/CoRN/algebra/CLogic/Zsgn_5.con.
+inline "cic:/CoRN/algebra/CLogic/nat_nat_pos.con".
-inline cic:/CoRN/algebra/CLogic/nat_nat_pos.con.
+inline "cic:/CoRN/algebra/CLogic/S_predn.con".
-inline cic:/CoRN/algebra/CLogic/S_predn.con.
+inline "cic:/CoRN/algebra/CLogic/absolu_1.con".
-inline cic:/CoRN/algebra/CLogic/absolu_1.con.
+inline "cic:/CoRN/algebra/CLogic/absolu_2.con".
-inline cic:/CoRN/algebra/CLogic/absolu_2.con.
+inline "cic:/CoRN/algebra/CLogic/Zgt_mult_conv_absorb_l.con".
-inline cic:/CoRN/algebra/CLogic/Zgt_mult_conv_absorb_l.con.
+inline "cic:/CoRN/algebra/CLogic/Zgt_mult_reg_absorb_l.con".
-inline cic:/CoRN/algebra/CLogic/Zgt_mult_reg_absorb_l.con.
+inline "cic:/CoRN/algebra/CLogic/Zmult_Sm_Sn.con".
-inline cic:/CoRN/algebra/CLogic/Zmult_Sm_Sn.con.
+(* NOTATION
+Notation ProjT1 := (proj1_sigT _ _).
+*)
+
+(* NOTATION
+Notation ProjT2 := (proj2_sigT _ _).
+*)