obtain tactic on exists-unique

Stream: new members

[Yakov Pechersky]

Here's what I mean. What's the difference in the usage of obtain in the first example vs the second one?

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]

noncomputable instance inv_mat_inv : has_inv (invertible_matrix n R) :=
⟨λ A, by { -- obtain ⟨Ainv,  hA⟩ := A.property, -- can't use obtain here for some reason
           -- induction tactic failed, recursor 'Exists.dcases_on' can only eliminate into Prop
           choose Ainv hA using A.property,
           obtain ⟨h, h'⟩ := hA,
           refine ⟨Ainv, _⟩,
           use A.val,
           split,
           { dsimp only [], exact (and.swap h)},
           { intros B hB, exact inv_mat_unique hB.left h.left } }⟩

instance inv_mat_mul : has_mul (invertible_matrix n R) :=
⟨λ A B, ⟨A.val * B.val, by {
   obtain ⟨Ainv, hA⟩ := A.property, -- but I can use it here!
   obtain ⟨Binv, hB⟩ := B.property,
   use Binv * Ainv,
   dsimp only [] at *,
   sorry }⟩

[Jalex Stark]

the error message you put into the comments tells you what's wrong

[Jalex Stark]

you can use an existential to prove things but not to construct data

[Yakov Pechersky]

So because I have to provide Ainv to the instance, I can't use obtain. But since I can construct A.val * B.val without inspecting their respective properties, I can obtain from the properties.

[Yakov Pechersky]

This matches intuition that an inverse would be noncomputable, but showing that an the product of two invertible matrices is still invertible does not rely on the construction of the inverse itself.

[Jalex Stark]

the things you're saying sound good, but i'm far from an expert and can't add anything useful

[Yakov Pechersky]

Before I had just plain \ex in the definition of the subtype, and that required a noncomputable. By setting it to exists-unique, the noncomputable requirement went away.

[Kevin Buzzard]

You shouldn't use tactics to construct data, you'll find the constructions generated by tactics very hard to prove things about in general. You can't get from Prop to Type with cases for constructivism reasons, you have to use classical.some to get there. Why not just ask for B such that AB=1 by the way? Making definitions simpler just makes life easier. You can prove the inverse is unique and two-sided later (you'll need that your matrices are finite in order to do this and it might be already done but it might not be)