From 8811829bd47cef3933b6544a457a226b6ff73f00 Mon Sep 17 00:00:00 2001
From: JJponce0913 <u1398911@umail.utah.edu>
Date: Thu, 10 Oct 2024 08:23:19 -0600
Subject: [PATCH 1/8] update rules

---
 src/core/rules.rkt | 479 ++++++++++++++++++++++++++++++++++++++++-----
 1 file changed, 432 insertions(+), 47 deletions(-)

diff --git a/src/core/rules.rkt b/src/core/rules.rkt
index 7fbcf1e81..96964c5b4 100644
--- a/src/core/rules.rkt
+++ b/src/core/rules.rkt
@@ -149,6 +149,7 @@
     [(define-ruleset* name groups #:type ([var type] ...) [rname input output] ...)
      (register-ruleset*! 'name 'groups `((var . type) ...) '((rname input output) ...))]))
 
+
 ; Commutativity
 (define-ruleset* commutativity
                  (arithmetic simplify fp-safe sound)
@@ -172,14 +173,20 @@
                  [associate-*l* (* (* a b) c) (* a (* b c))]
                  [associate-*r/ (* a (/ b c)) (/ (* a b) c)]
                  [associate-*l/ (* (/ a b) c) (/ (* a c) b)]
-                 [associate-/r* (/ a (* b c)) (/ (/ a b) c)]
+                 [associate-/r* (/ a (* b c)) (/ (/ a b) c)] ;
                  [associate-/r/ (/ a (/ b c)) (* (/ a b) c)]
-                 [associate-/l/ (/ (/ b c) a) (/ b (* a c))]
+                 [associate-/l/ (/ (/ b c) a) (/ b (* c a))] ;
                  [associate-/l* (/ (* b c) a) (* b (/ c a))])
 
 ; Counting
 (define-ruleset* counting (arithmetic simplify sound) #:type ([x real]) [count-2 (+ x x) (* 2 x)])
 
+;$$ Good
+(define-ruleset* counting-revv
+                 (arithmetic simplify sound)
+                 #:type ([x real])
+                 [2-split 2 (+ 1 1)]
+                 [count-2-rev (* 2 x) (+ x x)])
 ; Distributivity
 (define-ruleset* distributivity
                  (arithmetic simplify sound)
@@ -197,6 +204,7 @@
 (define-ruleset* distributivity-fp-safe
                  (arithmetic simplify fp-safe sound)
                  #:type ([a real] [b real])
+                 ;$$(* (neg a) b) (* a (neg b))
                  [distribute-lft-neg-in (neg (* a b)) (* (neg a) b)]
                  [distribute-rgt-neg-in (neg (* a b)) (* a (neg b))]
                  [distribute-lft-neg-out (* (neg a) b) (neg (* a b))]
@@ -208,11 +216,19 @@
                  [distribute-neg-frac (neg (/ a b)) (/ (neg a) b)]
                  [distribute-neg-frac2 (neg (/ a b)) (/ a (neg b))])
 
+;$$ This ruleset doesn't make sense because it is passing the negative to one of multiplied numbers but only ever to the new one of the variables.
 (define-ruleset* cancel-sign-fp-safe
                  (arithmetic simplify fp-safe sound)
                  #:type ([a real] [b real] [c real])
-                 [cancel-sign-sub (- a (* (neg b) c)) (+ a (* b c))]
-                 [cancel-sign-sub-inv (- a (* b c)) (+ a (* (neg b) c))])
+                 [cancel-sign-sub (- a (* (neg b) c)) (+ a (* b c))] ;old
+                 [cancel-sub-sign (+ a (* (neg b) c)) (- a (* b c))] ;new
+                 )
+
+(define-ruleset* cancel-sign-fp-safe-revv
+                 (arithmetic simplify fp-safe sound)
+                 #:type ([a real] [b real] [c real])
+                 [cancel-sign-sub-inv (+ a (* b c)) (- a (* (neg b) c))] ;old
+                 [cancel-sub-sign-inv (- a (* b c)) (+ a (* (neg b) c))]) ;old
 
 ; Difference of squares
 (define-ruleset* difference-of-squares-canonicalize
@@ -225,6 +241,17 @@
                  [difference-of-sqr--1 (+ (* a a) -1) (* (+ a 1) (- a 1))]
                  [pow-sqr (* (pow a b) (pow a b)) (pow a (* 2 b))])
 
+;$ reduces
+(define-ruleset* difference-of-squares-canonicalize-revv
+                 (polynomials simplify sound)
+                 #:type ([a real] [b real])
+                 [difference-of-sqr-1-rev (* (+ a 1) (- a 1)) (- (* a a) 1)];$$
+                 [difference-of-sqr--1-rev (* (+ a 1) (- a 1)) (+ (* a a) -1)];$$
+
+                 [difference-of-squares-rev (* (+ a b) (- a b)) (- (* a a) (* b b))];$$
+                 [pow-sqr-rev (pow a (* 2 b)) (* (pow a b) (pow a b))]);$)
+
+
 (define-ruleset* sqr-pow-expand
                  (polynomials)
                  #:type ([a real] [b real])
@@ -256,16 +283,28 @@
 (define-ruleset* id-reduce-fp-safe
                  (arithmetic simplify fp-safe sound)
                  #:type ([a real])
-                 [+-lft-identity (+ 0 a) a]
-                 [+-rgt-identity (+ a 0) a]
-                 [--rgt-identity (- a 0) a]
+                 [+-lft-identity (+ 0 a) a] ;
+                 [+-rgt-identity (+ a 0) a] ;
+                 [--rgt-identity (- a 0) a] ;
                  [sub0-neg (- 0 a) (neg a)]
                  [remove-double-neg (neg (neg a)) a]
                  [*-lft-identity (* 1 a) a]
-                 [*-rgt-identity (* a 1) a]
-                 [/-rgt-identity (/ a 1) a]
+                 [*-rgt-identity (* a 1) a] ;
+                 [/-rgt-identity (/ a 1) a] ;
                  [mul-1-neg (* -1 a) (neg a)])
 
+;? 1.Would adding the extra arithmetic do anything? 2.Why is the 6th rule implemented but not the rest? 3.Would adding adouble negative help?
+(define-ruleset* id-reduce-fp-safe-revv
+                 (arithmetic simplify)
+                 #:type ([a real])
+                 [*-rgt-identity-rev a (* a 1)]
+                 [+-rgt-identity-rev a (+ a 0)]
+                 [+-lft-identity-rev a (+ 0 a)]
+                 [/-rgt-identity-rev a (/ a 1)]
+                 [--rgt-identity-rev a (- a 0)]
+                 ;[*-lft-identity-rev a (* 1 a)]
+                 [remove-double-neg-rev a (neg (neg a))])
+
 (define-ruleset* nan-transform-fp-safe
                  (arithmetic simplify fp-safe sound)
                  #:type ([a real] [b real])
@@ -285,8 +324,15 @@
                  #:type ([a real] [b real])
                  [clear-num (/ a b) (/ 1 (/ b a))])
 
+;$$! this one seems important
+(define-ruleset* id-transform-clear-num-revv
+                 (arithmetic)
+                 #:type ([a real] [b real])
+                 [clear-num-rev (/ 1 (/ b a)) (/ a b)])
+
+;?? Why is this rule here but not the other?
 (define-ruleset* id-transform-fp-safe
-                 (arithmetic fp-safe sound)
+                 (arithmetic fp-safe)
                  #:type ([a real])
                  [*-un-lft-identity a (* 1 a)])
 
@@ -300,12 +346,27 @@
  [flip3-+ (+ a b) (/ (+ (pow a 3) (pow b 3)) (+ (* a a) (- (* b b) (* a b))))]
  [flip3-- (- a b) (/ (- (pow a 3) (pow b 3)) (+ (* a a) (+ (* b b) (* a b))))])
 
+;$$reduction
+(define-ruleset*
+ difference-of-cubes-revv
+ (polynomials sound)
+ #:type ([a real] [b real])
+ [difference-cubes-rev (* (+ (* a a) (+ (* b b) (* a b))) (- a b)) (- (pow a 3) (pow b 3))]
+ [sum-cubes-rev (* (+ (* a a) (- (* b b) (* a b))) (+ a b)) (+ (pow a 3) (pow b 3))])
+
 ; Dealing with fractions
 (define-ruleset* fractions-distribute
                  (fractions simplify sound)
                  #:type ([a real] [b real] [c real] [d real])
                  [div-sub (/ (- a b) c) (- (/ a c) (/ b c))]
-                 [times-frac (/ (* a b) (* c d)) (* (/ a c) (/ b d))])
+                 [times-frac (/ (* a b) (* c d)) (* (/ a c) (/ b d))]
+                 [div-add (/ (+ a b) c) (+ (/ a c) (/ b c))])
+
+;$$ Odd its not a rule (a/c)+(b/c) -> (a+b)/c
+(define-ruleset* fractions-distribute-revv
+                 (fractions simplify sound)
+                 #:type ([a real] [b real] [c real] [d real])
+                 [div-add-rev (+ (/ a c) (/ b c)) (/ (+ a b) c)])
 
 (define-ruleset* fractions-transform
                  (fractions sound)
@@ -316,12 +377,20 @@
                  [frac-times (* (/ a b) (/ c d)) (/ (* a c) (* b d))]
                  [frac-2neg (/ a b) (/ (neg a) (neg b))])
 
+;$$good simplification
+(define-ruleset* fractions-transform-revv
+                 (fractions sound)
+                 #:type ([a real] [b real] [c real] [d real])
+                 [frac-2neg-rev (/ (neg a) (neg b)) (/ a b)])
+
 ; Square root
 (define-ruleset* squares-reduce
                  (arithmetic simplify sound)
                  #:type ([x real])
                  [rem-square-sqrt (* (sqrt x) (sqrt x)) x]
-                 [rem-sqrt-square (sqrt (* x x)) (fabs x)])
+                 [rem-sqrt-square (sqrt (* x x)) (fabs x)]
+                 [rem-sqrt-square-rev (fabs x) (sqrt (* x x))] ;$$ sqrt might be the useful
+                 )
 
 (define-ruleset* squares-reduce-fp-sound
                  (arithmetic simplify fp-safe sound)
@@ -329,6 +398,13 @@
                  [sqr-neg (* (neg x) (neg x)) (* x x)]
                  [sqr-abs (* (fabs x) (fabs x)) (* x x)])
 
+;?
+(define-ruleset* squares-reduce-fp-sound-rev
+                 (arithmetic simplify fp-safe sound)
+                 #:type ([x real])
+                 [sqr-abs-rev (* x x) (* (fabs x) (fabs x))]
+                 [sqr-neg-rev (* x x) (* (neg x) (neg x))])
+
 (define-ruleset* fabs-reduce
                  (arithmetic simplify fp-safe sound)
                  #:type ([x real] [a real] [b real])
@@ -339,6 +415,13 @@
                  [fabs-mul (fabs (* a b)) (* (fabs a) (fabs b))]
                  [fabs-div (fabs (/ a b)) (/ (fabs a) (fabs b))])
 
+;? Would adding fabs help?
+(define-ruleset* fabs-reduce-rev
+                 (arithmetic simplify fp-safe sound)
+                 #:type ([x real] [a real] [b real])
+                 [fabs-sqr-rev (* x x) (fabs (* x x))]
+                 [fabs-fabs-rev (fabs x) (fabs (fabs x))])
+
 (define-ruleset* fabs-expand
                  (arithmetic fp-safe sound)
                  #:type ([x real] [a real] [b real])
@@ -369,17 +452,22 @@
                  [rem-cbrt-cube (cbrt (pow x 3)) x]
                  [rem-3cbrt-lft (* (* (cbrt x) (cbrt x)) (cbrt x)) x]
                  [rem-3cbrt-rft (* (cbrt x) (* (cbrt x) (cbrt x))) x]
-                 [cube-neg (pow (neg x) 3) (neg (pow x 3))])
+                 [cube-neg (pow (neg x) 3) (neg (pow x 3))]
+                 [cube-neg-rev (neg (pow x 3)) (pow (neg x) 3)] ;$$ seems reasonable
+                 )
+
 
 (define-ruleset* cubes-distribute
                  (arithmetic simplify sound)
                  #:type ([x real] [y real])
                  [cube-prod (pow (* x y) 3) (* (pow x 3) (pow y 3))]
                  [cube-div (pow (/ x y) 3) (/ (pow x 3) (pow y 3))]
-                 [cube-mult (pow x 3) (* x (* x x))])
+                 [cube-mult (pow x 3) (* x (* x x))]
+                 [cube-prod-rev (* (pow x 3) (pow y 3)) (pow (* x y) 3)] ;$reduction
+                 [cube-div-rev (/ (pow x 3) (pow y 3)) (pow (/ x y) 3)])
 
 (define-ruleset* cubes-transform
-                 (arithmetic sound)
+                 (arithmetic )
                  #:type ([x real] [y real])
                  [cbrt-prod (cbrt (* x y)) (* (cbrt x) (cbrt y))]
                  [cbrt-div (cbrt (/ x y)) (/ (cbrt x) (cbrt y))]
@@ -388,6 +476,12 @@
                  [add-cube-cbrt x (* (* (cbrt x) (cbrt x)) (cbrt x))]
                  [add-cbrt-cube x (cbrt (* (* x x) x))])
 
+;$$good simplifications
+(define-ruleset* cubes-transform-revv
+                 (arithmetic sound)
+                 #:type ([x real] [y real])
+                 [add-cbrt-cube-rev (cbrt (* (* x x) x)) x])
+
 (define-ruleset* cubes-canonicalize
                  (arithmetic simplify sound)
                  #:type ([x real])
@@ -430,6 +524,15 @@
                  [exp-lft-sqr (exp (* a 2)) (* (exp a) (exp a))]
                  [exp-lft-cube (exp (* a 3)) (pow (exp a) 3)])
 
+;? Maybe useful
+(define-ruleset* exp-factor-revv
+                 (exponents simplify sound)
+                 #:type ([a real] [b real])
+                 [exp-cbrt-rev (cbrt (exp a)) (exp (/ a 3))]
+                 [exp-lft-cube-rev (pow (exp a) 3) (exp (* a 3))]
+                 [exp-sqrt-rev (sqrt (exp a)) (exp (/ a 2))]
+                 [exp-lft-sqr-rev (* (exp a) (exp a)) (exp (* a 2))])
+
 ; Powers
 (define-ruleset* pow-reduce (exponents simplify sound) #:type ([a real]) [unpow-1 (pow a -1) (/ 1 a)])
 
@@ -455,6 +558,11 @@
                  [unpow3 (pow a 3) (* (* a a) a)]
                  [unpow1/3 (pow a 1/3) (cbrt a)]
                  [pow-plus (* (pow a b) a) (pow a (+ b 1))])
+;?maybe good expansion
+(define-ruleset* pow-canonicalize-revv
+                 (exponents simplify sound)
+                 #:type ([a real] [b real])
+                 [pow-plus-rev (pow a (+ b 1)) (* (pow a b) a)])
 
 (define-ruleset* pow-transform-sound
                  (exponents sound)
@@ -508,6 +616,12 @@
                  [log-div (log (/ a b)) (- (log a) (log b))]
                  [log-pow (log (pow a b)) (* b (log a))])
 
+;$$ Good expansion
+(define-ruleset* log-distribute-rev
+                 (exponents)
+                 #:type ([a real] [b real])
+                 [log-pow-rev (* b (log a)) (log (pow a b))])
+
 (define-ruleset* log-factor
                  (exponents sound)
                  #:type ([a real] [b real])
@@ -522,6 +636,7 @@
                  [cos-0 (cos 0) 1]
                  [tan-0 (tan 0) 0])
 
+
 (define-ruleset* trig-reduce-fp-sound-nan
                  (trigonometry simplify fp-safe-nan sound)
                  #:type ([x real])
@@ -529,11 +644,21 @@
                  [cos-neg (cos (neg x)) (cos x)]
                  [tan-neg (tan (neg x)) (neg (tan x))])
 
+;$$? Add neg?
+(define-ruleset* trig-reduce-fp-sound-nan-revv
+                 (trigonometry simplify fp-safe-nan sound)
+                 #:type ([x real])
+                 [cos-neg-rev (cos x) (cos (neg x))]
+                 [sin-neg-rev (neg (sin x)) (sin (neg x))]
+                 [tan-neg-rev (neg (tan x)) (tan (neg x))])
+
 (define-ruleset* trig-expand-fp-safe
                  (trignometry fp-safe sound)
                  #:type ([x real])
                  [sqr-sin-b (* (sin x) (sin x)) (- 1 (* (cos x) (cos x)))]
-                 [sqr-cos-b (* (cos x) (cos x)) (- 1 (* (sin x) (sin x)))])
+                 [sqr-cos-b (* (cos x) (cos x)) (- 1 (* (sin x) (sin x)))]
+                 [sqr-cos-b-rev (- 1 (* (sin x) (sin x))) (* (cos x) (cos x))]
+                 [sqr-sin-b-rev (- 1 (* (cos x) (cos x))) (* (sin x) (sin x))]) ;$$ simplification)
 
 (define-ruleset*
  trig-inverses
@@ -546,6 +671,17 @@
  [asin-sin (asin (sin x)) (- (fabs (remainder (+ x (/ (PI) 2)) (* 2 (PI)))) (/ (PI) 2))]
  [acos-cos (acos (cos x)) (fabs (remainder x (* 2 (PI))))])
 
+
+
+;$simplification
+(define-ruleset*
+ trig-inverses-revv
+ (trigonometry sound)
+ #:type ([x real])
+ [acos-cos-rev (fabs (remainder x (* 2 (PI)))) (acos (cos x))]
+ [asin-sin-rev (- (fabs (remainder (+ x (/ (PI) 2)) (* 2 (PI)))) (/ (PI) 2)) (asin (sin x))]
+ [atan-tan-rev (remainder x (PI)) (atan (tan x))])
+
 (define-ruleset* trig-inverses-simplified
                  (trigonometry)
                  #:type ([x real])
@@ -553,7 +689,9 @@
                  [asin-sin-s (asin (sin x)) x]
                  [acos-cos-s (acos (cos x)) x])
 
-(define-ruleset* trig-reduce-sound
+
+
+(define-ruleset* trig-reduce-expressions
                  (trigonometry simplify sound)
                  #:type ([a real] [b real] [x real])
                  [cos-sin-sum (+ (* (cos a) (cos a)) (* (sin a) (sin a))) 1]
@@ -589,16 +727,42 @@
                  [hang-p-tan (/ (+ (sin a) (sin b)) (+ (cos a) (cos b))) (tan (/ (+ a b) 2))]
                  [hang-m-tan (/ (- (sin a) (sin b)) (+ (cos a) (cos b))) (tan (/ (- a b) 2))])
 
+(define-ruleset* trig-reduce-expressions-revv
+                 (trigonometry simplify sound)
+                 #:type ([a real] [b real] [x real])
+                 [1-sub-sin-rev (* (cos a) (cos a)) (- 1 (* (sin a) (sin a)))]     
+                 [hang-m0-tan-rev (tan (/ (neg a) 2)) (/ (- 1 (cos a)) (neg (sin a)))]
+                 [hang-p0-tan-rev (tan (/ a 2)) (/ (- 1 (cos a)) (sin a))]
+                 [hang-0m-tan-rev (tan (/ (neg a) 2)) (/ (neg (sin a)) (+ 1 (cos a)))]
+                 [hang-0p-tan-rev (tan (/ a 2)) (/ (sin a) (+ 1 (cos a)))])
+
+(define-ruleset* trig-reduce-expressions-rev
+                 (trigonometry simplify sound)
+                 #:type ([a real] [b real] [x real])
+                 [tan-+PI-rev (tan x) (tan (+ x (PI)))]
+                 [cos-+PI/2-rev (neg (sin x)) (cos (+ x (/ (PI) 2)))]
+                 [sin-+PI/2-rev (cos x) (sin (+ x (/ (PI) 2)))]
+                 [sin-+PI-rev (neg (sin x)) (sin (+ x (PI)))]
+                 [cos-+PI-rev (neg (cos x)) (cos (+ x (PI)))])
+
 (define-ruleset* trig-reduce
                  (trigonometry)
                  #:type ([a real] [b real] [x real])
-                 [tan-+PI/2 (tan (+ x (/ (PI) 2))) (/ -1 (tan x))])
+                 [tan-+PI/2 (tan (+ x (/ (PI) 2))) (/ -1 (tan x))]
+                 [tan-+PI/2-rev (tan (+ (neg x) (/ (PI) 2))) (/ 1 (tan x)) ])
+
+(define-ruleset* trig-reduce-rev
+                 (trigonometry)
+                 #:type ([a real] [b real] [x real])
+                 [neg-tan-+PI/2-rev (/ -1 (tan x)) (tan (+ x (/ (PI) 2)))]
+                 [tan-+PI/2-rev (/ 1 (tan x)) (tan (+ (neg x) (/ (PI) 2)))]); make version where 1/tanx -> 
 
 (define-ruleset* trig-expand-sound
                  (trigonometry sound)
                  #:type ([x real] [y real] [a real] [b real])
                  [sin-sum (sin (+ x y)) (+ (* (sin x) (cos y)) (* (cos x) (sin y)))]
                  [cos-sum (cos (+ x y)) (- (* (cos x) (cos y)) (* (sin x) (sin y)))]
+                 [cos-sum-rev (- (* (cos x) (cos y)) (* (sin x) (sin y))) (cos (+ x y))]
                  [tan-sum (tan (+ x y)) (/ (+ (tan x) (tan y)) (- 1 (* (tan x) (tan y))))]
                  [sin-diff (sin (- x y)) (- (* (sin x) (cos y)) (* (cos x) (sin y)))]
                  [cos-diff (cos (- x y)) (+ (* (cos x) (cos y)) (* (sin x) (sin y)))]
@@ -611,6 +775,15 @@
                  [2-cos (- (* (cos x) (cos x)) (* (sin x) (sin x))) (cos (* 2 x))]
                  [3-cos (- (* 4 (pow (cos x) 3)) (* 3 (cos x))) (cos (* 3 x))])
 
+;$$simplification
+(define-ruleset* trig-expand-sound-revv
+                 (trigonometry sound)
+                 #:type ([x real] [y real] [a real] [b real])
+                 [cos-diff-rev (+ (* (cos x) (cos y)) (* (sin x) (sin y))) (cos (- x y))]
+                 [sin-diff-rev (- (* (sin x) (cos y)) (* (cos x) (sin y))) (sin (- x y))]
+                 [sin-sum-rev (+ (* (sin x) (cos y)) (* (cos x) (sin y))) (sin (+ x y))]
+                 [tan-sum-rev (/ (+ (tan x) (tan y)) (- 1 (* (tan x) (tan y)))) (tan (+ x y))])
+
 (define-ruleset* trig-expand-sound2
                  (trigonometry sound)
                  #:type ([x real] [y real] [a real] [b real])
@@ -630,6 +803,21 @@
                  [tan-2 (tan (* 2 x)) (/ (* 2 (tan x)) (- 1 (* (tan x) (tan x))))]
                  [2-tan (/ (* 2 (tan x)) (- 1 (* (tan x) (tan x)))) (tan (* 2 x))])
 
+;$$simplification
+(define-ruleset* trig-expand-sound2-revv
+                 (trigonometry sound)
+                 [diff-cos-rev (* -2 (* (sin (/ (- x y) 2)) (sin (/ (+ x y) 2)))) (- (cos x) (cos y))]
+                 [diff-sin-rev (* 2 (* (sin (/ (- x y) 2)) (cos (/ (+ x y) 2)))) (- (sin x) (sin y))]
+                 [diff-atan-rev (atan2 (- x y) (+ 1 (* x y))) (- (atan x) (atan y))]
+                 [sum-sin-rev (* 2 (* (sin (/ (+ x y) 2)) (cos (/ (- x y) 2)))) (+ (sin x) (sin y))]
+                 [sum-cos-rev (* 2 (* (cos (/ (+ x y) 2)) (cos (/ (- x y) 2)))) (+ (cos x) (cos y))]
+                 [sum-atan-rev (atan2 (+ x y) (- 1 (* x y))) (+ (atan x) (atan y))]
+                 [sqr-cos-a-rev (+ 1/2 (* 1/2 (cos (* 2 x)))) (* (cos x) (cos x))]
+                 [sqr-sin-a-rev (- 1/2 (* 1/2 (cos (* 2 x)))) (* (sin x) (sin x))]
+                 [cos-mult-rev (/ (+ (cos (+ x y)) (cos (- x y))) 2) (* (cos x) (cos y))]
+                 [sin-mult-rev (/ (- (cos (- x y)) (cos (+ x y))) 2) (* (sin x) (sin y))]
+                 [sin-cos-mult-rev (/ (+ (sin (- x y)) (sin (+ x y))) 2) (* (sin x) (cos y))])
+
 (define-ruleset* trig-expand
                  (trigonometry)
                  #:type ([x real] [y real] [a real] [b real])
@@ -651,6 +839,23 @@
                  [acos-neg (acos (neg x)) (- (PI) (acos x))]
                  [atan-neg (atan (neg x)) (neg (atan x))])
 
+;$$good simplification
+(define-ruleset* atrig-expand-revv
+                 (trigonometry sound)
+                 #:type ([x real])
+                 [acos-asin-rev (- (/ (PI) 2) (asin x)) (acos x)]
+                 [asin-acos-rev (- (/ (PI) 2) (acos x)) (asin x)]
+                 ;?Does moving the negative sign around do much?
+                 [asin-neg-rev (neg (asin x)) (asin (neg x))]
+                 [atan-neg-rev (neg (atan x)) (atan (neg x))]
+                 [acos-neg-rev (- (PI) (acos x)) (acos (neg x))]
+                 [cos-atan-rev (/ 1 (sqrt (+ 1 (* x x)))) (cos (atan x))]
+                 [tan-acos-rev (/ (sqrt (- 1 (* x x))) x) (tan (acos x))]
+                 [tan-asin-rev (/ x (sqrt (- 1 (* x x)))) (tan (asin x))]
+                 [cos-asin-rev (sqrt (- 1 (* x x))) (cos (asin x))]
+                 [sin-atan-rev (/ x (sqrt (+ 1 (* x x)))) (sin (atan x))]
+                 [sin-acos-rev (sqrt (- 1 (* x x))) (sin (acos x))])
+
 ; Hyperbolic trigonometric functions
 (define-ruleset* htrig-reduce
                  (hyperbolic simplify sound)
@@ -664,12 +869,23 @@
                  [sinh-+-cosh (+ (cosh x) (sinh x)) (exp x)]
                  [sinh---cosh (- (cosh x) (sinh x)) (exp (neg x))])
 
+;$$simplification
+(define-ruleset* htrig-reduce-revv
+                 (hyperbolic simplify sound)
+                 #:type ([x real])
+                 [tanh-def-b-rev (/ (- (exp (* 2 x)) 1) (+ (exp (* 2 x)) 1)) (tanh x)]
+                 [tanh-def-c-rev (/ (- 1 (exp (* -2 x))) (+ 1 (exp (* -2 x)))) (tanh x)]
+                 [sinh-def-rev (/ (- (exp x) (exp (neg x))) 2) (sinh x)]
+                 [cosh-def-rev (/ (+ (exp x) (exp (neg x))) 2) (cosh x)]
+                 [sinh-+-cosh-rev (exp x) (+ (cosh x) (sinh x))]
+[sinh---cosh-rev (exp (neg x)) (- (cosh x) (sinh x))])
+
 (define-ruleset* htrig-expand-sound
                  (hyperbolic sound)
                  #:type ([x real] [y real])
                  [sinh-undef (- (exp x) (exp (neg x))) (* 2 (sinh x))]
                  [cosh-undef (+ (exp x) (exp (neg x))) (* 2 (cosh x))]
-                 [tanh-undef (/ (- (exp x) (exp (neg x))) (+ (exp x) (exp (neg x)))) (tanh x)]
+                 [tanh-undef (/ (- (exp x) (exp (neg x))) (+ (exp x) (exp (neg x)))) (tanh x)] ;
                  [cosh-sum (cosh (+ x y)) (+ (* (cosh x) (cosh y)) (* (sinh x) (sinh y)))]
                  [cosh-diff (cosh (- x y)) (- (* (cosh x) (cosh y)) (* (sinh x) (sinh y)))]
                  [cosh-2 (cosh (* 2 x)) (+ (* (sinh x) (sinh x)) (* (cosh x) (cosh x)))]
@@ -686,18 +902,49 @@
                  [diff-cosh (- (cosh x) (cosh y)) (* 2 (* (sinh (/ (+ x y) 2)) (sinh (/ (- x y) 2))))]
                  [tanh-sum (tanh (+ x y)) (/ (+ (tanh x) (tanh y)) (+ 1 (* (tanh x) (tanh y))))])
 
+(define-ruleset*
+ htrig-expand-sound-revv
+ (hyperbolic sound)
+ #:type ([x real] [y real])
+ [sinh-undef-rev (* 2 (sinh x)) (- (exp x) (exp (neg x)))]
+ [cosh-undef-rev (* 2 (cosh x)) (+ (exp x) (exp (neg x)))]
+ [diff-cosh-rev (* 2 (* (sinh (/ (+ x y) 2)) (sinh (/ (- x y) 2)))) (- (cosh x) (cosh y))]
+ [diff-sinh-rev (* 2 (* (cosh (/ (+ x y) 2)) (sinh (/ (- x y) 2)))) (- (sinh x) (sinh y))]
+ [cosh-diff-rev (- (* (cosh x) (cosh y)) (* (sinh x) (sinh y))) (cosh (- x y))]
+ [sinh-diff-rev (- (* (sinh x) (cosh y)) (* (cosh x) (sinh y))) (sinh (- x y))]
+ [tanh-1/2-rev (/ (sinh x) (+ (cosh x) 1)) (tanh (/ x 2))]
+ [tanh-2-rev (/ (* 2 (tanh x)) (+ 1 (* (tanh x) (tanh x)))) (tanh (* 2 x))]
+ [sinh-1/2-rev (/ (sinh x) (sqrt (* 2 (+ (cosh x) 1)))) (sinh (/ x 2))]
+ [cosh-1/2-rev (sqrt (/ (+ (cosh x) 1) 2)) (cosh (/ x 2))]
+ [sinh-2-rev (* 2 (* (sinh x) (cosh x))) (sinh (* 2 x))]
+ [cosh-2-rev (+ (* (sinh x) (sinh x)) (* (cosh x) (cosh x))) (cosh (* 2 x))]
+ [sinh-sum-rev (+ (* (sinh x) (cosh y)) (* (cosh x) (sinh y))) (sinh (+ x y))]
+ [tanh-sum-rev (/ (+ (tanh x) (tanh y)) (+ 1 (* (tanh x) (tanh y)))) (tanh (+ x y))]
+ [cosh-sum-rev (+ (* (cosh x) (cosh y)) (* (sinh x) (sinh y))) (cosh (+ x y))]
+ [sum-cosh-rev (* 2 (* (cosh (/ (+ x y) 2)) (cosh (/ (- x y) 2)))) (+ (cosh x) (cosh y))]
+ [sum-sinh-rev (* 2 (* (sinh (/ (+ x y) 2)) (cosh (/ (- x y) 2)))) (+ (sinh x) (sinh y))])
+
 (define-ruleset* htrig-expand
                  (hyperbolic)
                  #:type ([x real] [y real])
-                 [tanh-1/2* (tanh (/ x 2)) (/ (- (cosh x) 1) (sinh x))])
+                 [tanh-1/2* (tanh (/ x 2)) (/ (- (cosh x) 1) (sinh x))]
+                 [tanh-1/2*-rev (/ (- (cosh x) 1) (sinh x)) (tanh (/ x 2))]) 
 
 (define-ruleset* htrig-expand-fp-safe
                  (hyperbolic fp-safe sound)
                  #:type ([x real])
                  [sinh-neg (sinh (neg x)) (neg (sinh x))]
                  [sinh-0 (sinh 0) 0]
+                 [sinh-0-rev 0 (sinh 0)]
                  [cosh-neg (cosh (neg x)) (cosh x)]
-                 [cosh-0 (cosh 0) 1])
+                 [cosh-0 (cosh 0) 1]
+                 [cosh-0-rev 1 (cosh 0)])
+
+(define-ruleset* htrig-expand-fp-safe-revv
+                 (hyperbolic fp-safe sound)
+                 #:type ([x real])
+                 [cosh-neg-rev (cosh x) (cosh (neg x))]
+                 [sinh-neg-rev (neg (sinh x)) (sinh (neg x))])
 
 (define-ruleset* ahtrig-expand-sound
                  (hyperbolic sound)
@@ -715,40 +962,68 @@
                  [tanh-acosh (tanh (acosh x)) (/ (sqrt (- (* x x) 1)) x)]
                  [tanh-atanh (tanh (atanh x)) x])
 
+
+(define-ruleset* ahtrig-expand-sound-simplify-revv
+                 (hyperbolic sound)
+                 #:type ([x real])
+                 [asinh-def-rev (log (+ x (sqrt (+ (* x x) 1)))) (asinh x)]
+                 [atanh-def-rev (/ (log (/ (+ 1 x) (- 1 x))) 2) (atanh x)]
+                 [acosh-def-rev (log (+ x (sqrt (- (* x x) 1)))) (acosh x)]
+                 [sinh-acosh-rev (sqrt (- (* x x) 1)) (sinh (acosh x))]
+                 [tanh-asinh-rev (/ x (sqrt (+ 1 (* x x)))) (tanh (asinh x))]
+                 [cosh-asinh-rev (sqrt (+ (* x x) 1)) (cosh (asinh x))]
+                 [sinh-atanh-rev (/ x (sqrt (- 1 (* x x)))) (sinh (atanh x))]
+                 [tanh-acosh-rev (/ (sqrt (- (* x x) 1)) x) (tanh (acosh x))]
+                 [cosh-atanh-rev (/ 1 (sqrt (- 1 (* x x)))) (cosh (atanh x))])
+
 (define-ruleset* ahtrig-expand
                  (hyperbolic)
                  #:type ([x real])
                  [asinh-2 (acosh (+ (* 2 (* x x)) 1)) (* 2 (asinh x))]
                  [acosh-2 (acosh (- (* 2 (* x x)) 1)) (* 2 (acosh x))])
 
-(define-ruleset* erf-rules (special simplify) #:type ([x real]) [erf-odd (erf (neg x)) (neg (erf x))])
+;? I think this expansion could be helpful
+(define-ruleset* ahtrig-expand-rev
+                 (hyperbolic)
+                 #:type ([x real])
+                 [asinh-2-rev (* 2 (asinh x)) (acosh (+ (* 2 (* x x)) 1))]
+                 [acosh-2-rev (* 2 (acosh x)) (acosh (- (* 2 (* x x)) 1))])
 
-; Specialized numerical functions
+#|; Specialized numerical functions
 ; TODO: These are technically rules over impls
-;
-; (define-ruleset* special-numerical-reduce
-;                  (numerics simplify)
-;                  #:type ([x real] [y real] [z real])
-;                  [log1p-expm1 (log1p (expm1 x)) x]
-;                  [hypot-1-def (sqrt (+ 1 (* y y))) (hypot 1 y)]
-;                  [fmm-def (- (* x y) z) (fma x y (neg z))]
-;                  [fmm-undef (fma x y (neg z)) (- (* x y) z)])
-
-; (define-ruleset* special-numerical-expand
-;                  (numerics)
-;                  #:type ([x real] [y real])
-;                  [log1p-expm1-u x (log1p (expm1 x))]
-;                  [expm1-log1p-u x (expm1 (log1p x))])
-
-; (define-ruleset* numerics-papers
-;                  (numerics)
-;                  #:type ([a real] [b real] [c real] [d real])
-;                  ;  "Further Analysis of Kahan's Algorithm for
-;                  ;   the Accurate Computation of 2x2 Determinants"
-;                  ;  Jeannerod et al., Mathematics of Computation, 2013
-;                  ;
-;                  ;  a * b - c * d  ===> fma(a, b, -(d * c)) + fma(-d, c, d * c)
-;                  [prod-diff (- (* a b) (* c d)) (+ (fma a b (neg (* d c))) (fma (neg d) c (* d c)))])
+(define-ruleset* special-numerical-reduce
+                 (numerics simplify)
+                 #:type ([x real] [y real] [z real])
+                 [log1p-expm1 (log1p (expm1 x)) x]
+                 [expm1-log1p (expm1 (log1p x)) x]
+                 [hypot-1-def (sqrt (+ 1 (* y y))) (hypot 1 y)]
+                 [fmm-def (- (* x y) z) (fma x y (neg z))]
+                 [fmm-undef (fma x y (neg z)) (- (* x y) z)])
+
+(define-ruleset* special-numerical-expand
+                 (numerics)
+                 #:type ([x real] [y real])
+                 [log1p-expm1-u x (log1p (expm1 x))]
+                 [expm1-log1p-u x (expm1 (log1p x))])
+
+(define-ruleset* erf-rules (special simplify) #:type ([x real]) [erf-odd (erf (neg x)) (neg (erf x))])
+
+(define-ruleset* erf-rules-rev
+                 (special simplify)
+                 #:type ([x real])
+                 [erf-odd-rev (neg (erf x)) (erf (neg x))]) 
+
+(define-ruleset* numerics-papers
+                 (numerics)
+                 #:type ([a real] [b real] [c real] [d real])
+                 ;  "Further Analysis of Kahan's Algorithm for
+                 ;   the Accurate Computation of 2x2 Determinants"
+                 ;  Jeannerod et al., Mathematics of Computation, 2013
+                 ;
+                 ;  a * b - c * d  ===> fma(a, b, -(d * c)) + fma(-d, c, d * c)
+                 [prod-diff (- (* a b) (* c d)) (+ (fma a b (neg (* d c))) (fma (neg d) c (* d c)))])
+ |#
+
 
 ;; Sound because it's about soundness over real numbers
 (define-ruleset* compare-reduce
@@ -763,6 +1038,8 @@
                  [not-lte (not (<= x y)) (> x y)]
                  [not-gte (not (>= x y)) (< x y)])
 
+
+
 (define-ruleset* branch-reduce
                  (branches simplify fp-safe sound)
                  #:type ([a bool] [b bool] [x real] [y real])
@@ -774,3 +1051,111 @@
                  [if-if-or-not (if a x (if b y x)) (if (or a (not b)) x y)]
                  [if-if-and (if a (if b x y) y) (if (and a b) x y)]
                  [if-if-and-not (if a (if b y x) y) (if (and a (not b)) x y)])
+
+
+#| ;--------Bool&Branch-------
+
+;!
+(define-ruleset* compare-reduce-revv
+                 (bools simplify fp-safe-nan sound)
+                 #:type ([x real] [y real])
+                 [not-gte-rev (< x y) (not (>= x y))]
+                 [not-gt-rev (<= x y) (not (> x y))]
+                 [not-lte-rev (> x y) (not (<= x y))]
+                 [not-lt-rev (>= x y) (not (< x y))])
+;! Boolean
+(define-ruleset* branch-reduce-revv
+                 (branches simplify fp-safe sound)
+                 #:type ([a bool] [b bool] [x real] [y real])
+                 [if-if-and-not-rev (if (and a (not b)) x y) (if a (if b y x) y)]
+                 [if-true-rev x (if (TRUE) x y)]
+                 [if-if-or-rev (if (or a b) x y) (if a x (if b x y))]
+                 [if-same-rev x (if a x x)]
+                 [if-not-rev (if a y x) (if (not a) x y)]
+                 [if-if-and-rev (if (and a b) x y) (if a (if b x y) y)]
+                 [if-false-rev y (if (FALSE) x y)]
+                 [if-if-or-not-rev (if (or a (not b)) x y) (if a x (if b y x))])
+
+
+
+;-------Expanding on constants------
+
+;! increasing constants won't do much
+(define-ruleset* trig-reduce-constants-revv
+                 (trigonometry simplify sound)
+                 #:type ([a real] [b real] [x real])
+                 [cos-PI-rev -1 (cos (PI))]
+                 [sin-PI-rev 0 (sin (PI))]
+                 [tan-PI-rev 0 (tan (PI))]
+                 [cos-PI/2-rev 0 (cos (/ (PI) 2))]
+                 [sin-PI/2-rev 1 (sin (/ (PI) 2))]
+                 [tan-PI/4-rev 1 (tan (/ (PI) 4))]
+                 [cos-PI/3-rev 1/2 (cos (/ (PI) 3))]
+                 [sin-PI/6-rev 1/2 (sin (/ (PI) 6))]
+                 [cos-PI/6-rev (/ (sqrt 3) 2) (cos (/ (PI) 6))]
+                 [cos-PI/4-rev (/ (sqrt 2) 2) (cos (/ (PI) 4))]
+                 [sin-PI/3-rev (/ (sqrt 3) 2) (sin (/ (PI) 3))]
+                 [tan-PI/6-rev (/ 1 (sqrt 3)) (tan (/ (PI) 6))]
+                 [sin-PI/4-rev (/ (sqrt 2) 2) (sin (/ (PI) 4))]
+                 [tan-PI/3-rev (sqrt 3) (tan (/ (PI) 3))])
+
+;! expanding on a constant
+(define-ruleset* log-distribute-sound-revv
+                 (exponents simplify sound)
+                 #:type ([a real] [b real])
+                 [log-E-rev 1 (log (E))])
+
+;! Seems like too much recursion
+(define-ruleset* trig-reduce-fp-sound-rev
+                 (trigonometry simplify fp-safe sound)
+                 [sin-0-rev 0 (sin 0)]
+                 [tan-0-rev 0 (tan 0)]
+                 [cos-0-rev 1 (cos 0)])
+
+
+;! Expanding single variable
+(define-ruleset* trig-inverses-from-x-revv
+                 (trigonometry sound)
+                 #:type ([x real])
+                 [cos-acos-rev x (cos (acos x))]
+                 [sin-asin-rev x (sin (asin x))]
+                 [tan-atan-rev x (tan (atan x))])
+
+;! Increasing a single variable
+(define-ruleset* trig-inverses-simplified-rev
+                 (trigonometry)
+                 #:type ([x real])
+                 [atan-tan-s-rev x (atan (tan x))]
+                 [acos-cos-s-rev x (acos (cos x))]
+                 [asin-sin-s-rev x (asin (sin x))]
+                 )
+
+;! Expanding on one variable
+(define-ruleset* ahtrig-expand-sound-revv
+                 (hyperbolic sound)
+                 #:type ([x real])
+                 [cosh-acosh-rev x (cosh (acosh x))]
+                 [sinh-asinh-rev x (sinh (asinh x))]
+                 [tanh-atanh-rev x (tanh (atanh x))])            
+
+
+;!Expanding on a variable
+(define-ruleset* cubes-reduce-revv
+                 (arithmetic simplify)
+                 #:type ([x real])
+                 [rem-cbrt-cube-rev x (cbrt (pow x 3))]
+                 [rem-cube-cbrt-rev x (pow (cbrt x) 3)]
+                 [rem-3cbrt-rft-rev x (* (cbrt x) (* (cbrt x) (cbrt x)))])
+
+;!expanding on variable
+(define-ruleset* id-reduce-revv
+                 (arithmetic simplify)
+                 #:type ([a real])
+                 [remove-double-div-rev a (/ 1 (/ 1 a))])
+
+;-------Odd Expansion-------
+(define-ruleset* special-numerical-reduce-rev
+                 (numerics simplify)
+                 #:type ([x real] [y real] [z real])
+                 [hypot-1-def-rev (hypot 1 y) (sqrt (+ 1 (* y y)))])
+                  |#
\ No newline at end of file

From e834b4f891ff151e018634ea30802d5649d3e873 Mon Sep 17 00:00:00 2001
From: JJponce0913 <u1398911@umail.utah.edu>
Date: Thu, 10 Oct 2024 08:28:28 -0600
Subject: [PATCH 2/8] raco fmt

---
 src/core/rules.rkt | 52 +++++++++++++++++-----------------------------
 1 file changed, 19 insertions(+), 33 deletions(-)

diff --git a/src/core/rules.rkt b/src/core/rules.rkt
index 96964c5b4..8d0cd0cce 100644
--- a/src/core/rules.rkt
+++ b/src/core/rules.rkt
@@ -101,8 +101,7 @@
 ;;
 
 (define ((type/repr-of-rule op-info name) input output ctx)
-  (let loop ([input input]
-             [output output])
+  (let loop ([input input] [output output])
     (match* (input output)
       ; first, try the input expression
       ; special case for `if` expressions
@@ -149,7 +148,6 @@
     [(define-ruleset* name groups #:type ([var type] ...) [rname input output] ...)
      (register-ruleset*! 'name 'groups `((var . type) ...) '((rname input output) ...))]))
 
-
 ; Commutativity
 (define-ruleset* commutativity
                  (arithmetic simplify fp-safe sound)
@@ -245,12 +243,10 @@
 (define-ruleset* difference-of-squares-canonicalize-revv
                  (polynomials simplify sound)
                  #:type ([a real] [b real])
-                 [difference-of-sqr-1-rev (* (+ a 1) (- a 1)) (- (* a a) 1)];$$
-                 [difference-of-sqr--1-rev (* (+ a 1) (- a 1)) (+ (* a a) -1)];$$
-
-                 [difference-of-squares-rev (* (+ a b) (- a b)) (- (* a a) (* b b))];$$
-                 [pow-sqr-rev (pow a (* 2 b)) (* (pow a b) (pow a b))]);$)
-
+                 [difference-of-sqr-1-rev (* (+ a 1) (- a 1)) (- (* a a) 1)] ;$$
+                 [difference-of-sqr--1-rev (* (+ a 1) (- a 1)) (+ (* a a) -1)] ;$$
+                 [difference-of-squares-rev (* (+ a b) (- a b)) (- (* a a) (* b b))] ;$$
+                 [pow-sqr-rev (pow a (* 2 b)) (* (pow a b) (pow a b))]) ;$)
 
 (define-ruleset* sqr-pow-expand
                  (polynomials)
@@ -456,7 +452,6 @@
                  [cube-neg-rev (neg (pow x 3)) (pow (neg x) 3)] ;$$ seems reasonable
                  )
 
-
 (define-ruleset* cubes-distribute
                  (arithmetic simplify sound)
                  #:type ([x real] [y real])
@@ -467,7 +462,7 @@
                  [cube-div-rev (/ (pow x 3) (pow y 3)) (pow (/ x y) 3)])
 
 (define-ruleset* cubes-transform
-                 (arithmetic )
+                 (arithmetic)
                  #:type ([x real] [y real])
                  [cbrt-prod (cbrt (* x y)) (* (cbrt x) (cbrt y))]
                  [cbrt-div (cbrt (/ x y)) (/ (cbrt x) (cbrt y))]
@@ -636,7 +631,6 @@
                  [cos-0 (cos 0) 1]
                  [tan-0 (tan 0) 0])
 
-
 (define-ruleset* trig-reduce-fp-sound-nan
                  (trigonometry simplify fp-safe-nan sound)
                  #:type ([x real])
@@ -671,8 +665,6 @@
  [asin-sin (asin (sin x)) (- (fabs (remainder (+ x (/ (PI) 2)) (* 2 (PI)))) (/ (PI) 2))]
  [acos-cos (acos (cos x)) (fabs (remainder x (* 2 (PI))))])
 
-
-
 ;$simplification
 (define-ruleset*
  trig-inverses-revv
@@ -689,8 +681,6 @@
                  [asin-sin-s (asin (sin x)) x]
                  [acos-cos-s (acos (cos x)) x])
 
-
-
 (define-ruleset* trig-reduce-expressions
                  (trigonometry simplify sound)
                  #:type ([a real] [b real] [x real])
@@ -730,7 +720,7 @@
 (define-ruleset* trig-reduce-expressions-revv
                  (trigonometry simplify sound)
                  #:type ([a real] [b real] [x real])
-                 [1-sub-sin-rev (* (cos a) (cos a)) (- 1 (* (sin a) (sin a)))]     
+                 [1-sub-sin-rev (* (cos a) (cos a)) (- 1 (* (sin a) (sin a)))]
                  [hang-m0-tan-rev (tan (/ (neg a) 2)) (/ (- 1 (cos a)) (neg (sin a)))]
                  [hang-p0-tan-rev (tan (/ a 2)) (/ (- 1 (cos a)) (sin a))]
                  [hang-0m-tan-rev (tan (/ (neg a) 2)) (/ (neg (sin a)) (+ 1 (cos a)))]
@@ -749,13 +739,14 @@
                  (trigonometry)
                  #:type ([a real] [b real] [x real])
                  [tan-+PI/2 (tan (+ x (/ (PI) 2))) (/ -1 (tan x))]
-                 [tan-+PI/2-rev (tan (+ (neg x) (/ (PI) 2))) (/ 1 (tan x)) ])
+                 [tan-+PI/2-rev (tan (+ (neg x) (/ (PI) 2))) (/ 1 (tan x))])
 
-(define-ruleset* trig-reduce-rev
-                 (trigonometry)
-                 #:type ([a real] [b real] [x real])
-                 [neg-tan-+PI/2-rev (/ -1 (tan x)) (tan (+ x (/ (PI) 2)))]
-                 [tan-+PI/2-rev (/ 1 (tan x)) (tan (+ (neg x) (/ (PI) 2)))]); make version where 1/tanx -> 
+(define-ruleset*
+ trig-reduce-rev
+ (trigonometry)
+ #:type ([a real] [b real] [x real])
+ [neg-tan-+PI/2-rev (/ -1 (tan x)) (tan (+ x (/ (PI) 2)))]
+ [tan-+PI/2-rev (/ 1 (tan x)) (tan (+ (neg x) (/ (PI) 2)))]) ; make version where 1/tanx ->
 
 (define-ruleset* trig-expand-sound
                  (trigonometry sound)
@@ -878,7 +869,7 @@
                  [sinh-def-rev (/ (- (exp x) (exp (neg x))) 2) (sinh x)]
                  [cosh-def-rev (/ (+ (exp x) (exp (neg x))) 2) (cosh x)]
                  [sinh-+-cosh-rev (exp x) (+ (cosh x) (sinh x))]
-[sinh---cosh-rev (exp (neg x)) (- (cosh x) (sinh x))])
+                 [sinh---cosh-rev (exp (neg x)) (- (cosh x) (sinh x))])
 
 (define-ruleset* htrig-expand-sound
                  (hyperbolic sound)
@@ -928,7 +919,7 @@
                  (hyperbolic)
                  #:type ([x real] [y real])
                  [tanh-1/2* (tanh (/ x 2)) (/ (- (cosh x) 1) (sinh x))]
-                 [tanh-1/2*-rev (/ (- (cosh x) 1) (sinh x)) (tanh (/ x 2))]) 
+                 [tanh-1/2*-rev (/ (- (cosh x) 1) (sinh x)) (tanh (/ x 2))])
 
 (define-ruleset* htrig-expand-fp-safe
                  (hyperbolic fp-safe sound)
@@ -962,7 +953,6 @@
                  [tanh-acosh (tanh (acosh x)) (/ (sqrt (- (* x x) 1)) x)]
                  [tanh-atanh (tanh (atanh x)) x])
 
-
 (define-ruleset* ahtrig-expand-sound-simplify-revv
                  (hyperbolic sound)
                  #:type ([x real])
@@ -1011,7 +1001,7 @@
 (define-ruleset* erf-rules-rev
                  (special simplify)
                  #:type ([x real])
-                 [erf-odd-rev (neg (erf x)) (erf (neg x))]) 
+                 [erf-odd-rev (neg (erf x)) (erf (neg x))])
 
 (define-ruleset* numerics-papers
                  (numerics)
@@ -1024,7 +1014,6 @@
                  [prod-diff (- (* a b) (* c d)) (+ (fma a b (neg (* d c))) (fma (neg d) c (* d c)))])
  |#
 
-
 ;; Sound because it's about soundness over real numbers
 (define-ruleset* compare-reduce
                  (bools simplify fp-safe-nan sound)
@@ -1038,8 +1027,6 @@
                  [not-lte (not (<= x y)) (> x y)]
                  [not-gte (not (>= x y)) (< x y)])
 
-
-
 (define-ruleset* branch-reduce
                  (branches simplify fp-safe sound)
                  #:type ([a bool] [b bool] [x real] [y real])
@@ -1052,7 +1039,6 @@
                  [if-if-and (if a (if b x y) y) (if (and a b) x y)]
                  [if-if-and-not (if a (if b y x) y) (if (and a (not b)) x y)])
 
-
 #| ;--------Bool&Branch-------
 
 ;!
@@ -1136,7 +1122,7 @@
                  #:type ([x real])
                  [cosh-acosh-rev x (cosh (acosh x))]
                  [sinh-asinh-rev x (sinh (asinh x))]
-                 [tanh-atanh-rev x (tanh (atanh x))])            
+                 [tanh-atanh-rev x (tanh (atanh x))])
 
 
 ;!Expanding on a variable
@@ -1158,4 +1144,4 @@
                  (numerics simplify)
                  #:type ([x real] [y real] [z real])
                  [hypot-1-def-rev (hypot 1 y) (sqrt (+ 1 (* y y)))])
-                  |#
\ No newline at end of file
+                  |#

From 8924ce3e12472cdf77184083203d334df2da7dfa Mon Sep 17 00:00:00 2001
From: JJponce0913 <u1398911@umail.utah.edu>
Date: Thu, 10 Oct 2024 08:30:27 -0600
Subject: [PATCH 3/8] minor naming error

---
 src/core/rules.rkt | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/src/core/rules.rkt b/src/core/rules.rkt
index 8d0cd0cce..da3856724 100644
--- a/src/core/rules.rkt
+++ b/src/core/rules.rkt
@@ -738,8 +738,8 @@
 (define-ruleset* trig-reduce
                  (trigonometry)
                  #:type ([a real] [b real] [x real])
-                 [tan-+PI/2 (tan (+ x (/ (PI) 2))) (/ -1 (tan x))]
-                 [tan-+PI/2-rev (tan (+ (neg x) (/ (PI) 2))) (/ 1 (tan x))])
+                 [neg-tan-+PI/2 (tan (+ x (/ (PI) 2))) (/ -1 (tan x))]
+                 [tan-+PI/2 (tan (+ (neg x) (/ (PI) 2))) (/ 1 (tan x))])
 
 (define-ruleset*
  trig-reduce-rev

From e9bd37a2fd4fd13154bcfa0fe930e43fda66326a Mon Sep 17 00:00:00 2001
From: JJponce0913 <u1398911@umail.utah.edu>
Date: Wed, 16 Oct 2024 11:58:47 -0600
Subject: [PATCH 4/8] Update

---
 src/core/rules.rkt | 228 ++++-----------------------------------------
 1 file changed, 18 insertions(+), 210 deletions(-)

diff --git a/src/core/rules.rkt b/src/core/rules.rkt
index da3856724..780895a97 100644
--- a/src/core/rules.rkt
+++ b/src/core/rules.rkt
@@ -179,7 +179,6 @@
 ; Counting
 (define-ruleset* counting (arithmetic simplify sound) #:type ([x real]) [count-2 (+ x x) (* 2 x)])
 
-;$$ Good
 (define-ruleset* counting-revv
                  (arithmetic simplify sound)
                  #:type ([x real])
@@ -202,7 +201,6 @@
 (define-ruleset* distributivity-fp-safe
                  (arithmetic simplify fp-safe sound)
                  #:type ([a real] [b real])
-                 ;$$(* (neg a) b) (* a (neg b))
                  [distribute-lft-neg-in (neg (* a b)) (* (neg a) b)]
                  [distribute-rgt-neg-in (neg (* a b)) (* a (neg b))]
                  [distribute-lft-neg-out (* (neg a) b) (neg (* a b))]
@@ -214,19 +212,17 @@
                  [distribute-neg-frac (neg (/ a b)) (/ (neg a) b)]
                  [distribute-neg-frac2 (neg (/ a b)) (/ a (neg b))])
 
-;$$ This ruleset doesn't make sense because it is passing the negative to one of multiplied numbers but only ever to the new one of the variables.
 (define-ruleset* cancel-sign-fp-safe
                  (arithmetic simplify fp-safe sound)
                  #:type ([a real] [b real] [c real])
-                 [cancel-sign-sub (- a (* (neg b) c)) (+ a (* b c))] ;old
-                 [cancel-sub-sign (+ a (* (neg b) c)) (- a (* b c))] ;new
-                 )
+                 [cancel-sign-sub (- a (* (neg b) c)) (+ a (* b c))]
+                 [cancel-sub-sign (+ a (* (neg b) c)) (- a (* b c))])
 
 (define-ruleset* cancel-sign-fp-safe-revv
                  (arithmetic simplify fp-safe sound)
                  #:type ([a real] [b real] [c real])
-                 [cancel-sign-sub-inv (+ a (* b c)) (- a (* (neg b) c))] ;old
-                 [cancel-sub-sign-inv (- a (* b c)) (+ a (* (neg b) c))]) ;old
+                 [cancel-sign-sub-inv (+ a (* b c)) (- a (* (neg b) c))]
+                 [cancel-sub-sign-inv (- a (* b c)) (+ a (* (neg b) c))])
 
 ; Difference of squares
 (define-ruleset* difference-of-squares-canonicalize
@@ -239,15 +235,13 @@
                  [difference-of-sqr--1 (+ (* a a) -1) (* (+ a 1) (- a 1))]
                  [pow-sqr (* (pow a b) (pow a b)) (pow a (* 2 b))])
 
-;$ reduces
 (define-ruleset* difference-of-squares-canonicalize-revv
                  (polynomials simplify sound)
                  #:type ([a real] [b real])
-                 [difference-of-sqr-1-rev (* (+ a 1) (- a 1)) (- (* a a) 1)] ;$$
-                 [difference-of-sqr--1-rev (* (+ a 1) (- a 1)) (+ (* a a) -1)] ;$$
-                 [difference-of-squares-rev (* (+ a b) (- a b)) (- (* a a) (* b b))] ;$$
-                 [pow-sqr-rev (pow a (* 2 b)) (* (pow a b) (pow a b))]) ;$)
-
+                 [difference-of-sqr-1-rev (* (+ a 1) (- a 1)) (- (* a a) 1)]
+                 [difference-of-sqr--1-rev (* (+ a 1) (- a 1)) (+ (* a a) -1)]
+                 [difference-of-squares-rev (* (+ a b) (- a b)) (- (* a a) (* b b))]
+                 [pow-sqr-rev (pow a (* 2 b)) (* (pow a b) (pow a b))])
 (define-ruleset* sqr-pow-expand
                  (polynomials)
                  #:type ([a real] [b real])
@@ -289,18 +283,6 @@
                  [/-rgt-identity (/ a 1) a] ;
                  [mul-1-neg (* -1 a) (neg a)])
 
-;? 1.Would adding the extra arithmetic do anything? 2.Why is the 6th rule implemented but not the rest? 3.Would adding adouble negative help?
-(define-ruleset* id-reduce-fp-safe-revv
-                 (arithmetic simplify)
-                 #:type ([a real])
-                 [*-rgt-identity-rev a (* a 1)]
-                 [+-rgt-identity-rev a (+ a 0)]
-                 [+-lft-identity-rev a (+ 0 a)]
-                 [/-rgt-identity-rev a (/ a 1)]
-                 [--rgt-identity-rev a (- a 0)]
-                 ;[*-lft-identity-rev a (* 1 a)]
-                 [remove-double-neg-rev a (neg (neg a))])
-
 (define-ruleset* nan-transform-fp-safe
                  (arithmetic simplify fp-safe sound)
                  #:type ([a real] [b real])
@@ -320,13 +302,6 @@
                  #:type ([a real] [b real])
                  [clear-num (/ a b) (/ 1 (/ b a))])
 
-;$$! this one seems important
-(define-ruleset* id-transform-clear-num-revv
-                 (arithmetic)
-                 #:type ([a real] [b real])
-                 [clear-num-rev (/ 1 (/ b a)) (/ a b)])
-
-;?? Why is this rule here but not the other?
 (define-ruleset* id-transform-fp-safe
                  (arithmetic fp-safe)
                  #:type ([a real])
@@ -342,7 +317,6 @@
  [flip3-+ (+ a b) (/ (+ (pow a 3) (pow b 3)) (+ (* a a) (- (* b b) (* a b))))]
  [flip3-- (- a b) (/ (- (pow a 3) (pow b 3)) (+ (* a a) (+ (* b b) (* a b))))])
 
-;$$reduction
 (define-ruleset*
  difference-of-cubes-revv
  (polynomials sound)
@@ -358,7 +332,6 @@
                  [times-frac (/ (* a b) (* c d)) (* (/ a c) (/ b d))]
                  [div-add (/ (+ a b) c) (+ (/ a c) (/ b c))])
 
-;$$ Odd its not a rule (a/c)+(b/c) -> (a+b)/c
 (define-ruleset* fractions-distribute-revv
                  (fractions simplify sound)
                  #:type ([a real] [b real] [c real] [d real])
@@ -373,7 +346,6 @@
                  [frac-times (* (/ a b) (/ c d)) (/ (* a c) (* b d))]
                  [frac-2neg (/ a b) (/ (neg a) (neg b))])
 
-;$$good simplification
 (define-ruleset* fractions-transform-revv
                  (fractions sound)
                  #:type ([a real] [b real] [c real] [d real])
@@ -385,8 +357,7 @@
                  #:type ([x real])
                  [rem-square-sqrt (* (sqrt x) (sqrt x)) x]
                  [rem-sqrt-square (sqrt (* x x)) (fabs x)]
-                 [rem-sqrt-square-rev (fabs x) (sqrt (* x x))] ;$$ sqrt might be the useful
-                 )
+                 [rem-sqrt-square-rev (fabs x) (sqrt (* x x))])
 
 (define-ruleset* squares-reduce-fp-sound
                  (arithmetic simplify fp-safe sound)
@@ -394,7 +365,6 @@
                  [sqr-neg (* (neg x) (neg x)) (* x x)]
                  [sqr-abs (* (fabs x) (fabs x)) (* x x)])
 
-;?
 (define-ruleset* squares-reduce-fp-sound-rev
                  (arithmetic simplify fp-safe sound)
                  #:type ([x real])
@@ -411,13 +381,6 @@
                  [fabs-mul (fabs (* a b)) (* (fabs a) (fabs b))]
                  [fabs-div (fabs (/ a b)) (/ (fabs a) (fabs b))])
 
-;? Would adding fabs help?
-(define-ruleset* fabs-reduce-rev
-                 (arithmetic simplify fp-safe sound)
-                 #:type ([x real] [a real] [b real])
-                 [fabs-sqr-rev (* x x) (fabs (* x x))]
-                 [fabs-fabs-rev (fabs x) (fabs (fabs x))])
-
 (define-ruleset* fabs-expand
                  (arithmetic fp-safe sound)
                  #:type ([x real] [a real] [b real])
@@ -449,8 +412,7 @@
                  [rem-3cbrt-lft (* (* (cbrt x) (cbrt x)) (cbrt x)) x]
                  [rem-3cbrt-rft (* (cbrt x) (* (cbrt x) (cbrt x))) x]
                  [cube-neg (pow (neg x) 3) (neg (pow x 3))]
-                 [cube-neg-rev (neg (pow x 3)) (pow (neg x) 3)] ;$$ seems reasonable
-                 )
+                 [cube-neg-rev (neg (pow x 3)) (pow (neg x) 3)])
 
 (define-ruleset* cubes-distribute
                  (arithmetic simplify sound)
@@ -458,7 +420,7 @@
                  [cube-prod (pow (* x y) 3) (* (pow x 3) (pow y 3))]
                  [cube-div (pow (/ x y) 3) (/ (pow x 3) (pow y 3))]
                  [cube-mult (pow x 3) (* x (* x x))]
-                 [cube-prod-rev (* (pow x 3) (pow y 3)) (pow (* x y) 3)] ;$reduction
+                 [cube-prod-rev (* (pow x 3) (pow y 3)) (pow (* x y) 3)]
                  [cube-div-rev (/ (pow x 3) (pow y 3)) (pow (/ x y) 3)])
 
 (define-ruleset* cubes-transform
@@ -471,7 +433,6 @@
                  [add-cube-cbrt x (* (* (cbrt x) (cbrt x)) (cbrt x))]
                  [add-cbrt-cube x (cbrt (* (* x x) x))])
 
-;$$good simplifications
 (define-ruleset* cubes-transform-revv
                  (arithmetic sound)
                  #:type ([x real] [y real])
@@ -519,7 +480,6 @@
                  [exp-lft-sqr (exp (* a 2)) (* (exp a) (exp a))]
                  [exp-lft-cube (exp (* a 3)) (pow (exp a) 3)])
 
-;? Maybe useful
 (define-ruleset* exp-factor-revv
                  (exponents simplify sound)
                  #:type ([a real] [b real])
@@ -553,7 +513,7 @@
                  [unpow3 (pow a 3) (* (* a a) a)]
                  [unpow1/3 (pow a 1/3) (cbrt a)]
                  [pow-plus (* (pow a b) a) (pow a (+ b 1))])
-;?maybe good expansion
+
 (define-ruleset* pow-canonicalize-revv
                  (exponents simplify sound)
                  #:type ([a real] [b real])
@@ -611,7 +571,6 @@
                  [log-div (log (/ a b)) (- (log a) (log b))]
                  [log-pow (log (pow a b)) (* b (log a))])
 
-;$$ Good expansion
 (define-ruleset* log-distribute-rev
                  (exponents)
                  #:type ([a real] [b real])
@@ -638,7 +597,6 @@
                  [cos-neg (cos (neg x)) (cos x)]
                  [tan-neg (tan (neg x)) (neg (tan x))])
 
-;$$? Add neg?
 (define-ruleset* trig-reduce-fp-sound-nan-revv
                  (trigonometry simplify fp-safe-nan sound)
                  #:type ([x real])
@@ -652,7 +610,7 @@
                  [sqr-sin-b (* (sin x) (sin x)) (- 1 (* (cos x) (cos x)))]
                  [sqr-cos-b (* (cos x) (cos x)) (- 1 (* (sin x) (sin x)))]
                  [sqr-cos-b-rev (- 1 (* (sin x) (sin x))) (* (cos x) (cos x))]
-                 [sqr-sin-b-rev (- 1 (* (cos x) (cos x))) (* (sin x) (sin x))]) ;$$ simplification)
+                 [sqr-sin-b-rev (- 1 (* (cos x) (cos x))) (* (sin x) (sin x))])
 
 (define-ruleset*
  trig-inverses
@@ -665,7 +623,6 @@
  [asin-sin (asin (sin x)) (- (fabs (remainder (+ x (/ (PI) 2)) (* 2 (PI)))) (/ (PI) 2))]
  [acos-cos (acos (cos x)) (fabs (remainder x (* 2 (PI))))])
 
-;$simplification
 (define-ruleset*
  trig-inverses-revv
  (trigonometry sound)
@@ -741,12 +698,11 @@
                  [neg-tan-+PI/2 (tan (+ x (/ (PI) 2))) (/ -1 (tan x))]
                  [tan-+PI/2 (tan (+ (neg x) (/ (PI) 2))) (/ 1 (tan x))])
 
-(define-ruleset*
- trig-reduce-rev
- (trigonometry)
- #:type ([a real] [b real] [x real])
- [neg-tan-+PI/2-rev (/ -1 (tan x)) (tan (+ x (/ (PI) 2)))]
- [tan-+PI/2-rev (/ 1 (tan x)) (tan (+ (neg x) (/ (PI) 2)))]) ; make version where 1/tanx ->
+(define-ruleset* trig-reduce-rev
+                 (trigonometry)
+                 #:type ([a real] [b real] [x real])
+                 [neg-tan-+PI/2-rev (/ -1 (tan x)) (tan (+ x (/ (PI) 2)))]
+                 [tan-+PI/2-rev (/ 1 (tan x)) (tan (+ (neg x) (/ (PI) 2)))])
 
 (define-ruleset* trig-expand-sound
                  (trigonometry sound)
@@ -766,7 +722,6 @@
                  [2-cos (- (* (cos x) (cos x)) (* (sin x) (sin x))) (cos (* 2 x))]
                  [3-cos (- (* 4 (pow (cos x) 3)) (* 3 (cos x))) (cos (* 3 x))])
 
-;$$simplification
 (define-ruleset* trig-expand-sound-revv
                  (trigonometry sound)
                  #:type ([x real] [y real] [a real] [b real])
@@ -794,7 +749,6 @@
                  [tan-2 (tan (* 2 x)) (/ (* 2 (tan x)) (- 1 (* (tan x) (tan x))))]
                  [2-tan (/ (* 2 (tan x)) (- 1 (* (tan x) (tan x)))) (tan (* 2 x))])
 
-;$$simplification
 (define-ruleset* trig-expand-sound2-revv
                  (trigonometry sound)
                  [diff-cos-rev (* -2 (* (sin (/ (- x y) 2)) (sin (/ (+ x y) 2)))) (- (cos x) (cos y))]
@@ -830,13 +784,11 @@
                  [acos-neg (acos (neg x)) (- (PI) (acos x))]
                  [atan-neg (atan (neg x)) (neg (atan x))])
 
-;$$good simplification
 (define-ruleset* atrig-expand-revv
                  (trigonometry sound)
                  #:type ([x real])
                  [acos-asin-rev (- (/ (PI) 2) (asin x)) (acos x)]
                  [asin-acos-rev (- (/ (PI) 2) (acos x)) (asin x)]
-                 ;?Does moving the negative sign around do much?
                  [asin-neg-rev (neg (asin x)) (asin (neg x))]
                  [atan-neg-rev (neg (atan x)) (atan (neg x))]
                  [acos-neg-rev (- (PI) (acos x)) (acos (neg x))]
@@ -860,7 +812,6 @@
                  [sinh-+-cosh (+ (cosh x) (sinh x)) (exp x)]
                  [sinh---cosh (- (cosh x) (sinh x)) (exp (neg x))])
 
-;$$simplification
 (define-ruleset* htrig-reduce-revv
                  (hyperbolic simplify sound)
                  #:type ([x real])
@@ -972,48 +923,12 @@
                  [asinh-2 (acosh (+ (* 2 (* x x)) 1)) (* 2 (asinh x))]
                  [acosh-2 (acosh (- (* 2 (* x x)) 1)) (* 2 (acosh x))])
 
-;? I think this expansion could be helpful
 (define-ruleset* ahtrig-expand-rev
                  (hyperbolic)
                  #:type ([x real])
                  [asinh-2-rev (* 2 (asinh x)) (acosh (+ (* 2 (* x x)) 1))]
                  [acosh-2-rev (* 2 (acosh x)) (acosh (- (* 2 (* x x)) 1))])
 
-#|; Specialized numerical functions
-; TODO: These are technically rules over impls
-(define-ruleset* special-numerical-reduce
-                 (numerics simplify)
-                 #:type ([x real] [y real] [z real])
-                 [log1p-expm1 (log1p (expm1 x)) x]
-                 [expm1-log1p (expm1 (log1p x)) x]
-                 [hypot-1-def (sqrt (+ 1 (* y y))) (hypot 1 y)]
-                 [fmm-def (- (* x y) z) (fma x y (neg z))]
-                 [fmm-undef (fma x y (neg z)) (- (* x y) z)])
-
-(define-ruleset* special-numerical-expand
-                 (numerics)
-                 #:type ([x real] [y real])
-                 [log1p-expm1-u x (log1p (expm1 x))]
-                 [expm1-log1p-u x (expm1 (log1p x))])
-
-(define-ruleset* erf-rules (special simplify) #:type ([x real]) [erf-odd (erf (neg x)) (neg (erf x))])
-
-(define-ruleset* erf-rules-rev
-                 (special simplify)
-                 #:type ([x real])
-                 [erf-odd-rev (neg (erf x)) (erf (neg x))])
-
-(define-ruleset* numerics-papers
-                 (numerics)
-                 #:type ([a real] [b real] [c real] [d real])
-                 ;  "Further Analysis of Kahan's Algorithm for
-                 ;   the Accurate Computation of 2x2 Determinants"
-                 ;  Jeannerod et al., Mathematics of Computation, 2013
-                 ;
-                 ;  a * b - c * d  ===> fma(a, b, -(d * c)) + fma(-d, c, d * c)
-                 [prod-diff (- (* a b) (* c d)) (+ (fma a b (neg (* d c))) (fma (neg d) c (* d c)))])
- |#
-
 ;; Sound because it's about soundness over real numbers
 (define-ruleset* compare-reduce
                  (bools simplify fp-safe-nan sound)
@@ -1038,110 +953,3 @@
                  [if-if-or-not (if a x (if b y x)) (if (or a (not b)) x y)]
                  [if-if-and (if a (if b x y) y) (if (and a b) x y)]
                  [if-if-and-not (if a (if b y x) y) (if (and a (not b)) x y)])
-
-#| ;--------Bool&Branch-------
-
-;!
-(define-ruleset* compare-reduce-revv
-                 (bools simplify fp-safe-nan sound)
-                 #:type ([x real] [y real])
-                 [not-gte-rev (< x y) (not (>= x y))]
-                 [not-gt-rev (<= x y) (not (> x y))]
-                 [not-lte-rev (> x y) (not (<= x y))]
-                 [not-lt-rev (>= x y) (not (< x y))])
-;! Boolean
-(define-ruleset* branch-reduce-revv
-                 (branches simplify fp-safe sound)
-                 #:type ([a bool] [b bool] [x real] [y real])
-                 [if-if-and-not-rev (if (and a (not b)) x y) (if a (if b y x) y)]
-                 [if-true-rev x (if (TRUE) x y)]
-                 [if-if-or-rev (if (or a b) x y) (if a x (if b x y))]
-                 [if-same-rev x (if a x x)]
-                 [if-not-rev (if a y x) (if (not a) x y)]
-                 [if-if-and-rev (if (and a b) x y) (if a (if b x y) y)]
-                 [if-false-rev y (if (FALSE) x y)]
-                 [if-if-or-not-rev (if (or a (not b)) x y) (if a x (if b y x))])
-
-
-
-;-------Expanding on constants------
-
-;! increasing constants won't do much
-(define-ruleset* trig-reduce-constants-revv
-                 (trigonometry simplify sound)
-                 #:type ([a real] [b real] [x real])
-                 [cos-PI-rev -1 (cos (PI))]
-                 [sin-PI-rev 0 (sin (PI))]
-                 [tan-PI-rev 0 (tan (PI))]
-                 [cos-PI/2-rev 0 (cos (/ (PI) 2))]
-                 [sin-PI/2-rev 1 (sin (/ (PI) 2))]
-                 [tan-PI/4-rev 1 (tan (/ (PI) 4))]
-                 [cos-PI/3-rev 1/2 (cos (/ (PI) 3))]
-                 [sin-PI/6-rev 1/2 (sin (/ (PI) 6))]
-                 [cos-PI/6-rev (/ (sqrt 3) 2) (cos (/ (PI) 6))]
-                 [cos-PI/4-rev (/ (sqrt 2) 2) (cos (/ (PI) 4))]
-                 [sin-PI/3-rev (/ (sqrt 3) 2) (sin (/ (PI) 3))]
-                 [tan-PI/6-rev (/ 1 (sqrt 3)) (tan (/ (PI) 6))]
-                 [sin-PI/4-rev (/ (sqrt 2) 2) (sin (/ (PI) 4))]
-                 [tan-PI/3-rev (sqrt 3) (tan (/ (PI) 3))])
-
-;! expanding on a constant
-(define-ruleset* log-distribute-sound-revv
-                 (exponents simplify sound)
-                 #:type ([a real] [b real])
-                 [log-E-rev 1 (log (E))])
-
-;! Seems like too much recursion
-(define-ruleset* trig-reduce-fp-sound-rev
-                 (trigonometry simplify fp-safe sound)
-                 [sin-0-rev 0 (sin 0)]
-                 [tan-0-rev 0 (tan 0)]
-                 [cos-0-rev 1 (cos 0)])
-
-
-;! Expanding single variable
-(define-ruleset* trig-inverses-from-x-revv
-                 (trigonometry sound)
-                 #:type ([x real])
-                 [cos-acos-rev x (cos (acos x))]
-                 [sin-asin-rev x (sin (asin x))]
-                 [tan-atan-rev x (tan (atan x))])
-
-;! Increasing a single variable
-(define-ruleset* trig-inverses-simplified-rev
-                 (trigonometry)
-                 #:type ([x real])
-                 [atan-tan-s-rev x (atan (tan x))]
-                 [acos-cos-s-rev x (acos (cos x))]
-                 [asin-sin-s-rev x (asin (sin x))]
-                 )
-
-;! Expanding on one variable
-(define-ruleset* ahtrig-expand-sound-revv
-                 (hyperbolic sound)
-                 #:type ([x real])
-                 [cosh-acosh-rev x (cosh (acosh x))]
-                 [sinh-asinh-rev x (sinh (asinh x))]
-                 [tanh-atanh-rev x (tanh (atanh x))])
-
-
-;!Expanding on a variable
-(define-ruleset* cubes-reduce-revv
-                 (arithmetic simplify)
-                 #:type ([x real])
-                 [rem-cbrt-cube-rev x (cbrt (pow x 3))]
-                 [rem-cube-cbrt-rev x (pow (cbrt x) 3)]
-                 [rem-3cbrt-rft-rev x (* (cbrt x) (* (cbrt x) (cbrt x)))])
-
-;!expanding on variable
-(define-ruleset* id-reduce-revv
-                 (arithmetic simplify)
-                 #:type ([a real])
-                 [remove-double-div-rev a (/ 1 (/ 1 a))])
-
-;-------Odd Expansion-------
-(define-ruleset* special-numerical-reduce-rev
-                 (numerics simplify)
-                 #:type ([x real] [y real] [z real])
-                 [hypot-1-def-rev (hypot 1 y) (sqrt (+ 1 (* y y)))])
-                  |#

From d3c9cb5ace2b81a7f158c5f249b84899f96b89d9 Mon Sep 17 00:00:00 2001
From: JJponce0913 <u1398911@umail.utah.edu>
Date: Wed, 16 Oct 2024 12:44:45 -0600
Subject: [PATCH 5/8] raco compliance

---
 infra/ci.rkt       | 3 +--
 src/core/rules.rkt | 4 ++++
 2 files changed, 5 insertions(+), 2 deletions(-)

diff --git a/infra/ci.rkt b/infra/ci.rkt
index cb3294e90..2f4649aa9 100644
--- a/infra/ci.rkt
+++ b/infra/ci.rkt
@@ -34,8 +34,7 @@
       (append-map load-tests bench-dirs)))
   (define seed (pseudo-random-generator->vector (current-pseudo-random-generator)))
   (printf "Running Herbie on ~a tests, seed: ~a\n" (length tests) seed)
-  (for/and ([the-test tests]
-            [i (in-naturals)])
+  (for/and ([the-test tests] [i (in-naturals)])
     (printf "~a/~a\t" (~a (+ 1 i) #:width 3 #:align 'right) (length tests))
     (define the-test* (if (*precision*) (override-test-precision the-test (*precision*)) the-test))
     (define result (run-herbie 'improve the-test* #:seed seed))
diff --git a/src/core/rules.rkt b/src/core/rules.rkt
index 780895a97..4a698d771 100644
--- a/src/core/rules.rkt
+++ b/src/core/rules.rkt
@@ -583,6 +583,10 @@
                  [diff-log (- (log a) (log b)) (log (/ a b))]
                  [neg-log (neg (log a)) (log (/ 1 a))])
 
+#| (define-ruleset* log-factor
+                 (exponents sound)
+                 #:type ([a real] [b real])                 
+                  [2log (/ (log x) (log 2)) (log2 a)] |#
 ; Trigonometry
 (define-ruleset* trig-reduce-fp-sound
                  (trigonometry simplify fp-safe sound)

From 5f4ea38a55723c5b85f320c7ca0aed956ff7b893 Mon Sep 17 00:00:00 2001
From: JJponce0913 <u1398911@umail.utah.edu>
Date: Wed, 16 Oct 2024 12:49:40 -0600
Subject: [PATCH 6/8] fmt compliance

---
 src/core/programs.rkt  |  9 +++------
 src/utils/timeline.rkt | 25 ++++++++-----------------
 2 files changed, 11 insertions(+), 23 deletions(-)

diff --git a/src/core/programs.rkt b/src/core/programs.rkt
index 7771fc6b7..a6dc49b55 100644
--- a/src/core/programs.rkt
+++ b/src/core/programs.rkt
@@ -103,8 +103,7 @@
        [(< len-a len-b) -1]
        [(> len-a len-b) 1]
        [else
-        (let loop ([a a]
-                   [b b])
+        (let loop ([a a] [b b])
           (if (null? a)
               0
               (let ([cmp (expr-cmp (car a) (car b))])
@@ -160,8 +159,7 @@
   (define (invalid! where loc)
     (error 'location-do "invalid location `~a` for `~a` in `~a`" loc where prog))
 
-  (let loop ([prog prog]
-             [loc loc])
+  (let loop ([prog prog] [loc loc])
     (match* (prog loc)
       [(_ (? null?)) (f prog)]
       [((or (? literal?) (? number?) (? symbol?)) _) (invalid! prog loc)]
@@ -171,8 +169,7 @@
          [(2) (approx spec (loop impl rest))]
          [else (invalid! prog loc)])]
       [((list op args ...) (cons idx rest)) ; operator
-       (let seek ([elts (cons op args)]
-                  [idx idx])
+       (let seek ([elts (cons op args)] [idx idx])
          (cond
            [(= idx 0) (cons (loop (car elts) rest) (cdr elts))]
            [(null? elts) (invalid! prog loc)]
diff --git a/src/utils/timeline.rkt b/src/utils/timeline.rkt
index 9841e1481..fa7164717 100644
--- a/src/utils/timeline.rkt
+++ b/src/utils/timeline.rkt
@@ -39,8 +39,7 @@
 
   (unless (*timeline-disabled*)
     (when (pair? (unbox (*timeline*)))
-      (for ([key (in-list always-compact)]
-            #:when (hash-has-key? (car (unbox (*timeline*))) key))
+      (for ([key (in-list always-compact)] #:when (hash-has-key? (car (unbox (*timeline*))) key))
         (timeline-compact! key)))
     (define live-memory (current-memory-use #f))
     (define alloc-memory (current-memory-use 'cumulative))
@@ -72,8 +71,7 @@
 
 (define (timeline-adjust! type key . values)
   (unless (*timeline-disabled*)
-    (for/first ([cell (unbox (*timeline*))]
-                #:when (equal? (hash-ref cell 'type) (~a type)))
+    (for/first ([cell (unbox (*timeline*))] #:when (equal? (hash-ref cell 'type) (~a type)))
       (hash-set! cell key values)
       true)
     (void)))
@@ -131,8 +129,7 @@
             (current-inexact-milliseconds)
             'memory
             (list (list (current-memory-use #f) (current-memory-use 'cumulative)))))
-  (reverse (for/list ([evt (unbox (*timeline*))]
-                      [next (cons end (unbox (*timeline*)))])
+  (reverse (for/list ([evt (unbox (*timeline*))] [next (cons end (unbox (*timeline*)))])
              (define evt* (hash-copy evt))
              (hash-update! evt* 'time (λ (v) (- (hash-ref next 'time) v)))
              (hash-update! evt* 'memory (λ (v) (diff-memory-records (hash-ref next 'memory) v)))
@@ -166,22 +163,18 @@
           (hash-update! groups
                         key
                         (λ (old)
-                          (for/list ([value2 old]
-                                     [(value1 fn) (in-dict values)])
+                          (for/list ([value2 old] [(value1 fn) (in-dict values)])
                             (fn value2 value1))))
           (hash-set! groups key (map car values))))
     (for/list ([(k v) (in-hash groups)])
-      (let loop ([fields fields]
-                 [k k]
-                 [v v])
+      (let loop ([fields fields] [k k] [v v])
         (match* (fields k v)
           [((cons #f f*) (cons k k*) v) (cons k (loop f* k* v))]
           [((cons _ f*) k (cons v v*)) (cons v (loop f* k v*))]
           [('() '() '()) '()])))))
 
 (define (merge-sampling-tables l1 l2)
-  (let loop ([l1 (sort l1 < #:key first)]
-             [l2 (sort l2 < #:key first)])
+  (let loop ([l1 (sort l1 < #:key first)] [l2 (sort l2 < #:key first)])
     (match-define (list n1 t1) (car l1))
     (match-define (list n2 t2) (car l2))
     (define rec (list n1 (hash-union t1 t2 #:combine +)))
@@ -235,11 +228,9 @@
 (define (timeline-merge . timelines)
   ;; The timelines in this case are JSON objects, as above
   (define types (make-hash))
-  (for* ([tl (in-list timelines)]
-         [event tl])
+  (for* ([tl (in-list timelines)] [event tl])
     (define data (hash-ref! types (hash-ref event 'type) (make-hash)))
-    (for ([(k v) (in-dict event)]
-          #:when (hash-ref timeline-types k #f))
+    (for ([(k v) (in-dict event)] #:when (hash-ref timeline-types k #f))
       (if (hash-has-key? data k)
           (hash-update! data k (λ (old) ((hash-ref timeline-types k) v old)))
           (hash-set! data k v))))

From 241516d7caeb16f62e567e4b3c7da7c6260616c3 Mon Sep 17 00:00:00 2001
From: JJponce0913 <u1398911@umail.utah.edu>
Date: Thu, 17 Oct 2024 07:53:15 -0600
Subject: [PATCH 7/8] Small fix

---
 src/core/rules.rkt | 42 +++++++++++++++++++++++++++++++++++++-----
 1 file changed, 37 insertions(+), 5 deletions(-)

diff --git a/src/core/rules.rkt b/src/core/rules.rkt
index abc2ef503..052a7b880 100644
--- a/src/core/rules.rkt
+++ b/src/core/rules.rkt
@@ -171,9 +171,9 @@
                  [associate-*l* (* (* a b) c) (* a (* b c))]
                  [associate-*r/ (* a (/ b c)) (/ (* a b) c)]
                  [associate-*l/ (* (/ a b) c) (/ (* a c) b)]
-                 [associate-/r* (/ a (* b c)) (/ (/ a b) c)] ;
+                 [associate-/r* (/ a (* b c)) (/ (/ a b) c)]
                  [associate-/r/ (/ a (/ b c)) (* (/ a b) c)]
-                 [associate-/l/ (/ (/ b c) a) (/ b (* c a))] ;
+                 [associate-/l/ (/ (/ b c) a) (/ b (* c a))]
                  [associate-/l* (/ (* b c) a) (* b (/ c a))])
 
 ; Counting
@@ -253,6 +253,33 @@
                  [flip-+ (+ a b) (/ (- (* a a) (* b b)) (- a b))]
                  [flip-- (- a b) (/ (- (* a a) (* b b)) (+ a b))])
 
+; Specialized numerical functions
+; TODO: These are technically rules over impls
+;
+; (define-ruleset* special-numerical-reduce
+;                  (numerics simplify)
+;                  #:type ([x real] [y real] [z real])
+;                  [log1p-expm1 (log1p (expm1 x)) x]
+;                  [hypot-1-def (sqrt (+ 1 (* y y))) (hypot 1 y)]
+;                  [fmm-def (- (* x y) z) (fma x y (neg z))]
+;                  [fmm-undef (fma x y (neg z)) (- (* x y) z)])
+
+; (define-ruleset* special-numerical-expand
+;                  (numerics)
+;                  #:type ([x real] [y real])
+;                  [log1p-expm1-u x (log1p (expm1 x))]
+;                  [expm1-log1p-u x (expm1 (log1p x))])
+
+; (define-ruleset* numerics-papers
+;                  (numerics)
+;                  #:type ([a real] [b real] [c real] [d real])
+;                  ;  "Further Analysis of Kahan's Algorithm for
+;                  ;   the Accurate Computation of 2x2 Determinants"
+;                  ;  Jeannerod et al., Mathematics of Computation, 2013
+;                  ;
+;                  ;  a * b - c * d  ===> fma(a, b, -(d * c)) + fma(-d, c, d * c)
+;                  [prod-diff (- (* a b) (* c d)) (+ (fma a b (neg (* d c))) (fma (neg d) c (* d c)))])
+
 ; Identity
 (define-ruleset* id-reduce
                  (arithmetic simplify sound)
@@ -351,6 +378,7 @@
                  #:type ([a real] [b real] [c real] [d real])
                  [frac-2neg-rev (/ (neg a) (neg b)) (/ a b)])
 
+
 ; Square root
 (define-ruleset* squares-reduce
                  (arithmetic simplify sound)
@@ -583,10 +611,14 @@
                  [diff-log (- (log a) (log b)) (log (/ a b))]
                  [neg-log (neg (log a)) (log (/ 1 a))])
 
-#| (define-ruleset* log-factor
+
+(define-ruleset* log2-factor
                  (exponents sound)
-                 #:type ([a real] [b real])                 
-                  [2log (/ (log x) (log 2)) (log2 a)] |#
+                 #:type ([a real] [b real])
+                 [log2-expand (log x 2) (/ (log x) (log 2))]
+                 [log2-expand-rev (/ (log x) (log 2)) (log x 2)])                 
+
+
 ; Trigonometry
 (define-ruleset* trig-reduce-fp-sound
                  (trigonometry simplify fp-safe sound)

From a2a530b2a66c05b6d0ad1908cf700393fe4f9dff Mon Sep 17 00:00:00 2001
From: JJponce0913 <u1398911@umail.utah.edu>
Date: Thu, 17 Oct 2024 10:12:37 -0600
Subject: [PATCH 8/8] turning off localize costs

---
 src/core/mainloop.rkt | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/src/core/mainloop.rkt b/src/core/mainloop.rkt
index b69c7a24a..bae91aca4 100644
--- a/src/core/mainloop.rkt
+++ b/src/core/mainloop.rkt
@@ -177,7 +177,7 @@
   (define localized-exprs empty)
   (define repr (context-repr (*context*)))
 
-  (when (flag-set? 'localize 'costs)
+  #| (when (flag-set? 'localize 'costs)
     (define loc-costss (batch-localize-costs exprs (*context*)))
     (define cost-localized
       (for/list ([loc-costs (in-list loc-costss)]
@@ -186,7 +186,7 @@
                  [_ (in-range (*localize-expressions-limit*))])
         (timeline-push! 'locations (~a expr) "cost-diff" cost-diff)
         expr))
-    (set! localized-exprs (remove-duplicates (append localized-exprs cost-localized))))
+    (set! localized-exprs (remove-duplicates (append localized-exprs cost-localized)))) |#
 
   (timeline-event! 'localize)
   (when (flag-set? 'localize 'errors)