From 58c80e82b2e0aea89e18e588028fb0f53479c219 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Fri, 29 Sep 2006 12:47:31 +0000 Subject: [PATCH] restored the good factorization file --- .../matita/library/nat/factorization.ma | 128 ------------------ 1 file changed, 128 deletions(-) diff --git a/helm/software/matita/library/nat/factorization.ma b/helm/software/matita/library/nat/factorization.ma index 6241244f3..4c8de0f51 100644 --- a/helm/software/matita/library/nat/factorization.ma +++ b/helm/software/matita/library/nat/factorization.ma @@ -18,133 +18,6 @@ include "nat/ord.ma". include "nat/gcd.ma". include "nat/nth_prime.ma". - -theorem prova : - \forall n,m:nat. - \forall P:nat \to Prop. - \forall H:P (S (S O)). - \forall H:P (S (S (S O))). - \forall H1: \forall x.P x \to O = x. - O = S (S (S (S (S O)))). - intros. - auto paramodulation. - qed. - -theorem example2: -\forall x: nat. (x+S O)*(x-S O) = x*x - S O. -intro; -apply (nat_case x); - [ auto paramodulation.|intro.auto paramodulation.] -qed. - -theorem prova3: - \forall A:Set. - \forall m:A \to A \to A. - \forall divides: A \to A \to Prop. - \forall o,a,b,two:A. - \forall H1:\forall x.m o x = x. - \forall H1:\forall x.m x o = x. - \forall H1:\forall x,y,z.m x (m y z) = m (m x y) z. - \forall H1:\forall x.m x o = x. - \forall H2:\forall x,y.m x y = m y x. - \forall H3:\forall x,y,z. m x y = m x z \to y = z. - (* \forall H4:\forall x,y.(\exists z.m x z = y) \to divides x y. *) - \forall H4:\forall x,y.(divides x y \to (\exists z.m x z = y)). - \forall H4:\forall x,y,z.m x z = y \to divides x y. - \forall H4:\forall x,y.divides two (m x y) \to divides two x ∨ divides two y. - \forall H5:m a a = m two (m b b). - \forall H6:\forall x.divides x a \to divides x b \to x = o. - two = o. - intros. - cut (divides two a); - [2:elim (H8 a a);[assumption.|assumption|rewrite > H9.auto.] - |elim (H6 ? ? Hcut). - cut (divides two b); - [ apply (H10 ? Hcut Hcut1). - | elim (H8 b b);[assumption.|assumption| - apply (H7 ? ? (m a1 a1)); - apply (H5 two ? ?);rewrite < H9. - rewrite < H11.rewrite < H2. - apply eq_f.rewrite > H2.rewrite > H4.reflexivity. - ] - ] - ] - qed. - -theorem prova31: - \forall A:Set. - \forall m,f:A \to A \to A. - \forall divides: A \to A \to Prop. - \forall o,a,b,two:A. - \forall H1:\forall x.m o x = x. - \forall H1:\forall x.m x o = x. - \forall H1:\forall x,y,z.m x (m y z) = m (m x y) z. - \forall H1:\forall x.m x o = x. - \forall H2:\forall x,y.m x y = m y x. - \forall H3:\forall x,y,z. m x y = m x z \to y = z. - (* \forall H4:\forall x,y.(\exists z.m x z = y) \to divides x y. *) - \forall H4:\forall x,y.(divides x y \to m x (f x y) = y). - \forall H4:\forall x,y,z.m x z = y \to divides x y. - \forall H4:\forall x,y.divides two (m x y) \to divides two x ∨ divides two y. - \forall H5:m a a = m two (m b b). - \forall H6:\forall x.divides x a \to divides x b \to x = o. - two = o. - intros. - cut (divides two a); - [2:elim (H8 a a);[assumption.|assumption|rewrite > H9.auto.] - |(*elim (H6 ? ? Hcut). *) - cut (divides two b); - [ apply (H10 ? Hcut Hcut1). - | elim (H8 b b);[assumption.|assumption| - - apply (H7 ? ? (m (f two a) (f two a))); - apply (H5 two ? ?); - rewrite < H9. - rewrite < (H6 two a Hcut) in \vdash (? ? ? %). - rewrite < H2.apply eq_f. - rewrite < H4 in \vdash (? ? ? %). - rewrite > H2.reflexivity. - ] - ] - ] - qed. - -theorem prova32: - \forall A:Set. - \forall m,f:A \to A \to A. - \forall divides: A \to A \to Prop. - \forall o,a,b,two:A. - \forall H1:\forall x.m o x = x. - \forall H1:\forall x.m x o = x. - \forall H1:\forall x,y,z.m x (m y z) = m (m x y) z. - \forall H1:\forall x.m x o = x. - \forall H2:\forall x,y.m x y = m y x. - \forall H3:\forall x,y,z. m x y = m x z \to y = z. - (* \forall H4:\forall x,y.(\exists z.m x z = y) \to divides x y. *) - \forall H4:\forall x,y.(divides x y \to m x (f x y) = y). - \forall H4:\forall x,y,z.m x z = y \to divides x y. - \forall H4:\forall x.divides two (m x x) \to divides two x. - \forall H5:m a a = m two (m b b). - \forall H6:\forall x.divides x a \to divides x b \to x = o. - two = o. - intros. - cut (divides two a);[|apply H8;rewrite > H9.auto]. - apply H10; - [ assumption. - | apply (H8 b); - apply (H7 ? ? (m (f two a) (f two a))); - apply (H5 two ? ?); - auto paramodulation. - (* - rewrite < H9. - rewrite < (H6 two a Hcut) in \vdash (? ? ? %). - rewrite < H2.apply eq_f. - rewrite < H4 in \vdash (? ? ? %). - rewrite > H2.reflexivity. - *) - ] -qed. - (* the following factorization algorithm looks for the largest prime factor. *) definition max_prime_factor \def \lambda n:nat. @@ -769,4 +642,3 @@ intros. apply injective_defactorize. apply defactorize_factorize. qed. - -- 2.39.2