← suite examples

sign

Case set df65d778fc5c

casesympy bestsympy-asksympy-refinesympy-simplifywolfram best wolfram-fullsimplify wolfram-refine wolfram-simplify
demo-nonzero-01 truetrue ✓no verdictno verdicttrue ✓true ✓true ✓true ✓true ✓
demo-sign-02 truetrue ✓no verdicttrue ✓true ✓true ✓true ✓no verdicttrue ✓
demo-sign-03 contingentno verdict ✓no verdict ✓no verdict ✓no verdict ✓no verdict ✓no verdict ✓no verdict ✓no verdict ✓
demo-sign-04 trueno verdictno verdictno verdictno verdicttrue ✓true ✓no verdictno verdict
demo-sign-05 truetrue ✓no verdicttrue ✓true ✓true ✓true ✓true ✓true ✓

demo-nonzero-01

Given
\(z \in \mathbb{C},\quad z \in i\mathbb{R}\)
Claim
\(\displaystyle \left|\operatorname{sgn}\left(z\right)\right| = 1\)
Expected
true equal at every admissible point

the two sides are equal at every admissible point

|sign z| = 1 says z != 0. Trap: SymPy's Q.nonzero means real-and-nonzero; our nonzero does not.

(case demo-nonzero-01 (category sign)
  (note "|sign z| = 1 says z != 0.  Trap: SymPy's Q.nonzero means real-and-nonzero; our nonzero does not.")
  (var z complex)
  (assume (imaginary z))
  (ask (= (abs (sign z)) 1))
  (expect true))

demo-sign-02

Given
\(x \in \mathbb{R},\quad x \neq 0\)
Claim
\(\displaystyle \operatorname{sgn}\left(x^{2}\right) = 1\)
Expected
true equal at every admissible point

the two sides are equal at every admissible point

(case demo-sign-02 (category sign)
  (var x real)
  (assume (nonzero x))
  (ask (= (sign (pow x 2)) 1))
  (expect true))

demo-sign-03

Given
\(x \in \mathbb{C},\quad x \neq 0\)
Claim
\(\displaystyle \operatorname{sgn}\left(x^{2}\right) \overset{?}{=} 1\)
Expected
contingent true at \(x = 1\); false at \(x = i\)

equal at some admissible points, different at others

witness (true): \(x = 1\)

witness (false): \(x = i\)

Same as demo-sign-02 but x is complex: sign(1^2) = 1, but sign(i^2) = -1.

(case demo-sign-03 (category sign)
  (note "Same as demo-sign-02 but x is complex: sign(1^2) = 1, but sign(i^2) = -1.")
  (var x complex)
  (assume (nonzero x))
  (ask (= (sign (pow x 2)) 1))
  (expect contingent)
  (witness true (x 1))
  (witness false (x i)))

demo-sign-04

Given
\(z \in \mathbb{C}\)
Claim
\(\displaystyle \left|z \, \overline{z}\right| = z \, \overline{z}\)
Expected
true equal at every admissible point

the two sides are equal at every admissible point

z conj(z) = |z|^2 is a nonnegative real, so it equals its absolute value.

(case demo-sign-04 (category sign)
  (note "z conj(z) = |z|^2 is a nonnegative real, so it equals its absolute value.")
  (var z complex)
  (ask (= (abs (* z (conj z))) (* z (conj z))))
  (expect true))

demo-sign-05

Given
\(x, y \in \mathbb{R},\quad x > 0,\quad y < 0\)
Claim
\(\displaystyle \left|x - y\right| = x - y\)
Expected
true equal at every admissible point

the two sides are equal at every admissible point

(case demo-sign-05 (category sign)
  (var x real) (var y real)
  (assume (positive x)) (assume (negative y))
  (ask (= (abs (- x y)) (- x y)))
  (expect true))

Case set 03f5149718d0

casesympy bestsympy-asksympy-refinesympy-simplifywolfram best wolfram-fullsimplify wolfram-refine wolfram-simplify
demo-nonzero-01 truetrue ✓no verdictno verdicttrue ✓true ✓true ✓true ✓true ✓
demo-sign-02 truetrue ✓no verdicttrue ✓true ✓true ✓true ✓no verdicttrue ✓
demo-sign-03 contingentno verdictno verdictno verdictno verdictno verdictno verdictno verdictno verdict
demo-sign-04 trueno verdictno verdictno verdictno verdicttrue ✓true ✓no verdictno verdict
demo-sign-05 truetrue ✓no verdicttrue ✓true ✓true ✓true ✓true ✓true ✓

demo-nonzero-01

Given
\(z \in \mathbb{C},\quad z \in i\mathbb{R}\)
Claim
\(\displaystyle \left|\operatorname{sgn}\left(z\right)\right| = 1\)
Expected
true equal at every admissible point

the two sides are equal at every admissible point

|sign z| = 1 says z != 0. Trap: SymPy's Q.nonzero means real-and-nonzero; our nonzero does not.

(case demo-nonzero-01 (category sign)
  (note "|sign z| = 1 says z != 0.  Trap: SymPy's Q.nonzero means real-and-nonzero; our nonzero does not.")
  (var z complex)
  (assume (imaginary z))
  (ask (= (abs (sign z)) 1))
  (expect true))

demo-sign-02

Given
\(x \in \mathbb{R},\quad x \neq 0\)
Claim
\(\displaystyle \operatorname{sgn}\left(x^{2}\right) = 1\)
Expected
true equal at every admissible point

the two sides are equal at every admissible point

(case demo-sign-02 (category sign)
  (var x real)
  (assume (nonzero x))
  (ask (= (sign (pow x 2)) 1))
  (expect true))

demo-sign-03

Given
\(x \in \mathbb{C},\quad x \neq 0\)
Claim
\(\displaystyle \operatorname{sgn}\left(x^{2}\right) \overset{?}{=} 1\)
Expected
contingent true at \(x = 1\); false at \(x = i\)

equal at some admissible points, different at others

witness (true): \(x = 1\)

witness (false): \(x = i\)

Same as demo-sign-02 but x is complex: sign(1^2) = 1, but sign(i^2) = -1.

(case demo-sign-03 (category sign)
  (note "Same as demo-sign-02 but x is complex: sign(1^2) = 1, but sign(i^2) = -1.")
  (var x complex)
  (assume (nonzero x))
  (ask (= (sign (pow x 2)) 1))
  (expect contingent)
  (witness true (x 1))
  (witness false (x i)))

demo-sign-04

Given
\(z \in \mathbb{C}\)
Claim
\(\displaystyle \left|z \, \overline{z}\right| = z \, \overline{z}\)
Expected
true equal at every admissible point

the two sides are equal at every admissible point

z conj(z) = |z|^2 is a nonnegative real, so it equals its absolute value.

(case demo-sign-04 (category sign)
  (note "z conj(z) = |z|^2 is a nonnegative real, so it equals its absolute value.")
  (var z complex)
  (ask (= (abs (* z (conj z))) (* z (conj z))))
  (expect true))

demo-sign-05

Given
\(x, y \in \mathbb{R},\quad x > 0,\quad y < 0\)
Claim
\(\displaystyle \left|x - y\right| = x - y\)
Expected
true equal at every admissible point

the two sides are equal at every admissible point

(case demo-sign-05 (category sign)
  (var x real) (var y real)
  (assume (positive x)) (assume (negative y))
  (ask (= (abs (- x y)) (- x y)))
  (expect true))

Case set d7af4def9aaa

casesympy bestsympy-asksympy-refinesympy-simplifywolfram best wolfram-fullsimplify wolfram-refine wolfram-simplify
demo-nonzero-01 truetrue ✓no verdictno verdicttrue ✓true ✓true ✓true ✓true ✓
demo-sign-02 truetrue ✓no verdicttrue ✓true ✓true ✓true ✓no verdicttrue ✓
demo-sign-03 contingentno verdictno verdictno verdictno verdictno verdictno verdictno verdictno verdict
demo-sign-04 trueno verdictno verdictno verdictno verdicttrue ✓true ✓no verdictno verdict
demo-sign-05 truetrue ✓no verdictno verdicttrue ✓true ✓true ✓true ✓true ✓

demo-nonzero-01

Given
\(z \in \mathbb{C},\quad z \in i\mathbb{R}\)
Claim
\(\displaystyle \left|\operatorname{sgn}\left(z\right)\right| = 1\)
Expected
true equal at every admissible point

the two sides are equal at every admissible point

|sign z| = 1 says z != 0. Trap: SymPy's Q.nonzero means real-and-nonzero; our nonzero does not.

(case demo-nonzero-01 (category sign)
  (note "|sign z| = 1 says z != 0.  Trap: SymPy's Q.nonzero means real-and-nonzero; our nonzero does not.")
  (var z complex)
  (assume (imaginary z))
  (ask (= (abs (sign z)) 1))
  (expect true))

demo-sign-02

Given
\(x \in \mathbb{R},\quad x \neq 0\)
Claim
\(\displaystyle \operatorname{sgn}\left(x^{2}\right) = 1\)
Expected
true equal at every admissible point

the two sides are equal at every admissible point

(case demo-sign-02 (category sign)
  (var x real)
  (assume (nonzero x))
  (ask (= (sign (pow x 2)) 1))
  (expect true))

demo-sign-03

Given
\(x \in \mathbb{C},\quad x \neq 0\)
Claim
\(\displaystyle \operatorname{sgn}\left(x^{2}\right) \overset{?}{=} 1\)
Expected
contingent true at \(x = 1\); false at \(x = i\)

equal at some admissible points, different at others

witness (true): \(x = 1\)

witness (false): \(x = i\)

Same as demo-sign-02 but x is complex: sign(1^2) = 1, but sign(i^2) = -1.

(case demo-sign-03 (category sign)
  (note "Same as demo-sign-02 but x is complex: sign(1^2) = 1, but sign(i^2) = -1.")
  (var x complex)
  (assume (nonzero x))
  (ask (= (sign (pow x 2)) 1))
  (expect contingent)
  (witness true (x 1))
  (witness false (x i)))

demo-sign-04

Given
\(z \in \mathbb{C}\)
Claim
\(\displaystyle \left|z \, \overline{z}\right| = z \, \overline{z}\)
Expected
true equal at every admissible point

the two sides are equal at every admissible point

z conj(z) = |z|^2 is a nonnegative real, so it equals its absolute value.

(case demo-sign-04 (category sign)
  (note "z conj(z) = |z|^2 is a nonnegative real, so it equals its absolute value.")
  (var z complex)
  (ask (= (abs (* z (conj z))) (* z (conj z))))
  (expect true))

demo-sign-05

Given
\(x, y \in \mathbb{R},\quad x > 0,\quad y < 0\)
Claim
\(\displaystyle \left|x - y\right| = x - y\)
Expected
true equal at every admissible point

the two sides are equal at every admissible point

(case demo-sign-05 (category sign)
  (var x real) (var y real)
  (assume (positive x)) (assume (negative y))
  (ask (= (abs (- x y)) (- x y)))
  (expect true))