Define equality for custom inductive types?

Stream: new members

[Vivek Rajesh Joshi]

I have defined row operations on matrices as terms of an inductive type (ElemOp) , and I want to use a function on them that requires synthesis of the typeBEq ElemOp. How do I do so?

import Mathlib.Data.Matrix.Notation
import Mathlib.Tactic.Linarith

variable (M : Matrix (Fin m) (Fin n) Rat) (hm : m>0) (hn : n>0)

inductive ElemOp : Type where
| scalarMul (c : Rat) (hc : c≠0) (i : Fin m) : ElemOp
| rowSwap (i : Fin m) (j : Fin m) : ElemOp
| rowMulAdd (c : Rat) (i : Fin m) (j : Fin m) : ElemOp

namespace ElemOp

def ElemOpOnMatrix  (E : ElemOp (m:=m)) (A : Matrix (Fin m) (Fin n) Rat) : Matrix (Fin m) (Fin n) 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 listElemOpOnMatrix (l : List (ElemOp (m:=m))) (A : Matrix (Fin m) (Fin n) Rat) : Matrix (Fin m) (Fin n) Rat :=
  match l with
  | [] => A
  | E::as => ElemOpOnMatrix E (listElemOpOnMatrix as A)

def elimColBelow_ij (i:Fin m) (j:Fin n) : List (ElemOp (m:=m)) :=
  List.ofFn fun r : Fin (m-i-1) =>
  have h : r.val+(i.val+1)<m := (Nat.add_lt_of_lt_sub (Eq.subst (Nat.sub_sub m i.1 1) (r.2)))
  rowMulAdd (-M ⟨r+i+1,h⟩ j) ⟨r+i+1,h⟩ i

example (Er : ElemOp) (hEr : Er ∈ elimColBelow_ij M i j) :
  listElemOpOnMatrix (elimColBelow_ij M i j) M = listElemOpOnMatrix ((elimColBelow_ij M i j).erase Er) (ElemOpOnMatrix Er M) := by

[Markus Schmaus]

What you want is the default BEq, which you can get using deriving BEq with your inductive type:

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

[Vivek Rajesh Joshi]

Thanks, that works

[Vivek Rajesh Joshi]

Hey, back here once again. I want to define equality of two of these ElemOp elements in terms of their elementary matrices, i.e. two ElemOps e and e' are equal if their ElemOpOnMatrix e 1 and their ElemOpOnMatrix e' 1 are equal. (Refer to the MWE in the 1st message). Do I have to take 3 cases each among e and e' to do this, or is there a neater way to do this?

[Yaël Dillies]

What do you mean by "defining equality"?

[Vivek Rajesh Joshi]

I want to prove the statement in the above message

[Vivek Rajesh Joshi]

Basically this:

import Mathlib.Data.Matrix.Notation
import Mathlib.Tactic.Linarith

variable (M : Matrix (Fin m) (Fin n) Rat) (hm : m>0) (hn : n>0)

inductive ElemOp : Type where
| scalarMul (c : Rat) (hc : c≠0) (i : Fin m) : ElemOp
| rowSwap (i : Fin m) (j : Fin m) : ElemOp
| rowMulAdd (c : Rat) (i : Fin m) (j : Fin m) : ElemOp

namespace ElemOp

def ElemOpOnMatrix  (E : ElemOp (m:=m)) (A : Matrix (Fin m) (Fin n) Rat) : Matrix (Fin m) (Fin n) 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:=m)) := ElemOpOnMatrix E (1:Matrix (Fin m) (Fin m) Rat)

theorem ElemOp_eq_iff_elemMat (e e' : ElemOp (m:=m)) : e = e' ↔ e.elemMat = e'.elemMat := by

[Yaël Dillies]

Yeah, you need to case

[Vivek Rajesh Joshi]

Sounds like a lot of work for something quite trivial, the proof will end up being around 50 lines. Are you sure there's no better way?

[Yaël Dillies]

You are trying to show injectivity of elemMat. There are two general strategies:

1. Show that e.elemMat = e'.elemMat → e = e'
2. Show that there is some function g such that g ∘ elemMat = id

[Yaël Dillies]

You could try the second strategy

[Vivek Rajesh Joshi]

I see, I'll try it out