Skip to content

less notE, etc. warnings #1824

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
affeldt-aist merged 1 commit into from
Jan 16, 2026
Merged

less notE, etc. warnings #1824

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 1 addition & 1 deletion classical/classical_sets.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -707,7 +707,7 @@ Lemma setDE A B : A `\` B = A `&` ~` B. Proof. by []. Qed.
Lemma setUDl A B C : (A `\` B) `|` C = (A `|` C) `\` (B `\` C).
Proof.
apply/seteqP; split => x /=; first tauto.
by move=> [[a|c]]; rewrite not_andE notE; tauto.
#[warnings="-deprecated-syntactic-definition"] by move=> [[a|c]]; rewrite not_andE notE; tauto.
Qed.

Lemma setUDr A B C : A `|` (B `\` C) = (A `|` B) `\` (C `\` A).
Expand Down
22 changes: 11 additions & 11 deletions classical/contra.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -297,19 +297,19 @@ Canonical and_nProp P tQ nQ Q :=
ProperNegatedProp (@and_nPropP P tQ nQ Q).

Fact and3_nPropP P Q tR nR R : (~ [/\ P, Q & nProp tR nR R]) = (P -> Q -> nR).
Proof. by hnf; rewrite and3E notE. Qed.
Proof. #[warnings="-user-warn"] by hnf; rewrite and3E notE. Qed.
Canonical and3_nProp P Q tR nR R :=
ProperNegatedProp (@and3_nPropP P Q tR nR R).

Fact and4_nPropP P Q R tS nS S :
(~ [/\ P, Q, R & nProp tS nS S]) = (P -> Q -> R -> nS).
Proof. by hnf; rewrite and4E notE. Qed.
Proof. #[warnings="-user-warn"] by hnf; rewrite and4E notE. Qed.
Canonical and4_nProp P Q R tS nS S :=
ProperNegatedProp (@and4_nPropP P Q R tS nS S).

Fact and5_nPropP P Q R S tT nT T :
(~ [/\ P, Q, R, S & nProp tT nT T]) = (P -> Q -> R -> S -> nT).
Proof. by hnf; rewrite and5E notE. Qed.
Proof. #[warnings="-user-warn"] by hnf; rewrite and5E notE. Qed.
Canonical and5_nProp P Q R S tT nT T :=
ProperNegatedProp (@and5_nPropP P Q R S tT nT T).

Expand All @@ -321,14 +321,14 @@ Canonical or_nProp tP nP P tQ nQ Q :=

Fact or3_nPropP tP nP P tQ nQ Q tR nR R :
(~ [\/ nProp tP nP P, nProp tQ nQ Q | nProp tR nR R]) = [/\ nP, nQ & nR].
Proof. by rewrite or3E notE and3E. Qed.
Proof. #[warnings="-user-warn"] by rewrite or3E notE and3E. Qed.
Canonical or3_nProp tP nP P tQ nQ Q tR nR R :=
ProperNegatedProp (@or3_nPropP tP nP P tQ nQ Q tR nR R).

Fact or4_nPropP tP nP P tQ nQ Q tR nR R tS nS S :
(~ [\/ nProp tP nP P, nProp tQ nQ Q, nProp tR nR R | nProp tS nS S])
= [/\ nP, nQ, nR & nS].
Proof. by rewrite or4E notE and4E. Qed.
Proof. #[warnings="-user-warn"] 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).

Expand Down Expand Up @@ -363,12 +363,12 @@ Canonical exists_nProp A tP nP P :=

Fact exists2_nPropP A P tQ nQ Q :
(~ exists2 x : A, P x & nPred tQ nQ Q x) = (forall x : A, P x -> nQ x).
Proof. by rewrite exists2E notE. Qed.
Proof. #[warnings="-user-warn"] by rewrite exists2E notE. Qed.
Canonical exists2_nProp A P tQ nQ Q :=
ProperNegatedProp (@exists2_nPropP A P tQ nQ Q).

Fact inhabited_nPropP T : (~ inhabited T) = (T -> False).
Proof. by rewrite inhabitedE notE. Qed.
Proof. #[warnings="-user-warn"] by rewrite inhabitedE notE. Qed.
Canonical inhabited_nProp T := ProperNegatedProp (inhabited_nPropP T).

(**md**************************************************************************)
Expand Down Expand Up @@ -463,7 +463,7 @@ Local Fact negb_negP P (b : positedBool P) : (~ ~~ b) = P.
Proof. by rewrite (reflect_eq negP) negbK; case: b. Qed.
Canonical negb_neg P b := NegatedBool (@negb_negP P b).
Local Fact negb_posP nP (b : negatedBool nP) : (~~ b = nP :> Prop).
Proof. by rewrite -(reflect_eq negP) notE. Qed.
Proof. #[warnings="-user-warn"] by rewrite -(reflect_eq negP) notE. Qed.
Canonical negb_pos nP b := PositedBool (@negb_posP nP b).

(**md**************************************************************************)
Expand All @@ -479,7 +479,7 @@ Canonical neg_ltn_LHS n m := @NegatedLeqLHS n (n <= m) m.+1 erefl.
Canonical neg_leq_LHS n m := @NegatedLeqLHS n (n < m) m erefl.

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.
Proof. #[warnings="-user-warn"] by rewrite notE -ltnNge; case: m => /= m ->. Qed.
Canonical leq_neg n lt_nm m := NegatedBool (@leq_negP n lt_nm m).

(**md**************************************************************************)
Expand Down Expand Up @@ -792,7 +792,7 @@ Proof. by rewrite 2!lax_notE. Qed.

End Internals.
Import Internals.
Definition notP := @Internals.notP.
#[warnings="-user-warn"] Definition notP := @Internals.notP.
Hint View for move/ move_viewP|2.
Hint View for move/ Internals.equivT_LR|2 Internals.equivT_RL|2.
Hint View for apply/ Internals.equivT_RL|2 Internals.equivT_LR|2.
Expand All @@ -815,7 +815,7 @@ 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/Internals.notP. Qed.
Lemma absurd_not {P} : (~ P -> False) -> P. Proof. #[warnings="-user-warn"] by move/Internals.notP. Qed.
Ltac absurd_not := assume_not; apply: Internals.absurdW.

(**md**************************************************************************)
Expand Down
2 changes: 1 addition & 1 deletion classical/internal_Eqdep_dec.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -2,7 +2,7 @@

Attributes deprecated(since="mathcomp-analysis 1.10.0",
note="This file is for internal purpose only and should not \
be imported nor used. It may removed in the future.").
be imported nor used. It may be removed in the future.").

Import EqNotations.

Expand Down