(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *) (* Nat.ma: Natural numbers and common arithmetical functions. *) (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *) include "Cartesian.ma". include "Bool.ma". include "Connectives.ma". (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *) (* The datatype. *) (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *) ninductive Nat: Type[0] ≝ Z: Nat | S: Nat → Nat. ntheorem S_inj: ∀n,m:Nat. S n = S m → n=m. #n m H; nchange with (n = match S m with [ Z ⇒ Z | S x ⇒ x]); napply (match H return λx.λ_. n = match x with [Z ⇒ Z | S x ⇒ x] with [ refl ⇒ ? ]); nnormalize; /3/. nqed. (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *) (* Orderings. *) (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *) ninductive less_than_or_equal_p (n: Nat): Nat → Prop ≝ ltoe_refl: less_than_or_equal_p n n | ltoe_step: ∀m: Nat. less_than_or_equal_p n m → less_than_or_equal_p n (S m). nlet rec less_than_or_equal_b (m: Nat) (n: Nat) on m: Bool ≝ match m with [ Z ⇒ true | S o ⇒ match n with [ Z ⇒ false | S p ⇒ less_than_or_equal_b o p ] ]. notation "hvbox(n break ≤ m)" non associative with precedence 47 for @{ 'less_than_or_equal \$n \$m }. interpretation "Nat less than or equal prop" 'less_than_or_equal n m = (less_than_or_equal_p n m). notation "hvbox(n break ≲ m)" non associative with precedence 47 for @{ 'less_than_or_equalb \$n \$m }. interpretation "Nat less than or equal bool" 'less_than_or_equalb n m = (less_than_or_equal_b n m). ndefinition greater_than_or_equal_p: Nat → Nat → Prop ≝ λm, n: Nat. n ≤ m. ndefinition greater_than_or_equal_b: ∀m, n: Nat. Bool ≝ λm, n: Nat. less_than_or_equal_b n m. notation "hvbox(n break ≥ m)" non associative with precedence 47 for @{ 'greater_than_or_equal \$n \$m }. interpretation "Nat greater than or equal prop" 'greater_than_or_equal n m = (greater_than_or_equal_p n m). notation "hvbox(n break ≳ m)" non associative with precedence 47 for @{ 'greater_than_or_equalb \$n \$m }. interpretation "Nat greater than or equal bool" 'greater_than_or_equalb n m = (greater_than_or_equal_b n m). (* Add Boolean versions. *) ndefinition less_than_p ≝ λm: Nat. λn: Nat. less_than_or_equal_p (S m) n. notation "hvbox(n break < m)" non associative with precedence 47 for @{ 'less_than \$n \$m }. interpretation "Nat less than prop" 'less_than n m = (less_than_p n m). ndefinition greater_than_p ≝ λm, n: Nat. n < m. notation "hvbox(n break > m)" non associative with precedence 47 for @{ 'greater_than \$n \$m }. interpretation "Nat greater than prop" 'greater_than n m = (greater_than_p n m). nlet rec less_than_b (m: Nat) (n: Nat) on m ≝ match m with [ Z ⇒ match n with [ Z ⇒ false | S o ⇒ true ] | S o ⇒ match n with [ Z ⇒ false | S p ⇒ less_than_b o p ] ]. (* interpretation "Nat less than bool" 'less_than n m = (less_than_b n m). *) ndefinition greater_than_b ≝ λm, n: Nat. less_than_b n m. (* interpretation "Nat greater than bool" 'greater_than n m = (greater_than_b n m). *) (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *) (* Addition and subtraction. *) (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *) nlet rec plus (n: Nat) (o: Nat) on n ≝ match n with [ Z ⇒ o | S p ⇒ S (plus p o) ]. notation "hvbox(n break + m)" right associative with precedence 52 for @{ 'plus \$n \$m }. interpretation "Nat plus" 'plus n m = (plus n m). nlet rec minus (n: Nat) (o: Nat) on n ≝ match n with [ Z ⇒ Z | S p ⇒ match o with [ Z ⇒ S p | S q ⇒ minus p q ] ]. notation "hvbox(n break - m)" right associative with precedence 47 for @{ 'minus \$n \$m }. interpretation "Nat minus" 'minus n m = (minus n m). (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *) (* Multiplication, modulus and division. *) (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *) nlet rec multiplication (n: Nat) (o: Nat) on n ≝ match n with [ Z ⇒ Z | S p ⇒ o + (multiplication p o) ]. notation "hvbox(n break * m)" right associative with precedence 47 for @{ 'multiplication \$n \$m }. interpretation "Nat multiplication" 'times n m = (multiplication n m). nlet rec division_aux (m: Nat) (n : Nat) (p: Nat) ≝ match less_than_or_equal_b n p with [ true ⇒ Z | false ⇒ match m with [ Z ⇒ Z | (S q) ⇒ S (division_aux q (n - (S p)) p) ] ]. ndefinition division ≝ λm, n: Nat. match n with [ Z ⇒ S m | S o ⇒ division_aux m m o ]. notation "hvbox(n break ÷ m)" right associative with precedence 47 for @{ 'division \$n \$m }. interpretation "Nat division" 'division n m = (division n m). nlet rec modulus_aux (m: Nat) (n: Nat) (p: Nat) ≝ match less_than_or_equal_b n p with [ true ⇒ n | false ⇒ match m with [ Z ⇒ n | S o ⇒ modulus_aux o (n - (S p)) p ] ]. ndefinition modulus ≝ λm, n: Nat. match n with [ Z ⇒ m | S o ⇒ modulus_aux m m o ]. notation "hvbox(n break 'mod' m)" right associative with precedence 47 for @{ 'modulus \$n \$m }. interpretation "Nat modulus" 'modulus m n = (modulus m n). ndefinition divide_with_remainder ≝ λm, n: Nat. mk_Cartesian Nat Nat (m ÷ n) (modulus m n). (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *) (* Exponentials, and square roots. *) (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *) nlet rec exponential (m: Nat) (n: Nat) on n ≝ match n with [ Z ⇒ S (Z) | S o ⇒ m * exponential m o ]. notation "hvbox(n ^ m)" left associative with precedence 52 for @{ 'exponential \$n \$m }. interpretation "Nat exponential" 'exponential n m = (exponential n m). nlet rec eq_n (m: Nat) (n: Nat) on m: Bool ≝ match m with [ Z ⇒ match n with [ Z ⇒ true | _ ⇒ false ] | S o ⇒ match n with [ S p ⇒ eq_n o p | _ ⇒ false ] ]. (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *) (* Greatest common divisor and least common multiple. *) (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *) (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *) (* Axioms. *) (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *) (*naxiom plus_minus_inverse_left: ∀m, n: Nat. (m + n) - n = m. *) ntheorem less_than_or_equal_monotone: ∀m, n: Nat. m ≤ n → (S m) ≤ (S n). #m n H; nelim H; /2/. nqed. nlemma trans_le: ∀n,m,l. n ≤ m → m ≤ l → n ≤ l. #n m l H H1; nelim H1; /2/. nqed. ntheorem less_than_or_equal_injective: ∀m, n: Nat. (S m) ≤ (S n) → m ≤ n. #m n H; nchange with (match S m with [ Z ⇒ Z | S x ⇒ x] ≤ match S n with [ Z ⇒ Z | S x ⇒ x]); napply (match H return λx.λ_. m ≤ match x with [Z ⇒ Z | S x ⇒ x] with [ ltoe_refl ⇒ ? | ltoe_step y H ⇒ ? ]); nnormalize; /3/. nqed. ntheorem succ_less_than_injective: ∀m, n: Nat. less_than_p (S m) (S n) → m < n. /2/. nqed. nlemma not_less_than_S_Z: ∀m,n: Nat. S m ≤ n → ¬ (n = Z). #m n H; nelim H [ @; #K; ndestruct | #y H1 H2; @; #K; ndestruct ] nqed. ntheorem nothing_less_than_Z: ∀m: Nat. ¬(m < Z). #m; @; #H; nlapply (not_less_than_S_Z m Z H); /2/; nqed. (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *) (* Lemmas. *) (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *) nlemma less_than_or_equal_zero: ∀n: Nat. Z ≤ n. #n. nelim n. //. #N. napply ltoe_step. nqed. (* nlemma less_than_or_equal_zero_equal_zero: ∀m: Nat. m ≤ Z → m = Z. #m. nelim m. //. #N H H2. nnormalize. *) nlemma less_than_or_equal_reflexive: ∀n: Nat. n ≤ n. #n. nelim n. nnormalize. @. #N H. nnormalize. //. nqed. (* nlemma less_than_or_equal_succ: ∀m, n: Nat. S m ≤ n → m ≤ n. #m n. nelim m. #H. napplyS less_than_or_equal_zero. #N H H2. nrewrite > H. nnormalize. nlemma less_than_or_equal_transitive: ∀m, n, o: Nat. m ≤ n ∧ n ≤ o → m ≤ o. #m n o. nelim m. #H. napply less_than_or_equal_zero. #N H H2. nnormalize. *) nlemma plus_zero: ∀n: Nat. n + Z = n. #n. nelim n. nnormalize. @. #N H. nnormalize. nrewrite > H. @. nqed. nlemma plus_associative: ∀m, n, o: Nat. (m + n) + o = m + (n + o). #m n o. nelim m. nnormalize. @. #N H. nnormalize. nrewrite > H. @. nqed. nlemma succ_plus: ∀m, n: Nat. S(m + n) = m + S(n). #m n. nelim m. nnormalize. @. #N H. nnormalize. nrewrite > H. @. nqed. nlemma succ_plus_succ_zero: ∀n: Nat. S n = plus n (S Z). #n. nelim n. //. #N H. nnormalize. nrewrite < H. @. nqed. nlemma plus_symmetrical: ∀m, n: Nat. m + n = n + m. #m n. nelim m. nnormalize. nelim n. nnormalize. @. #N H. nnormalize. nrewrite < H. @. #N H. nnormalize. nrewrite > H. napply succ_plus. nqed. nlemma multiplication_zero_right_neutral: ∀m: Nat. m * Z = Z. #m. nelim m. nnormalize. @. #N H. nnormalize. nrewrite > H. @. nqed. nlemma multiplication_succ: ∀m, n: Nat. m * S(n) = m + (m * n). #m n. nelim m. nnormalize. @. #N H. nnormalize. nrewrite > H. nrewrite < (plus_associative n N ?). nrewrite > (plus_symmetrical n N). nrewrite > (plus_associative N n ?). @. nqed. nlemma multiplication_symmetrical: ∀m, n: Nat. m * n = n * m. #m n. nelim m. nnormalize. nelim n. nnormalize. @. #N H. nnormalize. nrewrite < H. @. #N H. nnormalize. nrewrite > H. nrewrite > (multiplication_succ ? ?). @. nqed. nlemma multiplication_succ_zero_left_neutral: ∀m: Nat. (S Z) * m = m. #m. nelim m. nnormalize. @. #N H. nnormalize. nrewrite > (succ_plus ? ?). nrewrite < (succ_plus_succ_zero ?). @. nqed. nlemma multiplication_succ_zero_right_neutral: ∀m: Nat. m * (S Z) = m. #m. nelim m. nnormalize. @. #N H. nnormalize. nrewrite > H. @. nqed. nlemma multiplication_distributes_right_plus: ∀m, n, o: Nat. (m + n) * o = m * o + n * o. #m n o. nelim m. nnormalize. @. #N H. nnormalize. nrewrite > H. nrewrite < (plus_associative ? ? ?). @. nqed. nlemma multiplication_distributes_left_plus: ∀m, n, o: Nat. o * (m + n) = o * m + o * n. #m n o. nelim o. //. #N H. nnormalize. nrewrite > H. nrewrite < (plus_associative ? n (N * n)). nrewrite > (plus_symmetrical (m + N * m) n). nrewrite < (plus_associative n m (N * m)). nrewrite < (plus_symmetrical n m). nrewrite > (plus_associative (n + m) (N * m) (N * n)). @. nqed. nlemma mutliplication_associative: ∀m, n, o: Nat. m * (n * o) = (m * n) * o. #m n o. nelim m. nnormalize. @. #N H. nnormalize. nrewrite > H. nrewrite > (multiplication_distributes_right_plus ? ? ?). @. nqed. nlemma minus_minus: ∀n: Nat. n - n = Z. #n. nelim n. nnormalize. @. #N H. nnormalize. nrewrite > H. @. nqed. nlemma succ_injective: ∀m, n: Nat. S m = S n → m = n. #m n H; napply (match H return λy.λ_.m = match y with [Z ⇒ Z | S z ⇒ z] with [refl ⇒ ? ]); @; nqed. ntheorem eq_f: ∀A,B:Type[0].∀f:A→B.∀a,a'. a=a' → f a = f a'. //; nqed. ntheorem plus_minus_inverse_right: ∀m, n: Nat. n ≤ m → (m - n) + n = m. #m; nelim m [ #n; nelim n; //; #H1 H2 H3; ncases (nothing_less_than_Z H1); #K; ncases (K H3) | #y H1 x H2; nnormalize; ngeneralize in match H2; ncases x; nnormalize; /2/; #w; nrewrite < succ_plus; /4/. ##] nqed. (* nlemma plus_minus_associate: ∀m, n, o: Nat. (m + n) - o = m + (n - o). #m n o. nelim m. nnormalize. @. #N H. nlemma plus_minus_inverses: ∀m, n: Nat. (m + n) - n = m. #m n. nelim m. nnormalize. napply minus_minus. #N H. *) ntheorem less_than_or_equal_b_correct: ∀m,n. less_than_or_equal_b m n = true → m ≤ n. #m; nelim m; //; #y H1 z; ncases z; nnormalize [ #H; ndestruct | /3/ ] nqed. ntheorem less_than_or_equal_b_complete: ∀m,n. less_than_or_equal_b m n = false → ¬(m ≤ n). #m; nelim m; nnormalize [ #n H; ndestruct | #y H1 z; ncases z; nnormalize [ #H; /2/ | /3/ ] nqed. ndefinition less_than_or_equal_b_elim: ∀m,n. ∀P: Bool → Type[0]. (m ≤ n → P true) → (¬(m ≤ n) → P false) → P (less_than_or_equal_b m n). #m n P H1 H2; nlapply (less_than_or_equal_b_correct m n); nlapply (less_than_or_equal_b_complete m n); ncases (less_than_or_equal_b m n); /3/. nqed. ndefinition greater_than_or_equal_b_elim: ∀m,n. ∀P: Bool → Type[0]. (m ≥ n → P true) → (¬(m ≥ n) → P false) → P (greater_than_or_equal_b m n). #m n; napply less_than_or_equal_b_elim; nqed. ntheorem less_than_b_correct: ∀m,n. less_than_b m n = true → m < n. #m; nelim m [ #n; ncases n [ #H; nnormalize in H; ndestruct | #z H; /2/ ] ##| #y H z; ncases z [ nnormalize; #K; ndestruct | #o K; napply less_than_or_equal_monotone; napply H; napply K ] nqed. ntheorem less_than_b_complete: ∀m,n. less_than_b m n = false → ¬(m < n). #m; nelim m [ #n; ncases n; //; #y H1; nnormalize in H1; ndestruct | #y H z; ncases z; //; #o H2; nlapply (H … H2); /3/. nqed. ndefinition less_than_b_elim: ∀m,n. ∀P: Bool → Type[0]. (m < n → P true) → (¬(m < n) → P false) → P (less_than_b m n). #m n; nlapply (less_than_b_correct m n); nlapply (less_than_b_complete m n); ncases (less_than_b m n); /3/. nqed. ndefinition greater_than_b_elim: ∀m,n. ∀P: Bool → Type[0]. (m > n → P true) → (¬(m > n) → P false) → P (greater_than_b m n). #m n; napply less_than_b_elim. nqed. (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *) (* Numbers. *) (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *) ndefinition one ≝ S Z. ndefinition two ≝ (S(S(Z))). ndefinition three ≝ two + one. ndefinition four ≝ two + two. ndefinition five ≝ three + two. ndefinition six ≝ three + three. ndefinition seven ≝ three + four. ndefinition eight ≝ four + four. ndefinition nine ≝ five + four. ndefinition ten ≝ five + five. ndefinition eleven ≝ six + five. ndefinition twelve ≝ six + six. ndefinition thirteen ≝ seven + six. ndefinition fourteen ≝ seven + seven. ndefinition fifteen ≝ eight + seven. ndefinition sixteen ≝ eight + eight. ndefinition seventeen ≝ nine + eight. ndefinition eighteen ≝ nine + nine. ndefinition nineteen ≝ ten + nine. ndefinition twenty_four ≝ sixteen + eight. ndefinition thirty_two ≝ sixteen + sixteen. ndefinition one_hundred ≝ ten * ten. ndefinition one_hundred_and_twenty_eight ≝ sixteen * eight. ndefinition one_hundred_and_twenty_nine ≝ one_hundred_and_twenty_eight + one. ndefinition one_hundred_and_thirty ≝ one_hundred_and_twenty_nine + one. ndefinition one_hundred_and_thirty_one ≝ one_hundred_and_thirty + one. ndefinition one_hundred_and_thirty_five ≝ one_hundred_and_twenty_eight + seven. ndefinition one_hundred_and_thirty_six ≝ one_hundred_and_thirty_five + one. ndefinition one_hundred_and_thirty_seven ≝ one_hundred_and_thirty_six + one. ndefinition one_hundred_and_thirty_eight ≝ one_hundred_and_twenty_eight + ten. ndefinition one_hundred_and_thirty_nine ≝ one_hundred_and_thirty_eight + one. ndefinition one_hundred_and_forty ≝ one_hundred_and_thirty_nine + one. ndefinition one_hundred_and_forty_one ≝ one_hundred_and_forty + one. ndefinition one_hundred_and_forty_four ≝ one_hundred_and_twenty_eight + sixteen. ndefinition one_hundred_and_fifty_two ≝ one_hundred_and_forty_four + eight. ndefinition one_hundred_and_fifty_three ≝ one_hundred_and_forty_four + nine. ndefinition one_hundred_and_sixty ≝ one_hundred_and_forty_four + sixteen. ndefinition one_hundred_and_sixty_eight ≝ one_hundred_and_sixty + eight. ndefinition one_hundred_and_seventy_six ≝ one_hundred_and_sixty + sixteen. ndefinition one_hundred_and_eighty_four ≝ one_hundred_and_seventy_six + eight. ndefinition two_hundred ≝ one_hundred + one_hundred. ndefinition two_hundred_and_two ≝ two_hundred + two. ndefinition two_hundred_and_three ≝ two_hundred_and_two + one. ndefinition two_hundred_and_four ≝ two_hundred_and_three + one. ndefinition two_hundred_and_five ≝ two_hundred_and_four + one. ndefinition two_hundred_and_eight ≝ two_hundred_and_five + three. ndefinition two_hundred_and_twenty_four ≝ two_hundred_and_eight + sixteen. ndefinition two_hundred_and_forty ≝ two_hundred_and_twenty_four + sixteen. ndefinition two_hundred_and_fifty_six ≝ one_hundred_and_twenty_eight + one_hundred_and_twenty_eight.