change changelog and hide internals of contra.v (as suggested)

CHANGELOG_UNRELEASED.md

@@ -136,119 +136,7 @@
 
 - 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`
+  + lemma `assume_not`
   + tactic `assume_not`
   + lemma `absurd_not`
   + tactics `absurd_not`, `contrapose`

classical/contra.v

@@ -44,6 +44,10 @@ Unset Printing Implicit Defensive.
 (*               Finally the Ltac absurd term form is also supported.         *)
 (******************************************************************************)
 
+(* Hiding module for the internal definitions and lemmas used by the tactics
+  defined here. *)
+Module Internals.
+
 (******************************************************************************)
 (* A wrapper for view lemmas with an indeterminate conclusion (of the form    *)
 (* forall ... T ..., pattern -> T), and for which the intended view pattern   *)
@@ -743,6 +747,9 @@ 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.
 
+End Internals.
+Import Internals.
+
 (******************************************************************************)
 (* Lemma and tactic assume_not: add a goal negation assumption. The tactic    *)
 (* also works for goals in Type, simplifies the added assumption, and         *)
@@ -751,17 +758,16 @@ Proof. by rewrite 2!lax_notE. Qed.
 
 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.
+  apply Internals.push_goal_copy; apply: Internals.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.
+Lemma absurd_not {P} : (~ P -> False) -> P. Proof. by move/Internals.notP. Qed.
+Ltac absurd_not := assume_not; apply: Internals.absurdW.
 
 (******************************************************************************)
 (* Tactic contra: proof by contraposition. Assume the negation of the goal    *)
@@ -777,7 +783,7 @@ Ltac absurd_not := assume_not; apply: absurdW.
 (* switch.                                                                    *)
 (******************************************************************************)
 
-Ltac contrapose := apply: 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.