From 7efb15b93cf42eae8b34a12a327ee7213c1dbecc Mon Sep 17 00:00:00 2001
From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Mon, 19 Sep 2005 16:02:07 +0000
Subject: [PATCH] Notation for "ex" introduced. It is the same as the notation
 for forall, but it uses \exists.

NOTE: there is a bug now in cic_notation. The notation for ex is parsed, but
it is not pretty-printed correctly!
---
 .../library/higher_order_defs/functions.ma    |  2 +-
 helm/matita/library/logic/connectives.ma      |  3 ++
 helm/matita/library/nat/factorization.ma      |  2 +-
 helm/matita/library/nat/gcd.ma                | 43 ++++++++-----------
 helm/matita/library/nat/minimization.ma       |  8 ++--
 helm/matita/library/nat/nth_prime.ma          | 11 +++--
 helm/matita/library/nat/orders.ma             |  4 +-
 7 files changed, 35 insertions(+), 38 deletions(-)

diff --git a/helm/matita/library/higher_order_defs/functions.ma b/helm/matita/library/higher_order_defs/functions.ma
index da90d4211..d2a577a49 100644
--- a/helm/matita/library/higher_order_defs/functions.ma
+++ b/helm/matita/library/higher_order_defs/functions.ma
@@ -23,7 +23,7 @@ definition injective: \forall A,B:Type.\forall f:A \to B.Prop
 (* we have still to attach exists *)
 definition surjective: \forall A,B:Type.\forall f:A \to B.Prop
 \def \lambda A,B.\lambda f.
-  \forall z:B.ex A (\lambda x:A.z=f x).
+  \forall z:B. \exists x:A.z=f x.
 
 definition symmetric: \forall A:Type.\forall f:A \to A\to A.Prop
 \def \lambda A.\lambda f.\forall x,y.f x y = f y x.
diff --git a/helm/matita/library/logic/connectives.ma b/helm/matita/library/logic/connectives.ma
index 057bed878..6437bd132 100644
--- a/helm/matita/library/logic/connectives.ma
+++ b/helm/matita/library/logic/connectives.ma
@@ -61,5 +61,8 @@ definition decidable : Prop \to Prop \def \lambda A:Prop. A \lor \not A.
 inductive ex (A:Type) (P:A \to Prop) : Prop \def
     ex_intro: \forall x:A. P x \to ex A P.
 
+(*CSC: the URI must disappear: there is a bug now *)
+interpretation "exists" 'exists x y = (cic:/matita/logic/connectives/ex.ind#xpointer(1/1) x y).
+
 inductive ex2 (A:Type) (P,Q:A \to Prop) : Prop \def
     ex_intro2: \forall x:A. P x \to Q x \to ex2 A P Q.
diff --git a/helm/matita/library/nat/factorization.ma b/helm/matita/library/nat/factorization.ma
index 4628eca13..c8127a1fa 100644
--- a/helm/matita/library/nat/factorization.ma
+++ b/helm/matita/library/nat/factorization.ma
@@ -29,7 +29,7 @@ divides (nth_prime (max_prime_factor n)) n.
 intros.apply divides_b_true_to_divides.
 apply lt_O_nth_prime_n.
 apply f_max_true  (\lambda p:nat.eqb (mod n (nth_prime p)) O) n.
-cut ex nat (\lambda i. nth_prime i = smallest_factor n).
+cut \exists i. nth_prime i = smallest_factor n.
 elim Hcut.
 apply ex_intro nat ? a.
 split.
diff --git a/helm/matita/library/nat/gcd.ma b/helm/matita/library/nat/gcd.ma
index 587314315..b7ef49121 100644
--- a/helm/matita/library/nat/gcd.ma
+++ b/helm/matita/library/nat/gcd.ma
@@ -243,22 +243,21 @@ rewrite < H2.assumption.
 qed.
 
 theorem eq_minus_gcd_aux: \forall p,m,n.O < n \to n \le m \to n \le p \to
-ex nat (\lambda a. ex nat (\lambda b.
-a*n - b*m = (gcd_aux p m n) \lor b*m - a*n = (gcd_aux p m n))).
+\exists a,b. a*n - b*m = gcd_aux p m n \lor b*m - a*n = gcd_aux p m n.
 intro.
 elim p.
 absurd O < n.assumption.apply le_to_not_lt.assumption.
 cut O < m.
 cut (divides n1 m) \lor \not (divides n1 m).
 change with
-ex nat (\lambda a. ex nat (\lambda b.
+\exists a,b.
 a*n1 - b*m = match divides_b n1 m with
 [ true \Rightarrow n1
 | false \Rightarrow gcd_aux n n1 (mod m n1)]
 \lor 
 b*m - a*n1 = match divides_b n1 m with
 [ true \Rightarrow n1
-| false \Rightarrow gcd_aux n n1 (mod m n1)])).
+| false \Rightarrow gcd_aux n n1 (mod m n1)].
 elim Hcut1.
 rewrite > divides_to_divides_b_true.
 simplify.
@@ -269,15 +268,15 @@ apply sym_eq.apply minus_n_O.
 assumption.assumption.
 rewrite > not_divides_to_divides_b_false.
 change with
-ex nat (\lambda a. ex nat (\lambda b.
+\exists a,b.
 a*n1 - b*m = gcd_aux n n1 (mod m n1)
 \lor 
-b*m - a*n1 = gcd_aux n n1 (mod m n1))).
+b*m - a*n1 = gcd_aux n n1 (mod m n1).
 cut 
-ex nat (\lambda a. ex nat (\lambda b.
+\exists a,b.
 a*(mod m n1) - b*n1= gcd_aux n n1 (mod m n1)
 \lor
-b*n1 - a*(mod m n1) = gcd_aux n n1 (mod m n1))).
+b*n1 - a*(mod m n1) = gcd_aux n n1 (mod m n1).
 elim Hcut2.elim H5.elim H6.
 (* first case *)
 rewrite < H7.
@@ -335,12 +334,11 @@ apply decidable_divides n1 m.assumption.
 apply lt_to_le_to_lt ? n1.assumption.assumption.
 qed.
 
-theorem eq_minus_gcd: \forall m,n.
-ex nat (\lambda a. ex nat (\lambda b.
-a*n - b*m = (gcd n m) \lor b*m - a*n = (gcd n m))).
+theorem eq_minus_gcd:
+ \forall m,n.\exists a,b.a*n - b*m = (gcd n m) \lor b*m - a*n = (gcd n m).
 intros.
 change with
-ex nat (\lambda a. ex nat (\lambda b.
+\exists a,b.
 a*n - b*m = 
 match leb n m with
   [ true \Rightarrow 
@@ -360,8 +358,7 @@ match leb n m with
   | false \Rightarrow 
     match m with 
     [ O \Rightarrow n
-    | (S p) \Rightarrow gcd_aux (S p) n (S p) ]]
-)).
+    | (S p) \Rightarrow gcd_aux (S p) n (S p) ]].
 apply leb_elim n m.
 apply nat_case1 n.
 simplify.intros.
@@ -372,9 +369,9 @@ rewrite < plus_n_O.
 apply sym_eq.apply minus_n_O.
 intros.
 change with 
-ex nat (\lambda a. ex nat (\lambda b.
+\exists a,b.
 a*(S m1) - b*m = (gcd_aux (S m1) m (S m1)) 
-\lor b*m - a*(S m1) = (gcd_aux (S m1) m (S m1)))).
+\lor b*m - a*(S m1) = (gcd_aux (S m1) m (S m1)).
 apply eq_minus_gcd_aux.
 simplify. apply le_S_S.apply le_O_n.
 assumption.apply le_n.
@@ -387,14 +384,14 @@ rewrite < plus_n_O.
 apply sym_eq.apply minus_n_O.
 intros.
 change with 
-ex nat (\lambda a. ex nat (\lambda b.
+\exists a,b.
 a*n - b*(S m1) = (gcd_aux (S m1) n (S m1)) 
-\lor b*(S m1) - a*n = (gcd_aux (S m1) n (S m1)))).
+\lor b*(S m1) - a*n = (gcd_aux (S m1) n (S m1)).
 cut 
-ex nat (\lambda a. ex nat (\lambda b.
+\exists a,b.
 a*(S m1) - b*n = (gcd_aux (S m1) n (S m1))
 \lor
-b*n - a*(S m1) = (gcd_aux (S m1) n (S m1)))).
+b*n - a*(S m1) = (gcd_aux (S m1) n (S m1)).
 elim Hcut.elim H2.elim H3.
 apply ex_intro ? ? a1.
 apply ex_intro ? ? a.
@@ -493,8 +490,7 @@ intros.
 cut divides n p \lor \not (divides n p).
 elim Hcut.left.assumption.
 right.
-cut ex nat (\lambda a. ex nat (\lambda b.
-a*n - b*p = (S O) \lor b*p - a*n = (S O))).
+cut \exists a,b. a*n - b*p = (S O) \lor b*p - a*n = (S O).
 elim Hcut1.elim H3.*)
 
 theorem divides_times_to_divides: \forall n,p,q:nat.prime n \to divides n (p*q) \to
@@ -504,8 +500,7 @@ cut divides n p \lor \not (divides n p).
 elim Hcut.
 left.assumption.
 right.
-cut ex nat (\lambda a. ex nat (\lambda b.
-a*n - b*p = (S O) \lor b*p - a*n = (S O))).
+cut \exists a,b. a*n - b*p = (S O) \lor b*p - a*n = (S O).
 elim Hcut1.elim H3.elim H4.
 (* first case *)
 rewrite > times_n_SO q.rewrite < H5.
diff --git a/helm/matita/library/nat/minimization.ma b/helm/matita/library/nat/minimization.ma
index 4dfda0ba6..72812cb65 100644
--- a/helm/matita/library/nat/minimization.ma
+++ b/helm/matita/library/nat/minimization.ma
@@ -72,12 +72,13 @@ intro.simplify.rewrite < H3.
 rewrite > H2.simplify.apply le_n.
 qed.
 
+
 definition max_spec \def \lambda f:nat \to bool.\lambda n: nat.
-ex nat (\lambda i:nat. (le i n) \land (f i = true)) \to
+\exists i. (le i n) \land (f i = true) \to
 (f n) = true \land (\forall i. i < n \to (f i = false)).
 
 theorem f_max_true : \forall f:nat \to bool. \forall n:nat.
-ex nat (\lambda i:nat. (le i n) \land (f i = true)) \to f (max n f) = true. 
+(\exists i:nat. le i n \land f i = true) \to f (max n f) = true. 
 intros 2.
 elim n.elim H.elim H1.generalize in match H3.
 apply le_n_O_elim a H2.intro.simplify.rewrite > H4.
@@ -106,7 +107,6 @@ elim n.absurd le m O.assumption.
 cut O < m.apply lt_O_n_elim m Hcut.exact not_le_Sn_O.
 rewrite < max_O_f f.assumption.
 generalize in match H1.
-(* ?? non posso generalizzare su un goal implicativo ?? *)
 elim max_S_max f n1.
 elim H3.
 absurd m \le S n1.assumption.
@@ -152,7 +152,7 @@ simplify.right.split.reflexivity.reflexivity.
 qed.
 
 theorem f_min_aux_true: \forall f:nat \to bool. \forall off,m:nat.
-ex nat (\lambda i:nat. (le (m-off) i) \land (le i m) \land (f i = true)) \to
+(\exists i. le (m-off) i \land le i m \land f i = true) \to
 f (min_aux off m f) = true. 
 intros 2.
 elim off.elim H.elim H1.elim H2.
diff --git a/helm/matita/library/nat/nth_prime.ma b/helm/matita/library/nat/nth_prime.ma
index 0b8f2bbe2..8035d49dd 100644
--- a/helm/matita/library/nat/nth_prime.ma
+++ b/helm/matita/library/nat/nth_prime.ma
@@ -51,9 +51,8 @@ apply divides_smallest_factor_n.
 simplify.apply le_S_S.apply le_O_n.
 qed.
 
-(* mi sembra che il problem sia ex *)
-theorem ex_prime: \forall n. (S O) \le n \to ex nat (\lambda m.
-n < m \land m \le (S (fact n)) \land (prime m)).
+theorem ex_prime: \forall n. (S O) \le n \to \exists m.
+n < m \land m \le (S (fact n)) \land (prime m).
 intros.
 elim H.
 apply ex_intro nat ? (S(S O)).
@@ -163,7 +162,7 @@ qed.
 
 theorem ex_m_le_n_nth_prime_m: 
 \forall n: nat. nth_prime O \le n \to 
-ex nat (\lambda m. nth_prime m \le n \land n < nth_prime (S m)).
+\exists m. nth_prime m \le n \land n < nth_prime (S m).
 intros.
 apply increasing_to_le2.
 exact lt_nth_prime_n_nth_prime_Sn.assumption.
@@ -188,9 +187,9 @@ qed.
 
 (* nth_prime enumerates all primes *)
 theorem prime_to_nth_prime : \forall p:nat. prime p \to
-ex nat (\lambda i:nat. nth_prime i = p).
+\exists i. nth_prime i = p.
 intros.
-cut ex nat (\lambda m. nth_prime m \le p \land p < nth_prime (S m)).
+cut \exists m. nth_prime m \le p \land p < nth_prime (S m).
 elim Hcut.elim H1.
 cut nth_prime a < p \lor nth_prime a = p.
 elim Hcut1.
diff --git a/helm/matita/library/nat/orders.ma b/helm/matita/library/nat/orders.ma
index 1731f2bc2..71cd59450 100644
--- a/helm/matita/library/nat/orders.ma
+++ b/helm/matita/library/nat/orders.ma
@@ -282,7 +282,7 @@ simplify in H. apply H.
 qed.
 
 theorem increasing_to_le: \forall f:nat \to nat. (increasing f) 
-\to \forall m:nat. ex nat (\lambda i. m \le (f i)).
+\to \forall m:nat. \exists i. m \le (f i).
 intros.elim m.
 apply ex_intro ? ? O.apply le_O_n.
 elim H1.
@@ -295,7 +295,7 @@ qed.
 
 theorem increasing_to_le2: \forall f:nat \to nat. (increasing f) 
 \to \forall m:nat. (f O) \le m \to 
-ex nat (\lambda i. (f i) \le m \land m <(f (S i))).
+\exists i. (f i) \le m \land m <(f (S i)).
 intros.elim H1.
 apply ex_intro ? ? O.
 split.apply le_n.apply H.
-- 
2.39.2