From 27bd932eeab546b36d2750bd6f4d047ebf2964f6 Mon Sep 17 00:00:00 2001 From: Andrea Asperti Date: Fri, 23 Sep 2005 10:16:28 +0000 Subject: [PATCH] log.ma renamed into ord.ma --- helm/matita/library/nat/{log.ma => ord.ma} | 48 +++++++++++----------- 1 file changed, 24 insertions(+), 24 deletions(-) rename helm/matita/library/nat/{log.ma => ord.ma} (80%) diff --git a/helm/matita/library/nat/log.ma b/helm/matita/library/nat/ord.ma similarity index 80% rename from helm/matita/library/nat/log.ma rename to helm/matita/library/nat/ord.ma index 83c98b683..7b246be0e 100644 --- a/helm/matita/library/nat/log.ma +++ b/helm/matita/library/nat/ord.ma @@ -21,21 +21,21 @@ include "nat/primes.ma". (* this definition of log is based on pairs, with a remainder *) -let rec plog_aux p n m \def +let rec p_ord_aux p n m \def match (mod n m) with [ O \Rightarrow match p with [ O \Rightarrow pair nat nat O n | (S p) \Rightarrow - match (plog_aux p (div n m) m) with + match (p_ord_aux p (div n m) m) with [ (pair q r) \Rightarrow pair nat nat (S q) r]] | (S a) \Rightarrow pair nat nat O n]. -(* plog n m = if m divides n q times, with remainder r *) -definition plog \def \lambda n,m:nat.plog_aux n n m. +(* p_ord n m = if m divides n q times, with remainder r *) +definition p_ord \def \lambda n,m:nat.p_ord_aux n n m. -theorem plog_aux_to_Prop: \forall p,n,m. O < m \to - match plog_aux p n m with +theorem p_ord_aux_to_Prop: \forall p,n,m. O < m \to + match p_ord_aux p n m with [ (pair q r) \Rightarrow n = m \sup q *r ]. intro. elim p. @@ -54,7 +54,7 @@ change with match ( match (mod n1 m) with [ O \Rightarrow - match (plog_aux n (div n1 m) m) with + match (p_ord_aux n (div n1 m) m) with [ (pair q r) \Rightarrow pair nat nat (S q) r] | (S a) \Rightarrow pair nat nat O n1] ) with @@ -62,12 +62,12 @@ with apply nat_case1 (mod n1 m).intro. change with match ( - match (plog_aux n (div n1 m) m) with + match (p_ord_aux n (div n1 m) m) with [ (pair q r) \Rightarrow pair nat nat (S q) r]) with [ (pair q r) \Rightarrow n1 = m \sup q * r]. generalize in match (H (div n1 m) m). -elim plog_aux n (div n1 m) m. +elim p_ord_aux n (div n1 m) m. simplify. rewrite > assoc_times. rewrite < H3.rewrite > plus_n_O (m*(div n1 m)). @@ -78,19 +78,19 @@ assumption.assumption. intros.simplify.apply plus_n_O. qed. -theorem plog_aux_to_exp: \forall p,n,m,q,r. O < m \to - (pair nat nat q r) = plog_aux p n m \to n = m \sup q * r. +theorem p_ord_aux_to_exp: \forall p,n,m,q,r. O < m \to + (pair nat nat q r) = p_ord_aux p n m \to n = m \sup q * r. intros. change with match (pair nat nat q r) with [ (pair q r) \Rightarrow n = m \sup q * r ]. rewrite > H1. -apply plog_aux_to_Prop. +apply p_ord_aux_to_Prop. assumption. qed. (* questo va spostato in primes1.ma *) -theorem plog_exp: \forall n,m,i. O < m \to mod n m \neq O \to -\forall p. i \le p \to plog_aux p (m \sup i * n) m = pair nat nat i n. +theorem p_ord_exp: \forall n,m,i. O < m \to mod n m \neq O \to +\forall p. i \le p \to p_ord_aux p (m \sup i * n) m = pair nat nat i n. intros 5. elim i. simplify. @@ -106,7 +106,7 @@ intro. change with match (mod n m) with [ O \Rightarrow - match (plog_aux m1 (div n m) m) with + match (p_ord_aux m1 (div n m) m) with [ (pair q r) \Rightarrow pair nat nat (S q) r] | (S a) \Rightarrow pair nat nat O n] = pair nat nat O n. @@ -122,14 +122,14 @@ intros. change with match (mod (m \sup (S n1) *n) m) with [ O \Rightarrow - match (plog_aux m1 (div (m \sup (S n1) *n) m) m) with + match (p_ord_aux m1 (div (m \sup (S n1) *n) m) m) with [ (pair q r) \Rightarrow pair nat nat (S q) r] | (S a) \Rightarrow pair nat nat O (m \sup (S n1) *n)] = pair nat nat (S n1) n. cut (mod (m \sup (S n1)*n) m) = O. rewrite > Hcut. change with -match (plog_aux m1 (div (m \sup (S n1)*n) m) m) with +match (p_ord_aux m1 (div (m \sup (S n1)*n) m) m) with [ (pair q r) \Rightarrow pair nat nat (S q) r] = pair nat nat (S n1) n. cut div (m \sup (S n1) *n) m = m \sup n1 *n. @@ -148,8 +148,8 @@ simplify.rewrite > assoc_times. apply witness ? ? (m \sup n1 *n).reflexivity. qed. -theorem plog_aux_to_Prop1: \forall p,n,m. (S O) < m \to O < n \to n \le p \to - match plog_aux p n m with +theorem p_ord_aux_to_Prop1: \forall p,n,m. (S O) < m \to O < n \to n \le p \to + match p_ord_aux p n m with [ (pair q r) \Rightarrow mod r m \neq O]. intro.elim p.absurd O < n.assumption. apply le_to_not_lt.assumption. @@ -157,14 +157,14 @@ change with match (match (mod n1 m) with [ O \Rightarrow - match (plog_aux n(div n1 m) m) with + match (p_ord_aux n(div n1 m) m) with [ (pair q r) \Rightarrow pair nat nat (S q) r] | (S a) \Rightarrow pair nat nat O n1]) with [ (pair q r) \Rightarrow mod r m \neq O]. apply nat_case1 (mod n1 m).intro. generalize in match (H (div n1 m) m). -elim (plog_aux n (div n1 m) m). +elim (p_ord_aux n (div n1 m) m). apply H5.assumption. apply eq_mod_O_to_lt_O_div. apply trans_lt ? (S O).simplify.apply le_n. @@ -182,14 +182,14 @@ apply not_eq_O_S m1. rewrite > H5.reflexivity. qed. -theorem plog_aux_to_not_mod_O: \forall p,n,m,q,r. (S O) < m \to O < n \to n \le p \to - pair nat nat q r = plog_aux p n m \to mod r m \neq O. +theorem p_ord_aux_to_not_mod_O: \forall p,n,m,q,r. (S O) < m \to O < n \to n \le p \to + pair nat nat q r = p_ord_aux p n m \to mod r m \neq O. intros. change with match (pair nat nat q r) with [ (pair q r) \Rightarrow mod r m \neq O]. rewrite > H3. -apply plog_aux_to_Prop1. +apply p_ord_aux_to_Prop1. assumption.assumption.assumption. qed. -- 2.39.2