rebase and suggestions

CHANGELOG_UNRELEASED.md

@@ -9,130 +9,9 @@
 
 - in `lebesgue_measure.v`:
   + `sigma_finite_measure` HB instance on `lebesgue_measure`
-- in `normedtype.v`:
-  + hints for `at_right_proper_filter` and `at_left_proper_filter`
-
-- in `realfun.v`:
-  + notations `nondecreasing_fun`, `nonincreasing_fun`,
-    `increasing_fun`, `decreasing_fun`
-  + lemmas `cvg_addrl`, `cvg_addrr`, `cvg_centerr`, `cvg_shiftr`,
-    `nondecreasing_cvgr`,
-	`nonincreasing_at_right_cvgr`,
-	`nondecreasing_at_right_cvgr`,
-	`nondecreasing_cvge`, `nondecreasing_is_cvge`,
-	`nondecreasing_at_right_cvge`, `nondecreasing_at_right_is_cvge`,
-	`nonincreasing_at_right_cvge`, `nonincreasing_at_right_is_cvge`
-- in `ereal.v`:
-  + lemmas `ereal_sup_le`, `ereal_inf_le`
-
-- in `normedtype.v`:
-  + definition `lower_semicontinuous`
-  + lemma `lower_semicontinuousP`
-
-- in `numfun.v`:
-  + lemma `patch_indic`
-
-- in `lebesgue_measure.v`
-  + lemma `lower_semicontinuous_measurable`
 
 - in `lebesgue_integral.v`:
-  + definition `locally_integrable`
-  + lemmas `integrable_locally`, `locally_integrableN`, `locally_integrableD`,
-    `locally_integrableB`
-  + definition `iavg`
-  + lemmas `iavg0`, `iavg_ge0`, `iavg_restrict`, `iavgD`
-  + definitions `HL_maximal`
-  + lemmas `HL_maximal_ge0`, `HL_maximalT_ge0`,
-    `lower_semicontinuous_HL_maximal`, `measurable_HL_maximal`,
-    `maximal_inequality`
-
-- in file `measure.v`
-  + add lemmas `ae_eq_subset`, `measure_dominates_ae_eq`.
-
-- in `charge.v`
-  + definition `charge_of_finite_measure` (instance of `charge`)
-  + lemmas `dominates_cscalel`, `dominates_cscaler`
-  + definition `cpushforward` (instance of `charge`)
-  + lemma `dominates_pushforward`
-  + lemma `cjordan_posE`
-  + lemma `jordan_posE`
-  + lemma `cjordan_negE`
-  + lemma `jordan_negE`
-  + lemma `Radon_Nikodym_sigma_finite`
-  + lemma `Radon_Nikodym_fin_num`
-  + lemma `Radon_Nikodym_integral`
-  + lemma `ae_eq_Radon_Nikodym_SigmaFinite`
-  + lemma `Radon_Nikodym_change_of_variables`
-  + lemma `Radon_Nikodym_cscale`
-  + lemma `Radon_Nikodym_cadd`
-  + lemma `Radon_Nikodym_chain_rule`
-
-- in `sequences.v`:
-  + lemma `minr_cvg_0_cvg_0`
-  + lemma `mine_cvg_0_cvg_fin_num`
-  + lemma `mine_cvg_minr_cvg`
-  + lemma `mine_cvg_0_cvg_0`
-  + lemma `maxr_cvg_0_cvg_0`
-  + lemma `maxe_cvg_0_cvg_fin_num`
-  + lemma `maxe_cvg_maxr_cvg`
-  + lemma `maxe_cvg_0_cvg_0`
-- in `constructive_ereal.v`
-  + lemma `lee_subgt0Pr`
-
-- in `topology.v`:
-  + lemma `nbhs_dnbhs_neq`
-
-- in `normedtype.v`:
-  + lemma `not_near_at_rightP`
-
-- in `realfun.v`:
-  + lemma `cvg_at_right_left_dnbhs`
-  + lemma `cvg_at_rightP`
-  + lemma `cvg_at_leftP`
-  + lemma `cvge_at_rightP`
-  + lemma `cvge_at_leftP`
-  + lemma `lime_sup`
-  + lemma `lime_inf`
-  + lemma `lime_supE`
-  + lemma `lime_infE`
-  + lemma `lime_infN`
-  + lemma `lime_supN`
-  + lemma `lime_sup_ge0`
-  + lemma `lime_inf_ge0`
-  + lemma `lime_supD`
-  + lemma `lime_sup_le`
-  + lemma `lime_inf_sup`
-  + lemma `lim_lime_inf`
-  + lemma `lim_lime_sup`
-  + lemma `lime_sup_inf_at_right`
-  + lemma `lime_sup_inf_at_left`
-
-- in `normedtype.v`:
-  + lemmas `withinN`, `at_rightN`, `at_leftN`, `cvg_at_leftNP`, `cvg_at_rightNP`
-  + lemma `dnbhsN`
-  + lemma `limf_esup_dnbhsN`
-
-- in `topology.v`:
-  + lemma `dnbhs_ball`
-
-- in `normedtype.v`
-  + definitions `limf_esup`, `limf_einf`
-  + lemmas `limf_esupE`, `limf_einfE`, `limf_esupN`, `limf_einfN`
-
-- in `sequences.v`:
-  + lemmas `limn_esup_lim`, `limn_einf_lim`
-
-- in `realfun.v`:
-  + lemmas `lime_sup_lim`, `lime_inf_lim`
-
-- in `boolp.v`:
-  + tactic `eqProp`
-  + variant `BoolProp`
-  + lemmas `PropB`, `notB`, `andB`, `orB`, `implyB`, `decide_or`, `not_andE`,
-    `not_orE`, `orCA`, `orAC`, `orACA`, `orNp`, `orpN`, `or3E`, `or4E`, `andCA`,
-	 `andAC`, `andACA`, `and3E`, `and4E`, `and5E`, `implyNp`, `implypN`,
-	 `implyNN`, `or_andr`, `or_andl`, `and_orr`, `and_orl`, `exists2E`,
-	 `inhabitedE`, `inhabited_witness`
+  + `sigma_finite_measure` instance on product measure `\x`
 
 - file `contra.v`
 - in `contra.v`
@@ -148,47 +27,6 @@
     `absurd : ident(H)`, `absurd : { hyp_list(Hs) } constr(H)`,
 	 `absurd : { hyp_list(Hs) } ident(H)`
 
-### Changed
-- in `topology.v`
-  + definition `fct_restrictedUniformType` changed to use `weak_uniformType`
-  + definition `family_cvg_topologicalType` changed to use `sup_uniformType`
-
-- in `constructive_ereal.v`:
-  + lemmas `lee_paddl`, `lte_paddl`, `lee_paddr`, `lte_paddr`,
-    `lte_spaddr`, `lee_pdaddl`, `lte_pdaddl`, `lee_pdaddr`,
-    `lte_pdaddr`, `lte_spdaddr` generalized to `realDomainType`
-- in `constructive_ereal.v`:
-  + generalize `lte_addl`, `lte_addr`, `gte_subl`, `gte_subr`,
-    `lte_daddl`, `lte_daddr`, `gte_dsubl`, `gte_dsubr`
-- in `topology.v`:
-  + lemmas `continuous_subspace0`, `continuous_subspace1`
-
-- in `realfun.v`:
-  + notations `nondecreasing_fun`, `nonincreasing_fun`,
-    `increasing_fun`, `decreasing_fun`
-  + lemmas `cvg_addrl`, `cvg_addrr`, `cvg_centerr`, `cvg_shiftr`,
-    `nondecreasing_cvgr`,
-	`nonincreasing_at_right_cvgr`,
-	`nondecreasing_at_right_cvgr`,
-	`nondecreasing_cvge`, `nondecreasing_is_cvge`,
-	`nondecreasing_at_right_cvge`, `nondecreasing_at_right_is_cvge`,
-	`nonincreasing_at_right_cvge`, `nonincreasing_at_right_is_cvge`
-- in `ereal.v`:
-  + lemmas `ereal_sup_le`, `ereal_inf_le`
-
-- in `normedtype.v`:
-  + definition `lower_semicontinuous`
-  + lemma `lower_semicontinuousP`
-
-- in `numfun.v`:
-  + lemma `patch_indic`
-
-- in `lebesgue_measure.v`
-  + lemma `lower_semicontinuous_measurable`
-
-- in `lebesgue_integral.v`:
-  + `sigma_finite_measure` instance on product measure `\x`
-
 - in `topology.v`:
   + lemma `filter_bigI_within`
   + lemma `near_powerset_map`
@@ -221,21 +59,13 @@
   + lemma `continuous_uncurry`
   + lemma `curry_continuous`
   + lemma `uncurry_continuous`
-- in `boolp.v`:
-  + tactic `eqProp`
-  + variant `BoolProp`
-  + lemmas `PropB`, `notB`, `andB`, `orB`, `implyB`, `decide_or`, `not_andE`,
-    `not_orE`, `orCA`, `orAC`, `orACA`, `orNp`, `orpN`, `or3E`, `or4E`, `andCA`,
-	 `andAC`, `andACA`, `and3E`, `and4E`, `and5E`, `implyNp`, `implypN`,
-	 `implyNN`, `or_andr`, `or_andl`, `and_orr`, `and_orl`, `exists2E`,
-	 `inhabitedE`, `inhabited_witness`
 
 ### Changed
 
 - in `topology.v`:
   + lemmas `nbhsx_ballx` and `near_ball` take a parameter of type `R` instead of `{posnum R}`
   + lemma `pointwise_compact_cvg`
-  
+
 ### Renamed
 
 ### Generalized

classical/contra.v

@@ -20,11 +20,8 @@ Unset Printing Implicit Defensive.
 (*               Caveat: absurd_not cannot be used as a move/ view because    *)
 (*               its conclusion is indeterminate. The more general notP can   *)
 (*               be used instead.                                             *)
-(*     contra == proof by contraposition. Assume the negation of the goal     *)
-(*               conclusion, and prove the negation of a given assumption.    *)
-(*               The defective form contra (which can also be written         *)
-(*               contrapose) expects the assumption to be pushed on the goal  *)
-(*               which thus has the form assumption -> conclusion.            *)
+(*     contra == proof by contraposition. Change a goal of the form           *)
+(*               assumption -> conclusion to ~ conclusion -> ~ assumption.    *)
 (*               As with assume_not, contra allows both assumption and        *)
 (*               conclusion to be in Type, simplifies the negation of both    *)
 (*               assumption and conclusion, and exposes the constructive      *)
@@ -299,7 +296,7 @@ Canonical or4_nProp tP nP P tQ nQ Q tR nR R tS nS S :=
 (* both here for the imply_nProp instance and for bounded_forall_nProp below. *)
 (* Because the andRHS instances match the Prop RETURNED by negatedProp they   *)
 (* do not need to expand definitions, hence do not need to use the wrapper    *)
-(* telescope pattern.                                         *)
+(* telescope pattern.                                                         *)
 (******************************************************************************)
 
 Notation and_def binary P Q PQ := (PQ = if binary then P /\ Q else Q)%type.
@@ -338,8 +335,8 @@ Canonical inhabited_nProp T := ProperNegatedProp (inhabited_nPropP T).
 (*   We use tertiary structures to recognize bounded foralls and simplify,    *)
 (* e.g., ~ forall x, P -> Q to exists2 x, P & ~ Q, or even exists x, P when   *)
 (* Q :=  False (as above for imply).                                          *)
-(*   As forall_body_nProp and forall_body_proper_nProp are telescopes   *)
-(* over negatedProp and properNegatedProp, respectively, their instances *)
+(*   As forall_body_nProp and forall_body_proper_nProp are telescopes         *)
+(* over negatedProp and properNegatedProp, respectively, their instances      *)
 (* match instances declared above without the need to expand definitions,     *)
 (* hence do not need to use the wrapper telescope idiom.                      *)
 (******************************************************************************)
@@ -355,7 +352,7 @@ Notation nBody b P nQ t nR x := (negatedForallBody b (P x) (nQ x) t (nR x)).
 (* unification code that prevents default instances from ever matching match  *)
 (* constructs. Furthermore rewriting with ifE would not work here, because    *)
 (* the if_expr definition would be expanded by the eta expansion needed to    *)
-(* match the exists_nProp rule.                                            *)
+(* match the exists_nProp rule.                                               *)
 (******************************************************************************)
 
 Fact forall_nPropP A b P nQ tR nR (R : forall x, nBody b P nQ tR nR x) :
@@ -731,7 +728,7 @@ Canonical exists2_wProp A s S P0 P t T Q0 Q :=
 (*   contra_Type converts an arbitrary function goal (with assumption and     *)
 (*     conclusion in Type) to an equivalent contrapositive Prop implication.  *)
 (*   contra_notP simplifies a contrapositive ~ Q -> ~ P goal using            *)
-(*     negatedProp instances.                                               *)
+(*     negatedProp instances.                                                 *)
 (******************************************************************************)
 
 Local Fact push_goal_copy {T} : ((T -> T) -> T) -> T. Proof. exact. Qed.
@@ -749,6 +746,76 @@ Proof. by rewrite 2!lax_notE. Qed.
 
 End Internals.
 Import Internals.
+Canonical TypeForall.
+Canonical PropForall.
+Canonical SetForall.
+Canonical wrap1Prop.
+Canonical wrap1Type.
+Canonical proper_nProp.
+Canonical trivial_nProp.
+Canonical True_nProp.
+Canonical False_nProp.
+Canonical not_nProp.
+Canonical and_nProp.
+Canonical and3_nProp.
+Canonical and4_nProp.
+Canonical and5_nProp.
+Canonical or_nProp.
+Canonical or3_nProp.
+Canonical or4_nProp.
+Canonical unary_and_rhs.
+Canonical binary_and_rhs.
+Canonical imply_nProp.
+Canonical exists_nProp.
+Canonical exists2_nProp.
+Canonical inhabited_nProp.
+Canonical forall_nProp.
+Canonical proper_nBody.
+Canonical nonproper_nBody.
+Canonical bounded_nBody.
+Canonical unbounded_nBody.
+Canonical is_true_nProp.
+Canonical true_neg.
+Canonical true_pos.
+Canonical false_neg.
+Canonical false_pos.
+Canonical id_neg.
+Canonical id_pos.
+Canonical negb_neg.
+Canonical negb_pos.
+Canonical neg_ltn_LHS.
+Canonical neg_leq_LHS.
+Canonical leq_neg.
+Canonical eq_nProp.
+Canonical bool_neq.
+Canonical true_neq.
+Canonical false_neq.
+Canonical eqType_neq.
+Canonical eq_op_pos.
+Canonical Prop_wType.
+Canonical proper_wType.
+Canonical forall_wType.
+Canonical inhabited_wType.
+Canonical void_wType.
+Canonical unit_wType.
+Canonical pair_wType.
+Canonical sum_wType.
+Canonical sumbool_wType.
+Canonical sumor_wType.
+Canonical sig1_wType.
+Canonical sig2_wType.
+Canonical sigT_wType.
+Canonical sigT2_wType.
+Canonical proper_wProp.
+Canonical forall_wProp.
+Canonical trivial_wProp.
+Canonical inhabited_wProp.
+Canonical nand_false_bool.
+Canonical nand_true_bool.
+Canonical and_wProp.
+Canonical or_wProp.
+Canonical exists_wProp.
+Canonical exists2_wProp.
 
 (******************************************************************************)
 (* Lemma and tactic assume_not: add a goal negation assumption. The tactic    *)
@@ -758,7 +825,8 @@ Import Internals.
 
 Lemma assume_not {P} : (~ P -> P) -> P. Proof. by rewrite implyNp orB. Qed.
 Ltac assume_not :=
-  apply Internals.push_goal_copy; apply: Internals.assume_not_with => /lax_notP-/lax_witness.
+  apply: Internals.push_goal_copy; apply: Internals.assume_not_with
+    => /Internals.lax_notP-/Internals.lax_witness.
 
 (******************************************************************************)
 (* Lemma and tactic absurd_not: proof by contradiction. Same as assume_not,   *)
@@ -783,7 +851,9 @@ Ltac absurd_not := assume_not; apply: Internals.absurdW.
 (* switch.                                                                    *)
 (******************************************************************************)
 
-Ltac contrapose := apply: Internals.contra_Type; apply: contra_notP => /lax_witness.
+Ltac contrapose :=
+  apply: Internals.contra_Type;
+  apply: contra_notP => /lax_witness.
 Tactic Notation "contra" := contrapose.
 Tactic Notation "contra" ":" constr(H) := move: (H); contra.
 Tactic Notation "contra" ":" ident(H) := move: H; contra.