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

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