diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index 978bc7020d..cd01743597 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/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` diff --git a/classical/contra.v b/classical/contra.v index f11935631a..6e311cc255 100644 --- a/classical/contra.v +++ b/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,7 +758,7 @@ 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, *) @@ -759,9 +766,8 @@ Ltac assume_not := (* 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.