From 2b2bc388ba8bff4fff4f3ae30814a09ee5c6d289 Mon Sep 17 00:00:00 2001 From: Andrea Asperti Date: Fri, 8 May 2009 14:40:41 +0000 Subject: [PATCH] versione automatizzata --- helm/software/matita/library/nat/minus.ma | 110 ++++++++++++++-------- 1 file changed, 71 insertions(+), 39 deletions(-) diff --git a/helm/software/matita/library/nat/minus.ma b/helm/software/matita/library/nat/minus.ma index a8e987fc4..4f789a230 100644 --- a/helm/software/matita/library/nat/minus.ma +++ b/helm/software/matita/library/nat/minus.ma @@ -23,9 +23,13 @@ let rec minus n m \def match m with [O \Rightarrow (S p) | (S q) \Rightarrow minus p q ]]. - + interpretation "natural minus" 'minus x y = (minus x y). +theorem minus_S_S: ∀n,m:nat.S n - S m = n -m. +intros;reflexivity. +qed. + theorem minus_n_O: \forall n:nat.n=n-O. intros.elim n.simplify.reflexivity. simplify.reflexivity. @@ -74,14 +78,13 @@ intros.simplify.apply H.apply le_S_S_to_le.assumption. qed. theorem minus_plus_m_m: \forall n,m:nat.n = (n+m)-m. -intros 2. -elim m in n ⊢ %. +intros 2 .elim m in n ⊢ %. rewrite < minus_n_O.apply plus_n_O. -elim n1.simplify. -apply minus_n_n. -rewrite < plus_n_Sm. +elim n1.simplify. apply minus_n_n. +autobatch by H. +(* rewrite < plus_n_Sm. change with (S n2 = (S n2 + n)-n). -apply H. +apply H. *) qed. theorem plus_minus_m_m: \forall n,m:nat. @@ -91,11 +94,19 @@ apply (nat_elim2 (\lambda n,m.m \leq n \to n = (n-m)+m)). intros.apply (le_n_O_elim n1 H). reflexivity. intros.simplify.rewrite < plus_n_O.reflexivity. -intros.simplify.rewrite < sym_plus.simplify. -apply eq_f.rewrite < sym_plus.apply H. +intros. +rewrite < sym_plus.simplify. apply eq_f. +rewrite < sym_plus.apply H. apply le_S_S_to_le.assumption. qed. +theorem le_plus_minus_m_m: \forall n,m:nat. n \le (n-m)+m. +intro.elim n; + [apply le_O_n + |cases m; simplify[autobatch|autobatch by H, le_S_S] + ] +qed. + theorem minus_to_plus :\forall n,m,p:nat.m \leq n \to n-m = p \to n = m+p. intros.apply (trans_eq ? ? ((n-m)+m)). @@ -107,19 +118,15 @@ qed. theorem plus_to_minus :\forall n,m,p:nat. n = m+p \to n-m = p. intros. -apply (inj_plus_r m). +(* autobatch by transitive_eq, eq_f2, H. *) +autobatch depth=4 by inj_plus_r, symmetric_eq, minus_to_plus, le_plus_n_r. +(* rewrite < H. rewrite < sym_plus. symmetry. apply plus_minus_m_m.rewrite > H. rewrite > sym_plus. -apply le_plus_n. -qed. - -theorem minus_S_S : \forall n,m:nat. -eq nat (minus (S n) (S m)) (minus n m). -intros. -reflexivity. +apply le_plus_n.*) qed. theorem minus_pred_pred : \forall n,m:nat. lt O n \to lt O m \to @@ -150,7 +157,8 @@ apply lt_to_le.assumption. qed. theorem minus_le_S_minus_S: \forall n,m:nat. m-n \leq S (m-(S n)). -intros.apply (nat_elim2 (\lambda n,m.m-n \leq S (m-(S n)))). +intros. +apply (nat_elim2 (\lambda n,m.m-n \leq S (m-(S n)))). intro.elim n1.simplify.apply le_n_Sn. simplify.rewrite < minus_n_O.apply le_n. intros.simplify.apply le_n_Sn. @@ -158,7 +166,9 @@ intros.simplify.apply H. qed. theorem lt_minus_S_n_to_le_minus_n : \forall n,m,p:nat. m-(S n) < p \to m-n \leq p. -intros 3.simplify.intro. +intros 3.intro. +(* autobatch *) +(* end auto($Revision$) proof: TIME=1.33 SIZE=100 DEPTH=100 *) apply (trans_le (m-n) (S (m-(S n))) p). apply minus_le_S_minus_S. assumption. @@ -188,36 +198,49 @@ qed. (* galois *) theorem monotonic_le_minus_r: \forall p,q,n:nat. q \leq p \to n-p \le n-q. -simplify.intros 2.apply (nat_elim2 -(\lambda p,q.\forall a.q \leq p \to a-p \leq a-q)). -intros.apply (le_n_O_elim n H).apply le_n. -intros.rewrite < minus_n_O. -apply le_minus_m. -intros.elim a.simplify.apply le_n. -simplify.apply H.apply le_S_S_to_le.assumption. +intros 2.apply (nat_elim2 ???? p q); intros; + [apply (le_n_O_elim n H).apply le_n. + |applyS le_minus_m. + |elim n1;intros;[apply le_n|simplify.apply H.apply le_S_S_to_le.assumption] + ] +qed. + +theorem monotonic_le_minus_l: +∀p,q,n:nat. q \leq p \to q-n \le p-n. +intros 2.apply (nat_elim2 ???? p q); intros; + [apply (le_n_O_elim n H).apply le_n. + |apply le_O_n. + |cases n1;[apply H1|simplify. apply H.apply le_S_S_to_le.assumption] + ] qed. theorem le_minus_to_plus: \forall n,m,p. (le (n-m) p) \to (le n (p+m)). -intros 2.apply (nat_elim2 (\lambda n,m.\forall p.(le (n-m) p) \to (le n (p+m)))). -intros.apply le_O_n. -simplify.intros.rewrite < plus_n_O.assumption. intros. -rewrite < plus_n_Sm. -apply le_S_S.apply H. -exact H1. +(* autobatch by transitive_le, le_plus_minus_m_m, le_plus_l, H.*) +apply transitive_le + [2:apply le_plus_minus_m_m. + |3:apply le_plus_l.apply H. + ] + skip. qed. theorem le_plus_to_minus: \forall n,m,p. (le n (p+m)) \to (le (n-m) p). +intros. +autobatch by (monotonic_le_minus_l (p+m) n m), H. +(* intros 2.apply (nat_elim2 (\lambda n,m.\forall p.(le n (p+m)) \to (le (n-m) p))). intros.simplify.apply le_O_n. intros 2.rewrite < plus_n_O.intro.simplify.assumption. intros.simplify.apply H. -apply le_S_S_to_le.rewrite > plus_n_Sm.assumption. +apply le_S_S_to_le.rewrite > plus_n_Sm.assumption. *) qed. (* the converse of le_plus_to_minus does not hold *) theorem le_plus_to_minus_r: \forall n,m,p. (le (n+m) p) \to (le n (p-m)). -intros 3.apply (nat_elim2 (\lambda m,p.(le (n+m) p) \to (le n (p-m)))). +intros. +autobatch by trans_le, le_plus_to_le, H, le_plus_minus_m_m. +(* +apply (nat_elim2 (\lambda m,p.(le (n+m) p) \to (le n (p-m)))). intro.rewrite < plus_n_O.rewrite < minus_n_O.intro.assumption. intro.intro.cut (n=O).rewrite > Hcut.apply le_O_n. apply sym_eq. apply le_n_O_to_eq. @@ -226,7 +249,7 @@ rewrite < sym_plus. apply le_plus_n.assumption. intros.simplify. apply H.apply le_S_S_to_le. -rewrite > plus_n_Sm.assumption. +rewrite > plus_n_Sm.assumption. *) qed. (* minus and lt - to be completed *) @@ -234,9 +257,10 @@ theorem lt_minus_l: \forall m,l,n:nat. l < m \to m \le n \to n - m < n - l. apply nat_elim2 [intros.apply False_ind.apply (not_le_Sn_O ? H) - |intros.rewrite < minus_n_O. - change in H1 with (n eq_minus_S_pred. + |(* + letin x ≝ (lt_pred (l-n1) (m-n1)). + clearbody x. + unfold lt in x. + autobatch depth=4 width=5 size=10 by + x, H, H1, H2, trans_le, le_n_Sn, le_n. + ]*) + rewrite > eq_minus_S_pred. rewrite > eq_minus_S_pred. apply lt_pred [unfold lt.apply le_plus_to_minus_r.applyS H1 -- 2.39.2