include "Cartesian.ma". include "Maybe.ma". include "Bool.ma". include "logic/pts.ma". include "Plogic/equality.ma". ninductive Nat: Type[0] ≝ Z: Nat | S: Nat → Nat. nlet rec plus (n: Nat) (o: Nat) on n ≝ match n with [ Z ⇒ o | S p ⇒ S (plus p o) ]. notation "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 "n break - m" right associative with precedence 47 for @{ 'minus \$n \$m }. interpretation "Nat minus" 'minus n m = (minus n m). nlet rec multiplication (n: Nat) (o: Nat) on n ≝ match n with [ Z ⇒ Z | S p ⇒ o + (multiplication p o) ]. notation "n break * m" right associative with precedence 47 for @{ 'multiplication \$n \$m }. interpretation "Nat multiplication" 'times n m = (multiplication n m). nlet rec less_than_or_equal (n: Nat) (m: Nat) ≝ match n with [ Z ⇒ True | S o ⇒ match m with [ Z ⇒ False | S p ⇒ less_than_or_equal o p ] ]. notation "n break ≤ m" non associative with precedence 47 for @{ 'less_than_or_equal \$n \$m }. interpretation "Nat less than or equal" 'less_than_or_equal n m = (less_than_or_equal n m). 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 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. napplyS 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. napplyS plus_symmetrical. 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. napplyS multiplication_succ. nqed. nlemma multiplication_succ_zero_left_neutral: ∀m: Nat. (S Z) * m = m. #m. nelim m. nnormalize. @. #N H. nnormalize. napplyS succ_plus. 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. napplyS plus_associative. nqed. nlemma multiplication_distributes_left_plus: ∀m, n, o: Nat. o * (m + n) = o * m + o * n. #m n o. napplyS multiplication_symmetrical. 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. napplyS 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. nelim m. #H. ninversion H. #H. ndestruct 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. *)