From: Claudio Sacerdoti Coen Date: Mon, 19 Sep 2005 16:02:07 +0000 (+0000) Subject: Notation for "ex" introduced. It is the same as the notation for forall, X-Git-Tag: LAST_BEFORE_NEW~91 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=7efb15b93cf42eae8b34a12a327ee7213c1dbecc;p=helm.git 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! --- 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.