Symmetric function as constructor of inductive type

Stream: new members

[Vivek Rajesh Joshi]

import Mathlib.Data.Matrix.Notation

inductive ElemOp (m : ℕ) : Type where
| scalarMul (c : Rat) (hc : c≠0) (i : Fin m) : ElemOp m
| rowSwap (i : Fin m) (j : Fin m) : ElemOp m
| rowMulAdd (c : Rat) (i : Fin m) (j : Fin m) (hij : i≠j) : ElemOp m
deriving Repr,BEq

namespace ElemOp

def ElemOpOnMatrix (E : ElemOp m) (A : Matrix (Fin m) (Fin k) Rat) : Matrix (Fin m) (Fin k) Rat :=
match E with
| scalarMul c _ i => A.updateRow i (c • (A i))
| rowSwap i j => let newr := (A i)
    Matrix.updateRow (Matrix.updateRow A i (A j)) j newr
| rowMulAdd c i j _ => A.updateRow i (A i + (c • (A j)))

def elemMat (E : ElemOp m) := ElemOpOnMatrix E (1:Matrix (Fin m) (Fin m) Rat)

I'm in a catch-22 situation here. I want to prove that two ElemOps are equal if their respectiveelemMats are equal, given that the elemMats aren't 1. To do so, I realised that I need to show that ElemOp.rowSwap is symmetric, i.e. rowSwap i j = rowSwap j i. But I don't know any way to do so other than through this theorem I'm currently proving. Any suggestions?

[Kevin Buzzard]

That claim isn't true, the rowSwaps are different terms of your type (because they were made in different ways) but they do the same thing to matrices.

[Kevin Buzzard]

Why do you care about the behaviour of equality on ElemOp by the way? You could work your way around it by asking instead for an unordered pair input plus a proof that the elements in the pair are distinct but this seems like a lot of fuss and I'm not really clear about what your actual goal is.

[Vivek Rajesh Joshi]

I see. I wanted the equality to prove that a function I designed to return ElemOps that eliminate a column of a matrix actually does that. It does seem better to redefine the function to work around the problem, thanks for the suggestion!