Grace/Cumulus/Cardinal/SumParity.g17

Open in Workbench Download source

Imports

NaturalSum · Nat.Parity

Declarations

Source

1-- Parity of a sum of weights at most two: it is the parity of the number2-- of points of weight one3-- Part of Cumulus, the Grace17 mathematics library.4-- Copyright (c) 2026 Grant Passmore.5-- Released under the Apache License 2.0. See LICENSE in the repository root.6-- Authors: Grant Passmore78module Grace.Cumulus.Cardinal.SumParity9import NaturalSum10import Nat.Parity1112def ones (V w : Set) : Set := { v ∈ V | w(v) = 1 }1314theorem ones.subset (V w : Set)15  shows ones(V, w) ⊆ V16proof17  intros v hv18  have parts := ones.membership.forward with hv19  exact parts.left2021theorem ones.insert_other (V w a : Set)22  requires other : w(a) ≠ 123  shows ones(insert(a, V), w) = ones(V, w)24proof25  ext v26  constructor27  . intro hv28    have parts := ones.membership.forward with hv29    have split := insert.membership.forward with parts.left30    cases split with same | inV31    . exfalso32      rw same at parts33      exact other with parts.right34    . exact ones.membership.backward with ⟨inV, parts.right⟩35  . intro hv36    have parts := ones.membership.forward with hv37    have inserted : v ∈ insert(a, V)38      apply insert.membership.backward39      right40      exact parts.left41    exact ones.membership.backward with ⟨inserted, parts.right⟩4243theorem ones.insert_one (V w a : Set)44  requires one : w(a) = 145  shows ones(insert(a, V), w) = insert(a, ones(V, w))46proof47  ext v48  constructor49  . intro hv50    have parts := ones.membership.forward with hv51    have split := insert.membership.forward with parts.left52    apply insert.membership.backward53    cases split with same | inV54    . left55      exact same56    . right57      exact ones.membership.backward with ⟨inV, parts.right⟩58  . intro hv59    have split := insert.membership.forward with hv60    cases split with same | inOnes61    . rw same62      apply ones.membership.backward63      have inserted : a ∈ insert(a, V)64        apply insert.membership.backward65        left66        rfl67      exact ⟨inserted, one⟩68    . have parts := ones.membership.forward with inOnes69      have inserted : v ∈ insert(a, V)70        apply insert.membership.backward71        right72        exact parts.left73      exact ones.membership.backward with ⟨inserted, parts.right⟩7475theorem Even.two76  shows Even(2)77proof78  have double := Even.double at 179  have same : add(1, 1) = 2 by compute80  rwa same at double8182theorem Even.add_two_iff (s : Nat)83  shows Even(s + 2) ↔ Even(s)84proof85  constructor86  . intro even87    have split := parity.exhaustive at s88    cases split with evenS | oddS89    . exact evenS90    . exfalso91      have odd := Odd.add_even with oddS, Even.two92      exact Odd.not_even with odd, even93  . intro even94    exact Even.add with even, Even.two9596theorem Even.add_one_iff (s : Nat)97  shows Even(s + 1) ↔ Odd(s)98proof99  rw add.right_one100  exact Even.succ_iff101102-- The sum of weights in {0, 1, 2} has the parity of the number of ones.103theorem natSum.parity_of_size (V w : Set, n : Nat)104  requires finite : Finite(V)105  requires size : cardinality(V) = n106  requires weights : ∀ v ∈ V, w(v) = 0 ∨ w(v) = 1 ∨ w(v) = 2107  shows Even(natSum(V, w)) ↔ Even(cardinality(ones(V, w)))108proof109  induction n generalizing V110  | zero =>111    intros V finite size weights112    have has := cardinality.correct with finite113    rw size at has114    have empty := HasCardinality.empty_of_zero at V with has115    have onesEmpty : ones(∅, w) = ∅116      apply Subset.antisymmetric117      . exact ones.subset at ∅, w118      . exact empty.subset at ones(∅, w)119    rw [empty, natSum.empty, onesEmpty]120    rw ← nat.zero121    rw cardinality.natural122    constructor123    . intro h124      exact h125    . intro h126      exact h127  | succ(k) using ih =>128    intros V finite size weights129    have has := cardinality.correct with finite130    rw size at has131    obtain ⟨a, ha⟩ := HasCardinality.exists_member with has132    have removed := cardinality.remove with finite, ha133    rw size at removed134    have smaller := Naturals.injective.succ with removed135    have restSize : cardinality(V ∖ {a}) = k136      symm137      exact smaller138    have restFinite := Finite.subset with finite, (difference.subset_left at V, {a})139    have restWeights : ∀ v ∈ V ∖ {a}, w(v) = 0 ∨ w(v) = 1 ∨ w(v) = 2140      intros v hv141      have parts := difference.singleton_membership.forward with hv142      exact weights with v, parts.left143    have rest := ih with V ∖ {a}, restFinite, restSize, restWeights144    have naturals : ∀ v ∈ V ∖ {a}, w(v) ∈ ℕ145      intros v hv146      have split := restWeights with v, hv147      cases split with zero | more148      . rw zero149        typecheck150      . cases more with one | two151        . rw one152          typecheck153        . rw two154          typecheck155    have fresh : ¬a ∈ V ∖ {a}156      intro inside157      have parts := difference.singleton_membership.forward with inside158      apply parts.right159      rfl160    have restore := insert.restore with ha161    have onesFinite := Finite.subset with restFinite, (ones.subset at V ∖ {a}, w)162    have onesFresh : ¬a ∈ ones(V ∖ {a}, w)163      intro inside164      exact fresh with (ones.subset at V ∖ {a}, w with a, inside)165    have split := weights with a, ha166    have sumNat := natSum.natural with restFinite, naturals167    have onesCorrect := cardinality.correct with onesFinite168    have onesNat := onesCorrect.left169    rw ← restore170    cases split with zero | more171    . have weightA : w(a) ∈ ℕ172        rw zero173        typecheck174      have inserted := natSum.insert with restFinite, naturals, weightA, fresh175      have other : w(a) ≠ 1176        rw zero177        exact zero.ne_one178      have onesSame := ones.insert_other at V ∖ {a}, w, a with other179      rw [inserted, onesSame, zero, add.right_unit]180      exact rest181    . cases more with one | two182      . have weightA : w(a) ∈ ℕ183          rw one184          typecheck185        have inserted := natSum.insert with restFinite, naturals, weightA, fresh186        have onesIns := ones.insert_one at V ∖ {a}, w, a with one187        have onesCard := cardinality.insert with onesFinite, onesFresh188        rw [inserted, onesIns, one, onesCard]189        have left := Even.add_one_iff at natSum(V ∖ {a}, w)190        have right := Even.succ_iff at cardinality(ones(V ∖ {a}, w))191        have oddSum := Odd.iff_not_even at natSum(V ∖ {a}, w)192        have oddOnes := Odd.iff_not_even at cardinality(ones(V ∖ {a}, w))193        constructor194        . intro h195          have oddS := left.forward with h196          have notEvenS := oddSum.forward with oddS197          have notEvenC : ¬Even(cardinality(ones(V ∖ {a}, w)))198            intro evenC199            exact notEvenS with (rest.backward with evenC)200          exact right.backward with (oddOnes.backward with notEvenC)201        . intro h202          have oddC := right.forward with h203          have notEvenC := oddOnes.forward with oddC204          have notEvenS : ¬Even(natSum(V ∖ {a}, w))205            intro evenS206            exact notEvenC with (rest.forward with evenS)207          exact left.backward with (oddSum.backward with notEvenS)208      . have weightA : w(a) ∈ ℕ209          rw two210          typecheck211        have inserted := natSum.insert with restFinite, naturals, weightA, fresh212        have other : w(a) ≠ 1213          rw two214          decide215        have onesSame := ones.insert_other at V ∖ {a}, w, a with other216        rw [inserted, onesSame, two]217        have shift := Even.add_two_iff at natSum(V ∖ {a}, w)218        constructor219        . intro h220          exact rest.forward with (shift.forward with h)221        . intro h222          exact shift.backward with (rest.backward with h)223224225-- The same for a finite set, with no size parameter.226theorem natSum.parity (V w : Set)227  requires finite : Finite(V)228  requires weights : ∀ v ∈ V, w(v) = 0 ∨ w(v) = 1 ∨ w(v) = 2229  shows Even(natSum(V, w)) ↔ Even(cardinality(ones(V, w)))230proof231  have correct := cardinality.correct with finite232  have natural := correct.left233  have size : cardinality(V) = cardinality(V) by rfl234  exact natSum.parity_of_size at V, w, cardinality(V)235    with natural, finite, size, weights236237