From 9561644af880654188116a55389adfcc75088a36 Mon Sep 17 00:00:00 2001 From: Quentin Vermande Date: Fri, 22 Dec 2023 16:22:26 +0100 Subject: [PATCH] doc and CHANGELOG --- CHANGELOG_UNRELEASED.md | 159 ++++++++++++++++++++++++++++++++++++++++ classical/contra.v | 81 +++++++++++++++++++- 2 files changed, 236 insertions(+), 4 deletions(-) diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index 3c9ab85141..e8f54ae1f3 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -18,6 +18,162 @@ - in `normedtype.v`: + hints for `at_right_proper_filter` and `at_left_proper_filter` +- in `sequences.v`: + + lemma `invr_cvg0` and `invr_cvg_pinfty` + + lemma `cvgPninfty_lt`, `cvgPpinfty_near`, `cvgPninfty_near`, + `cvgPpinfty_lt_near` and `cvgPninfty_lt_near` +- in `classical_sets.v`: + + notations `\bigcup_(i < n) F` and `\bigcap_(i < n) F` + +- in `boolp.v`: + + tactic `eqProp` + + definition `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` + +- file `contra.v` +- in `contra.v` + + definitions `move_view`, `move_viewP`, `forallSort` + + notation `mkForallSort` + + definitions `TypeForall`, `PropForall`, `SetForall`, `Forall` + + notation `\Forall x .. z, T` + + tactic notation `ForallI` + + definitions `wrappedProp`, `wrap4Prop`, `wrap3Prop`, `wrap2Prop`, + `wrap1Prop`, `wrappedType`, `wrap4Type`, `wrap3Type`, `wrap2Type`, + `wrap1Type` + + lemma `generic_forall_extensionality` + + definitions `negatedProp`, `properNegatedProp` + + lemmas `lax_notE`, `lax_notP` + + definitions `notE`, `notP` + + lemma `proper_nPropP` + + definitions `notI`, `proper_nProp`, `trivial_nProp`, `True_nProp`, + `False_nProp`, `not_nProp` + + lemma `and_nPropP` + + definition `and_nProp` + + lemma `and3_nPropP` + + definition `and3_nProp` + + lemma `and4_nPropP` + + definition `and4_nProp` + + lemma `and5_nPropP` + + definition `and5_nProp` + + lemma `or_nPropP` + + definition `or_nProp` + + lemma `or3_nPropP` + + definition `or3_nProp` + + lemma `or4_nPropP` + + definition `or4_nProp` + + notation `and_def binary P Q PQ` + + definitions `andRHS`, `unary_and_rhs`, `binary_and_rhs` + + lemma `imply_nPropP` + + definition `imply_nProp` + + lemma `exists_nPropP` + + definition `exists_nProp` + + lemma `exists2_nPropP` + + definition `exists2_nProp` + + lemma `inhabited_nPropP` + + definitions `inhabited_nProp`, `negatedForallBody`, + `properNegatedForallBody` + + notation `nBody b P nQ t nR x` + + lemma `forall_nPropP` + + definition `forall_nProp` + + lemma `proper_nBodyP` + + definition `proper_nBody`, `nonproper_nBody` + + lemma `andRHS_def` + + definitions `bounded_nBody`, `unbounded_nBody`, `negatedBool`, + `positedBool` + + lemma `is_true_nPropP` + + definition `is_true_nProp` + + lemmas `true_negP`, `true_posP`, `false_negP`, `false_posP` + + definitions `true_neg`, `true_pos`, `false_neg`, `false_pos` + + lemma `id_negP` + + definitions `id_neg`, `id_pos` + + lemma `negb_negP` + + definition `negb_neg` + + lemma `negb_posP` + + definitions `negb_pos`, `negatedLeqLHS`, `neg_ltn_LHS`, `neg_leq_LHS` + + lemma `leq_negP` + + definitions `leq_neg`, `neqRHS`, `boolNeqRHS` + + lemma `eq_nPropP` + + definition `eq_nProp` + + lemma `bool_neqP` + + definitions `bool_neq`, `true_neq` + + lemma `false_neqP` + + definition `false_neq` + + lemma `eqType_neqP` + + definition `eqType_neq` + + lemma `eq_op_posP` + + definitionss `eq_op_pos`, `witnessedType`, `properWitnessedType` + + lemmas `witnessedType_intro`, `witnessedType_elim`, `eq_inhabited` + + definition `Prop_wType` + + lemma `proper_wTypeP` + + definition `proper_wType` + + lemma `forall_wTypeP` + + definitions `forall_wType`, `inhabited_wType` + + lemma `void_wTypeP` + + definition `void_wType` + + lemma `unit_wTypeP` + + definition `unit_wType` + + lemma `pair_wTypeP` + + definition `pair_wType` + + lemma `sum_wTypeP` + + definition `sum_wTypeP` + + lemma `sumbool_wTypeP` + + definition `sumbool_wType` + + lemma `sumor_wTypeP` + + definition `sumor_wType` + + lemma `sig1_wTypeP` + + definition `sig1_wType` + + lemma `sig2_wTypeP` + + definition `sig2_wType` + + lemma `sigT_wTypeP` + + definition `sigT_wType` + + lemma `sigT2_wTypeP` + + definitions `sigT2_wType`, `witnessProp`, `properWitnessProp` + + lemmas `wPropP`, `lax_witness` + + definition `witness` + + lemma `proper_wPropP` + + definition `proper_wProp` + + lemma `forall_wPropP` + + definitions `forall_wProp`, `trivial_wProp`, `inhabited_wProp`, `nandBool`, + `nand_false_bool`, `nand_true_bool` + + lemma `and_wPropP` + + definition `and_wProp` + + lemma `or_wPropP` + + definition `or_wProp` + + lemma `exists_wPropP` + + definition `exists_wProp` + + lemma `exists2_wPropP` + + definition `exists2_wProp` + + lemma `push_goal_copy`, `assume_not_with`, `absurdW`, `contra_Type`, + `contra_notP`, `assume_not` + + tactic `assume_not` + + lemma `absurd_not` + + tactics `absurd_not`, `contrapose` + + tactic notations `contra`, `contra : constr(H)`, `contra : ident(H)`, + `contra : { hyp_list(Hs) } constr(H)`, `contra : { hyp_list(Hs) } ident(H)`, + `contra : { - } constr(H)` + + lemma `absurd` + + tactic notations `absurd`, `absurd constr(P)`, `absurd : constr(H)`, + `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`, @@ -76,6 +232,9 @@ `ae_eq_mul1l`, `ae_eq_abse` +-in `boolp.v` + - lemmas `orC` and `andC` now use `commutative` + ### Renamed - in `exp.v`: diff --git a/classical/contra.v b/classical/contra.v index d13aec55fa..a2691ee7ab 100644 --- a/classical/contra.v +++ b/classical/contra.v @@ -1,5 +1,4 @@ (* mathcomp analysis (c) 2017 Inria and AIST. License: CeCILL-C. *) -(* Distributed under the terms of CeCILL-B. *) From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq. Require Import boolp. @@ -7,6 +6,44 @@ Set Implicit Arguments. Unset Strict Implicit. Unset Printing Implicit Defensive. +(******************************************************************************) +(* Contraposition *) +(* *) +(* This file provides tactics to reason by contraposition and contradiction. *) +(* *) +(* * Tactics *) +(* assume_not == add a goal negation assumption. The tactic also works for *) +(* goals in Type, simplifies the added assumption, and *) +(* exposes its top-level constructive content. *) +(* absurd_not == proof by contradiction. Same as assume_not, but the goal is *) +(* erased and replaced by False. *) +(* 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. *) +(* 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 *) +(* contents of the negated conclusion. *) +(* The contra tactic also supports a limited form of the ':' *) +(* discharge pseudo tactical, whereby contra: means *) +(* move: ; contra. *) +(* The only allowed are one term, possibly preceded *) +(* by a clear switch. *) +(* absurd == proof by contradiction. The defective form of the tactic *) +(* simply replaces the entire goal with False (just as the Ltac *) +(* exfalso), leaving the user to derive a contradiction from *) +(* the assumptions. *) +(* The ':' form absurd: replaces the goal with the *) +(* negation of the (single) (as with contra:, a clear *) +(* switch is also allowed. *) +(* Finally the Ltac absurd term form is also supported. *) +(******************************************************************************) + (******************************************************************************) (* A wrapper for view lemmas with an indeterminate conclusion (of the form *) (* forall ... T ..., pattern -> T), and for which the intended view pattern *) @@ -86,7 +123,6 @@ Tactic Notation "ForallI" ssrpatternarg(pat) := case: F / (@erefl _ F : Forall _ = _). Tactic Notation "ForallI" := ForallI (forall x, _). - (******************************************************************************) (* We define specialized copies of the wrapped structure of ssrfun for Prop *) (* and Type, as we need more than two alternative rules (indeed, 3 for Prop *) @@ -110,7 +146,6 @@ Canonical wrap1Type. Lemma generic_forall_extensionality {A} {S : forallSort A} {P Q : A -> S} : P =1 Q -> Forall P = Forall Q. Proof. by move/funext->. Qed. -Notation AEXT := generic_forall_extensionality. (******************************************************************************) (* A set of tools (tactics, views, and rewrite rules) to facilitate the *) @@ -154,6 +189,7 @@ Notation AEXT := generic_forall_extensionality. (* predicates can be added by declaring instances of proper_negatedProp. *) (******************************************************************************) +(******************************************************************************) (* The implementation follows the wrapper telescope pattern outlined above: *) (* negatedProp instances match on the wrappedProp wrapper to try three *) (* generic matching rules, in sucession: *) @@ -169,6 +205,7 @@ Notation AEXT := generic_forall_extensionality. (* that is set when Rule 3 is used, but this is actually used in the reverse *) (* direction: views notP and rewrite rule notE force trivial := false, thus *) (* excluding trivial instances. *) +(******************************************************************************) Structure negatedProp (trivial : bool) nP := NegatedProp {negated_Prop :> wrappedProp; _ : (~ negated_Prop) = nP}. @@ -180,10 +217,12 @@ Local Notation nProp t nP P := (unwrap_Prop (@negated_Prop t nP P)). Local Notation nPred t nP P x := (nProp t (nP x) (P x)). Local Notation pnProp nP P := (@proper_negated_Prop nP P). +(******************************************************************************) (* User views and rewrite rules. The plain versions (notP, notE and notI) do *) (* not match trivial instances; lax_XXX versions allow them. In addition, *) (* the negation introduction rewrite rule notI does not match forall or -> *) (* statements - lax_notI must be used for these. *) +(******************************************************************************) Lemma lax_notE {t nP} P : (~ nProp t nP P) = nP. Proof. by case: P. Qed. Lemma lax_notP {t nP P} : ~ nProp t nP P -> nP. Proof. by rewrite lax_notE. Qed. @@ -251,11 +290,13 @@ Proof. by rewrite or4E notE and4E. Qed. Canonical or4_nProp tP nP P tQ nQ Q tR nR R tS nS S := ProperNegatedProp (@or4_nPropP tP nP P tQ nQ Q tR nR R tS nS S). +(******************************************************************************) (* The andRHS tertiary structure used to simplify (~ (P -> False)) to P, *) (* 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. *) +(******************************************************************************) Notation and_def binary P Q PQ := (PQ = if binary then P /\ Q else Q)%type. Structure andRHS binary P Q PQ := @@ -288,6 +329,7 @@ Fact inhabited_nPropP T : (~ inhabited T) = (T -> False). Proof. by rewrite inhabitedE notE. Qed. Canonical inhabited_nProp T := ProperNegatedProp (inhabited_nPropP T). +(******************************************************************************) (* Rule 2: forall negation, including (T : Type) -> P statements. *) (* 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 *) @@ -296,6 +338,7 @@ Canonical inhabited_nProp T := ProperNegatedProp (inhabited_nPropP T). (* 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. *) +(******************************************************************************) Structure negatedForallBody bounded P nQ tR nR := NegatedForallBody { negated_forall_body :> negatedProp tR nR; _ : and_def bounded P nQ nR}. @@ -303,16 +346,20 @@ Structure properNegatedForallBody b P nQ nR := ProperNegatedForallBody { proper_negated_forall_body :> properNegatedProp nR; _ : and_def b P nQ nR}. Notation nBody b P nQ t nR x := (negatedForallBody b (P x) (nQ x) t (nR x)). +(******************************************************************************) (* The explicit argument to fun_if is a workaround for a bug in the Coq *) (* 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. *) +(******************************************************************************) + Fact forall_nPropP A b P nQ tR nR (R : forall x, nBody b P nQ tR nR x) : (~ forall x : A, R x) = if b then exists2 x, P x & nQ x else exists x, nQ x. Proof. rewrite exists2E -(fun_if (fun P => exists x, idfun P x)) notI /=; congr not. -by apply/AEXT=> x; rewrite if_arg lax_notI; case: (R x) => _ <-. +apply/generic_forall_extensionality=> x; rewrite if_arg lax_notI. +by case: (R x) => _ <-. Qed. Canonical forall_nProp A b P nQ tR nR (R : forall x, nBody b P nQ tR nR x) := @NegatedProp false _ (wrap2Prop (forall x : A, R x)) (forall_nPropP R). @@ -333,6 +380,7 @@ Canonical bounded_nBody b P nQ PnQ tR nR R := Canonical unbounded_nBody nQ Q := @ProperNegatedForallBody false True nQ nQ Q erefl. +(******************************************************************************) (* The properNegatedProp instance that handles boolean statements. We use *) (* two tertiary structures to handle positive and negative boolean statements *) (* so that the contra tactic below will mostly subsume the collection of *) @@ -342,6 +390,7 @@ Canonical unbounded_nBody nQ Q := (* Morgan laws to push boolean negation into connectives, as we did above for *) (* Prop connectives. It will be up to the user to use rewriting to put the *) (* negated statement in its desired shape. *) +(******************************************************************************) Structure negatedBool nP := NegatedBool {negated_bool :> bool; _ : (~ negated_bool) = nP}. @@ -372,10 +421,12 @@ Local Fact negb_posP nP (b : negatedBool nP) : (~~ b = nP :> Prop). Proof. by rewrite -(reflect_eq negP) notE. Qed. Canonical negb_pos nP b := PositedBool (@negb_posP nP b). +(******************************************************************************) (* We use a tertiary structure to handle the negation of nat comparisons, and *) (* simplify ~ m <= n to n < m, and ~ m < n to n <= m. As m < n is merely *) (* notation for m.+1 <= n, we need to dispatch on the left hand side of the *) (* comparison to perform the latter simplification. *) +(******************************************************************************) Structure negatedLeqLHS n lt_nm := NegatedLeqLHS {negated_leq_LHS :> nat; _ : (n < negated_leq_LHS) = lt_nm}. @@ -386,6 +437,7 @@ Local Fact leq_negP n lt_nm (m : negatedLeqLHS n lt_nm) : (~ m <= n) = lt_nm. Proof. by rewrite notE -ltnNge; case: m => /= m ->. Qed. Canonical leq_neg n lt_nm m := NegatedBool (@leq_negP n lt_nm m). +(******************************************************************************) (* We use two tertiary structures to simplify negation of boolean constant *) (* and decidable equalities, simplifying b <> true to ~~ b, b <> false to b, *) (* x <> y to x != y, and ~ x != y to x = y. We do need to use the wrapper *) @@ -395,6 +447,7 @@ Canonical leq_neg n lt_nm m := NegatedBool (@leq_negP n lt_nm m). (* The actual matching of the true and false RHS is delegated to a fourth *) (* level bool_eq_negation_rhs structure. Finally observe that the ~ x != y to *) (* x = y simplification can be handled by a bool_affirmation instance. *) +(******************************************************************************) Structure neqRHS nP T x := NeqRHS {neq_RHS :> wrapped T; _ : (x <> unwrap neq_RHS) = nP}. @@ -435,11 +488,13 @@ Canonical eq_op_pos T x y := PositedBool (@eq_op_posP T x y). (* provides simplification for ~ P for standard connectives and predicates. *) (******************************************************************************) +(******************************************************************************) (* Similarly to negatedProp, witnessedType returns the witness proposition *) (* via a projection argument P, but does not need to signal "trivial" *) (* instances as the default value for P is nontrivial (namely, inhabited T), *) (* while the "trivial" case where P = T is actually desireable and handled *) (* by an extra top-priority rule. *) +(******************************************************************************) Structure witnessedType P := WitnessedType { witnessed_Type :> wrappedType; _ : inhabited witnessed_Type = P}. @@ -538,6 +593,7 @@ Canonical sigT2_wType A P Q S T := (* finds a P such that P -> T (and T -> P for the converse direction). *) (******************************************************************************) +(******************************************************************************) (* The implementation follows the wrapper telescope pattern similarly to *) (* negatedProp, with three rules, one for Prop constructors with proper *) (* constructive contents, one for forall propositions (also with proper *) @@ -571,6 +627,7 @@ Canonical sigT2_wType A P Q S T := (* which fails Type/Prop universe constraints, and then fails outright, *) (* instead of using pattern unification to solve (2) as ?P := ?Q x, ?T := ?Q *) (* for a fresh ?Q : A -> Prop. *) +(******************************************************************************) Structure witnessProp (trivial : bool) (P0 : Prop) (T : Type) := WitnessProp {witness_Prop :> wrappedProp; _ : witness_Prop -> T * P0}. @@ -606,12 +663,14 @@ Canonical trivial_wProp P := Canonical inhabited_wProp T := ProperWitnessProp (@inhabited_witness T). +(******************************************************************************) (* Conjunctions P /\ Q are a little delicate to handle, as we should not *) (* produce a proper instance (and thus fail) if neither P nor Q is proper. *) (* We use a tertiary structure for this : nand_bool b, which has instances *) (* only for booleans b0 such that ~~ (b0 && b). We allow the witness_Prop *) (* instance for P to return an arbitrary 'trivial' flag s, but then force the *) (* 'trivial' flag for Q to be an instance of nand_bool s. *) +(******************************************************************************) Structure nandBool b := NandBool {nand_bool :> bool; _ : ~~ (nand_bool && b)}. Canonical nand_false_bool b := @NandBool b false isT. @@ -654,6 +713,7 @@ Canonical exists2_wProp A s S P0 P t T Q0 Q := (* User lemmas and tactics for proof by contradiction and contraposition. *) (******************************************************************************) +(******************************************************************************) (* Helper lemmas: *) (* push_goal_copy makes a copy of the goal that can then be matched with *) (* witnessedType and negatedProp instances to generate a contradiction *) @@ -668,6 +728,7 @@ Canonical exists2_wProp A s S P0 P t T Q0 Q := (* conclusion in Type) to an equivalent contrapositive Prop implication. *) (* contra_notP simplifies a contrapositive ~ Q -> ~ P goal using *) (* negatedProp instances. *) +(******************************************************************************) Local Fact push_goal_copy {T} : ((T -> T) -> T) -> T. Proof. exact. Qed. Local Fact assume_not_with {R P T} : (~ P -> R) -> (wType P T -> R) -> R. @@ -682,20 +743,27 @@ Local Fact contra_notP tP tQ (nP nQ : Prop) P Q : (nP -> nQ) -> (~ nProp tP nP P -> ~ nProp tQ nQ Q). Proof. by rewrite 2!lax_notE. Qed. +(******************************************************************************) (* Lemma and tactic assume_not: add a goal negation assumption. The tactic *) (* also works for goals in Type, simplifies the added assumption, and *) (* exposes its top-level constructive content. *) +(******************************************************************************) + Lemma assume_not {P} : (~ P -> P) -> P. Proof. by rewrite implyNp orB. Qed. Ltac assume_not := apply push_goal_copy; apply: assume_not_with => /lax_notP-/lax_witness. +(******************************************************************************) (* Lemma and tactic absurd_not: proof by contradiction. Same as assume_not, *) (* but the goal is erased and replaced by False. *) (* Caveat: absurd_not cannot be used as a move/ view because its conclusion *) (* is indeterminate. The more general notP defined above can be used instead. *) +(******************************************************************************) + Lemma absurd_not {P} : (~ P -> False) -> P. Proof. by move/notP. Qed. Ltac absurd_not := assume_not; apply: absurdW. +(******************************************************************************) (* Tactic 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 *) @@ -707,6 +775,8 @@ Ltac absurd_not := assume_not; apply: absurdW. (* pseudo tactical, whereby contra: means move: ; contra. *) (* The only allowed are one term, possibly preceded by a clear *) (* switch. *) +(******************************************************************************) + Ltac contrapose := apply: contra_Type; apply: contra_notP => /lax_witness. Tactic Notation "contra" := contrapose. Tactic Notation "contra" ":" constr(H) := move: (H); contra. @@ -717,12 +787,15 @@ Tactic Notation "contra" ":" "{" hyp_list(Hs) "}" ident(H) := contra: H; clear Hs. Tactic Notation "contra" ":" "{" "-" "}" constr(H) := contra: (H). +(******************************************************************************) (* Lemma and tactic absurd: proof by contradiction. The defective form of the *) (* lemma simply replaces the entire goal with False (just as the Ltac *) (* exfalso), leaving the user to derive a contradiction from the assumptions. *) (* The ':' form absurd: replaces the goal with the negation of the *) (* (single) (as with contra:, a clear switch is also allowed. *) (* Finally the Ltac absurd term form is also supported. *) +(******************************************************************************) + Lemma absurd T : False -> T. Proof. by []. Qed. Tactic Notation (at level 0) "absurd" := apply absurd. Tactic Notation (at level 0) "absurd" constr(P) := have []: ~ P.