From 06a19bec47845ecffe3bf9d9a95d3d4dadf76861 Mon Sep 17 00:00:00 2001
From: Andrea Asperti <andrea.asperti@unibo.it>
Date: Wed, 9 May 2007 10:55:32 +0000
Subject: [PATCH] A few extensions for the moebius inversion theorem

---
 helm/software/matita/library/nat/exp.ma      |  27 ++-
 helm/software/matita/library/nat/gcd.ma      | 192 +++++++++++--------
 helm/software/matita/library/nat/le_arith.ma |  34 ++++
 helm/software/matita/library/nat/lt_arith.ma |  18 ++
 helm/software/matita/library/nat/ord.ma      |  87 +++------
 helm/software/matita/library/nat/primes.ma   |   4 +
 helm/software/matita/library/nat/times.ma    |  10 +
 7 files changed, 231 insertions(+), 141 deletions(-)

diff --git a/helm/software/matita/library/nat/exp.ma b/helm/software/matita/library/nat/exp.ma
index c69be6b5f..193478c0f 100644
--- a/helm/software/matita/library/nat/exp.ma
+++ b/helm/software/matita/library/nat/exp.ma
@@ -113,7 +113,7 @@ apply nat_elim2
     ]
   ]
 qed.
- 
+
 theorem lt_exp: \forall n,m,p:nat. S O < p \to n < m \to exp p n < exp p m.
 apply nat_elim2
   [intros.
@@ -140,6 +140,31 @@ apply nat_elim2
   ]
 qed.
 
+theorem le_exp_to_le: 
+\forall a,n,m. S O < a \to exp a n \le exp a m \to n \le m.
+intro.
+apply nat_elim2;intros
+  [apply le_O_n
+  |apply False_ind.
+   apply (le_to_not_lt ? ? H1).
+   simplify.
+   rewrite > times_n_SO.
+   apply lt_to_le_to_lt_times
+    [assumption
+    |apply lt_O_exp.apply lt_to_le.assumption
+    |apply lt_O_exp.apply lt_to_le.assumption
+    ]
+  |simplify in H2.
+   apply le_S_S.
+   apply H
+    [assumption
+    |apply (le_times_to_le a)
+      [apply lt_to_le.assumption|assumption]
+    ]
+  ]
+qed.
+
+
      
    
    
diff --git a/helm/software/matita/library/nat/gcd.ma b/helm/software/matita/library/nat/gcd.ma
index 6da8e13d0..0568536dc 100644
--- a/helm/software/matita/library/nat/gcd.ma
+++ b/helm/software/matita/library/nat/gcd.ma
@@ -227,86 +227,116 @@ qed.
 theorem eq_minus_gcd_aux: \forall p,m,n.O < n \to n \le m \to n \le p \to
 \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 (n1 \divides m \lor  n1 \ndivides m).
-simplify.
-elim Hcut1.
-rewrite > divides_to_divides_b_true.
-simplify.
-apply (ex_intro ? ? (S O)).
-apply (ex_intro ? ? O).
-left.simplify.rewrite < plus_n_O.
-apply sym_eq.apply minus_n_O.
-assumption.assumption.
-rewrite > not_divides_to_divides_b_false.
-change with
-(\exists a,b.
-a*n1 - b*m = gcd_aux n n1 (m \mod n1)
-\lor 
-b*m - a*n1 = gcd_aux n n1 (m \mod n1)).
-cut 
-(\exists a,b.
-a*(m \mod n1) - b*n1= gcd_aux n n1 (m \mod n1)
-\lor
-b*n1 - a*(m \mod n1) = gcd_aux n n1 (m \mod n1)).
-elim Hcut2.elim H5.elim H6.
-(* first case *)
-rewrite < H7.
-apply (ex_intro ? ? (a1+a*(m / n1))).
-apply (ex_intro ? ? a).
-right.
-rewrite < sym_plus.
-rewrite < (sym_times n1).
-rewrite > distr_times_plus.
-rewrite > (sym_times n1).
-rewrite > (sym_times n1).
-rewrite > (div_mod m n1) in \vdash (? ? (? % ?) ?).
-rewrite > assoc_times.
-rewrite < sym_plus.
-rewrite > distr_times_plus.
-rewrite < eq_minus_minus_minus_plus.
-rewrite < sym_plus.
-rewrite < plus_minus.
-rewrite < minus_n_n.reflexivity.
-apply le_n.
-assumption.
-(* second case *)
-rewrite < H7.
-apply (ex_intro ? ? (a1+a*(m / n1))).
-apply (ex_intro ? ? a).
-left.
-(* clear Hcut2.clear H5.clear H6.clear H. *)
-rewrite > sym_times.
-rewrite > distr_times_plus.
-rewrite > sym_times.
-rewrite > (sym_times n1).
-rewrite > (div_mod m n1) in \vdash (? ? (? ? %) ?).
-rewrite > distr_times_plus.
-rewrite > assoc_times.
-rewrite < eq_minus_minus_minus_plus.
-rewrite < sym_plus.
-rewrite < plus_minus.
-rewrite < minus_n_n.reflexivity.
-apply le_n.
-assumption.
-apply (H n1 (m \mod n1)).
-cut (O \lt m \mod n1 \lor O = m \mod n1).
-elim Hcut2.assumption. 
-absurd (n1 \divides m).apply mod_O_to_divides.
-assumption.
-symmetry.assumption.assumption.
-apply le_to_or_lt_eq.apply le_O_n.
-apply lt_to_le.
-apply lt_mod_m_m.assumption.
-apply le_S_S_to_le.
-apply (trans_le ? n1).
-change with (m \mod n1 < n1).
-apply lt_mod_m_m.
-assumption.assumption.assumption.assumption.
-apply (decidable_divides n1 m).assumption.
-apply (lt_to_le_to_lt ? n1).assumption.assumption.
+elim p
+  [absurd (O < n)
+    [assumption
+    |apply le_to_not_lt.assumption
+    ]
+  |cut (O < m)
+    [cut (n1 \divides m \lor  n1 \ndivides m)
+      [simplify.
+       elim Hcut1
+        [rewrite > divides_to_divides_b_true
+          [simplify.
+           apply (ex_intro ? ? (S O)).
+           apply (ex_intro ? ? O).
+           left.
+           simplify.
+           rewrite < plus_n_O.
+           apply sym_eq.
+           apply minus_n_O
+          |assumption
+          |assumption
+          ]
+        |rewrite > not_divides_to_divides_b_false
+          [change with
+           (\exists a,b.a*n1 - b*m = gcd_aux n n1 (m \mod n1)
+            \lor b*m - a*n1 = gcd_aux n n1 (m \mod n1)).
+           cut 
+           (\exists a,b.a*(m \mod n1) - b*n1= gcd_aux n n1 (m \mod n1)
+            \lor b*n1 - a*(m \mod n1) = gcd_aux n n1 (m \mod n1))
+            [elim Hcut2.elim H5.elim H6
+              [(* first case *)
+               rewrite < H7.
+               apply (ex_intro ? ? (a1+a*(m / n1))).
+               apply (ex_intro ? ? a).
+               right.
+               rewrite < sym_plus.
+               rewrite < (sym_times n1).
+               rewrite > distr_times_plus.
+               rewrite > (sym_times n1).
+               rewrite > (sym_times n1).
+               rewrite > (div_mod m n1) in \vdash (? ? (? % ?) ?)
+                [rewrite > assoc_times.
+                 rewrite < sym_plus.
+                 rewrite > distr_times_plus.
+                 rewrite < eq_minus_minus_minus_plus.
+                 rewrite < sym_plus.
+                 rewrite < plus_minus
+                  [rewrite < minus_n_n.reflexivity
+                  |apply le_n
+                  ]
+                |assumption
+                ]
+              |(* second case *)
+              rewrite < H7.
+               apply (ex_intro ? ? (a1+a*(m / n1))).
+               apply (ex_intro ? ? a).
+               left.
+               (* clear Hcut2.clear H5.clear H6.clear H. *)
+               rewrite > sym_times.
+               rewrite > distr_times_plus.
+               rewrite > sym_times.
+               rewrite > (sym_times n1).
+               rewrite > (div_mod m n1) in \vdash (? ? (? ? %) ?)
+                [rewrite > distr_times_plus.
+                 rewrite > assoc_times.
+                 rewrite < eq_minus_minus_minus_plus.
+                 rewrite < sym_plus.
+                 rewrite < plus_minus
+                  [rewrite < minus_n_n.reflexivity
+                  |apply le_n
+                  ]
+                |assumption
+                ]
+              ]
+            |apply (H n1 (m \mod n1))
+              [cut (O \lt m \mod n1 \lor O = m \mod n1)
+                [elim Hcut2
+                  [assumption 
+                  |absurd (n1 \divides m)
+                    [apply mod_O_to_divides
+                      [assumption
+                      |symmetry.assumption
+                      ]
+                    |assumption
+                    ]
+                  ]
+                |apply le_to_or_lt_eq.
+                 apply le_O_n
+                ]
+              |apply lt_to_le.
+               apply lt_mod_m_m.
+               assumption
+              |apply le_S_S_to_le.
+               apply (trans_le ? n1)
+                [change with (m \mod n1 < n1).
+                 apply lt_mod_m_m.
+                 assumption
+                |assumption
+                ]
+              ]
+            ]
+          |assumption
+          |assumption
+          ]
+        ]
+      |apply (decidable_divides n1 m).
+       assumption
+      ]
+    |apply (lt_to_le_to_lt ? n1);assumption
+    ]
+  ]
 qed.
 
 theorem eq_minus_gcd:
@@ -525,7 +555,7 @@ cut (O < n2)
     |apply (trans_lt ? (S O))[apply le_n|assumption]
     |assumption
     ]
-  |elim (le_to_or_lt_eq O n2 (le_O_n n2))
+  |elim (le_to_or_lt_eq O n2 (le_O_n n2));
     [assumption
     |apply False_ind.
      apply (le_to_not_lt n (S O))
diff --git a/helm/software/matita/library/nat/le_arith.ma b/helm/software/matita/library/nat/le_arith.ma
index ae386d313..90f3e182b 100644
--- a/helm/software/matita/library/nat/le_arith.ma
+++ b/helm/software/matita/library/nat/le_arith.ma
@@ -62,6 +62,16 @@ rewrite < sym_plus.
 apply le_plus_n.
 qed.
 
+theorem le_plus_to_le: 
+\forall a,n,m. a + n \le a + m \to n \le m.
+intro.
+elim a
+  [assumption
+  |apply H.
+   apply le_S_S_to_le.assumption
+  ]
+qed.
+
 (* times *)
 theorem monotonic_le_times_r: 
 \forall n:nat.monotonic nat le (\lambda m. n * m).
@@ -98,3 +108,27 @@ intros.elim H.simplify.
 elim (plus_n_O ?).apply le_n.
 simplify.rewrite < sym_plus.apply le_plus_n.
 qed.
+
+theorem le_times_to_le: 
+\forall a,n,m. S O \le a \to a * n \le a * m \to n \le m.
+intro.
+apply nat_elim2;intros
+  [apply le_O_n
+  |apply False_ind.
+   rewrite < times_n_O in H1.
+   generalize in match H1.
+   apply (lt_O_n_elim ? H).
+   intros.
+   simplify in H2.
+   apply (le_to_not_lt ? ? H2).
+   apply lt_O_S
+  |apply le_S_S.
+   apply H
+    [assumption
+    |rewrite < times_n_Sm in H2.
+     rewrite < times_n_Sm in H2.
+     apply (le_plus_to_le a).
+     assumption
+    ]
+  ]
+qed.
\ No newline at end of file
diff --git a/helm/software/matita/library/nat/lt_arith.ma b/helm/software/matita/library/nat/lt_arith.ma
index b01bd5461..f0fdbdbd6 100644
--- a/helm/software/matita/library/nat/lt_arith.ma
+++ b/helm/software/matita/library/nat/lt_arith.ma
@@ -148,6 +148,15 @@ assumption.
 exact (decidable_lt p q).
 qed.
 
+theorem lt_times_n_to_lt: 
+\forall n,p,q:nat. O < n \to p*n < q*n \to p < q.
+intro.
+apply (nat_case n)
+  [intros.apply False_ind.apply (not_le_Sn_n ? H)
+  |intros 4.apply lt_times_to_lt_l
+  ]
+qed.
+
 theorem lt_times_to_lt_r: 
 \forall n,p,q:nat. (S n)*p < (S n)*q \to lt p q.
 intros.
@@ -157,6 +166,15 @@ rewrite < (sym_times (S n)).
 assumption.
 qed.
 
+theorem lt_times_n_to_lt_r: 
+\forall n,p,q:nat. O < n \to n*p < n*q \to lt p q.
+intro.
+apply (nat_case n)
+  [intros.apply False_ind.apply (not_le_Sn_n ? H)
+  |intros 4.apply lt_times_to_lt_r
+  ]
+qed.
+
 theorem nat_compare_times_l : \forall n,p,q:nat. 
 nat_compare p q = nat_compare ((S n) * p) ((S n) * q).
 intros.apply nat_compare_elim.intro.
diff --git a/helm/software/matita/library/nat/ord.ma b/helm/software/matita/library/nat/ord.ma
index 159e8613b..c45bfe701 100644
--- a/helm/software/matita/library/nat/ord.ma
+++ b/helm/software/matita/library/nat/ord.ma
@@ -240,65 +240,6 @@ rewrite < times_n_SO.
 apply exp_n_SO.
 qed.
 
-(* spostare *)
-theorem le_plus_to_le: 
-\forall a,n,m. a + n \le a + m \to n \le m.
-intro.
-elim a
-  [assumption
-  |apply H.
-   apply le_S_S_to_le.assumption
-  ]
-qed.
-  
-theorem le_times_to_le: 
-\forall a,n,m. O < a \to a * n \le a * m \to n \le m.
-intro.
-apply nat_elim2;intros
-  [apply le_O_n
-  |apply False_ind.
-   rewrite < times_n_O in H1.
-   generalize in match H1.
-   apply (lt_O_n_elim ? H).
-   intros.
-   simplify in H2.
-   apply (le_to_not_lt ? ? H2).
-   apply lt_O_S
-  |apply le_S_S.
-   apply H
-    [assumption
-    |rewrite < times_n_Sm in H2.
-     rewrite < times_n_Sm in H2.
-     apply (le_plus_to_le a).
-     assumption
-    ]
-  ]
-qed.
-
-theorem le_exp_to_le: 
-\forall a,n,m. S O < a \to exp a n \le exp a m \to n \le m.
-intro.
-apply nat_elim2;intros
-  [apply le_O_n
-  |apply False_ind.
-   apply (le_to_not_lt ? ? H1).
-   simplify.
-   rewrite > times_n_SO.
-   apply lt_to_le_to_lt_times
-    [assumption
-    |apply lt_O_exp.apply lt_to_le.assumption
-    |apply lt_O_exp.apply lt_to_le.assumption
-    ]
-  |simplify in H2.
-   apply le_S_S.
-   apply H
-    [assumption
-    |apply (le_times_to_le a)
-      [apply lt_to_le.assumption|assumption]
-    ]
-  ]
-qed.
-
 theorem divides_to_p_ord: \forall p,a,b,c,d,n,m:nat. 
 O < n \to O < m \to prime p 
 \to divides n m \to p_ord n p = pair ? ? a b \to
@@ -439,3 +380,31 @@ elim (le_to_or_lt_eq O (ord_rem n p))
   |apply le_O_n
   ]
 qed.
+
+(* p_ord_inv is the inverse of ord *)
+definition p_ord_inv \def
+\lambda p,m,x.
+  match p_ord x p with
+  [pair q r \Rightarrow r*m+q].
+  
+theorem  eq_p_ord_inv: \forall p,m,x.
+p_ord_inv p m x = (ord_rem x p)*m+(ord x p).
+intros.unfold p_ord_inv. unfold ord_rem.
+unfold ord.
+elim (p_ord x p).
+reflexivity.
+qed.
+
+theorem div_p_ord_inv: 
+\forall p,m,x. ord x p < m \to p_ord_inv p m x / m = ord_rem x p.
+intros.rewrite > eq_p_ord_inv.
+apply div_plus_times.
+assumption.
+qed.
+
+theorem mod_p_ord_inv: 
+\forall p,m,x. ord x p < m \to p_ord_inv p m x \mod m = ord x p.
+intros.rewrite > eq_p_ord_inv.
+apply mod_plus_times.
+assumption.
+qed.
\ No newline at end of file
diff --git a/helm/software/matita/library/nat/primes.ma b/helm/software/matita/library/nat/primes.ma
index 4298eb942..d2e89b8f1 100644
--- a/helm/software/matita/library/nat/primes.ma
+++ b/helm/software/matita/library/nat/primes.ma
@@ -385,6 +385,10 @@ theorem not_prime_SO: \lnot (prime (S O)).
 unfold Not.unfold prime.intro.elim H.apply (not_le_Sn_n (S O) H1).
 qed.
 
+theorem prime_to_lt_O: \forall p. prime p \to O < p.
+intros.elim H.apply lt_to_le.assumption.
+qed.
+
 (* smallest factor *)
 definition smallest_factor : nat \to nat \def
 \lambda n:nat. 
diff --git a/helm/software/matita/library/nat/times.ma b/helm/software/matita/library/nat/times.ma
index c2f25e731..24a2846d7 100644
--- a/helm/software/matita/library/nat/times.ma
+++ b/helm/software/matita/library/nat/times.ma
@@ -43,6 +43,16 @@ reflexivity.
 apply assoc_plus.
 qed.
 
+theorem times_O_to_O: \forall n,m:nat.n*m = O \to n = O \lor m= O.
+apply nat_elim2;intros
+  [left.reflexivity
+  |right.reflexivity
+  |apply False_ind.
+   simplify in H1.
+   apply (not_eq_O_S ? (sym_eq  ? ? ? H1))
+  ]
+qed.
+
 theorem times_n_SO : \forall n:nat. n = n * S O.
 intros.
 rewrite < times_n_Sm.
-- 
2.39.2