Zulip Chat Archive

Stream: new members

Topic: obtain tactic on exists-unique


view this post on Zulip Yakov Pechersky (Jun 18 2020 at 01:45):

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 }

view this post on Zulip Jalex Stark (Jun 18 2020 at 01:47):

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

view this post on Zulip Jalex Stark (Jun 18 2020 at 01:47):

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

view this post on Zulip Yakov Pechersky (Jun 18 2020 at 01:49):

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.

view this post on Zulip Yakov Pechersky (Jun 18 2020 at 01:50):

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.

view this post on Zulip Jalex Stark (Jun 18 2020 at 01:51):

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

view this post on Zulip Yakov Pechersky (Jun 18 2020 at 01:51):

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.

view this post on Zulip Kevin Buzzard (Jun 18 2020 at 06:53):

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)


Last updated: May 08 2021 at 09:11 UTC