taking a setoid apart

Stream: new members

[Kevin Buzzard]

I must be making a really basic error here. How do I extract rel from setoid?

import Mathlib.Tactic

def rel (a b : ℕ) : Prop := True
def setoid : Setoid ℕ := Setoid.mk rel sorry

example : True := by
  obtain ⟨r, hr⟩ := setoid
  have foo : r = rel := rfl -- fails
  -- foo looks unprovable to me.

[Markus Himmel]

You can use match to take something apart with proof:

example : True := by
  match h : setoid with
  | ⟨r, hr⟩ =>
    have foo : r = rel := (congrArg (@Setoid.r _) h).symm
    sorry

[Kevin Buzzard]

This worked in my use case but I have no idea why what I was trying doesn't work whereas what you suggest does!

[Adam Topaz]

Minimized:

structure A where
  a : Nat

def t : A := ⟨1⟩

example : True := by
  obtain ⟨a⟩ := t
  have : a = 1 := rfl
  sorry

If you take it apart with let r := setoid.r etc., then it does work BTW.

[Adam Topaz]

I guess the point is that obtain and/or rcases don't actually retain the value, but just the type.

[Adam Topaz]

Actually the same is true with match (otherwise you wouldn't need the h).