ParityStarter

General parity through the public natural-number entrypoint

Open in Workbench View on GitHub

1-- General parity through the public natural-number entrypoint.2-- Part of the Grace17 proof assistant for mathematics based on set theory.3-- Copyright (c) 2026 Grant Passmore.4-- Released under the Apache License 2.0. See LICENSE in the repository root.5-- Authors: Grant Passmore67module User.ParityStarter8import Grace.Cumulus.Nat910theorem every_natural_has_parity (n : Nat)11  shows Even(n) ∨ Odd(n)12proof13  exact parity.exhaustive at n with *1415theorem consecutive_numbers_have_opposite_parity (n : Nat)16  shows (Even(n) ∧ Odd(succ(n))) ∨ (Odd(n) ∧ Even(succ(n)))17proof18  have alternatives := parity.exhaustive at n with *19  have fromEven := Odd.succ_of_even at n20  have fromOdd := Even.succ_of_odd at n21  tauto2223theorem two_odd_counts_make_even (a b : Set)24  requires first : Odd(a)25  requires second : Odd(b)26  shows Even(add(a, b))27proof28  exact Odd.add_odd at a, b with *2930theorem double_plus_one_is_odd (n : Nat)31  shows Odd(2 * n + 1)32proof33  have result := Odd.double_successor at n with *34  rw mul.two_left35  rw add.right_one36  exact result37