1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
|
; cert_param: (uses-acl2r)
(in-package "ACL2")
(include-book "vectors")
;; this is actually norm squared
(define norm^2 ((vec real-listp))
:returns (ret realp)
(cond ((null vec) 0)
((not (real-listp vec)) 0)
(t (+ (* (car vec) (car vec))
(norm^2 (cdr vec)))))
///
(more-returns
(ret realp :name norm-is-real) ;; keeping this name temporarily b/c its used
(ret (implies (real-listp vec) (<= 0 ret))
:hints (("GOAL" :in-theory (enable norm^2)))
:name norm-positive-definite-1)
(ret (implies (real-listp vec)
(<= (norm^2 (cdr vec)) ret))
; Commented out by Matt K.; see GitHub Issue #1320
; :hints (("GOAL" :expand (ret)))
:rule-classes ((:linear))
:name norm-monotonicity-1)))
;; the definite part of "norm is positive-definite"
(encapsulate
nil
(local
(defthm lemma-1
(implies (and (real-listp vec) (zvecp vec))
(= (norm^2 vec) 0))
:hints (("GOAL" :in-theory (enable zvecp norm^2)))))
(local
(defthm lemma-2
(implies (and (real-listp vec)
(not (equal (norm^2 (cdr vec)) 0)))
(not (equal (norm^2 vec) 0)))
:hints (("GOAL" :expand ((norm^2 vec))
:use ((:instance norm-positive-definite-1
(vec (cdr vec))))))))
(local
(defthm lemma-3
(implies (and (real-listp vec)
(realp (car vec))
(zvecp (cdr vec))
(equal (norm^2 vec) 0))
(equal (car vec) 0))
:hints (("GOAL" :expand ((norm^2 vec))))))
(defthm zvecp-monotonicity-2-2
(implies (and (zvecp (cdr vec)) (consp vec))
(equal (zvecp vec) (= (car vec) 0)))
:hints (("GOAL" :in-theory (enable zvecp))))
;; norm-positive-definite-2
(defthm zvecp-iff-zp-vec
(implies (real-listp vec)
(equal (= (norm^2 vec) 0) (zvecp vec))))
)
;; the norm of -x is the same as x
(defthm norms-under-negative-vec
(implies (real-listp vec)
(equal (norm^2 (scalar-* -1 vec)) (norm^2 vec)))
:hints (("GOAL" :in-theory (enable scalar-* norm^2))))
;; norms are commutative wrt to differences
(defthm norm-vec--x-commutative
(implies (and (real-listp vec1)
(real-listp vec2)
(= (len vec1) (len vec2)))
(= (norm^2 (vec--x vec1 vec2)) (norm^2 (vec--x vec2 vec1))))
:hints (("GOAL" :in-theory (enable norm^2 vec--x)
:induct (and (nth i vec1) (nth i vec2)))))
(defthm norm-vec---commutative
(implies (and (real-listp vec1)
(real-listp vec2)
(= (len vec1) (len vec2)))
(= (norm^2 (vec-- vec1 vec2)) (norm^2 (vec-- vec2 vec1))))
:hints (("GOAL" :in-theory (enable vec---equivalence))))
(defthm norm-scalar-*
(implies (and (realp a) (real-listp vec))
(equal (norm^2 (scalar-* a vec))
(* (* a a) (norm^2 vec))))
:hints (("GOAL" :in-theory (enable scalar-* norm^2))))
(defthm norm-inner-product-equivalence
(equal (norm^2 vec) (dot vec vec))
:hints (("GOAL" :in-theory (enable norm^2 dot)))
:rule-classes nil)
(include-book "nonstd/nsa/sqrt" :dir :system)
(defun eu-norm (vec)
(acl2-sqrt (norm^2 vec)))
(defthm eu-norm->=-0
(<= 0 (eu-norm vec)))
;; definite part of "norm is positive definite" but with a different name
(encapsulate
nil
(local (defthm lemma-1
(implies (zvecp vec)
(= (eu-norm vec) 0))
:hints (("GOAL" :use (:instance zvecp-iff-zp-vec)
:in-theory (enable zvecp)))))
(local (defthm lemma-2
(implies (and (real-listp vec) (= (eu-norm vec) 0))
(= (norm^2 vec) 0))
:hints (("GOAL" :use ((:instance norm-positive-definite-1)
(:instance sqrt->-0 (x (norm^2 vec))))))))
(defthm eu-norm-zero-iff-zvecp
(implies (real-listp vec)
(iff (= (eu-norm vec) 0)
(zvecp vec)))
:hints (("GOAL" :use ((:instance lemma-1)
(:instance zvecp-iff-zp-vec)
(:instance lemma-2)))))
)
(defthm eu-norm-scalar-*
(implies (and (real-listp vec) (realp a))
(equal (eu-norm (scalar-* a vec))
(* (abs a) (eu-norm vec))))
:hints (("GOAL" :in-theory (disable abs)
:do-not-induct t
:use ((:instance norm-scalar-*)
(:instance sqrt-* (x (* a a)) (y (norm^2 vec)))))))
(defthm eu-norm-*-eu-norm
(implies (real-listp vec)
(equal (* (eu-norm vec) (eu-norm vec))
(norm^2 vec))))
(defthm abs-eu-norm
(implies (real-listp vec)
(equal (abs (eu-norm vec)) (eu-norm vec))))
(defthm dot-eu-norm
(implies (real-listp vec)
(equal (dot vec vec) (* (eu-norm vec) (eu-norm vec))))
:hints (("GOAL" :use ((:instance norm-inner-product-equivalence)
(:instance eu-norm-*-eu-norm)))))
(defthm eu-norm-negative-vec
(implies (real-listp vec)
(equal (eu-norm (scalar-* -1 vec)) (eu-norm vec))))
(in-theory (disable dot-eu-norm))
|
