Giving multiple names to a custom type

Stream: new members

[Vivek Rajesh Joshi]

Suppose I have defined a custom inductive type called RowEchelonForm as below:

variable (F : Type) [Field F] [DecidableEq F]

inductive RowEchelonForm : (m n : Nat) → Type where
| nil : RowEchelonForm m 0
| pad : RowEchelonForm m n → RowEchelonForm m (n+1)
| extend : RowEchelonForm m n → (Fin n → F) → RowEchelonForm (m+1) (n+1)
deriving Repr

Is it possible to also assign the name REF to this type, for the sake of convenience?

[Johan Commelin]

Do you mean something like

abbrev REF := RowEchelonForm

[Johan Commelin]

Or do you want local notation?

[Vivek Rajesh Joshi]

No, not local. I guess the former is what I was looking for.
Thanks!

[Vivek Rajesh Joshi]

Doesn't quite work the way I want it to, though. I want to be able to use RowEchelonForm and REF interchangeably, but I'm facing a problem here:

import Mathlib.Data.Matrix.Notation
import Mathlib.Data.Fin.Tuple.Reflection

variable {F : Type} [Field F] [DecidableEq F]

variable (F) in
inductive RowEchelonForm : (m n : Nat) → Type where
| nil : RowEchelonForm m 0
| pad : RowEchelonForm m n → RowEchelonForm m (n+1)
| extend : RowEchelonForm m n → (Fin n → F) → RowEchelonForm (m+1) (n+1)
deriving Repr

abbrev REF := RowEchelonForm

def REF.toMatrix (R : REF F m n) : Matrix (Fin m) (Fin n) F :=
  match R with
  | nil => fun _ => ![]        --gives an error
  | pad R0 => FinVec.map (fun r => (Matrix.vecCons 0 r)) R0.toMatrix
  | extend R0 v => Matrix.vecCons (Matrix.vecCons 1 v) (FinVec.map (fun r => (Matrix.vecCons 0 r)) R0.toMatrix)

def RowEchelonForm.toMatrix (R : RowEchelonForm F m n) : Matrix (Fin m) (Fin n) F :=
  match R with
  | nil => fun _ => ![]        --works fine
  | pad R0 => FinVec.map (fun r => (Matrix.vecCons 0 r)) R0.toMatrix
  | extend R0 v => Matrix.vecCons (Matrix.vecCons 1 v) (FinVec.map (fun r => (Matrix.vecCons 0 r)) R0.toMatrix)

[Kevin Buzzard]

What happens if you open RowEchelonForm? This is done automatically with the second definition

[Vivek Rajesh Joshi]

This is what happens:

import Mathlib.Data.Matrix.Notation
import Mathlib.Data.Fin.Tuple.Reflection

variable {F : Type} [Field F] [DecidableEq F]

variable (F) in
inductive RowEchelonForm : (m n : Nat) → Type where
| nil : RowEchelonForm m 0
| pad : RowEchelonForm m n → RowEchelonForm m (n+1)
| extend : RowEchelonForm m n → (Fin n → F) → RowEchelonForm (m+1) (n+1)
deriving Repr

abbrev REF := RowEchelonForm

open RowEchelonForm

def REF.toMatrix (R : REF F m n) : Matrix (Fin m) (Fin n) F :=
  match R with
  | nil => fun _ => ![]
  | pad R0 => FinVec.map (fun r => (Matrix.vecCons 0 r)) R0.toMatrix    --does not recognise R0.toMatrix
  | extend R0 v => Matrix.vecCons (Matrix.vecCons 1 v) (FinVec.map (fun r => (Matrix.vecCons 0 r)) R0.toMatrix)

[Vivek Rajesh Joshi]

I know I can get by with some small changes to the function definition, but I want to see if there's a way to use RowEchelonForm and REF interchangeably first

[Eric Wieser]

but I want to see if there's a way to use RowEchelonForm and REF interchangeably first

I don't think there is. Making REF F m n work the same way as RowEchelonForm F m n is easy, but there's nothing you can do to make def REF.foo work the same way as def RowEchelonForm.foo