-- Exchanging two elements of a set, without Choice.
-- 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.Transposition
import Involution

defunique exchangedValue (I a b x : Set) (y ∈ I) :=
  (x = a ∧ y = b) ∨ (x = b ∧ y = a) ∨ (x ≠ a ∧ x ≠ b ∧ y = x)
requires ha : a ∈ I
requires hb : b ∈ I
requires member : x ∈ I
proof
  have alternatives : x = a ∨ x = b ∨ (x ≠ a ∧ x ≠ b)
    tauto
  cases alternatives with atFirst | remaining
  . refine ⟨b, hb, ?_⟩
    settle
  . cases remaining with atSecond | outside
    . refine ⟨a, ha, ?_⟩
      settle
    . refine ⟨x, member, ?_⟩
      settle
uniqueness
  intros u hu firstValue v hv secondValue
  cases firstValue with atFirst | remaining
  . cases secondValue with atFirstAgain | other
    . cc
    . cases other with atSecond | outside
      . cc
      . cc
  . cases remaining with atSecond | outside
    . cases secondValue with atFirst | other
      . cc
      . cases other with atSecondAgain | outsideAgain
        . cc
        . cc
    . cases secondValue with atFirst | other
      . cc
      . cases other with atSecond | outsideAgain
        . cc
        . cc

defgraph transposition (I a b : Set) (x ∈ I) : I := exchangedValue(I, a, b, x)
requires ha : a ∈ I
requires hb : b ∈ I
proof
  have selected := exchangedValue.selected at I, a, b, x with *
  exact selected.left

section Exchanges
variable (I a b : Set)
hypothesis ha : a ∈ I
hypothesis hb : b ∈ I

theorem transposition.first
  shows transposition(I, a, b)(a) = b
proof
  have selected := exchangedValue.selected at I, a, b, a with *
  have value := transposition.value at I, a, b, a with *
  have alternatives := selected.right
  cases alternatives with atFirst | remaining
  . cc
  . cases remaining with atSecond | outside
    . cc
    . cc

theorem transposition.second
  shows transposition(I, a, b)(b) = a
proof
  have selected := exchangedValue.selected at I, a, b, b with *
  have value := transposition.value at I, a, b, b with *
  have alternatives := selected.right
  cases alternatives with atFirst | remaining
  . cc
  . cases remaining with atSecond | outside
    . cc
    . cc

theorem transposition.other (x : Set)
  requires member : x ∈ I
  requires notFirst : x ≠ a
  requires notSecond : x ≠ b
  shows transposition(I, a, b)(x) = x
proof
  have selected := exchangedValue.selected at I, a, b, x with *
  have value := transposition.value at I, a, b, x with *
  have alternatives := selected.right
  cases alternatives with atFirst | remaining
  . cc
  . cases remaining with atSecond | outside
    . cc
    . cc

theorem transposition.involution
  shows InvolutionOn(transposition(I, a, b), I)
proof
  have function := transposition.function at I, a, b with *
  have atFirst := transposition.first at I, a, b with *
  have atSecond := transposition.second at I, a, b with *
  unfold InvolutionOn
  refine ⟨function, ?_⟩
  intros x member
  have alternatives : x = a ∨ x = b ∨ (x ≠ a ∧ x ≠ b) by tauto
  cases alternatives with same | remaining
  . cc
  . cases remaining with same | outside
    . cc
    . have unchanged := transposition.other with ha, hb, member, outside.left, outside.right
      cc

theorem transposition.bijective
  shows BijectiveBetween(transposition(I, a, b), I, I)
proof
  simp [transposition.involution, InvolutionOn.bijective]

theorem transposition.symmetric
  shows transposition(I, a, b) = transposition(I, b, a)
proof
  have firstFunction := transposition.function at I, a, b with *
  have secondFunction := transposition.function at I, b, a with *
  have firstA := transposition.first at I, a, b with *
  have firstB := transposition.second at I, a, b with *
  have secondA := transposition.second at I, b, a with *
  have secondB := transposition.first at I, b, a with *
  apply FunctionBetween.ext with firstFunction, secondFunction
  intros i member
  have alternatives : i = a ∨ i = b ∨ (i ≠ a ∧ i ≠ b) by tauto
  cases alternatives with atA | rest
  . cc
  . cases rest with atB | outside
    . cc
    . have first := transposition.other with ha, hb, member, outside.left, outside.right
      have second := transposition.other with hb, ha, member, outside.right, outside.left
      cc

end Exchanges
-- Conjugating (a b) by (b c) gives (a c).
theorem transposition.conjugate (I a b c i : Set)
  requires ha : a ∈ I
  requires hb : b ∈ I
  requires hc : c ∈ I
  requires hi : i ∈ I
  requires ab : a ≠ b
  requires ac : a ≠ c
  requires bc : b ≠ c
  shows transposition(I, b, c)(transposition(I, a, b)(transposition(I, b, c)(i))) = transposition(I, a, c)(i)
proof
  have ba : b ≠ a by simp
  have ca : c ≠ a by simp
  have cb : c ≠ b by simp
  have bcFirst := transposition.first at I, b, c with *
  have bcSecond := transposition.second at I, b, c with *
  have bcOther := transposition.other at I, b, c, a with *
  have abFirst := transposition.first at I, a, b with *
  have abSecond := transposition.second at I, a, b with *
  have abOther := transposition.other at I, a, b, c with *
  have acFirst := transposition.first at I, a, c with *
  have acSecond := transposition.second at I, a, c with *
  have acOther := transposition.other at I, a, c, b with *
  have alternatives : i = a ∨ i = b ∨ i = c ∨ (i ≠ a ∧ i ≠ b ∧ i ≠ c) by tauto
  cases alternatives with first | rest
  . cc
  . cases rest with second | restAgain
    . cc
    . cases restAgain with third | outside
      . cc
      . have outsideBC := transposition.other with hb, hc, hi, outside.right.left, outside.right.right
        have outsideAB := transposition.other with ha, hb, hi, outside.left, outside.right.left
        have outsideAC := transposition.other with ha, hc, hi, outside.left, outside.right.right
        cc