-- Involutions and restriction to unions of their orbits (ZF).
-- 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.Involution
import Function

predicate InvolutionOn (t D : Set) := FunctionBetween(t, D, D) ∧ (∀ x ∈ D, t(t(x)) = x)

theorem InvolutionOn.function (t D : Set)
  requires involution : InvolutionOn(t, D)
  shows t : D → D
proof
  simp [InvolutionOn]

theorem InvolutionOn.apply (t D x : Set)
  requires involution : InvolutionOn(t, D)
  requires member : x ∈ D
  shows t(t(x)) = x
proof
  ext y
  simp [InvolutionOn]

theorem InvolutionOn.bijective (t D : Set)
  requires involution : InvolutionOn(t, D)
  shows BijectiveBetween(t, D, D)
proof
  have function := InvolutionOn.function with involution
  constructor
  . unfold InjectiveBetween
    refine ⟨function, ?_⟩
    intros x hx y hy z hz first second
    have tx := FunctionBetween.apply_value with function, hx, first
    have ty := FunctionBetween.apply_value with function, hy, second
    have inverseX := InvolutionOn.apply with involution, hx
    have inverseY := InvolutionOn.apply with involution, hy
    cc
  . unfold SurjectiveBetween
    refine ⟨function, ?_⟩
    intros y hy
    have image := FunctionBetween.apply_closed with function, hy
    have inverse := InvolutionOn.apply with involution, hy
    have graph := FunctionBetween.relates_apply with function, image
    refine ⟨t(y), image, ?_⟩
    rwa inverse at graph

theorem InvolutionOn.remove_pair (t D V a : Set)
  requires involution : InvolutionOn(t, D)
  requires subset : V ⊆ D
  requires closed : ∀ x ∈ V, t(x) ∈ V
  requires member : a ∈ V
  shows ∀ x ∈ (V ∖ {a}) ∖ {t(a)}, t(x) ∈ (V ∖ {a}) ∖ {t(a)}
proof
  have aIn := subset with a, member
  have inverseA := InvolutionOn.apply with involution, aIn
  intros x hx
  have outer := difference.membership.forward with hx
  have inner := difference.membership.forward with outer.left
  have xIn := subset with x, inner.left
  have inverseX := InvolutionOn.apply with involution, xIn
  have image := closed with x, inner.left
  have notA : ¬(t(x) ∈ {a})
    intro singleton
    have equal := singleton.membership.forward with singleton
    have same : x = t(a) by cc
    have forbidden : x ∈ {t(a)} by simp
    exact outer.right with forbidden
  have notPartner : ¬(t(x) ∈ {t(a)})
    intro singleton
    have equal := singleton.membership.forward with singleton
    have same : x = a by cc
    have forbidden : x ∈ {a} by simp
    exact inner.right with forbidden
  exact difference.membership.backward with ⟨(difference.membership.backward with ⟨image, notA⟩), notPartner⟩

-- Restrict an involution when it exchanges two (possibly overlapping) subsets.
theorem InvolutionOn.restrict_between (t D S T : Set)
  requires involution : InvolutionOn(t, D)
  requires subsetS : S ⊆ D
  requires subsetT : T ⊆ D
  requires forward : ∀ x ∈ S, t(x) ∈ T
  requires backward : ∀ y ∈ T, t(y) ∈ S
  shows BijectiveBetween(restrict(t, S), S, T)
proof
  have function := InvolutionOn.function with involution
  have restricted := restrict.function at t, D, D, S, T with *
  constructor
  . unfold InjectiveBetween
    refine ⟨restricted, ?_⟩
    intros x hx y hy z hz first second
    have valueX := FunctionBetween.apply_value with restricted, hx, first
    have valueY := FunctionBetween.apply_value with restricted, hy, second
    have restrictedX := restrict.apply with hx
    have restrictedY := restrict.apply with hy
    have xIn := subsetS with x, hx
    have yIn := subsetS with y, hy
    have inverseX := InvolutionOn.apply with involution, xIn
    have inverseY := InvolutionOn.apply with involution, yIn
    cc
  . unfold SurjectiveBetween
    refine ⟨restricted, ?_⟩
    intros y hy
    have preimage := backward with y, hy
    have yIn := subsetT with y, hy
    have inverse := InvolutionOn.apply with involution, yIn
    have value := restrict.apply at t, D, D, S, T, t(y) with *
    have graph := FunctionBetween.relates_apply with restricted, preimage
    refine ⟨t(y), preimage, ?_⟩
    have same : restrict(t, S)(t(y)) = y by cc
    rwa same at graph