Grace/Cumulus/Nat/Parity.g17

Open in Workbench Download source

Imports

Order · Foundation

Declarations

Source

1-- Even and odd natural numbers, their dichotomy, and addition laws.2-- Part of Cumulus, the Grace17 mathematics library.3-- Copyright (c) 2026 Grant Passmore.4-- Released under the Apache License 2.0. See LICENSE in the repository root.5-- Authors: Grant Passmore67module Grace.Cumulus.Nat.Parity8import Order9import Foundation1011predicate Even (n : Set) := ∃ k ∈ ℕ, n = add(k, k)12predicate Odd (n : Set) := ∃ k ∈ ℕ, n = succ(add(k, k))1314theorem Even.double (k : Nat)15  shows Even(add(k, k))16proof17  unfold Even18  refine ⟨k, nat.omega.forward at k with *, rfl⟩1920theorem Even.zero21  shows Even(0)22proof23  have doubled := Even.double at 0 with *24  simpa [add] using doubled2526theorem Even.natural (n : Set)27  requires even : Even(n)28  shows Nat(n)29proof30  rcases even with ⟨k, member, equality⟩31  have natural := nat.omega.backward with member32  rw equality33  typecheck3435theorem Even.add (a b : Set)36  requires evenA : Even(a)37  requires evenB : Even(b)38  shows Even(add(a, b))39proof40  rcases evenA with ⟨k, hk, aEq⟩41  rcases evenB with ⟨m, hm, bEq⟩42  have kNat := nat.omega.backward with hk43  have mNat := nat.omega.backward with hm44  have sumNat : Nat(add(k, m)) by typecheck45  witness add(k, m)46  constructor47  . exact nat.omega.forward at add(k, m) with sumNat48  . rw [aEq, bEq]49    ring5051-- Integer rounding excludes a half-integer witness for any double plus one.52theorem Even.not_successor_double (n : Nat)53  shows ¬Even(succ(add(n, n)))54proof55  intro even56  rcases even with ⟨k, member, equation⟩57  have natural := nat.omega.backward with member58  have low : k ≤ n by arith59  have high : succ(n) ≤ k by arith60  have impossible : k < k by arith61  exact Less.irreflexive with *, impossible6263theorem Odd.double_successor (k : Nat)64  shows Odd(succ(add(k, k)))65proof66  unfold Odd67  refine ⟨k, nat.omega.forward at k with *, rfl⟩6869theorem Odd.natural (n : Set)70  requires odd : Odd(n)71  shows Nat(n)72proof73  rcases odd with ⟨k, member, equality⟩74  have natural := nat.omega.backward with member75  rw equality76  typecheck7778theorem Odd.not_even (n : Set)79  requires odd : Odd(n)80  shows ¬Even(n)81proof82  rcases odd with ⟨k, member, equality⟩83  have natural := nat.omega.backward with member84  rw equality85  exact Even.not_successor_double with *8687theorem Even.not_odd (n : Set)88  requires even : Even(n)89  shows ¬Odd(n)90proof91  simp [Odd.not_even]9293theorem Odd.succ_of_even (n : Set)94  requires even : Even(n)95  shows Odd(succ(n))96proof97  rcases even with ⟨k, member, equality⟩98  have natural := nat.omega.backward with member99  rw equality100  exact Odd.double_successor with *101102theorem Even.succ_of_odd (n : Set)103  requires odd : Odd(n)104  shows Even(succ(n))105proof106  rcases odd with ⟨k, member, equality⟩107  have natural := nat.omega.backward with member108  have nextNat : Nat(succ(k)) by typecheck109  witness succ(k)110  constructor111  . exact nat.omega.forward at succ(k) with nextNat112  . rw equality113    ring114115theorem parity.exhaustive (n : Nat)116  shows Even(n) ∨ Odd(n)117proof118  induction n119  | zero =>120    left121    exact Even.zero122  | succ(k) using ih =>123    cases ih with even | odd124    . right125      exact Odd.succ_of_even with even126    . left127      exact Even.succ_of_odd with odd128129theorem Even.iff_not_odd (n : Nat)130  shows Even(n) ↔ ¬Odd(n)131proof132  simp [parity.exhaustive, Even.not_odd]133134theorem Odd.iff_not_even (n : Nat)135  shows Odd(n) ↔ ¬Even(n)136proof137  simp [parity.exhaustive, Odd.not_even]138139theorem Odd.add_even (a b : Set)140  requires oddA : Odd(a)141  requires evenB : Even(b)142  shows Odd(add(a, b))143proof144  rcases oddA with ⟨k, hk, aEq⟩145  rcases evenB with ⟨m, hm, bEq⟩146  have kNat := nat.omega.backward with hk147  have mNat := nat.omega.backward with hm148  have sumNat : Nat(add(k, m)) by typecheck149  witness add(k, m)150  constructor151  . exact nat.omega.forward at add(k, m) with sumNat152  . rw [aEq, bEq]153    ring154155theorem Odd.add_odd (a b : Set)156  requires oddA : Odd(a)157  requires oddB : Odd(b)158  shows Even(add(a, b))159proof160  rcases oddA with ⟨k, hk, aEq⟩161  rcases oddB with ⟨m, hm, bEq⟩162  have kNat := nat.omega.backward with hk163  have mNat := nat.omega.backward with hm164  have sumNat : Nat(succ(add(k, m))) by typecheck165  witness succ(add(k, m))166  constructor167  . exact nat.omega.forward at succ(add(k, m)) with sumNat168  . rw [aEq, bEq]169    ring170171theorem Odd.even_add (a b : Set)172  requires evenA : Even(a)173  requires oddB : Odd(b)174  shows Odd(add(a, b))175proof176  have swapped : add(a, b) = add(b, a) by ring177  rw swapped178  exact Odd.add_even with *179180theorem Even.succ_iff (n : Nat)181  shows Even(succ(n)) ↔ Odd(n)182proof183  have alternatives := parity.exhaustive with *184  have fromEven := Odd.succ_of_even at n185  have fromOdd := Even.succ_of_odd at n186  have excluded := Odd.not_even at succ(n)187  tauto188189theorem Odd.succ_iff (n : Nat)190  shows Odd(succ(n)) ↔ Even(n)191proof192  have alternatives := parity.exhaustive with *193  have fromEven := Odd.succ_of_even at n194  have fromOdd := Even.succ_of_odd at n195  have excluded := Even.not_odd at succ(n)196  tauto197198theorem Odd.three199  shows Odd(3)200proof201  have result := Odd.double_successor at 1 with *202  simpa [add] using result203204theorem Odd.five205  shows Odd(5)206proof207  have result := Odd.double_successor at 2 with *208  simpa [add] using result209210theorem Even.not_three211  shows ¬Even(3)212proof213  exact Odd.not_even with Odd.three214215theorem Even.not_five216  shows ¬Even(5)217proof218  exact Odd.not_even with Odd.five219