source: Deliverables/D4.1/Matita/Exponential.ma @ 289

Last change on this file since 289 was 268, checked in by sacerdot, 9 years ago
  • notation moved to proper places
  • new function split on Vectors
File size: 2.0 KB
Line 
1(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
2(* Exponential.ma: Exponential (raising to a power) over the natural numbers. *)
3(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
4
5include "Nat.ma".
6
7include "Plogic/equality.ma".
8include "Connectives.ma".
9
10(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
11(* Exponential.                                                               *)
12(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
13
14nlet rec exponential (m: Nat) (n: Nat) on n ≝
15  match n with
16    [ Z ⇒ S (Z)
17    | S o ⇒ m * (exponential m o)
18    ].
19   
20(* DPM Bug: Matita's standard notation gets in the way here.  Cannot use
21            'exponential instead of 'exp.                                     *)
22interpretation "Nat exponential" 'exp n m = (exponential n m).
23
24(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
25(* Lemmas.                                                                    *)
26(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
27
28nlemma exponential_zero_succ_zero:
29  ∀n: Nat.
30    ¬(n = Z) → n^Z = (S Z).
31  #n.
32  nelim n.
33  //.
34  #N H.
35  //.
36nqed.
37
38nlemma exponential_succ_zero_neutral:
39  ∀n: Nat.
40    n^(S Z) = n.
41  #n.
42  nelim n.
43  //.
44  #N H.
45  nnormalize.
46  nrewrite > (multiplication_succ_zero_right_neutral ?).
47  @.
48nqed.
49
50nlemma succ_zero_exponential_succ_zero:
51  ∀m: Nat.
52    (S Z)^m = S Z.
53  #m.
54  nelim m.
55  //.
56  #N H.
57  nnormalize.
58  nrewrite > H.
59  nrewrite > (plus_zero ?).
60  @.
61nqed.
62
63naxiom exponential_addition_exponential_multiplication:
64  ∀m, n, o: Nat.
65    (m^n) * (m^o) = m^(n + o).
66
67(*
68nlemma exponential_exponential_multiplication:
69  ∀m, n, o: Nat.
70    (m^n)^o = m^(n × o).
71  #m n o.
72  nelim n.
73  nnormalize.
74  //.
75  #N H.
76  nnormalize.
77  nrewrite > H.
78  nrewrite < (exponential_addition_exponential_multiplication m o (N × o)).
79  nrewrite < H.
80*)
Note: See TracBrowser for help on using the repository browser.