-- Inversion pairs under exchanges of permutation inputs (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.Cardinal.InversionExchange
import PermutationExchange
import Counting

theorem inversions.pair (I p i j : Set)
  shows (i, j) ∈ inversions(I, p) ↔ i ∈ I ∧ j ∈ I ∧ i ∈ j ∧ p(j) ∈ p(i)
proof
  constructor
  . intro member
    obtain ⟨bound, a, ha, b, hb, shape, ordered, reversed⟩ := inversions.forward with member
    have coordinates := orderedPair.injective with shape
    rw [coordinates.left, coordinates.right]
    refine ⟨ha, hb, ordered, reversed⟩
  . intro data
    obtain ⟨hi, hj, ordered, reversed⟩ := data
    have pair := product.pair with hi, hj
    have witness : ∃ a ∈ I, ∃ b ∈ I, (i, j) = (a, b) ∧ a ∈ b ∧ p(b) ∈ p(a)
      refine ⟨i, hi, j, hj, rfl, ordered, reversed⟩
    apply inversions.backward
    constructor
    . exact pair
    . exact witness

theorem productMap.involution (I t : Set)
  requires involution : InvolutionOn(t, I)
  shows InvolutionOn(productMap(t, t, I, I, I, I), I × I)
proof
  have function := InvolutionOn.function with involution
  have product := productMap.function with *
  unfold InvolutionOn
  refine ⟨product, ?_⟩
  intros q member
  obtain ⟨bound, i, hi, j, hj, shape⟩ := product.membership.forward with member
  have imageI := FunctionBetween.apply_closed with function, hi
  have imageJ := FunctionBetween.apply_closed with function, hj
  have first := productMap.apply with hi, hj
  have second := productMap.apply at t, t, I, I, I, I, t(i), t(j) with *
  have inverseI := InvolutionOn.apply with involution, hi
  have inverseJ := InvolutionOn.apply with involution, hj
  cc

-- An adjacent swap preserves the order of every pair other than its own.
theorem transposition.adjacent_order (n a i j : Nat)
  requires ha : a ∈ n
  requires hb : succ(a) ∈ n
  requires hi : i ∈ n
  requires hj : j ∈ n
  requires ordered : i < j
  requires other : ¬(i = a ∧ j = succ(a))
  shows transposition(n, a, succ(a))(i) < transposition(n, a, succ(a))(j)
proof
  have atFirst := transposition.first at n, a, succ(a) with *
  have atSecond := transposition.second at n, a, succ(a) with *
  have casesI : i = a ∨ i = succ(a) ∨ (i ≠ a ∧ i ≠ succ(a)) by tauto
  have casesJ : j = a ∨ j = succ(a) ∨ (j ≠ a ∧ j ≠ succ(a)) by tauto
  cases casesI with firstI | remainingI
  . rw [firstI, atFirst]
    cases casesJ with firstJ | remainingJ
    . have impossible : i < i
        arith
      have excluded := Less.irreflexive at i with *
      exfalso
      exact excluded with impossible
    . cases remainingJ with secondJ | outsideJ
      . exfalso
        apply other
        refine ⟨firstI, secondJ⟩
      . have unchanged := transposition.other with ha, hb, hj, outsideJ.left, outsideJ.right
        rw unchanged
        have below : a < j by arith
        have separated := outsideJ.right
        exact Less.successor_lower_of_ne with *
  . cases remainingI with secondI | outsideI
    . rw [secondI, atSecond]
      cases casesJ with firstJ | remainingJ
      . have impossible : i < i
          arith
        have excluded := Less.irreflexive at i with *
        exfalso
        exact excluded with impossible
      . cases remainingJ with secondJ | outsideJ
        . have impossible : i < i
            arith
          have excluded := Less.irreflexive at i with *
          exfalso
          exact excluded with impossible
        . have unchanged := transposition.other with ha, hb, hj, outsideJ.left, outsideJ.right
          rw unchanged
          arith
    . have unchangedI := transposition.other with ha, hb, hi, outsideI.left, outsideI.right
      rw unchangedI
      cases casesJ with firstJ | remainingJ
      . rw [firstJ, atFirst]
        arith
      . cases remainingJ with secondJ | outsideJ
        . rw [secondJ, atSecond]
          have below : i < succ(a) by arith
          have separated := outsideI.left
          exact Less.of_successor_upper_ne with *
        . have unchangedJ := transposition.other with ha, hb, hj, outsideJ.left, outsideJ.right
          rwa unchangedJ

-- Remove the distinguished pair before transporting inversion pairs.
theorem inversions.adjacent_transport (n a : Nat) (p q : Set)
  requires ha : a ∈ n
  requires hb : succ(a) ∈ n
  requires permutation : p ∈ permutations(n)
  requires member : q ∈ inversions(n, p) ∖ {(a, succ(a))}
  shows productMap(transposition(n, a, succ(a)), transposition(n, a, succ(a)), n, n, n, n)(q) ∈ inversions(n, permutationExchange(n, a, succ(a))(p)) ∖ {(a, succ(a))}
proof
  have data := difference.membership.forward with member
  have bound : q ∈ n × n by simp [inversions]
  obtain ⟨productBound, i, hi, j, hj, shape⟩ := product.membership.forward with bound
  have inversion := data.left
  rw shape at inversion
  have facts := inversions.pair.forward with inversion
  have naturals := natural.member at n with *
  have ni := naturals with i, hi
  have nj := naturals with j, hj
  have orderBridge := Less.of_membership at i, j with *
  have ordered := orderBridge with facts.right.right.left
  have other : ¬(i = a ∧ j = succ(a)) by simp
  have orderedSwap := transposition.adjacent_order with *
  have function := transposition.function at n, a, succ(a) with *
  have involution := transposition.involution at n, a, succ(a) with *
  have imageI := FunctionBetween.apply_closed with function, hi
  have imageJ := FunctionBetween.apply_closed with function, hj
  have naturalI := naturals with transposition(n, a, succ(a))(i), imageI
  have naturalJ := naturals with transposition(n, a, succ(a))(j), imageJ
  have swappedOrder := membership.of_Less with naturalI, naturalJ, orderedSwap
  have inverseI := InvolutionOn.apply with involution, hi
  have inverseJ := InvolutionOn.apply with involution, hj
  have firstValue := transposition.first at n, a, succ(a) with *
  have secondValue := transposition.second at n, a, succ(a) with *
  have evaluatedI := permutationExchange.apply at n, a, succ(a), p, transposition(n, a, succ(a))(i) with *
  have evaluatedJ := permutationExchange.apply at n, a, succ(a), p, transposition(n, a, succ(a))(j) with *
  have pairedValue := productMap.apply with hi, hj
  have swappedInversion : (transposition(n, a, succ(a))(i), transposition(n, a, succ(a))(j)) ∈ inversions(n, permutationExchange(n, a, succ(a))(p)) by simp [inversions.pair, facts.right.right]
  have notDistinguished : ¬((transposition(n, a, succ(a))(i), transposition(n, a, succ(a))(j)) ∈ {(a, succ(a))})
    intro singleton
    have equal := singleton.membership.forward with singleton
    have coordinates := orderedPair.injective with equal
    have reversedI : i = succ(a) by cc
    have reversedJ : j = a by cc
    have reverse := ordered
    rw [reversedI, reversedJ] at reverse
    have successorMember := membership.self_successor at a with *
    have increaseBridge := Less.of_membership at a, succ(a) with *
    have increase := increaseBridge with successorMember
    have impossible := Less.transitive at a, succ(a), a with *
    have excluded := Less.irreflexive at a with *
    exact excluded with impossible
  rw [shape, pairedValue]
  exact difference.membership.backward with ⟨swappedInversion, notDistinguished⟩

theorem inversions.adjacent_count_off_pair (n a : Nat) (p : Set)
  requires ha : a ∈ n
  requires hb : succ(a) ∈ n
  requires permutation : p ∈ permutations(n)
  shows cardinality(inversions(n, p) ∖ {(a, succ(a))}) = cardinality(inversions(n, permutationExchange(n, a, succ(a))(p)) ∖ {(a, succ(a))})
proof
  have exchange := permutationExchange.function at n, a, succ(a) with *
  have paired := FunctionBetween.apply_closed with exchange, permutation
  have exchangeInvolution := permutationExchange.involution at n, a, succ(a) with *
  have twice := InvolutionOn.apply with exchangeInvolution, permutation
  have swap := transposition.involution at n, a, succ(a) with *
  have product := productMap.involution with swap
  have subsetS : inversions(n, p) ∖ {(a, succ(a))} ⊆ n × n by simp [Subset, difference.membership, inversions]
  have subsetT : inversions(n, permutationExchange(n, a, succ(a))(p)) ∖ {(a, succ(a))} ⊆ n × n
    simp [Subset, difference.membership, inversions]
  have forward : ∀ q ∈ inversions(n, p) ∖ {(a, succ(a))}, productMap(transposition(n, a, succ(a)), transposition(n, a, succ(a)), n, n, n, n)(q) ∈ inversions(n, permutationExchange(n, a, succ(a))(p)) ∖ {(a, succ(a))} by simp [inversions.adjacent_transport]
  have backward : ∀ q ∈ inversions(n, permutationExchange(n, a, succ(a))(p)) ∖ {(a, succ(a))}, productMap(transposition(n, a, succ(a)), transposition(n, a, succ(a)), n, n, n, n)(q) ∈ inversions(n, p) ∖ {(a, succ(a))}
    intros q member
    have transport := inversions.adjacent_transport with *
    rwa twice at transport
  have bijective := InvolutionOn.restrict_between with product, subsetS, subsetT, forward, backward
  have finite := Finite.natural at n with *
  have square := Finite.product with finite, finite
  have finiteS := Finite.subset with square, subsetS
  exact cardinality.bijective with finiteS, bijective

theorem inversions.exchange_distinguished (n a b : Nat) (p : Set)
  requires ha : a ∈ n
  requires hb : b ∈ n
  requires ordered : a < b
  requires permutation : p ∈ permutations(n)
  shows (a, b) ∈ inversions(n, permutationExchange(n, a, b)(p)) ↔ ¬((a, b) ∈ inversions(n, p))
proof
  have bijective := permutations.mem_iff.forward with permutation
  have injective := Bijective.injective with bijective
  have function := Injective.function with injective
  have imageA := FunctionBetween.apply_closed with function, ha
  have imageB := FunctionBetween.apply_closed with function, hb
  have naturals := natural.member at n with *
  have naturalA := naturals with p(a), imageA
  have naturalB := naturals with p(b), imageB
  have distinct : p(a) ≠ p(b)
    intro same
    have edgeA := FunctionBetween.relates_apply with function, ha
    have edgeB := FunctionBetween.relates_apply with function, hb
    rw same at edgeA
    have equal := Injective.cancel at p, n, n, a, b, p(b) with *
    arith
  have first := permutationExchange.apply at n, a, b, p, a with *
  have second := permutationExchange.apply at n, a, b, p, b with *
  have swapA := transposition.first at n, a, b with *
  have swapB := transposition.second at n, a, b with *
  rw swapA at first
  rw swapB at second
  have indexOrder := membership.of_Less at a, b with *, ordered
  constructor
  . intros inverted original
    have left := inversions.pair.forward with inverted
    have right := inversions.pair.forward with original
    have forwardMember := left.right.right.right
    rw [first, second] at forwardMember
    have forwardBridge := Less.of_membership at p(a), p(b) with *
    have reverseBridge := Less.of_membership at p(b), p(a) with *
    have forward := forwardBridge with forwardMember
    have reverse := reverseBridge with right.right.right.right
    arith
  . intro absent
    have comparison := Less.trichotomy at p(a), p(b) with *
    have forward : p(a) < p(b) by simp [membership.of_Less, inversions.pair]
    have forwardMember := membership.of_Less with naturalA, naturalB, forward
    apply inversions.pair.backward
    refine ⟨ha, hb, indexOrder, ?_⟩
    rwa [first, second]

theorem inversions.adjacent_count (n a : Nat) (p : Set)
  requires ha : a ∈ n
  requires hb : succ(a) ∈ n
  requires permutation : p ∈ permutations(n)
  shows cardinality(inversions(n, permutationExchange(n, a, succ(a))(p))) = succ(cardinality(inversions(n, p))) ∨ cardinality(inversions(n, p)) = succ(cardinality(inversions(n, permutationExchange(n, a, succ(a))(p))))
proof
  have finite := Finite.natural at n with *
  have originalFinite := inversions.finite at n, p with finite
  have pairedFinite := inversions.finite at n, permutationExchange(n, a, succ(a))(p) with finite
  have ordered : a < succ(a) by arith
  have flip := inversions.exchange_distinguished with *
  have rest := inversions.adjacent_count_off_pair with *
  have alternatives : (a, succ(a)) ∈ inversions(n, p) ∨ ¬((a, succ(a)) ∈ inversions(n, p)) by tauto
  cases alternatives with present | absent
  . have pairedAbsent : ¬((a, succ(a)) ∈ inversions(n, permutationExchange(n, a, succ(a))(p)))
      tauto
    have unchanged : inversions(n, permutationExchange(n, a, succ(a))(p)) ∖ {(a, succ(a))} = inversions(n, permutationExchange(n, a, succ(a))(p))
      ext q
      simp
    have removed := cardinality.remove at inversions(n, p), (a, succ(a)) with *
    right
    cc
  . have pairedPresent : (a, succ(a)) ∈ inversions(n, permutationExchange(n, a, succ(a))(p))
      tauto
    have unchanged : inversions(n, p) ∖ {(a, succ(a))} = inversions(n, p)
      ext q
      simp
    have removed := cardinality.remove at inversions(n, permutationExchange(n, a, succ(a))(p)), (a, succ(a)) with *
    left
    cc