Copy-pasting identity matrix from infoview

Stream: new members

[Vivek Rajesh Joshi]

I want to copy the LHS of this equality that's currently in my infoview, but the 1 keeps giving me errors no matter how hard I try to specify its type. How do I do this?

∑ x : Fin m,
    (OfNat.ofNat 1 ⟨↑r + ↑i + 1, ⋯⟩ x + -(cr * OfNat.ofNat 1 i x)) *
      Matrix.updateRow 1 ⟨↑s + ↑i + 1, ⋯⟩ (OfNat.ofNat 1 ⟨↑s + ↑i + 1, ⋯⟩ + -(cs • OfNat.ofNat 1 i)) x
        ⟨↑r + ↑i + 1, ⋯⟩ =
  ∑ x : Fin m,
    OfNat.ofNat 1 ⟨↑r + ↑i + 1, ⋯⟩ x *
      Matrix.updateRow 1 ⟨↑r + ↑i + 1, ⋯⟩ (OfNat.ofNat 1 ⟨↑r + ↑i + 1, ⋯⟩ + -(cr • OfNat.ofNat 1 i)) x ⟨↑r + ↑i + 1, ⋯⟩

[Kyle Miller]

What version of Lean are you using? (You can do #eval Lean.versionString). I'm a bit surprised to see OfNat.ofNat 1 here.

Could you make a #mwe that creates this term in the Infoview?

[Vivek Rajesh Joshi]

Sure, here you go:

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) --(Matrix.diagonal (fun _:Fin m => (1:Rat)))

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

lemma rval_ival_lt (i : Fin m) (r : Fin (m-i-1)) : r.1+i.1+1 < m :=
  Nat.add_assoc _ _ _ ▸ (Nat.add_lt_of_lt_sub (Eq.subst (Nat.sub_sub m i.1 1) (r.2)))

lemma elt_elimColBelow_eq_rowMulAdd : E ∈ elimColBelow_ij M i j → ∃ r, E = rowMulAdd (-M ⟨↑r+↑i+1,rval_ival_lt i r⟩ j) ⟨↑r+↑i+1,rval_ival_lt i r⟩ i := by
  unfold elimColBelow_ij
  rw [List.mem_ofFn]
  simp
  intro r hE
  exact ⟨r,symm hE⟩

lemma elimEltBelow (hpiv : M i j = 1) (r : Fin (m-i-1)) :
  (ElemOpOnMatrix (rowMulAdd (-M ⟨r+i+1,rval_ival_lt i r⟩ j) ⟨r+i+1,rval_ival_lt i r⟩ i) M) ⟨r+i+1,rval_ival_lt i r⟩ j = 0 := by
  rw [ElemOpOnMatrix]; simp [hpiv]

theorem elimColBelow_length : (elimColBelow_ij M i j).length = m-i-1 := by
  rw [elimColBelow_ij]; simp

lemma elimColBelow_get_eq_rowMulAdd (i : Fin m) (j : Fin n) (r : Fin (m-i-1)) :
  (elimColBelow_ij M i j).get (r.cast (Eq.symm (elimColBelow_length M))) = rowMulAdd (-M ⟨↑r+↑i+1,rval_ival_lt i r⟩ j) ⟨↑r+↑i+1,rval_ival_lt i r⟩ i := by
  unfold elimColBelow_ij
  simp

lemma elimColbelow_get_elim_r (i : Fin m) (j : Fin n) (r : Fin (m-i-1)) (hpiv : M i j = 1) :
  (ElemOpOnMatrix ((elimColBelow_ij M i j).get (r.cast (Eq.symm (elimColBelow_length M)))) M) ⟨r+i+1,rval_ival_lt i r⟩ j = 0 := by
  rw [elimColBelow_get_eq_rowMulAdd,elimEltBelow _ hpiv]

lemma rowMulAdd_otherRows (i j : Fin m) (k : Fin m) (hk : k ≠ i) (c : Rat) :
  (ElemOpOnMatrix (rowMulAdd c i j) M) k = M k := by
  rw [ElemOpOnMatrix]; simp; exact Matrix.updateRow_ne hk

lemma elimColBelow_get_elim_notr (i : Fin m) (j : Fin n) (r : Fin (m-i-1)) (s : Fin (m-i-1)) (hsr : s≠r) :
  (ElemOpOnMatrix ((elimColBelow_ij M i j).get (r.cast (Eq.symm (elimColBelow_length M)))) M) ⟨s+i+1,rval_ival_lt i s⟩ j = M ⟨s+i+1,rval_ival_lt i s⟩ j := by
  rw [elimColBelow_get_eq_rowMulAdd,rowMulAdd_otherRows]
  simp [Fin.val_ne_of_ne hsr]

lemma elimColBelow_elt_commute (e e' : ElemOp) (he : e ∈ elimColBelow_ij M i j) (he' : e' ∈ elimColBelow_ij M i j) (hee' : e ≠ e') :
  e.elemMat * e'.elemMat = e'.elemMat * e.elemMat := by
  obtain ⟨r,hr⟩ := elt_elimColBelow_eq_rowMulAdd M he
  obtain ⟨s,hs⟩ := elt_elimColBelow_eq_rowMulAdd M he'
  set cr := M ⟨↑r + ↑i + 1, ⋯⟩ j with hcr
  set cs := M ⟨↑s + ↑i + 1, ⋯⟩ j with hcs
  rw [hr,hs] at hee' ⊢
  apply Matrix.ext
  intro p q
  rw [Matrix.mul_apply,Matrix.mul_apply]
  have hrs : r.1+i+1≠s+i+1 := by
    simp only [ne_eq, rowMulAdd.injEq, neg_inj, Fin.mk.injEq, add_left_inj, and_true, not_and'] at hee'
    by_cases h0 : r=s
    · have h1 := hee' (Fin.val_eq_of_eq h0)
      rw [hcr,hcs,h0] at h1
      contradiction
    · simp [Fin.val_ne_of_ne h0]
  by_cases hp : p=⟨↑r + ↑i + 1,rval_ival_lt i r⟩
  · have hrs' : Fin.mk (↑r + ↑i + 1) (rval_ival_lt i r) ≠ ⟨↑s + ↑i + 1,rval_ival_lt i s⟩ := by simp [hrs]
    simp_rw [hp,elemMat,ElemOpOnMatrix,Matrix.updateRow_self,Matrix.updateRow_ne hrs']
    by_cases hq : q=⟨↑r + ↑i + 1,rval_ival_lt i r⟩
    · simp [hq]
      have h1 : ∑ x : Fin m, ((1:Matrix (Fin m) (Fin n) Rat) ⟨↑r + ↑i + 1, ⋯⟩ x + -(cr * (1:Matrix (Fin m) (Fin n) Rat) i x)) * Matrix.updateRow (1:Matrix (Fin m) (Fin n) Rat) ⟨↑s + ↑i + 1, ⋯⟩ ((1:Matrix (Fin m) (Fin n) Rat) ⟨↑s + ↑i + 1, ⋯⟩ + -(cs • (1:Matrix (Fin m) (Fin n) Rat) i)) x ⟨↑r + ↑i + 1, ⋯⟩ = 1 := by
        simp

I'm using 4.9.0-rc1

[Kyle Miller]

Thanks. There seems to be a bug in simp leading to nested OfNat.ofNat expressions.

The OfNat.ofNat 1 is supposed to be 1. You can write (1 : Matrix (Fin m) (Fin m) ℚ) in place of it. I figured that out by hovering over OfNat.ofNat.

By the way, if this bug weren't there, you could set the following option to see type ascriptions on numbers.

set_option pp.numericTypes true

[Kyle Miller]

(Issue reported at lean4#4462)

[Vivek Rajesh Joshi]

Kyle Miller said:

The OfNat.ofNat 1 is supposed to be 1. You can write (1 : Matrix (Fin m) (Fin m) ℚ) in place of it. I figured that out by hovering over OfNat.ofNat.

I did that for h1, but it says that type cannot be synthesised

[Kyle Miller]

I see you updated your MWE with what you tried. Notice that in what I wrote it's m and m, but you have m and n.

[Vivek Rajesh Joshi]

No updates, it was already there. But yea, it is m and n, my bad. m and m should work

[Vivek Rajesh Joshi]

Thanks for the help!

[Eric Wieser]

Kyle Miller said:

Thanks. There seems to be a bug in simp leading to nested OfNat.ofNat expressions.

The OfNat.ofNat 1 is supposed to be 1.

Is this a nested ofNat, or a delaboration bug?

[Kyle Miller]

It's definitely a nested ofNat, you can check out the mwe on the issue