Grace/Cumulus/Set/Indicator.g17

Open in Workbench Download source

Imports

Nat · Function · Core

Declarations

Source

1-- Natural-valued characteristic functions of sets.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.Set.Indicator8import Nat9import Function10import Core1112defunique indicator (A x : Set) (value ∈ ℕ) :=13  (x ∈ A → value = 1) ∧ (¬(x ∈ A) → value = 0)14proof15  have alternatives : x ∈ A ∨ ¬(x ∈ A)16    tauto17  cases alternatives with member | absent18  . witness 119    refine ⟨nat.omega.forward at 1 with assumption, _, _⟩20    . intro present21      rfl22    . intro impossible23      exfalso24      exact impossible with member25  . witness 026    refine ⟨nat.omega.forward at 0 with assumption, _, _⟩27    . intro impossible28      exfalso29      exact absent with impossible30    . intro missing31      rfl3233uniqueness34  intros u uMember first v vMember second35  have alternatives : x ∈ A ∨ ¬(x ∈ A)36    tauto37  cases alternatives with present | absent38  . have uValue : u = 139      tauto40    have vValue : v = 141      tauto42    cc43  . have uValue : u = 044      tauto45    have vValue : v = 046      tauto47    cc4849theorem indicator.natural (A x : Set)50  shows Nat(indicator(A, x))51proof52  obtain ⟨natural, present, absent⟩ := indicator.selected at A, x53  exact nat.omega.backward with natural5455theorem indicator.member (A x : Set)56  requires member : x ∈ A57  shows indicator(A, x) = 158proof59  have selected := indicator.selected at A, x60  tauto6162theorem indicator.absent (A x : Set)63  requires absent : ¬(x ∈ A)64  shows indicator(A, x) = 065proof66  have selected := indicator.selected at A, x67  tauto6869theorem indicator.congr (A B x y : Set)70  requires equivalent : x ∈ A ↔ y ∈ B71  shows indicator(A, x) = indicator(B, y)72proof73  have alternatives : x ∈ A ∨ ¬(x ∈ A) by tauto74  cases alternatives with present | absent75  . have other : y ∈ B76      tauto77    have left := indicator.member with present78    have right := indicator.member with other79    rw [left, right]80    rfl81  . have other : ¬(y ∈ B)82      tauto83    have left := indicator.absent with absent84    have right := indicator.absent with other85    rw [left, right]86    rfl8788theorem indicator.singleton_self (x : Set)89  shows indicator({x}, x) = 190proof91  have member := singleton.self at x92  exact indicator.member with member9394theorem indicator.singleton_other (x y : Set)95  requires different : x ≠ y96  shows indicator({x}, y) = 097proof98  have absent : ¬(y ∈ {x}) by simp99  simp [singleton.membership, indicator.absent]100101-- Count membership along a finite enumeration f[0], ..., f[n-1].102-- With a bijective enumeration this is the cardinality of the intersection.103def countMembers (A f : Set, n : Nat) → Set104  | A, f, zero => 0105  | A, f, succ(k) => add(countMembers(A, f, k), indicator(A, f[k]))106107theorem countMembers.natural (A f : Set, n : Nat)108  shows Nat(countMembers(A, f, n))109proof110  induction n111  | zero =>112    rw countMembers113    typecheck114  | succ(k) using ih =>115    rw countMembers116    typecheck117