Carrying inverse in subtype

Stream: new members

[Yakov Pechersky]

How do I encode a subtype of matrices that have inverses, and then utilize those inverses in a function? I've read the source for #doc/linear_algebra/special_linear_group and #doc/algebra/invertible for ideas on how it operates. I guess my current issue is how to provide a value I have instead of a classical.some _. I thought that my encoding would have inv_matcarry the parent with it. Is it better to encode invertible_matrix as a pair of matrices?

import data.real.basic
import data.matrix.basic
import linear_algebra.matrix

variables (n : ℕ) (R : Type*) [field R]

def invertible_matrix := { A : matrix (fin n) (fin n) R // ∃! B, A * B = 1 ∧ B * A = 1 }

variables {n} {R}
lemma inv_mat_unique {A B C: matrix (fin n) (fin n ) R}
                     (hB : A * B = 1) (hC : C * A = 1) : B = C :=
by rw [<-one_mul B, <-hC, mul_assoc, hB, mul_one]

instance coe_matrix : has_coe (invertible_matrix n R) (matrix (fin n) (fin n) R) :=
⟨λ A, A.val⟩

-- ... proving an existence of an inverse is noncomputable
-- ... because we do not construct it
noncomputable def inv_mat (A : invertible_matrix n R) : matrix (fin n) (fin n) R :=
begin
  choose Ainv hinv using A.property,
  exact Ainv
end

lemma inv_mat_cancel_self (A : invertible_matrix n R) : inv_mat A * A = 1 :=
begin
  obtain ⟨Ainv, ⟨hleft, hright⟩, huniq⟩ := A.property,
  dsimp only [] at *,
  specialize huniq (inv_mat A),
  rw <-hright,
  rw inv_mat at huniq,
  simp at huniq,
  -- huniq : A.val.mul (classical.some _) = 1 →
  --         (classical.some _).mul A.val = 1 →
  --         classical.some _ = Ainv
  rw [huniq hleft hright], -- can't supply a specified value instead of classical.some
  sorry
end

[Yakov Pechersky]

I'm basically struggling to unify the Ainv I get from A.property in the latter lemma with how inv_mat A should be that Ainv due to the definition.

[Kenny Lau]

units

[Yakov Pechersky]

So, forgo subtypes and head directly to structures.

[Kenny Lau]

what is the benefit of using subtype?

[Kenny Lau]

don't use tactics in definitions

[Kevin Buzzard]

Mathematicians are trained to think about subobjects because in set theory the map from the subobject to the object is completely transparent. This can't happen in lean so why bother with subtypes at all?

[Yakov Pechersky]

The special_linear_group in mathlib is defined using a subtype, so I tried emulating that: https://github.com/leanprover-community/mathlib/blob/0736c95c61521f5040666d5832d808f71c537ab8/src/linear_algebra/special_linear_group.lean#L54

[Kenny Lau]

import data.matrix.basic
import linear_algebra.matrix

open_locale classical

variables (n : Type*) [fintype n] (R : Type*) [ring R]

def invertible_matrix := { A : matrix n n R // ∃! B, A * B = 1 ∧ B * A = 1 }

variables {n R}
lemma inv_mat_unique {A B C: matrix n n R}
                     (hB : A * B = 1) (hC : C * A = 1) : B = C :=
by rw [<-one_mul B, <-hC, mul_assoc, hB, mul_one]

instance coe_matrix : has_coe (invertible_matrix n R) (matrix n n R) :=
by delta invertible_matrix; apply_instance

-- ... proving an existence of an inverse is noncomputable
-- ... because we do not construct it
noncomputable def inv_mat (A : invertible_matrix n R) : matrix n n R :=
classical.some A.property

lemma inv_mat_cancel_self (A : invertible_matrix n R) : inv_mat A * A = 1 :=
(classical.some_spec A.property).1.2

[Kevin Buzzard]

units has an API and is perfect for general linear groups

[Yakov Pechersky]

units looks pretty slick to use. What's the reason why SL_n would be in the library as a subtype?

[Kenny Lau]

because the inverse can be explicitly given I assume

[Kevin Buzzard]

Because it's not the units of something :-)

[Kenny Lau]

https://github.com/leanprover-community/mathlib/blob/b91909e77e219098a2f8cc031f89d595fe274bd2/src/linear_algebra/special_linear_group.lean#L83-L84

instance has_inv : has_inv (special_linear_group n R) :=
⟨λ A, ⟨adjugate A, det_adjugate_eq_one A.2⟩⟩

[Yakov Pechersky]

I see, and because the inverse is given explicitly, we don't need to rely on noncomputable, and the usage of subtype makes sense.

[Yakov Pechersky]

Just as an exercise, I finished the has_inv instance without using tactics in the proof of the instance itself, and did the same for has_mul, has_one. But I'll follow your suggestions and rely on structure-based encoding instead.

import data.real.basic
import data.matrix.basic
import linear_algebra.matrix

variables (n : ℕ) (R : Type*) [field R]

def invertible_matrix := { A : matrix (fin n) (fin n) R // ∃! B, A * B = 1 ∧ B * A = 1 }

variables {n} {R}
lemma inv_mat_unique {A B C: matrix (fin n) (fin n ) R}
                     (hB : A * B = 1) (hC : C * A = 1) : B = C :=
by rw [<-one_mul B, <-hC, mul_assoc, hB, mul_one]

instance coe_matrix : has_coe (invertible_matrix n R) (matrix (fin n) (fin n) R) :=
⟨λ A, A.val⟩

-- ... proving an existence of an inverse is noncomputable
-- ... because we do not construct it
noncomputable def inv_mat (A : invertible_matrix n R) : matrix (fin n) (fin n) R :=
classical.some A.property

@[simp] lemma inv_mat_cancel_self (A : invertible_matrix n R) : inv_mat A * A = 1 :=
(classical.some_spec A.property).1.2

@[simp] lemma mat_cancel_inv_self (A : invertible_matrix n R) : ↑A * inv_mat A = 1 :=
(classical.some_spec A.property).1.1

lemma inv_mat_has_inv (A : invertible_matrix n R) :
  ∃! B, inv_mat A * B = 1 ∧ B * inv_mat A = 1 :=
begin
  use A.val,
  split,
  { split,
    { exact inv_mat_cancel_self _ },
    { exact mat_cancel_inv_self _ } },
  { rintros a' ⟨hleft', hright'⟩,
    refine inv_mat_unique hleft' _,
    exact mat_cancel_inv_self _ }
end

noncomputable instance inv_mat_inv : has_inv (invertible_matrix n R) :=
⟨λ A, ⟨inv_mat A, inv_mat_has_inv _⟩⟩

[Kevin Buzzard]

You can use tactics for proofs -- you should just be clear about whether you're defining a term of type P : Prop or of type T : Type. For example a term of type fin n is a pair consisting of a natural (data, which should be defined without tactics) and a proof (for which tactics are fine)

[Yakov Pechersky]

Got it. Can you clarify what you mean by "ask for a B such at BA = 1"? And how does delta work?

[Yakov Pechersky]

Do you mean that the lemmas (and possibly definitions) should require a Prop term of h : BA = 1?

[Yakov Pechersky]

I really appreciate all the help and insight -- formalizing is difficult for me because of how ingrained some assumptions about conversions between mathematical definitions are for me. Like what was highlighted earlier about mapping from subobject to object.

[Kevin Buzzard]

I just meant: instead of saying that A is invertible if there exists a unique B such that AB=BA=1, you could just ask for a B with AB=BA=1, or even, in your specific situation, for a B with AB=1

[Kevin Buzzard]

They all give the same answer, but my gut feeling is that asking for uniqueness in your definition is just going to make it harder to use it

[Yakov Pechersky]

Asking for uniqueness requires maybe 3 or 4 additional lines in the proofs portions of instance definitions. Having the uniqueness lemma and the cancellation lemmas make that portion of the proof pretty straightforward. The example above was

  { rintros a' ⟨hleft', hright'⟩,
    refine inv_mat_unique hleft' _,
    exact mat_cancel_inv_self _ }

or from the has_mul proof:

  { intros C hC,
    refine inv_mat_unique hC.left _,
    rw [mul_assoc, <-mul_assoc Ainv, hA.2, one_mul, hB.2]}

[Yakov Pechersky]

I'll take your word for it that the uniqueness in the definition can cause issues later on -- I've stripped it out.

[Kevin Buzzard]

I'm not claiming a theorem, I'm just making an observation based on a gut instinct. I guess that actually it doesn't really matter what your definition it, because you can make constructors for the type given any of the other proofs, e.g. you can just construct a function which given B such that BA=1 produces a term of your type. I'm not very good at definitions in Lean -- mathematicians understand specifications well, but this is an implementation issue.

[Alex J. Best]

Kevin Buzzard said:

can just construct a function which given B such that BA=1 produces a term of your type

For general matrices it is a slightly non-trivial theorem that having a left inverse gives you a right inverse for free, a while ago I proved some bits for this, https://github.com/leanprover-community/mathlib/pull/1822/files .
One advantage of the subtype approach is that lean knows how to iterate over a subtype if the original type is finite and the condition is decidable as there is no new data. I think with this branch I got lean to #eval fintype.card (general_linear 3 (zmod 5)) in this way, as lean already knows this set is finite and can just run over all matrices checking if they have a right inverse. Of course this is a bit silly but I found forcing lean to calculate the size of this group by hand oddly fun.

[Reid Barton]

There's no reason this couldn't also be easy for structures with a little derive handler magic.

[Yakov Pechersky]

Since we're on the topic of defintions, and invertible matrices, I have this other way of defining them, using Prop instead of Type. I thoughtunfold was usually not necessary. Why is it necessary here?

import data.matrix.basic
import linear_algebra.matrix

variables (n : ℕ) (R : Type*) [field R]
variables (A B C : matrix (fin n) (fin n) R)

variables {n} {R}
@[reducible] def mat_invertible : Prop := A * B = 1

example (h : mat_invertible A B) : A * B * C = C :=
begin
  rw h, -- rewrite tactic failed, lemma is not an equality nor a iff
  rw one_mul
end

@[simp] lemma mat_inv_left_cancel (h : mat_invertible A B) : A * B * C = C :=
begin
  unfold mat_invertible at h,
  rw [h, one_mul]
end

[Yakov Pechersky]

simp [h] also only works after an unfold.

[Kevin Buzzard]

rw and simp work up to syntactic equality, as opposed to things like exact and apply which work up to definitional equality.

[Kevin Buzzard]

You could add a simp lemma @[simp] lemma mat_invertible_def : mat_invertible A B \iff A * B = 1 := iff.rfl and then maybe simp [h] would work. I'm not a simp expert though

[Yakov Pechersky]

I tried that, but that still doesn't make simp happy. At least using the lemma you provided directly in rw will work:

import data.matrix.basic
import linear_algebra.matrix

variables (n : ℕ) (R : Type*) [field R]
variables (A B C : matrix (fin n) (fin n) R)

variables {n} {R}
@[reducible] def mat_invertible : Prop := A * B = 1

@[simp] lemma mat_invertible_def : mat_invertible A B ↔ A * B = 1 := iff.rfl

@[simp] lemma mat_inv_left_cancel (h : mat_invertible A B) : A * B * C = C :=
begin
  simp [h, one_mul], -- does not prove
  sorry
end

@[simp] lemma mat_inv_left_cancel' (h : mat_invertible A B) : A * B * C = C :=
begin
  rw (mat_invertible_def _ _).mp h,
  simp,
end

[Yakov Pechersky]

I guess I don't understand something about simp, because I thought now this would work, but it doesn't.

import data.matrix.basic
import linear_algebra.matrix

variables (n : ℕ) (R : Type*) [field R]
variables (A B C : matrix (fin n) (fin n) R)

variables {n} {R}
@[reducible] def mat_invertible : Prop := A * B = 1

@[simp] lemma mat_invertible_def : mat_invertible A B ↔ A * B = 1 := iff.rfl

@[simp] lemma mat_inv_left_cancel (h : mat_invertible A B) : A * B * C = C :=
begin
  rw (mat_invertible_def _ _).mp h,
  simp,
end

example (h : mat_invertible A B) : A * B * C = C :=
mat_inv_left_cancel A B C h

example (h : mat_invertible A B) : A * B * C = C :=
by simp [h] -- fails