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!
(* we have still to attach exists *)
definition surjective: \forall A,B:Type.\forall f:A \to B.Prop
\def \lambda A,B.\lambda f.
(* 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.
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.
inductive ex (A:Type) (P:A \to Prop) : Prop \def
ex_intro: \forall x:A. P x \to ex A P.
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.
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.
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.
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.
elim Hcut.
apply ex_intro nat ? a.
split.
qed.
theorem eq_minus_gcd_aux: \forall p,m,n.O < n \to n \le m \to n \le p \to
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
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.
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
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.
elim Hcut1.
rewrite > divides_to_divides_b_true.
simplify.
assumption.assumption.
rewrite > not_divides_to_divides_b_false.
change with
assumption.assumption.
rewrite > not_divides_to_divides_b_false.
change with
-ex nat (\lambda a. ex nat (\lambda b.
a*n1 - b*m = gcd_aux n n1 (mod m n1)
\lor
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).
-ex nat (\lambda a. ex nat (\lambda b.
a*(mod m n1) - b*n1= gcd_aux n n1 (mod m n1)
\lor
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.
elim Hcut2.elim H5.elim H6.
(* first case *)
rewrite < H7.
apply lt_to_le_to_lt ? n1.assumption.assumption.
qed.
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).
-ex nat (\lambda a. ex nat (\lambda b.
a*n - b*m =
match leb n m with
[ true \Rightarrow
a*n - b*m =
match leb n m with
[ true \Rightarrow
| false \Rightarrow
match m with
[ O \Rightarrow n
| 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.
apply leb_elim n m.
apply nat_case1 n.
simplify.intros.
apply sym_eq.apply minus_n_O.
intros.
change with
apply sym_eq.apply minus_n_O.
intros.
change with
-ex nat (\lambda a. ex nat (\lambda b.
a*(S m1) - b*m = (gcd_aux (S m1) m (S m1))
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.
apply eq_minus_gcd_aux.
simplify. apply le_S_S.apply le_O_n.
assumption.apply le_n.
apply sym_eq.apply minus_n_O.
intros.
change with
apply sym_eq.apply minus_n_O.
intros.
change with
-ex nat (\lambda a. ex nat (\lambda b.
a*n - b*(S m1) = (gcd_aux (S m1) n (S m1))
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)).
-ex nat (\lambda a. ex nat (\lambda b.
a*(S m1) - b*n = (gcd_aux (S m1) n (S m1))
\lor
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.
elim Hcut.elim H2.elim H3.
apply ex_intro ? ? a1.
apply ex_intro ? ? a.
cut divides n p \lor \not (divides n p).
elim Hcut.left.assumption.
right.
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
elim Hcut1.elim H3.*)
theorem divides_times_to_divides: \forall n,p,q:nat.prime n \to divides n (p*q) \to
elim Hcut.
left.assumption.
right.
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.
elim Hcut1.elim H3.elim H4.
(* first case *)
rewrite > times_n_SO q.rewrite < H5.
rewrite > H2.simplify.apply le_n.
qed.
rewrite > H2.simplify.apply le_n.
qed.
definition max_spec \def \lambda f:nat \to bool.\lambda n: nat.
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.
(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.
intros 2.
elim n.elim H.elim H1.generalize in match H3.
apply le_n_O_elim a H2.intro.simplify.rewrite > H4.
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.
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.
elim max_S_max f n1.
elim H3.
absurd m \le S n1.assumption.
qed.
theorem f_min_aux_true: \forall f:nat \to bool. \forall off,m:nat.
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.
f (min_aux off m f) = true.
intros 2.
elim off.elim H.elim H1.elim H2.
simplify.apply le_S_S.apply le_O_n.
qed.
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)).
intros.
elim H.
apply ex_intro nat ? (S(S O)).
theorem ex_m_le_n_nth_prime_m:
\forall n: nat. nth_prime O \le n \to
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.
intros.
apply increasing_to_le2.
exact lt_nth_prime_n_nth_prime_Sn.assumption.
(* nth_prime enumerates all primes *)
theorem prime_to_nth_prime : \forall p:nat. prime p \to
(* 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.
-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.
elim Hcut.elim H1.
cut nth_prime a < p \lor nth_prime a = p.
elim Hcut1.
qed.
theorem increasing_to_le: \forall f:nat \to nat. (increasing f)
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.
intros.elim m.
apply ex_intro ? ? O.apply le_O_n.
elim H1.
theorem increasing_to_le2: \forall f:nat \to nat. (increasing f)
\to \forall m:nat. (f O) \le m \to
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.
intros.elim H1.
apply ex_intro ? ? O.
split.apply le_n.apply H.