branch-cuts

Case set `df65d778fc5c`

case	sympy best	sympy-ask	sympy-refine	sympy-simplify	wolfram best	wolfram-fullsimplify	wolfram-refine	wolfram-simplify
demo-atan2-01 true	true ✓	no verdict	true ✓	true ✓	true ✓	true ✓	true ✓	true ✓
demo-atan2-02 false	false ✓	no verdict	false ✓	false ✓	false ✓	false ✓	false ✓	false ✓
demo-log-01 true	true ✓	no verdict	no verdict	true ✓	true ✓	true ✓	no verdict	true ✓
demo-log-02 contingent	no verdict ✓	no verdict ✓	no verdict ✓	no verdict ✓	no verdict ✓	no verdict ✓	no verdict ✓	no verdict ✓
demo-log-03 false	false ✓	false ✓	no verdict	false ✓	false ✓	false ✓	false ✓	false ✓

demo-atan2-01

Given

\(x, y \in \mathbb{R},\quad x > 0\)

Claim

\(\displaystyle \operatorname{atan2}\left(y, x\right) = \arctan\left(\frac{y}{x}\right)\)

Expected

true equal at every admissible point

the two sides are equal at every admissible point

(case demo-atan2-01 (category branch-cuts)
  (var x real) (var y real)
  (assume (positive x))
  (ask (= (atan2 y x) (atan (/ y x))))
  (expect true))

demo-atan2-02

Given

\(x, y \in \mathbb{R},\quad x < 0,\quad y > 0\)

Claim

\(\displaystyle \operatorname{atan2}\left(y, x\right) \neq \arctan\left(\frac{y}{x}\right)\)

Expected

false unequal at every admissible point (e.g. at \(y = 1, x = -1\))

the two sides differ at every admissible point

witness (false): \(y = 1, x = -1\)

(case demo-atan2-02 (category branch-cuts)
  (var x real) (var y real)
  (assume (negative x)) (assume (positive y))
  (ask (= (atan2 y x) (atan (/ y x))))
  (expect false)
  (witness false (y 1) (x -1)))

demo-log-01

Given

\(x, y \in \mathbb{R},\quad x > 0,\quad y > 0\)

Claim

\(\displaystyle \log\left(x \, y\right) = \log x + \log y\)

Expected

true equal at every admissible point

the two sides are equal at every admissible point

(case demo-log-01 (category branch-cuts)
  (var x real) (var y real)
  (assume (positive x)) (assume (positive y))
  (ask (= (log (* x y)) (+ (log x) (log y))))
  (expect true))

demo-log-02

Given

\(z, w \in \mathbb{C},\quad z \neq 0,\quad w \neq 0\)

Claim

\(\displaystyle \log\left(z \, w\right) \overset{?}{=} \log z + \log w\)

Expected

contingent true at \(z = 1, w = 1\); false at \(z = -1, w = -1\)

equal at some admissible points, different at others

witness (true): \(z = 1, w = 1\)

witness (false): \(z = -1, w = -1\)

Lean proof: included

(case demo-log-02 (category branch-cuts)
  (var z complex) (var w complex)
  (assume (nonzero z)) (assume (nonzero w))
  (ask (= (log (* z w)) (+ (log z) (log w))))
  (expect contingent)
  (witness true (z 1) (w 1)
    (lean-proof "simp [AE.nonzero, AE.nonzero.D, AE.log]"))
  (witness false (z -1) (w -1)
    (lean-proof "refine ⟨by simp [AE.nonzero, AE.nonzero.D], by simp [AE.nonzero, AE.nonzero.D], by norm_num, fun h => ?_⟩; have h1 := congrArg Complex.im h; simp [AE.log, Complex.log_neg_one] at h1; linarith [Real.pi_pos]")))

demo-log-03

Given

\(x \in \mathbb{R},\quad x < 0\)

Claim

\(\displaystyle \log x \neq \log\left(-x\right)\)

Expected

false unequal at every admissible point (e.g. at \(x = -1\))

the two sides differ at every admissible point

witness (false): \(x = -1\)

log x has imaginary part pi for x < 0, while log(-x) is real.

Lean proof: included

(case demo-log-03 (category branch-cuts)
  (note "log x has imaginary part pi for x < 0, while log(-x) is real.")
  (var x real)
  (assume (negative x))
  (ask (= (log x) (log (- x))))
  (expect false)
  (witness false (x -1)
    (lean-proof "refine ⟨by simp [AE.IsReal], by simp [AE.negative, AE.negative.D, AE.real, AE.real.D, AE.lt, AE.re, AE.im, AE.IsReal], by norm_num, ?_⟩; simp [AE.log, Complex.log_neg_one, Real.pi_ne_zero, Complex.I_ne_zero]"))
  (lean-proof "have hx : x.im = 0 := hd0; have hr : x.re < 0 := (by simpa [AE.negative, AE.lt, AE.re] using h0.2.2); have e : x = ((x.re : ℝ) : ℂ) := Complex.ext (by simp) (by simp [hx]); refine ⟨⟨fun h => by simp [h] at hr, fun h => by simp [neg_eq_zero.mp h] at hr⟩, fun h => ?_⟩; have h1 := congrArg Complex.im h; rw [e, AE.log, AE.log, ← Complex.ofReal_neg, AE.log_neg_real _ hr, Complex.log_im, Complex.arg_ofReal_of_nonneg (by linarith)] at h1; exact Real.pi_ne_zero h1"))

Case set `03f5149718d0`

case	sympy best	sympy-ask	sympy-refine	sympy-simplify	wolfram best	wolfram-fullsimplify	wolfram-refine	wolfram-simplify
demo-atan2-01 true	true ✓	no verdict	true ✓	true ✓	true ✓	true ✓	true ✓	true ✓
demo-atan2-02 false	false ✓	no verdict	false ✓	false ✓	false ✓	false ✓	false ✓	false ✓
demo-log-01 true	true ✓	no verdict	no verdict	true ✓	true ✓	true ✓	no verdict	true ✓
demo-log-02 contingent	no verdict	no verdict	no verdict	no verdict	no verdict	no verdict	no verdict	no verdict
demo-log-03 false	false ✓	false ✓	no verdict	false ✓	false ✓	false ✓	false ✓	false ✓

demo-atan2-01

Given

\(x, y \in \mathbb{R},\quad x > 0\)

Claim

\(\displaystyle \operatorname{atan2}\left(y, x\right) = \arctan\left(\frac{y}{x}\right)\)

Expected

true equal at every admissible point

the two sides are equal at every admissible point

(case demo-atan2-01 (category branch-cuts)
  (var x real) (var y real)
  (assume (positive x))
  (ask (= (atan2 y x) (atan (/ y x))))
  (expect true))

demo-atan2-02

Given

\(x, y \in \mathbb{R},\quad x < 0,\quad y > 0\)

Claim

\(\displaystyle \operatorname{atan2}\left(y, x\right) \neq \arctan\left(\frac{y}{x}\right)\)

Expected

false unequal at every admissible point (e.g. at \(y = 1, x = -1\))

the two sides differ at every admissible point

witness (false): \(y = 1, x = -1\)

(case demo-atan2-02 (category branch-cuts)
  (var x real) (var y real)
  (assume (negative x)) (assume (positive y))
  (ask (= (atan2 y x) (atan (/ y x))))
  (expect false)
  (witness false (y 1) (x -1)))

demo-log-01

Given

\(x, y \in \mathbb{R},\quad x > 0,\quad y > 0\)

Claim

\(\displaystyle \log\left(x \, y\right) = \log x + \log y\)

Expected

true equal at every admissible point

the two sides are equal at every admissible point

(case demo-log-01 (category branch-cuts)
  (var x real) (var y real)
  (assume (positive x)) (assume (positive y))
  (ask (= (log (* x y)) (+ (log x) (log y))))
  (expect true))

demo-log-02

Given

\(z, w \in \mathbb{C},\quad z \neq 0,\quad w \neq 0\)

Claim

\(\displaystyle \log\left(z \, w\right) \overset{?}{=} \log z + \log w\)

Expected

contingent true at \(z = 1, w = 1\); false at \(z = -1, w = -1\)

equal at some admissible points, different at others

witness (true): \(z = 1, w = 1\)

witness (false): \(z = -1, w = -1\)

Lean proof: included

(case demo-log-02 (category branch-cuts)
  (var z complex) (var w complex)
  (assume (nonzero z)) (assume (nonzero w))
  (ask (= (log (* z w)) (+ (log z) (log w))))
  (expect contingent)
  (witness true (z 1) (w 1)
    (lean-proof "simp [AE.nonzero, AE.nonzero.D, AE.log]"))
  (witness false (z -1) (w -1)
    (lean-proof "refine ⟨by simp [AE.nonzero, AE.nonzero.D], by simp [AE.nonzero, AE.nonzero.D], by norm_num, fun h => ?_⟩; have h1 := congrArg Complex.im h; simp [AE.log, Complex.log_neg_one] at h1; linarith [Real.pi_pos]")))

demo-log-03

Given

\(x \in \mathbb{R},\quad x < 0\)

Claim

\(\displaystyle \log x \neq \log\left(-x\right)\)

Expected

false unequal at every admissible point (e.g. at \(x = -1\))

the two sides differ at every admissible point

witness (false): \(x = -1\)

log x has imaginary part pi for x < 0, while log(-x) is real.

Lean proof: included

(case demo-log-03 (category branch-cuts)
  (note "log x has imaginary part pi for x < 0, while log(-x) is real.")
  (var x real)
  (assume (negative x))
  (ask (= (log x) (log (- x))))
  (expect false)
  (witness false (x -1)
    (lean-proof "refine ⟨by simp [AE.IsReal], by simp [AE.negative, AE.negative.D, AE.real, AE.real.D, AE.lt, AE.re, AE.im, AE.IsReal], by norm_num, ?_⟩; simp [AE.log, Complex.log_neg_one, Real.pi_ne_zero, Complex.I_ne_zero]"))
  (lean-proof "have hx : x.im = 0 := hd0; have hr : x.re < 0 := (by simpa [AE.negative, AE.lt, AE.re] using h0.2.2); have e : x = ((x.re : ℝ) : ℂ) := Complex.ext (by simp) (by simp [hx]); refine ⟨⟨fun h => by simp [h] at hr, fun h => by simp [neg_eq_zero.mp h] at hr⟩, fun h => ?_⟩; have h1 := congrArg Complex.im h; rw [e, AE.log, AE.log, ← Complex.ofReal_neg, AE.log_neg_real _ hr, Complex.log_im, Complex.arg_ofReal_of_nonneg (by linarith)] at h1; exact Real.pi_ne_zero h1"))

Case set `d7af4def9aaa`

case	sympy best	sympy-ask	sympy-refine	sympy-simplify	wolfram best	wolfram-fullsimplify	wolfram-refine	wolfram-simplify
demo-atan2-01 true	true ✓	no verdict	true ✓	true ✓	true ✓	true ✓	true ✓	true ✓
demo-atan2-02 false	false ✓	no verdict	false ✓	false ✓	false ✓	false ✓	false ✓	false ✓
demo-log-01 true	true ✓	no verdict	no verdict	true ✓	true ✓	true ✓	no verdict	true ✓
demo-log-02 contingent	no verdict	no verdict	no verdict	no verdict	no verdict	no verdict	no verdict	no verdict
demo-log-03 false	false ✓	false ✓	no verdict	false ✓	false ✓	false ✓	false ✓	false ✓

demo-atan2-01

Given

\(x, y \in \mathbb{R},\quad x > 0\)

Claim

\(\displaystyle \operatorname{atan2}\left(y, x\right) = \arctan\left(\frac{y}{x}\right)\)

Expected

true equal at every admissible point

the two sides are equal at every admissible point

(case demo-atan2-01 (category branch-cuts)
  (var x real) (var y real)
  (assume (positive x))
  (ask (= (atan2 y x) (atan (/ y x))))
  (expect true))

demo-atan2-02

Given

\(x, y \in \mathbb{R},\quad x < 0,\quad y > 0\)

Claim

\(\displaystyle \operatorname{atan2}\left(y, x\right) \neq \arctan\left(\frac{y}{x}\right)\)

Expected

false unequal at every admissible point (e.g. at \(y = 1, x = -1\))

the two sides differ at every admissible point

witness (false): \(y = 1, x = -1\)

(case demo-atan2-02 (category branch-cuts)
  (var x real) (var y real)
  (assume (negative x)) (assume (positive y))
  (ask (= (atan2 y x) (atan (/ y x))))
  (expect false)
  (witness false (y 1) (x -1)))

demo-log-01

Given

\(x, y \in \mathbb{R},\quad x > 0,\quad y > 0\)

Claim

\(\displaystyle \log\left(x \, y\right) = \log x + \log y\)

Expected

true equal at every admissible point

the two sides are equal at every admissible point

(case demo-log-01 (category branch-cuts)
  (var x real) (var y real)
  (assume (positive x)) (assume (positive y))
  (ask (= (log (* x y)) (+ (log x) (log y))))
  (expect true))

demo-log-02

Given

\(z, w \in \mathbb{C},\quad z \neq 0,\quad w \neq 0\)

Claim

\(\displaystyle \log\left(z \, w\right) \overset{?}{=} \log z + \log w\)

Expected

contingent true at \(z = 1, w = 1\); false at \(z = -1, w = -1\)

equal at some admissible points, different at others

witness (true): \(z = 1, w = 1\)

witness (false): \(z = -1, w = -1\)

Lean proof: included

(case demo-log-02 (category branch-cuts)
  (var z complex) (var w complex)
  (assume (nonzero z)) (assume (nonzero w))
  (ask (= (log (* z w)) (+ (log z) (log w))))
  (expect contingent)
  (witness true (z 1) (w 1)
    (lean-proof "simp [AE.nonzero, AE.nonzero.D, AE.log]"))
  (witness false (z -1) (w -1)
    (lean-proof "refine ⟨by simp [AE.nonzero, AE.nonzero.D], by simp [AE.nonzero, AE.nonzero.D], by norm_num, fun h => ?_⟩; have h1 := congrArg Complex.im h; simp [AE.log, Complex.log_neg_one] at h1; linarith [Real.pi_pos]")))

demo-log-03

Given

\(x \in \mathbb{R},\quad x < 0\)

Claim

\(\displaystyle \log x \neq \log\left(-x\right)\)

Expected

false unequal at every admissible point (e.g. at \(x = -1\))

the two sides differ at every admissible point

witness (false): \(x = -1\)

log x has imaginary part pi for x < 0, while log(-x) is real.

Lean proof: included

(case demo-log-03 (category branch-cuts)
  (note "log x has imaginary part pi for x < 0, while log(-x) is real.")
  (var x real)
  (assume (negative x))
  (ask (= (log x) (log (- x))))
  (expect false)
  (witness false (x -1)
    (lean-proof "refine ⟨by simp [AE.IsReal], by simp [AE.negative, AE.negative.D, AE.real, AE.real.D, AE.lt, AE.re, AE.im, AE.IsReal], by norm_num, ?_⟩; simp [AE.log, Complex.log_neg_one, Real.pi_ne_zero, Complex.I_ne_zero]"))
  (lean-proof "have hx : x.im = 0 := hd0; have hr : x.re < 0 := (by simpa [AE.negative, AE.lt, AE.re] using h0.2.2); have e : x = ((x.re : ℝ) : ℂ) := Complex.ext (by simp) (by simp [hx]); refine ⟨⟨fun h => by simp [h] at hr, fun h => by simp [neg_eq_zero.mp h] at hr⟩, fun h => ?_⟩; have h1 := congrArg Complex.im h; rw [e, AE.log, AE.log, ← Complex.ofReal_neg, AE.log_neg_real _ hr, Complex.log_im, Complex.arg_ofReal_of_nonneg (by linarith)] at h1; exact Real.pi_ne_zero h1"))

branch-cuts

Case set df65d778fc5c

Case set 03f5149718d0

Case set d7af4def9aaa

Case set `df65d778fc5c`

Case set `03f5149718d0`

Case set `d7af4def9aaa`