-- Copying a matrix row as a function graph, with coordinate equations (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.MatrixRows
import Determinant

defunique matrixCopyRowEntry (I A M i r p : Set) (a ∈ A) :=
  ∃ k ∈ I, ∃ j ∈ I, p = (k, j) ∧
    (k = i → a = M[r, j]) ∧ (k ≠ i → a = M[k, j])
requires matrix : RingMatrix(I, A, M)
requires source : r ∈ I
requires pair : p ∈ I × I
proof
  obtain ⟨bound, k, hk, j, hj, shape⟩ := product.membership.forward at
    I, I, p with pair
  have original := RingMatrix.entry at I, A, M, k, j with *
  have copied := RingMatrix.entry at I, A, M, r, j with *
  have alternatives : k = i ∨ k ≠ i
    tauto
  cases alternatives with same | different
  . refine ⟨M[r, j], copied, k, hk, j, hj, shape, ?_⟩
    constructor
    . intro equal
      rfl
    . intro unequal
      exfalso
      exact unequal with same
  . refine ⟨M[k, j], original, k, hk, j, hj, shape, ?_⟩
    constructor
    . intro equal
      exfalso
      exact different with equal
    . intro unequal
      rfl
uniqueness
  intros u hu first v hv second
  obtain ⟨k, hk, j, hj, shapeU, sameU, otherU⟩ := first
  obtain ⟨l, hl, s, hs, shapeV, sameV, otherV⟩ := second
  have pairs : (k, j) = (l, s)
    cc
  have coordinates := orderedPair.injective at k, j, l, s with pairs
  have alternatives : k = i ∨ k ≠ i
    tauto
  cases alternatives with same | different
  . have left : u = M[r, j]
      exact sameU with same
    have right : v = M[r, s]
      apply sameV
      cc
    cc
  . have left : u = M[k, j]
      exact otherU with different
    have distinct : l ≠ i
      intro equal
      apply different
      cc
    have right := otherV with distinct
    cc

defgraph matrixCopyRow (I A M i r : Set) (p ∈ I × I) : A := matrixCopyRowEntry(I, A, M, i, r, p)
requires matrix : RingMatrix(I, A, M)
requires source : r ∈ I
proof
  have selected := matrixCopyRowEntry.selected at I, A, M, i, r, p with *
  exact selected.left

theorem matrixCopyRow.matrix (I A M i r : Set)
  requires matrix : RingMatrix(I, A, M)
  requires source : r ∈ I
  shows RingMatrix(I, A, matrixCopyRow(I, A, M, i, r))
proof
  unfold RingMatrix
  exact matrixCopyRow.function with *

theorem matrixCopyRow.entry (I A M i r k j : Set)
  requires matrix : RingMatrix(I, A, M)
  requires source : r ∈ I
  requires row : k ∈ I
  requires column : j ∈ I
  shows (k = i → matrixCopyRow(I, A, M, i, r)[k, j] = M[r, j]) ∧
    (k ≠ i → matrixCopyRow(I, A, M, i, r)[k, j] = M[k, j])
proof
  have pair := product.pair at k, j, I, I with *
  have value := matrixCopyRow.value at I, A, M, i, r, (k, j) with *
  have selected := matrixCopyRowEntry.selected at I, A, M, i, r, (k, j) with *
  obtain ⟨l, hl, s, hs, shape, same, other⟩ := selected.right
  have coordinates := orderedPair.injective with shape
  rw value
  constructor
  . intro equal
    have match : l = i by cc
    have result := same with match
    cc
  . intro different
    have distinct : l ≠ i
      intro equal
      apply different
      cc
    have result := other with distinct
    cc

-- Public rewrite lemmas avoid unpacking the conditional specification.
theorem matrixCopyRow.same (I A M i r j : Set)
  requires matrix : RingMatrix(I, A, M)
  requires source : r ∈ I
  requires row : i ∈ I
  requires column : j ∈ I
  shows matrixCopyRow(I, A, M, i, r)[i, j] = M[r, j]
proof
  have entry := matrixCopyRow.entry at I, A, M, i, r, i, j with *
  have equal : i = i by rfl
  exact entry.left with equal

theorem matrixCopyRow.other (I A M i r k j : Set)
  requires matrix : RingMatrix(I, A, M)
  requires source : r ∈ I
  requires row : k ∈ I
  requires column : j ∈ I
  requires different : k ≠ i
  shows matrixCopyRow(I, A, M, i, r)[k, j] = M[k, j]
proof
  have entry := matrixCopyRow.entry at I, A, M, i, r, k, j with *
  exact entry.right with different