-- Natural-valued characteristic functions of sets.
-- Part of Cumulus, the Grace17 mathematics library.
-- Copyright (c) 2026 Grant Passmore.
-- Released under the Apache License 2.0. See LICENSE in the repository root.
-- Authors: Grant Passmore

module Grace.Cumulus.Set.Indicator
import Nat
import Function
import Core

defunique indicator (A x : Set) (value ∈ ℕ) :=
  (x ∈ A → value = 1) ∧ (¬(x ∈ A) → value = 0)
proof
  have alternatives : x ∈ A ∨ ¬(x ∈ A)
    tauto
  cases alternatives with member | absent
  . witness 1
    refine ⟨nat.omega.forward at 1 with assumption, _, _⟩
    . intro present
      rfl
    . intro impossible
      exfalso
      exact impossible with member
  . witness 0
    refine ⟨nat.omega.forward at 0 with assumption, _, _⟩
    . intro impossible
      exfalso
      exact absent with impossible
    . intro missing
      rfl

uniqueness
  intros u uMember first v vMember second
  have alternatives : x ∈ A ∨ ¬(x ∈ A)
    tauto
  cases alternatives with present | absent
  . have uValue : u = 1
      tauto
    have vValue : v = 1
      tauto
    cc
  . have uValue : u = 0
      tauto
    have vValue : v = 0
      tauto
    cc

theorem indicator.natural (A x : Set)
  shows Nat(indicator(A, x))
proof
  obtain ⟨natural, present, absent⟩ := indicator.selected at A, x
  exact nat.omega.backward with natural

theorem indicator.member (A x : Set)
  requires member : x ∈ A
  shows indicator(A, x) = 1
proof
  have selected := indicator.selected at A, x
  tauto

theorem indicator.absent (A x : Set)
  requires absent : ¬(x ∈ A)
  shows indicator(A, x) = 0
proof
  have selected := indicator.selected at A, x
  tauto

theorem indicator.congr (A B x y : Set)
  requires equivalent : x ∈ A ↔ y ∈ B
  shows indicator(A, x) = indicator(B, y)
proof
  have alternatives : x ∈ A ∨ ¬(x ∈ A) by tauto
  cases alternatives with present | absent
  . have other : y ∈ B
      tauto
    have left := indicator.member with present
    have right := indicator.member with other
    rw [left, right]
    rfl
  . have other : ¬(y ∈ B)
      tauto
    have left := indicator.absent with absent
    have right := indicator.absent with other
    rw [left, right]
    rfl

theorem indicator.singleton_self (x : Set)
  shows indicator({x}, x) = 1
proof
  have member := singleton.self at x
  exact indicator.member with member

theorem indicator.singleton_other (x y : Set)
  requires different : x ≠ y
  shows indicator({x}, y) = 0
proof
  have absent : ¬(y ∈ {x}) by simp
  simp [singleton.membership, indicator.absent]

-- Count membership along a finite enumeration f[0], ..., f[n-1].
-- With a bijective enumeration this is the cardinality of the intersection.
def countMembers (A f : Set, n : Nat) → Set
  | A, f, zero => 0
  | A, f, succ(k) => add(countMembers(A, f, k), indicator(A, f[k]))

theorem countMembers.natural (A f : Set, n : Nat)
  shows Nat(countMembers(A, f, n))
proof
  induction n
  | zero =>
    rw countMembers
    typecheck
  | succ(k) using ih =>
    rw countMembers
    typecheck