Just disable all unsound rules, probably we can bring some back

Author: pavpanchekha

src/core/prove-rules.rkt

@@ -172,7 +172,9 @@
     (hang-0m-tan-rev (implies (== (cos a) -1) (== (cos (/ (neg a) 2)) 0)))
     (tanh-sum (implies (== (* (tanh x) (tanh y)) -1) (FALSE)))
     (tanh-def-a (implies (== (+ (exp x) (exp (neg x))) 0) (FALSE)))
-    (acosh-def (implies (< x -1) (< x 1)) (implies (== x -1) (< x 1)) (implies (< (fabs x) 1) (< x 1)))
+    (acosh-def (implies (< x -1) (< x 1))
+               (implies (== x -1) (< x 1))
+               (implies (< (fabs x) 1) (< x 1)))
     (acosh-def-rev (implies (< x 1) (or (< x -1) (== x -1) (< (fabs x) 1))))
     (sqrt-undiv (implies (< (/ x y) 0) (or (< x 0) (< y 0))))
     (sqrt-unprod (implies (< (* x y) 0) (or (< x 0) (< y 0))))

src/core/rules.rkt

@@ -166,9 +166,9 @@
 
 ; Fractions
 (define-rules arithmetic
-  [sum-to-mult (+ a b) (* (+ 1 (/ b a)) a) #:unsound] ; unsound @ a = 0, b = 1
+  #;[sum-to-mult (+ a b) (* (+ 1 (/ b a)) a) #:unsound] ; unsound @ a = 0, b = 1
   [sum-to-mult-rev (* (+ 1 (/ b a)) a) (+ a b)]
-  [sub-to-mult (- a b) (* (- 1 (/ b a)) a) #:unsound] ; unsound @ a = 0, b = 1
+  #;[sub-to-mult (- a b) (* (- 1 (/ b a)) a) #:unsound] ; unsound @ a = 0, b = 1
   [sub-to-mult-rev (* (- 1 (/ b a)) a) (- a b)]
   [add-to-fraction (+ c (/ b a)) (/ (+ (* c a) b) a)]
   [add-to-fraction-rev (/ (+ (* c a) b) a) (+ c (/ b a))]
@@ -177,7 +177,7 @@
   [common-denominator (+ (/ a b) (/ c d)) (/ (+ (* a d) (* c b)) (* b d))])
 
 (define-rules polynomials
-  [sqr-pow (pow a b) (* (pow a (/ b 2)) (pow a (/ b 2))) #:unsound] ; unsound @ a = -1, b = 1
+  [sqr-pow (pow a b) (copysign (* (pow (fabs a) (/ b 2)) (pow (fabs a) (/ b 2))) a)]
   [flip-+ (+ a b) (sound-/ (- (* a a) (* b b)) (- a b) (+ a b))]
   [flip-- (- a b) (sound-/ (- (* a a) (* b b)) (+ a b) (- a b))])
 
@@ -254,7 +254,7 @@
 (define-rules arithmetic
   [sqrt-prod (sqrt (* x y)) (* (sqrt (fabs x)) (sqrt (fabs y)))]
   [sqrt-div (sqrt (/ x y)) (/ (sqrt (fabs x)) (sqrt (fabs y)))]
-  [add-sqr-sqrt x (* (sqrt x) (sqrt x)) #:unsound]) ; unsound @ x = -1
+  [add-sqr-sqrt x (copysign (* (sqrt (fabs x)) (sqrt (fabs x))) x)])
 
 ; Cubing
 (define-rules arithmetic
@@ -296,7 +296,7 @@
 ; Exponentials
 (define-rules exponents
   [add-log-exp x (log (exp x))]
-  [add-exp-log x (exp (log x)) #:unsound] ; unsound @ x = 0
+  #;[add-exp-log x (exp (log x)) #:unsound] ; unsound @ x = -1
   [rem-exp-log (exp (log x)) x]
   [rem-log-exp (log (exp x)) x])
 
@@ -355,13 +355,14 @@
   [pow-div (/ (pow a b) (pow a c)) (pow a (- b c))])
 
 (define-rules exponents
-  [pow-plus-rev (pow a (+ b 1)) (* (pow a b) a) #:unsound] ; unsound @ a = 0, b = -1/2
-  [pow-neg (pow a (neg b)) (/ 1 (pow a b)) #:unsound]) ; unsound @ a = 0, b = -1
+  [pow-plus-rev (pow a (+ b 1)) (* (sound-pow a b 1) a)]
+  [pow-neg (pow a (neg b)) (sound-/ 1 (sound-pow a b 0) 0)])
 
 (define-rules exponents
-  [pow-to-exp (pow a b) (exp (* (log a) b)) #:unsound] ; unsound @ a = -1, b = 1
-  [pow-add (pow a (+ b c)) (* (pow a b) (pow a c)) #:unsound] ; unsound @ a = -1, b = c = 1/2
-  [pow-sub (pow a (- b c)) (/ (pow a b) (pow a c)) #:unsound] ; unsound @ a = -1, b = c = 1/2
+  #;[pow-to-exp (pow a b) (exp (* (log a) b)) #:unsound] ; unsound @ a = -1, b = 1
+  #;[pow-add (pow a (+ b c)) (* (pow a b) (pow a c)) #:unsound] ; unsound @ a = -1, b = c = 1/2
+  #;[pow-sub (pow a (- b c)) (/ (pow a b) (pow a c)) #:unsound] ; unsound @ a = -1, b = c = 1/2
+  #;
   [unpow-prod-down (pow (* b c) a) (* (pow b a) (pow c a)) #:unsound]) ; unsound @ a = 1/2, b = c = -1
 
 ; Logarithms
@@ -373,7 +374,7 @@
 (define-rules exponents
   [log-prod (log (* a b)) (+ (log (fabs a)) (log (fabs b)))]
   [log-div (log (/ a b)) (- (log (fabs a)) (log (fabs b)))]
-  [log-pow (log (pow a b)) (* b (log (fabs a))) #:unsound]) ; unsound @ a == b == 0
+  [log-pow (log (pow a b)) (* b (sound-log (fabs a) 0))])
 
 (define-rules exponents
   [sum-log (+ (log a) (log b)) (log (* a b))]