aboutsummaryrefslogtreecommitdiff
path: root/theories/Logic
diff options
context:
space:
mode:
Diffstat (limited to 'theories/Logic')
-rw-r--r--theories/Logic/ChoiceFacts.v30
-rw-r--r--theories/Logic/ClassicalChoice.v4
-rw-r--r--theories/Logic/ClassicalDescription.v10
-rwxr-xr-xtheories/Logic/Classical_Pred_Set.v12
-rwxr-xr-xtheories/Logic/Classical_Pred_Type.v12
-rw-r--r--theories/Logic/Diaconescu.v20
-rw-r--r--theories/Logic/RelationalChoice.v10
7 files changed, 49 insertions, 49 deletions
diff --git a/theories/Logic/ChoiceFacts.v b/theories/Logic/ChoiceFacts.v
index 1926032733..ca9bea5094 100644
--- a/theories/Logic/ChoiceFacts.v
+++ b/theories/Logic/ChoiceFacts.v
@@ -19,20 +19,20 @@
Definition RelationalChoice :=
forall (A B:Type) (R:A -> B -> Prop),
- (forall x:A, exists y : B | R x y) ->
- exists R' : A -> B -> Prop
- | (forall x:A,
- exists y : B | R x y /\ R' x y /\ (forall y':B, R' x y' -> y = y')).
+ (forall x:A, exists y : B, R x y) ->
+ exists R' : A -> B -> Prop,
+ (forall x:A,
+ exists y : B, R x y /\ R' x y /\ (forall y':B, R' x y' -> y = y')).
Definition FunctionalChoice :=
forall (A B:Type) (R:A -> B -> Prop),
- (forall x:A, exists y : B | R x y) ->
- exists f : A -> B | (forall x:A, R x (f x)).
+ (forall x:A, exists y : B, R x y) ->
+ exists f : A -> B, (forall x:A, R x (f x)).
Definition ParamDefiniteDescription :=
forall (A B:Type) (R:A -> B -> Prop),
- (forall x:A, exists y : B | R x y /\ (forall y':B, R x y' -> y = y')) ->
- exists f : A -> B | (forall x:A, R x (f x)).
+ (forall x:A, exists y : B, R x y /\ (forall y':B, R x y' -> y = y')) ->
+ exists f : A -> B, (forall x:A, R x (f x)).
Lemma description_rel_choice_imp_funct_choice :
ParamDefiniteDescription -> RelationalChoice -> FunctionalChoice.
@@ -86,11 +86,11 @@ Qed.
Definition GuardedRelationalChoice :=
forall (A B:Type) (P:A -> Prop) (R:A -> B -> Prop),
- (forall x:A, P x -> exists y : B | R x y) ->
- exists R' : A -> B -> Prop
- | (forall x:A,
+ (forall x:A, P x -> exists y : B, R x y) ->
+ exists R' : A -> B -> Prop,
+ (forall x:A,
P x ->
- exists y : B | R x y /\ R' x y /\ (forall y':B, R' x y' -> y = y')).
+ exists y : B, R x y /\ R' x y /\ (forall y':B, R' x y' -> y = y')).
Definition ProofIrrelevance := forall (A:Prop) (a1 a2:A), a1 = a2.
@@ -103,7 +103,7 @@ destruct (rel_choice _ _ (fun (x:sigT P) (y:B) => R (projT1 x) y)) as [R' H0].
intros [x HPx].
destruct (H x HPx) as [y HRxy].
exists y; exact HRxy.
-pose (R'' := fun (x:A) (y:B) => exists H : P x | R' (existT P x H) y).
+pose (R'' := fun (x:A) (y:B) => exists H : P x, R' (existT P x H) y).
exists R''; intros x HPx.
destruct (H0 (existT P x HPx)) as [y [HRxy [HR'xy Huniq]]].
exists y. split.
@@ -120,7 +120,7 @@ Qed.
Definition IndependenceOfPremises :=
forall (A:Type) (P:A -> Prop) (Q:Prop),
- (Q -> exists x : _ | P x) -> exists x : _ | Q -> P x.
+ (Q -> exists x : _, P x) -> exists x : _, Q -> P x.
Lemma rel_choice_indep_of_premises_imp_guarded_rel_choice :
RelationalChoice -> IndependenceOfPremises -> GuardedRelationalChoice.
@@ -136,4 +136,4 @@ destruct (RelCh A B (fun x y => P x -> R x y)) as [R' H0].
exists y. split.
apply (H1 HPx).
exact H2.
-Qed. \ No newline at end of file
+Qed.
diff --git a/theories/Logic/ClassicalChoice.v b/theories/Logic/ClassicalChoice.v
index 80bbce461c..7b6fcdf53d 100644
--- a/theories/Logic/ClassicalChoice.v
+++ b/theories/Logic/ClassicalChoice.v
@@ -23,8 +23,8 @@ Require Import ChoiceFacts.
Theorem choice :
forall (A B:Type) (R:A -> B -> Prop),
- (forall x:A, exists y : B | R x y) ->
- exists f : A -> B | (forall x:A, R x (f x)).
+ (forall x:A, exists y : B, R x y) ->
+ exists f : A -> B, (forall x:A, R x (f x)).
Proof.
apply description_rel_choice_imp_funct_choice.
exact description.
diff --git a/theories/Logic/ClassicalDescription.v b/theories/Logic/ClassicalDescription.v
index 26e696a7cd..a20036f0a5 100644
--- a/theories/Logic/ClassicalDescription.v
+++ b/theories/Logic/ClassicalDescription.v
@@ -26,15 +26,15 @@ Axiom
dependent_description :
forall (A:Type) (B:A -> Type) (R:forall x:A, B x -> Prop),
(forall x:A,
- exists y : B x | R x y /\ (forall y':B x, R x y' -> y = y')) ->
- exists f : forall x:A, B x | (forall x:A, R x (f x)).
+ exists y : B x, R x y /\ (forall y':B x, R x y' -> y = y')) ->
+ exists f : forall x:A, B x, (forall x:A, R x (f x)).
(** Principle of definite description (aka axiom of unique choice) *)
Theorem description :
forall (A B:Type) (R:A -> B -> Prop),
- (forall x:A, exists y : B | R x y /\ (forall y':B, R x y' -> y = y')) ->
- exists f : A -> B | (forall x:A, R x (f x)).
+ (forall x:A, exists y : B, R x y /\ (forall y':B, R x y' -> y = y')) ->
+ exists f : A -> B, (forall x:A, R x (f x)).
Proof.
intros A B.
apply (dependent_description A (fun _ => B)).
@@ -46,7 +46,7 @@ Theorem classic_set : ((forall P:Prop, {P} + {~ P}) -> False) -> False.
Proof.
intro HnotEM.
pose (R := fun A b => A /\ true = b \/ ~ A /\ false = b).
-assert (H : exists f : Prop -> bool | (forall A:Prop, R A (f A))).
+assert (H : exists f : Prop -> bool, (forall A:Prop, R A (f A))).
apply description.
intro A.
destruct (classic A) as [Ha| Hnota].
diff --git a/theories/Logic/Classical_Pred_Set.v b/theories/Logic/Classical_Pred_Set.v
index e308eff143..a06be5ae2a 100755
--- a/theories/Logic/Classical_Pred_Set.v
+++ b/theories/Logic/Classical_Pred_Set.v
@@ -18,7 +18,7 @@ Variable U : Set.
(** de Morgan laws for quantifiers *)
Lemma not_all_ex_not :
- forall P:U -> Prop, ~ (forall n:U, P n) -> exists n : U | ~ P n.
+ forall P:U -> Prop, ~ (forall n:U, P n) -> exists n : U, ~ P n.
Proof.
unfold not in |- *; intros P notall.
apply NNPP; unfold not in |- *.
@@ -30,7 +30,7 @@ apply abs; exists n; trivial.
Qed.
Lemma not_all_not_ex :
- forall P:U -> Prop, ~ (forall n:U, ~ P n) -> exists n : U | P n.
+ forall P:U -> Prop, ~ (forall n:U, ~ P n) -> exists n : U, P n.
Proof.
intros P H.
elim (not_all_ex_not (fun n:U => ~ P n) H); intros n Pn; exists n.
@@ -38,7 +38,7 @@ apply NNPP; trivial.
Qed.
Lemma not_ex_all_not :
- forall P:U -> Prop, ~ ( exists n : U | P n) -> forall n:U, ~ P n.
+ forall P:U -> Prop, ~ (exists n : U, P n) -> forall n:U, ~ P n.
Proof.
unfold not in |- *; intros P notex n abs.
apply notex.
@@ -46,7 +46,7 @@ exists n; trivial.
Qed.
Lemma not_ex_not_all :
- forall P:U -> Prop, ~ ( exists n : U | ~ P n) -> forall n:U, P n.
+ forall P:U -> Prop, ~ (exists n : U, ~ P n) -> forall n:U, P n.
Proof.
intros P H n.
apply NNPP.
@@ -54,14 +54,14 @@ red in |- *; intro K; apply H; exists n; trivial.
Qed.
Lemma ex_not_not_all :
- forall P:U -> Prop, ( exists n : U | ~ P n) -> ~ (forall n:U, P n).
+ forall P:U -> Prop, (exists n : U, ~ P n) -> ~ (forall n:U, P n).
Proof.
unfold not in |- *; intros P exnot allP.
elim exnot; auto.
Qed.
Lemma all_not_not_ex :
- forall P:U -> Prop, (forall n:U, ~ P n) -> ~ ( exists n : U | P n).
+ forall P:U -> Prop, (forall n:U, ~ P n) -> ~ (exists n : U, P n).
Proof.
unfold not in |- *; intros P allnot exP; elim exP; intros n p.
apply allnot with n; auto.
diff --git a/theories/Logic/Classical_Pred_Type.v b/theories/Logic/Classical_Pred_Type.v
index 6bfd08e43e..f3f29747cf 100755
--- a/theories/Logic/Classical_Pred_Type.v
+++ b/theories/Logic/Classical_Pred_Type.v
@@ -18,7 +18,7 @@ Variable U : Type.
(** de Morgan laws for quantifiers *)
Lemma not_all_ex_not :
- forall P:U -> Prop, ~ (forall n:U, P n) -> exists n : U | ~ P n.
+ forall P:U -> Prop, ~ (forall n:U, P n) -> exists n : U, ~ P n.
Proof.
unfold not in |- *; intros P notall.
apply NNPP; unfold not in |- *.
@@ -30,7 +30,7 @@ apply abs; exists n; trivial.
Qed.
Lemma not_all_not_ex :
- forall P:U -> Prop, ~ (forall n:U, ~ P n) -> exists n : U | P n.
+ forall P:U -> Prop, ~ (forall n:U, ~ P n) -> exists n : U, P n.
Proof.
intros P H.
elim (not_all_ex_not (fun n:U => ~ P n) H); intros n Pn; exists n.
@@ -38,7 +38,7 @@ apply NNPP; trivial.
Qed.
Lemma not_ex_all_not :
- forall P:U -> Prop, ~ ( exists n : U | P n) -> forall n:U, ~ P n.
+ forall P:U -> Prop, ~ (exists n : U, P n) -> forall n:U, ~ P n.
Proof.
unfold not in |- *; intros P notex n abs.
apply notex.
@@ -46,7 +46,7 @@ exists n; trivial.
Qed.
Lemma not_ex_not_all :
- forall P:U -> Prop, ~ ( exists n : U | ~ P n) -> forall n:U, P n.
+ forall P:U -> Prop, ~ (exists n : U, ~ P n) -> forall n:U, P n.
Proof.
intros P H n.
apply NNPP.
@@ -54,14 +54,14 @@ red in |- *; intro K; apply H; exists n; trivial.
Qed.
Lemma ex_not_not_all :
- forall P:U -> Prop, ( exists n : U | ~ P n) -> ~ (forall n:U, P n).
+ forall P:U -> Prop, (exists n : U, ~ P n) -> ~ (forall n:U, P n).
Proof.
unfold not in |- *; intros P exnot allP.
elim exnot; auto.
Qed.
Lemma all_not_not_ex :
- forall P:U -> Prop, (forall n:U, ~ P n) -> ~ ( exists n : U | P n).
+ forall P:U -> Prop, (forall n:U, ~ P n) -> ~ (exists n : U, P n).
Proof.
unfold not in |- *; intros P allnot exP; elim exP; intros n p.
apply allnot with n; auto.
diff --git a/theories/Logic/Diaconescu.v b/theories/Logic/Diaconescu.v
index b03ec80e8c..e1fb12f398 100644
--- a/theories/Logic/Diaconescu.v
+++ b/theories/Logic/Diaconescu.v
@@ -63,11 +63,11 @@ Variable rel_choice : RelationalChoice.
Lemma guarded_rel_choice :
forall (A B:Type) (P:A -> Prop) (R:A -> B -> Prop),
- (forall x:A, P x -> exists y : B | R x y) ->
- exists R' : A -> B -> Prop
- | (forall x:A,
+ (forall x:A, P x -> exists y : B, R x y) ->
+ exists R' : A -> B -> Prop,
+ (forall x:A,
P x ->
- exists y : B | R x y /\ R' x y /\ (forall y':B, R' x y' -> y = y')).
+ exists y : B, R x y /\ R' x y /\ (forall y':B, R' x y' -> y = y')).
Proof.
exact
(rel_choice_and_proof_irrel_imp_guarded_rel_choice rel_choice proof_irrel).
@@ -79,13 +79,13 @@ Qed.
Require Import Bool.
Lemma AC :
- exists R : (bool -> Prop) -> bool -> Prop
- | (forall P:bool -> Prop,
- ( exists b : bool | P b) ->
- exists b : bool | P b /\ R P b /\ (forall b':bool, R P b' -> b = b')).
+ exists R : (bool -> Prop) -> bool -> Prop,
+ (forall P:bool -> Prop,
+ (exists b : bool, P b) ->
+ exists b : bool, P b /\ R P b /\ (forall b':bool, R P b' -> b = b')).
Proof.
apply guarded_rel_choice with
- (P := fun Q:bool -> Prop => exists y : _ | Q y)
+ (P := fun Q:bool -> Prop => exists y : _, Q y)
(R := fun (Q:bool -> Prop) (y:bool) => Q y).
exact (fun _ H => H).
Qed.
@@ -135,4 +135,4 @@ left; assumption.
Qed.
-End PredExt_GuardRelChoice_imp_EM. \ No newline at end of file
+End PredExt_GuardRelChoice_imp_EM.
diff --git a/theories/Logic/RelationalChoice.v b/theories/Logic/RelationalChoice.v
index c55095e473..12c3f746a0 100644
--- a/theories/Logic/RelationalChoice.v
+++ b/theories/Logic/RelationalChoice.v
@@ -13,8 +13,8 @@
Axiom
relational_choice :
forall (A B:Type) (R:A -> B -> Prop),
- (forall x:A, exists y : B | R x y) ->
- exists R' : A -> B -> Prop
- | (forall x:A,
- exists y : B
- | R x y /\ R' x y /\ (forall y':B, R' x y' -> y = y')). \ No newline at end of file
+ (forall x:A, exists y : B, R x y) ->
+ exists R' : A -> B -> Prop,
+ (forall x:A,
+ exists y : B,
+ R x y /\ R' x y /\ (forall y':B, R' x y' -> y = y')).
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-17 18:56:50 +0000