-- Inversion-count signs under adjacent 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.Algebra.Ring.PermutationSign
import DeterminantCancellation
import Cardinal.InversionExchange

section Signs
variable (A add zero neg mul one : Set)
notation ring R := (A, add, zero, neg, mul, one)
hypothesis ring : IsCommRing(R)

theorem permutationSign.adjacent (n a : Nat) (p : Set)
  requires ha : a ∈ n
  requires hb : succ(a) ∈ n
  requires permutation : p ∈ permutations(n)
  shows permutationSign(n, A, add, zero, neg, mul, one, permutationExchange(n, a, succ(a))(p)) = R[-permutationSign(n, A, add, zero, neg, mul, one, 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 originalCount := cardinality.correct with originalFinite
  have pairedCount := cardinality.correct with pairedFinite
  have originalNatural := HasCardinality.natural with originalCount
  have pairedNatural := HasCardinality.natural with pairedCount
  have originalClosed := permutationSign.closed at A, add, zero, neg, mul, one, n, p with *
  have pairedClosed := permutationSign.closed at A, add, zero, neg, mul, one, n, permutationExchange(n, a, succ(a))(p) with *
  unfold permutationSign at originalClosed
  unfold permutationSign at pairedClosed
  have count := inversions.adjacent_count with *
  unfold permutationSign
  cases count with increases | decreases
  . rw [increases, monoidPow.succ]
    ring
  . rw [decreases, monoidPow.succ]
    ring

-- Induct on the upper position, conjugating the smaller exchange by the
-- adjacent exchange (b, b+1). Three sign reversals give one sign reversal.
theorem permutationSign.exchange_ordered_induction (n b : Nat)
  shows ∀ a, Nat(a) → a ∈ n → b ∈ n → a < b → ∀ p ∈ permutations(n),
    permutationSign(n, A, add, zero, neg, mul, one, permutationExchange(n, a, b)(p)) = R[-permutationSign(n, A, add, zero, neg, mul, one, p)]
proof
  induction b
  | zero =>
    intros a natural ha hb below p permutation
    have impossible := membership.of_Less with natural, below
    rw nat.zero at impossible
    exfalso
    exact set.empty with impossible
  | succ(k) using ih =>
    intros a natural ha hb below p permutation
    have alternatives : a = k ∨ a ≠ k by tauto
    cases alternatives with same | different
    . rw same
      have hk : k ∈ n by rwa ← same
      exact permutationSign.adjacent with *
    . have smaller := Less.of_successor_upper_ne at a, k with *
      have ordinal := Ordinal.natural at n with *
      have transitive := Ordinal.transitive with ordinal
      have prefix := transitive with succ(k), hb
      have kBefore := membership.self_successor at k with *
      have hk := prefix with k, kBefore
      have lowerDistinct : k ≠ succ(k)
        intro equal
        have bad : k ∈ k by rwa ← equal at kBefore
        exact membership.irreflexive with bad
      have outerDistinct : a ≠ succ(k)
        intro equal
        have membership := membership.of_Less with natural, below
        rw ← equal at membership
        exact membership.irreflexive with membership
      have function := permutationExchange.function at n, k, succ(k) with *
      have middleFunction := permutationExchange.function at n, a, k with *
      have p1 := FunctionBetween.apply_closed with function, permutation
      have p2 := FunctionBetween.apply_closed with middleFunction, p1
      have first := permutationSign.adjacent at A, add, zero, neg, mul, one, n, k, p with *
      have middle := ih with a, natural, ha, hk, smaller, permutationExchange(n, k, succ(k))(p), p1
      have last := permutationSign.adjacent at A, add, zero, neg, mul, one, n, k, permutationExchange(n, a, k)(permutationExchange(n, k, succ(k))(p)) with *
      have conjugate := permutationExchange.conjugate at n, a, k, succ(k), p with *
      have value := permutationSign.closed at A, add, zero, neg, mul, one, n, p with *
      rw [← conjugate, last, middle, first]
      ring

theorem permutationSign.exchange (n : Nat) (a b p : Set)
  requires ha : a ∈ n
  requires hb : b ∈ n
  requires distinct : a ≠ b
  requires permutation : p ∈ permutations(n)
  shows permutationSign(n, A, add, zero, neg, mul, one, permutationExchange(n, a, b)(p)) = R[-permutationSign(n, A, add, zero, neg, mul, one, p)]
proof
  have naturals := natural.member with *
  have naturalA := naturals with a, ha
  have naturalB := naturals with b, hb
  have comparison := Less.trichotomy at a, b with *
  cases comparison with before | remaining
  . have induction := permutationSign.exchange_ordered_induction at A, add, zero, neg, mul, one, n, b with *
    exact induction with a, naturalA, ha, hb, before, p, permutation
  . cases remaining with same | after
    . exfalso
      exact distinct with same
    . have induction := permutationSign.exchange_ordered_induction at A, add, zero, neg, mul, one, n, a with *
      have reverse := induction with b, naturalB, hb, ha, after, p, permutation
      have symmetric := permutationExchange.symmetric with ha, hb
      rwa symmetric

theorem determinant.equal_rows (n : Nat) (a b M : Set)
  requires matrix : RingMatrix(n, R, M)
  requires ha : a ∈ n
  requires hb : b ∈ n
  requires distinct : a ≠ b
  requires rows : ∀ j ∈ n, M[a, j] = M[b, j]
  shows determinant(n, R, M) = R[0]
proof
  have signs : ∀ p ∈ permutations(n), permutationSign(n, A, add, zero, neg, mul, one, permutationExchange(n, a, b)(p)) = R[-permutationSign(n, A, add, zero, neg, mul, one, p)]
    intros p member
    exact permutationSign.exchange with *
  exact determinant.equal_rows_of_exchange_sign with *

theorem determinant.equal_adjacent_rows (n a : Nat) (M : Set)
  requires matrix : RingMatrix(n, R, M)
  requires ha : a ∈ n
  requires hb : succ(a) ∈ n
  requires rows : ∀ j ∈ n, M[a, j] = M[succ(a), j]
  shows determinant(n, R, M) = R[0]
proof
  have distinct : a ≠ succ(a)
    have below : a < succ(a) by arith
    intro same
    have impossible : a < a by arith
    have excluded := Less.irreflexive at a with *
    exact excluded with impossible
  have signs : ∀ p ∈ permutations(n), permutationSign(n, A, add, zero, neg, mul, one, permutationExchange(n, a, succ(a))(p)) = R[-permutationSign(n, A, add, zero, neg, mul, one, p)]
    intros p member
    exact permutationSign.adjacent with *
  exact determinant.equal_rows_of_exchange_sign with *

end Signs