Matrix inverse and group structure

Stream: new members

[gjohn]

Hello everyone,
I have started learning lean recently ( <3 weeks) and need some help with making a proof more readable.

import Mathlib.Algebra.Group.Defs
import Mathlib.Data.Matrix.Basic
import Mathlib.Data.Fin.Basic
import Mathlib.Data.Real.Basic
import Mathlib.Tactic

open Matrix

namespace GTheory_Physics

abbrev M2R := Matrix ( Fin 2) (Fin 2) ℚ

namespace M2R

-- def I2 : M2R := 1

@[simp] def e : M2R := !![1,0; 0,1]

@[simp] def a : M2R := !![0, -1; 1,  0]

@[simp] def b : M2R := !![-1,  0; 0, -1]

@[simp] def c : M2R := !![0,  1;-1, 0]


@[simp] def S: Finset M2R := {e, a, b, c}

abbrev M2R₄ := {m: M2R // m ∈ S}

theorem mul_closed (a b: M2R) (ha: a ∈ S) (hb: b ∈ S ) : (a * b) ∈ S := by
    sorry

instance: Mul M2R₄ where
    mul a b := ⟨a.val * b.val, mul_closed a.val b.val a.prop b.prop ⟩

noncomputable def m2r_inv (x: M2R) : M2R :=
    if x = e then e
    else if x = a then c
    else if x = c then a
    else if x = b then b
    else x⁻¹

theorem inv_closed (a : M2R) (ha: a ∈ S) : m2r_inv a ∈ S := by
    sorry

noncomputable instance: Inv M2R₄ where
    inv a := ⟨m2r_inv a.val, inv_closed a.val a.prop⟩

instance : One M2R₄  :=
    ⟨e, by decide⟩

theorem mul_def (a b: M2R₄) :
    a * b = ⟨a.val * b.val, mul_closed a.val b.val a.prop b.prop ⟩ :=
    rfl

theorem inv_def (a: M2R₄) :
    a⁻¹ = ⟨m2r_inv a.val, inv_closed a.val a.prop⟩ :=
    rfl

theorem one_def : ( 1: M2R₄) = ⟨e, by decide⟩ :=
    rfl

noncomputable def M2RGroup: Group M2R₄ where
  mul := ( · * · )
  mul_assoc a b c := by sorry
  one := 1
  one_mul := by
    intro x
    ext i j
    fin_cases i; fin_cases j
    repeat
        rw [one_def]
        rw[mul_def]
        dsimp [Matrix.mul_apply]
        rw [Fin.sum_univ_two]
        norm_num
  mul_one := by
    intro x
    ext i j
    fin_cases i; fin_cases j
    repeat
        rw [mul_def]
        rw [one_def]
        dsimp [Matrix.mul_apply]
        rw [Fin.sum_univ_two]
        norm_num
    fin_cases j
    repeat
        norm_num
  inv := ( · ⁻¹ )
  inv_mul_cancel := by
    intro x
    obtain ⟨m, hm⟩ := x
    ext i j
    rw [inv_def]
    rw [mul_def]
    rw[one_def]
    dsimp [Matrix.mul_apply]
    dsimp [m2r_inv]
    rw [Fin.sum_univ_two]
    fin_cases i; fin_cases j
    repeat
            fin_cases hm;
            dsimp [m2r_inv]
            norm_num
            repeat
                dsimp [m2r_inv]
                simp
                exact rfl
    repeat
        fin_cases j
        repeat
            dsimp [m2r_inv]
            simp
            exact rfl

1. Primary Question: Is there a better definition of inverse - one which doesn't use if else? If i try to use simply $$ x\inv $$ it gets really weird knowing that $$ x\inv $$ doesn't always exist.
2. Optional: can i avoid very basic arithmatic and work on a little higher level knowing the equation of matrices can be unbundled to a equation involving individual elements? Maybe it is because i am new to lean, it seems like a lot of work to prove the simple structure.

Thank you for your time and attention.

[gjohn]

i could simplify a lot after tagging my theorems with @[simp]

@[simp] def e : M2R := !![1,0; 0,1]

@[simp] def a : M2R := !![0, -1; 1,  0]

@[simp] def b : M2R := !![-1,  0; 0, -1]

@[simp] def c : M2R := !![0,  1;-1, 0]


@[simp] def S: Finset M2R := {e, a, b, c}

abbrev M2R₄ := {m: M2R // m ∈ S}

theorem mul_closed (a b: M2R) (ha: a ∈ S) (hb: b ∈ S ) : (a * b) ∈ S := by
    sorry

instance: Mul M2R₄ where
    mul a b := ⟨a.val * b.val, mul_closed a.val b.val a.prop b.prop ⟩

@[simp]
noncomputable def m2r_inv (x: M2R) : M2R :=
    if x = e then e
    else if x = a then c
    else if x = c then a
    else if x = b then b
    else x⁻¹

theorem inv_closed (a : M2R) (ha: a ∈ S) : m2r_inv a ∈ S := by
    sorry
    -- simp
    -- fin_cases ha
    -- any_goals
    --     simp

noncomputable instance: Inv M2R₄ where
    inv a := ⟨m2r_inv a.val, inv_closed a.val a.prop⟩

instance : One M2R₄  :=
    ⟨e, by decide⟩

@[simp]
theorem mul_def (a b: M2R₄) :
    a * b = ⟨a.val * b.val, mul_closed a.val b.val a.prop b.prop ⟩ :=
    rfl

@[simp]
theorem inv_def (a: M2R₄) :
    a⁻¹ = ⟨m2r_inv a.val, inv_closed a.val a.prop⟩ :=
    rfl

@[simp]
theorem one_def : ( 1: M2R₄) = ⟨e, by decide⟩ :=
    rfl

noncomputable def M2RGroup: Group M2R₄ where
  mul := ( · * · )
  mul_assoc a b c := by
    simp
    apply Matrix.mul_assoc
  one := 1
  one_mul := by
    intro x
    simp
    ext i j
    fin_cases i;
    all_goals
        simp
        fin_cases j;
        all_goals
            simp
            fin_cases x
            all_goals
                simp
  mul_one := by
    intro x
    simp
    ext i j
    fin_cases i;
    all_goals
        simp
        fin_cases j;
        all_goals
            simp
            fin_cases x
            all_goals
                simp
  inv := ( · ⁻¹ )
  inv_mul_cancel := by
    intro x
    simp
    ext i j
    fin_cases i;
    all_goals
        simp
        fin_cases j;
        all_goals
            simp
            fin_cases x
            any_goals
                simp
            any_goals
                exact rfl

some goals get proved using just simp while some need first simp and then exact refl.
is there a tactic which allows specifying a set of tactics and applies them only till a goal is solved and then moves on to next case? so that i would be able to say:

            fin_cases x
            any_partial_goals
                simp          -- stop here if you are done
                exact rfl    -- come here only if you need to

[Matt Diamond]

I don't think it's "really weird" to use x⁻¹ when the inverse doesn't always exist. This is actually a common strategy that's used throughout Lean/Mathlib. This blog post might help explain it:

https://xenaproject.wordpress.com/2020/07/05/division-by-zero-in-type-theory-a-faq/

[Matt Diamond]

the idea is that the validity of the operation doesn't matter when you're performing it... it only matters when you're trying to prove something about the result of performing it

[Matt Diamond]

It's simpler this way:

noncomputable def m2r_inv (x: M2R) : M2R := x⁻¹

theorem inv_closed (a : M2R) (ha: a ∈ S) : m2r_inv a ∈ S := by
  fin_cases ha <;> simp [Matrix.inv_def]

Also, here's a simpler proof of inv_mul_cancel:

inv_mul_cancel := by
  intro x
  simp
  rw [Matrix.nonsing_inv_mul]
  · decide
  · fin_cases x <;> simp

In general you can save some lines by making use of the <;> operator. It takes the result of the left-hand side and applies the right-hand side to all generated goals. For example:

one_mul := by
  intro x
  ext i j
  fin_cases i <;> fin_cases j <;> fin_cases x <;> simp

(and you can use the same proof for mul_one)

[Aaron Liu]

gjohn said:

is there a tactic which allows specifying a set of tactics and applies them only till a goal is solved and then moves on to next case? so that i would be able to say:

            fin_cases x
            any_partial_goals
                simp          -- stop here if you are done
                exact rfl    -- come here only if you need to

I wrote one just now:

import Lean

syntax (name := partialGoals)
  "partial_goals" withPosition((ppLine linebreak ppIndent(colEq tactic))+) : tactic

@[tactic partialGoals]
def elabPartialGoals : Lean.Elab.Tactic.Tactic := fun stx => do
  for tac in stx[1].getArgs do
    Lean.Elab.Tactic.evalTactic tac
    if (← Lean.Elab.Tactic.getUnsolvedGoals).length = 0 then return

You can combine this with any_goals to get what you want.

[Yakov Pechersky]

any_goals try simp
any_goals try rfl

also?

[gjohn]

Thank you @Matt Diamond it makes sense to use inverse directly. also <;> makes it much cleaner.
Thanks @Aaron Liu i tried it and it works nicely. also the syntax of defining tactic is pretty readable.

[gjohn]

I have a related syntactical question.

-- Z4 is ZMod 4
def m2r_eq_z4 : M2R.M2R₄ ≃ Z4 where
  toFun := fun x =>
    if x.val = M2R.e then 0
    else if x.val = M2R.a then 1
    else if x.val = M2R.b then 2
    else 3  -- This must be M2R.c due to the subset type constraint

  invFun := fun x =>
    if x = 0 then ⟨M2R.e, by decide⟩
    else if x = 1 then ⟨M2R.a, by decide⟩
    else if x = 2 then ⟨M2R.b, by decide⟩
    else ⟨M2R.c, by decide⟩  -- This must be 3 due to Z4 having only 4 elements

  left_inv := by
    sorry

  right_inv := by
    sorry

Can i avoid if else if blocks? Because of it, simp results in some really big if else intermediate statements which makes it harder to reason about where things went wrong.
I tried following syntax:

  toFun := fun x =>
    match x.val with
    | M2R.e => 0
    | M2R.a => 1
    | M2R.b => 2
    | M2R.c => 3

but compiler complains invalid pattern variable, must be atomic.

[Yakov Pechersky]

MWE would help. You can make your own custom recursor first

def M2R.M2R4.rec {motive : M2R.M2R₄ -> Sort*} (he : motive M2R.e) (ha : motive M2R.a) (hb : motive M2R.b) (hc : motive M2R.c) (x : M2R.M2R₄) : motive x := by
  _

[Yakov Pechersky]

and stuff the ugly case bashing in there

[gjohn]

Thank you @Yakov Pechersky
Let me try this.
I would post mwe if this doesn't help directly.

[gjohn]

Here it is @Yakov Pechersky

import Mathlib.Algebra.Group.Defs
import Mathlib.Data.Matrix.Basic
import Mathlib.Data.Fin.Basic
import Mathlib.Data.Real.Basic
import Mathlib.Tactic

abbrev M2R := Matrix ( Fin 2) (Fin 2) ℚ

@[simp] def e : M2R := !![1,0; 0,1]

@[simp] def a : M2R := !![0, -1; 1,  0]

@[simp] def b : M2R := !![-1,  0; 0, -1]

@[simp] def c : M2R := !![0,  1;-1, 0]


@[simp] def S: Finset M2R := {e, a, b, c}

abbrev M2R₄ := {m: M2R // m ∈ S}
abbrev Z4 := ZMod 4


def m2r_eq_z4 : M2R₄ ≃ Z4 where
  toFun := fun x =>
    if x.val = e then 0
    else if x.val = a then 1
    else if x.val = b then 2
    else 3  -- This must be M2R.c due to the subset type constraint

  invFun := fun x =>
    if x = 0 then ⟨e, by decide⟩
    else if x = 1 then ⟨a, by decide⟩
    else if x = 2 then ⟨b, by decide⟩
    else ⟨c, by decide⟩  -- This must be 3 due to Z4 having only 4 elements

  left_inv := by
    sorry

  right_inv := by
    sorry

[Yakov Pechersky]

import Mathlib.Algebra.Group.Defs
import Mathlib.Data.Matrix.Basic
import Mathlib.Data.Fin.Basic
import Mathlib.Data.Real.Basic
import Mathlib.Tactic

abbrev M2R := Matrix ( Fin 2) (Fin 2) ℚ

namespace M2R

abbrev e' : M2R := !![1,0; 0,1]

abbrev a' : M2R := !![0, -1; 1,  0]

abbrev b' : M2R := !![-1,  0; 0, -1]

abbrev c' : M2R := !![0,  1;-1, 0]

def S : Finset M2R := {e', a', b', c'}

abbrev e : S := ⟨e', by simp [S]⟩
abbrev a : S := ⟨a', by simp [S]⟩
abbrev b : S := ⟨b', by simp [S]⟩
abbrev c : S := ⟨c', by simp [S]⟩

abbrev Z4 := ZMod 4

@[elab_as_elim]
protected def rec {motive : S → Sort*} (he : motive e) (ha : motive a) (hb : motive b) (hc : motive c)
    (x : S) : motive x :=
  if He : x = e then He ▸ he else
  if Ha : x = a then Ha ▸ ha else
  if Hb : x = b then Hb ▸ hb else
  if Hc : x = c then Hc ▸ hc else
  False.elim <| by
    rcases x with ⟨x, hx⟩
    rw [S] at hx
    simp_all

lemma rec_e {motive : S → Sort*} (he ha hb hc) : (M2R.rec he ha hb hc e : motive e) = he := by
  simp [M2R.rec]
lemma rec_a {motive : S → Sort*} (he ha hb hc) : (M2R.rec he ha hb hc a : motive e) = ha := by
  simp only [M2R.rec, Subtype.mk.injEq, EmbeddingLike.apply_eq_iff_eq, eq_rec_constant, ↓reduceDIte,
    dite_eq_ite, ite_eq_right_iff]
  intro H
  simpa using congr_fun₂ H 0 0
lemma rec_b {motive : S → Sort*} (he ha hb hc) : (M2R.rec he ha hb hc b : motive e) = hb := by
  simp only [M2R.rec, Subtype.mk.injEq, EmbeddingLike.apply_eq_iff_eq, eq_rec_constant, ↓reduceDIte,
    dite_eq_ite]
  rw [if_neg, if_neg]
  all_goals
  · intro H
    first
    | simpa using congr_fun₂ H 1 0
    | simpa [neg_eq_iff_add_eq_zero] using congr_fun₂ H 0 0
lemma rec_c {motive : S → Sort*} (he ha hb hc) : (M2R.rec he ha hb hc c : motive e) = hc := by
  simp only [M2R.rec, Subtype.mk.injEq, EmbeddingLike.apply_eq_iff_eq, eq_rec_constant, ↓reduceDIte,
    dite_eq_ite]
  rw [if_neg, if_neg, if_neg]
  all_goals
  · intro H
    simpa [neg_eq_iff_add_eq_zero] using congr_fun₂ H 1 0

lemma S_spec (x : S) : x = e ∨ x = a ∨ x = b ∨ x = c := by
  rcases x with ⟨x, hx⟩
  simpa [S] using hx

def m2r_eq_z4 : S ≃ Z4 where
  toFun := fun x => M2R.rec 0 1 2 3 x
  invFun := fun x => match x with
    | 0 => e
    | 1 => a
    | 2 => b
    | 3 => c
  left_inv := by
    intro x
    dsimp
    generalize hy : (M2R.rec 0 1 2 3 x : Z4) = y
    rcases S_spec x with rfl|rfl|rfl|rfl
    all_goals
    · simp [@rec_e (fun _ ↦ Z4), @rec_a (fun _ ↦ Z4), @rec_b (fun _ ↦ Z4), @rec_c (fun _ ↦ Z4)] at hy
      simp [← hy]
  right_inv := by
    intro y
    fin_cases y
    all_goals
    simp [@rec_e (fun _ ↦ Z4), @rec_a (fun _ ↦ Z4), @rec_b (fun _ ↦ Z4), @rec_c (fun _ ↦ Z4)]
end M2R

[gjohn]

Thanks a lot @Yakov Pechersky
I see it's a little involved - i'll try the definition on my end and see if i can come up with proofs myself.

[gjohn]

I ended up using the if else method:

import Mathlib.Algebra.Group.Defs
import Mathlib.Data.Matrix.Basic
import Mathlib.Data.Fin.Basic
import Mathlib.Data.Real.Basic
import Mathlib.Tactic

abbrev M2R := Matrix ( Fin 2) (Fin 2) ℚ

@[simp] def e : M2R := !![1,0; 0,1]

@[simp] def a : M2R := !![0, -1; 1,  0]

@[simp] def b : M2R := !![-1,  0; 0, -1]

@[simp] def c : M2R := !![0,  1;-1, 0]


@[simp] def S: Finset M2R := {e, a, b, c}

abbrev M2R₄ := {m: M2R // m ∈ S}
abbrev Z4 := ZMod 4

-- Z4 is ZMod 4
def m2r_eq_z4 : M2R₄ ≃ Z4 where
  toFun := fun x =>
    if x.val = e then 0
    else if x.val = a then 1
    else if x.val = b then 2
    else if x.val = c then 3
    else 3  -- This must be c due to the subset type constraint

  invFun := fun x =>
    if x = 0 then ⟨e, by decide⟩
    else if x = 1 then ⟨a, by decide⟩
    else if x = 2 then ⟨b, by decide⟩
    else if x = 3 then ⟨c, by decide⟩
    else ⟨c, by decide⟩  -- This must be 3 due to Z4 having only 4 elements

  left_inv := by
    intro x
    fin_cases x
    any_goals try simp
    any_goals try exact rfl

  right_inv := by
    intro x
    fin_cases x
    any_goals try simp
    any_goals try exact rfl

The reason why i was having issues before was my definition of 1 for Z4. In order to define a group on it i was marking 0 as One and thus my toFun and invFun definitions were incorrect.
that being said the alternative path mentioned above is interesting because it introduces some new syntax to me.
thanks @Yakov Pechersky