Skip to content

Commit

Permalink
Browse files Browse the repository at this point in the history
renaming of lemmas for classical reasoning
  • Loading branch information
affeldt-aist committed Jun 17, 2020
1 parent 55e6be3 commit ecd914f
Show file tree
Hide file tree
Showing 5 changed files with 42 additions and 29 deletions.
8 changes: 8 additions & 0 deletions CHANGELOG_UNRELEASED.md
Expand Up @@ -6,9 +6,17 @@

### Changed

- moved from `normedtype.v` to `boolp.v` and renamed:
+ `forallN` -> `forallNE`
+ `existsN` -> `existsNE`

### Renamed

- in `classical_sets.v`, `ub` and `lb` are renamed to `ubound` and `lbound`
- in `boolp.v`,
+ `existsPN` -> `not_existsP`
+ `forallPN` -> `not_forallP`
+ `Nimply` -> `not_implyP`

### Removed

Expand Down
55 changes: 30 additions & 25 deletions theories/boolp.v
Expand Up @@ -553,42 +553,47 @@ apply: (asbool_equiv_eqP existsp_asboolPn);
by split=> -[x h]; exists x; apply/negP.
Qed.

Lemma existsNP (T : Type) (P : T -> Prop) :
(exists x : T, ~ P x) <-> (~ forall x : T, P x).
Lemma not_implyP (P Q : Prop) : ~ (P -> Q) <-> P /\ ~ Q.
Proof.
split => [[x Px h]|/asboolP]; [exact: Px|].
by rewrite asbool_neg => /existsp_asboolPn.
split=> [/asboolP|[p nq pq]]; [|exact/nq/pq].
by rewrite asbool_neg => /imply_asboolPn.
Qed.

Lemma existsPN (T : Type) (P : T -> Prop) :
(exists x : T, P x) <-> (~ forall x : T, ~ P x).
Proof.
split => [[x Px h]|/asboolP]; [exact: (h x)|].
by move/asboolP/existsNP => [x /contrapT Px]; exists x.
Qed.
Lemma not_implyE (P Q : Prop) : (~ (P -> Q)) = (P /\ ~ Q).
Proof. by rewrite propeqE not_implyP. Qed.

Lemma forallNP (T : Type) (P : T -> Prop) :
(forall x : T, ~ P x) <-> (~ exists x : T, P x).
Proof.
split => [h [x Px]|/asboolP]; [exact: (h x)|].
by rewrite asbool_neg => /forallp_asboolPn.
Qed.
Lemma orC (P Q : Prop) : (P \/ Q) = (Q \/ P).
Proof. rewrite propeqE; tauto. Qed.

Lemma forallPN (T : Type) (P : T -> Prop) :
(forall x : T, P x) <-> (~ exists x : T, ~ P x).
Lemma eqNN (P : Prop) : (~ ~ P) = P.
Proof. by rewrite propeqE; split=> [/contrapT|?]. Qed.

Lemma forallNE {T} (P : T -> Prop) : (forall x, ~ P x) = ~ exists x, P x.
Proof.
split => [h [x px]|]; [exact/px/h|move=> /forallNP h x].
by move/contrapT : (h x).
by rewrite propeqE; split => [fP [x /fP]//|nexP x Px]; apply: nexP; exists x.
Qed.

Lemma Nimply (P Q : Prop) : ~ (P -> Q) <-> (P /\ ~ Q).
Lemma existsNE {T} (P : T -> Prop) : (exists x, ~ P x) = ~ forall x, P x.
Proof.
split=> [/asboolP|[p nq pq]]; [|exact/nq/pq].
by rewrite asbool_neg => /imply_asboolPn.
rewrite propeqE; split=> [[x Px] aP //|NaP].
by apply: contrapT; rewrite -forallNE => aP; apply: NaP => x; apply: contrapT.
Qed.

Lemma orC (P Q : Prop) : (P \/ Q) = (Q \/ P).
Proof. rewrite propeqE; tauto. Qed.
Lemma existsNP T (P : T -> Prop) :
(exists x : T, ~ P x) <-> ~ forall x : T, P x.
Proof. by rewrite existsNE. Qed.

Lemma not_existsP T (P : T -> Prop) :
(exists x : T, P x) <-> ~ forall x : T, ~ P x.
Proof. by rewrite forallNE eqNN. Qed.

Lemma forallNP T (P : T -> Prop) :
(forall x : T, ~ P x) <-> ~ exists x : T, P x.
Proof. by rewrite forallNE. Qed.

Lemma _not_forallP T (P : T -> Prop) :
(forall x : T, P x) <-> ~ exists x : T, ~ P x.
Proof. by rewrite existsNE eqNN. Qed.

(* -------------------------------------------------------------------- *)
Definition xchooseb {T : choiceType} (P : pred T) (h : `[exists x, P x]) :=
Expand Down
4 changes: 2 additions & 2 deletions theories/ereal.v
Expand Up @@ -458,7 +458,7 @@ have [Spoo|Spoo] := pselect (S +oo).
by exists +oo; split; [apply/ereal_ub_pinfty | apply/lbP => /= y /ubP; apply].
have [r Sr] : exists r, S r%:E.
move: S0 Snoo Spoo => [[r Sr _ _|//|Snoo Snoo1 Spoo]]; first by exists r.
apply/existsPN => nS; move: Snoo1; apply; apply/eqP; rewrite predeqE.
apply/not_existsP => nS; move: Snoo1; apply; apply/eqP; rewrite predeqE.
by case=> // r; split => // /nS.
set U := [set x | (real_of_er_def r @` S) x ].
have [ubU|/set0P/negP] := pselect (ubound U !=set0); last first.
Expand Down Expand Up @@ -530,7 +530,7 @@ have : ~ ubound S (ereal_sup S - e%:num%:E)%E.
move/ub_ereal_sup; apply/negP.
by rewrite -ltNge Sr lte_subl_addr lte_fin ltr_addl.
move/asboolP; rewrite asbool_neg; case/existsp_asboolPn => /= x.
case/Nimply => ? ?; exists x; split => //.
rewrite not_implyE => -[? ?]; exists x; split => //.
by rewrite ltNge; apply/negP.
Qed.

Expand Down
2 changes: 1 addition & 1 deletion theories/reals.v
Expand Up @@ -327,7 +327,7 @@ split; last first.
move=> h [x] /ubP hle; case/(_ x): h => y /hle.
by rewrite leNgt => /negbTE ->.
move/forallNP => h x; have {h} := h x.
move=> /ubP /existsNP => -[y /Nimply[Ey /negP]].
move=> /ubP /existsNP => -[y /not_implyP[Ey /negP]].
by rewrite -ltNge => ltx; exists y.
Qed.

Expand Down
2 changes: 1 addition & 1 deletion theories/sequences.v
Expand Up @@ -771,7 +771,7 @@ have [/eqP {lnoo}loo|lpoo] := boolP (l == +oo%E).
near: n.
suff [n Hn] : exists n, (expand (contract +oo - (e)%:num)%R < u_ n)%E.
by exists n => // m nm; rewrite (lt_le_trans Hn) //; apply nd_u_.
apply/existsPN => abs.
apply/not_existsP => abs.
have : (l <= expand (contract +oo - (e)%:num)%R)%E.
apply: ub_ereal_sup => x [n _ <-{x}].
rewrite leNgt; apply/negP/abs.
Expand Down

0 comments on commit ecd914f

Please sign in to comment.