(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *) (* Exponential.ma: Exponential (raising to a power) over the natural numbers. *) (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *) include "Nat.ma". include "Plogic/equality.ma". include "Connectives.ma". (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *) (* Exponential. *) (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *) nlet rec exponential (m: Nat) (n: Nat) on n ≝ match n with [ Z ⇒ S (Z) | S o ⇒ m * (exponential m o) ]. (* DPM Bug: Matita's standard notation gets in the way here. Cannot use 'exponential instead of 'exp. *) interpretation "Nat exponential" 'exp n m = (exponential n m). (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *) (* Lemmas. *) (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *) nlemma exponential_zero_succ_zero: ∀n: Nat. ¬(n = Z) → n^Z = (S Z). #n. nelim n. //. #N H. //. nqed. nlemma exponential_succ_zero_neutral: ∀n: Nat. n^(S Z) = n. #n. nelim n. //. #N H. nnormalize. nrewrite > (multiplication_succ_zero_right_neutral ?). @. nqed. nlemma succ_zero_exponential_succ_zero: ∀m: Nat. (S Z)^m = S Z. #m. nelim m. //. #N H. nnormalize. nrewrite > H. nrewrite > (plus_zero ?). @. nqed. naxiom exponential_addition_exponential_multiplication: ∀m, n, o: Nat. (m^n) * (m^o) = m^(n + o). (* nlemma exponential_exponential_multiplication: ∀m, n, o: Nat. (m^n)^o = m^(n × o). #m n o. nelim n. nnormalize. //. #N H. nnormalize. nrewrite > H. nrewrite < (exponential_addition_exponential_multiplication m o (N × o)). nrewrite < H. *)