← suite examples

parity

Case set df65d778fc5c

casesympy bestsympy-asksympy-refinesympy-simplifywolfram best wolfram-fullsimplify wolfram-refine wolfram-simplify
demo-parity-01 truetrue ✓no verdicttrue ✓true ✓true ✓true ✓true ✓true ✓
demo-parity-02 falsefalse ✓false ✓false ✓false ✓false ✓false ✓false ✓false ✓
demo-parity-03 truetrue ✓true ✓true ✓true ✓true ✓true ✓true ✓true ✓
demo-parity-04 contingentno verdict ✓no verdict ✓no verdict ✓no verdict ✓no verdict ✓no verdict ✓no verdict ✓no verdict ✓
demo-parity-05 truetrue ✓no verdicttrue ✓true ✓true ✓true ✓true ✓true ✓

demo-parity-01

Given
\(n \in \mathbb{Z},\quad n \in 2\mathbb{Z} + 1\)
Claim
\(\displaystyle \left(-1\right)^{n + 1} = 1\)
Expected
true equal at every admissible point

the two sides are equal at every admissible point

(case demo-parity-01 (category parity)
  (var n integer)
  (assume (odd n))
  (ask (= (pow -1 (+ n 1)) 1))
  (expect true))

demo-parity-02

Given
\(n, m \in \mathbb{Z},\quad n \in 2\mathbb{Z} + 1,\quad m \in 2\mathbb{Z} + 1\)
Claim
\(\displaystyle \left(-1\right)^{n \, m} \neq 1\)
Expected
false unequal at every admissible point (e.g. at \(n = 1, m = 3\))

the two sides differ at every admissible point

witness (false): \(n = 1, m = 3\)

n m is odd, so (-1)^(n m) = -1: the difference is the constant -2.

(case demo-parity-02 (category parity)
  (note "n m is odd, so (-1)^(n m) = -1: the difference is the constant -2.")
  (var n integer) (var m integer)
  (assume (odd n)) (assume (odd m))
  (ask (= (pow -1 (* n m)) 1))
  (expect false)
  (witness false (n 1) (m 3)))

demo-parity-03

Given
\(n \in \mathbb{Z}\)
Claim
\(\displaystyle \left(-1\right)^{n \, \left(n + 1\right)} = 1\)
Expected
true equal at every admissible point

the two sides are equal at every admissible point

(case demo-parity-03 (category parity)
  (var n integer)
  (ask (= (pow -1 (* n (+ n 1))) 1))
  (expect true))

demo-parity-04

Given
\(n \in \mathbb{Z},\quad n \in 2\mathbb{Z}\)
Claim
\(\displaystyle i^{n} \overset{?}{=} 1\)
Expected
contingent true at \(n = 4\); false at \(n = 2\)

equal at some admissible points, different at others

witness (true): \(n = 4\)

witness (false): \(n = 2\)

i^n = (-1)^(n/2) for even n. Written with (pow -1 (/ n 2)) it hits a SymPy 1.14 bug: ask(Q.zero((-1)**(k/2) - 1), Q.integer(k)) is False, though k = 4 gives 0.

(case demo-parity-04 (category parity)
  (note "i^n = (-1)^(n/2) for even n.  Written with (pow -1 (/ n 2)) it hits a SymPy 1.14 bug: ask(Q.zero((-1)**(k/2) - 1), Q.integer(k)) is False, though k = 4 gives 0.")
  (var n integer)
  (assume (even n))
  (ask (= (pow i n) 1))
  (expect contingent)
  (witness true (n 4))
  (witness false (n 2)))

demo-parity-05

Given
\(n, m \in \mathbb{Z},\quad n \in 2\mathbb{Z} + 1,\quad m \in 2\mathbb{Z} + 1\)
Claim
\(\displaystyle \left(-1\right)^{n \, m} = -1\)
Expected
true equal at every admissible point

the two sides are equal at every admissible point

(case demo-parity-05 (category parity)
  (var n integer) (var m integer)
  (assume (odd n)) (assume (odd m))
  (ask (= (pow -1 (* n m)) -1))
  (expect true))

Case set 03f5149718d0

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

demo-parity-01

Given
\(n \in \mathbb{Z},\quad n \in 2\mathbb{Z} + 1\)
Claim
\(\displaystyle \left(-1\right)^{n + 1} = 1\)
Expected
true equal at every admissible point

the two sides are equal at every admissible point

(case demo-parity-01 (category parity)
  (var n integer)
  (assume (odd n))
  (ask (= (pow -1 (+ n 1)) 1))
  (expect true))

demo-parity-02

Given
\(n, m \in \mathbb{Z},\quad n \in 2\mathbb{Z} + 1,\quad m \in 2\mathbb{Z} + 1\)
Claim
\(\displaystyle \left(-1\right)^{n \, m} \neq 1\)
Expected
false unequal at every admissible point (e.g. at \(n = 1, m = 3\))

the two sides differ at every admissible point

witness (false): \(n = 1, m = 3\)

n m is odd, so (-1)^(n m) = -1: the difference is the constant -2.

(case demo-parity-02 (category parity)
  (note "n m is odd, so (-1)^(n m) = -1: the difference is the constant -2.")
  (var n integer) (var m integer)
  (assume (odd n)) (assume (odd m))
  (ask (= (pow -1 (* n m)) 1))
  (expect false)
  (witness false (n 1) (m 3)))

demo-parity-03

Given
\(n \in \mathbb{Z}\)
Claim
\(\displaystyle \left(-1\right)^{n \, \left(n + 1\right)} = 1\)
Expected
true equal at every admissible point

the two sides are equal at every admissible point

(case demo-parity-03 (category parity)
  (var n integer)
  (ask (= (pow -1 (* n (+ n 1))) 1))
  (expect true))

demo-parity-04

Given
\(n \in \mathbb{Z},\quad n \in 2\mathbb{Z}\)
Claim
\(\displaystyle i^{n} \overset{?}{=} 1\)
Expected
contingent true at \(n = 4\); false at \(n = 2\)

equal at some admissible points, different at others

witness (true): \(n = 4\)

witness (false): \(n = 2\)

i^n = (-1)^(n/2) for even n. Written with (pow -1 (/ n 2)) it hits a SymPy 1.14 bug: ask(Q.zero((-1)**(k/2) - 1), Q.integer(k)) is False, though k = 4 gives 0.

(case demo-parity-04 (category parity)
  (note "i^n = (-1)^(n/2) for even n.  Written with (pow -1 (/ n 2)) it hits a SymPy 1.14 bug: ask(Q.zero((-1)**(k/2) - 1), Q.integer(k)) is False, though k = 4 gives 0.")
  (var n integer)
  (assume (even n))
  (ask (= (pow i n) 1))
  (expect contingent)
  (witness true (n 4))
  (witness false (n 2)))

demo-parity-05

Given
\(n, m \in \mathbb{Z},\quad n \in 2\mathbb{Z} + 1,\quad m \in 2\mathbb{Z} + 1\)
Claim
\(\displaystyle \left(-1\right)^{n \, m} = -1\)
Expected
true equal at every admissible point

the two sides are equal at every admissible point

(case demo-parity-05 (category parity)
  (var n integer) (var m integer)
  (assume (odd n)) (assume (odd m))
  (ask (= (pow -1 (* n m)) -1))
  (expect true))

Case set d7af4def9aaa

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

demo-parity-01

Given
\(n \in \mathbb{Z},\quad n \in 2\mathbb{Z} + 1\)
Claim
\(\displaystyle \left(-1\right)^{n + 1} = 1\)
Expected
true equal at every admissible point

the two sides are equal at every admissible point

(case demo-parity-01 (category parity)
  (var n integer)
  (assume (odd n))
  (ask (= (pow -1 (+ n 1)) 1))
  (expect true))

demo-parity-02

Given
\(n, m \in \mathbb{Z},\quad n \in 2\mathbb{Z} + 1,\quad m \in 2\mathbb{Z} + 1\)
Claim
\(\displaystyle \left(-1\right)^{n \, m} \neq 1\)
Expected
false unequal at every admissible point (e.g. at \(n = 1, m = 3\))

the two sides differ at every admissible point

witness (false): \(n = 1, m = 3\)

n m is odd, so (-1)^(n m) = -1: the difference is the constant -2.

(case demo-parity-02 (category parity)
  (note "n m is odd, so (-1)^(n m) = -1: the difference is the constant -2.")
  (var n integer) (var m integer)
  (assume (odd n)) (assume (odd m))
  (ask (= (pow -1 (* n m)) 1))
  (expect false)
  (witness false (n 1) (m 3)))

demo-parity-03

Given
\(n \in \mathbb{Z}\)
Claim
\(\displaystyle \left(-1\right)^{n \, \left(n + 1\right)} = 1\)
Expected
true equal at every admissible point

the two sides are equal at every admissible point

(case demo-parity-03 (category parity)
  (var n integer)
  (ask (= (pow -1 (* n (+ n 1))) 1))
  (expect true))

demo-parity-04

Given
\(n \in \mathbb{Z},\quad n \in 2\mathbb{Z}\)
Claim
\(\displaystyle i^{n} \overset{?}{=} 1\)
Expected
contingent true at \(n = 4\); false at \(n = 2\)

equal at some admissible points, different at others

witness (true): \(n = 4\)

witness (false): \(n = 2\)

i^n = (-1)^(n/2) for even n. Written with (pow -1 (/ n 2)) it hits a SymPy 1.14 bug: ask(Q.zero((-1)**(k/2) - 1), Q.integer(k)) is False, though k = 4 gives 0.

(case demo-parity-04 (category parity)
  (note "i^n = (-1)^(n/2) for even n.  Written with (pow -1 (/ n 2)) it hits a SymPy 1.14 bug: ask(Q.zero((-1)**(k/2) - 1), Q.integer(k)) is False, though k = 4 gives 0.")
  (var n integer)
  (assume (even n))
  (ask (= (pow i n) 1))
  (expect contingent)
  (witness true (n 4))
  (witness false (n 2)))

demo-parity-05

Given
\(n, m \in \mathbb{Z},\quad n \in 2\mathbb{Z} + 1,\quad m \in 2\mathbb{Z} + 1\)
Claim
\(\displaystyle \left(-1\right)^{n \, m} = -1\)
Expected
true equal at every admissible point

the two sides are equal at every admissible point

(case demo-parity-05 (category parity)
  (var n integer) (var m integer)
  (assume (odd n)) (assume (odd m))
  (ask (= (pow -1 (* n m)) -1))
  (expect true))