A twist on `obtain`

Stream: mathlib4

[Heather Macbeth]

I'm looking for metaprogramming help on a macro which is intended to slightly extend the capabilities of obtain, letting it deal with equalities in products like (x, 3) = (1, 3) as if they were "and"-statements like x = 1 ∧ 3 = 3. Here's what I have currently:

import Mathlib.Data.Prod.Basic

macro_rules
| `(tactic| obtain $pat? $[ :  $ty]? := $val) =>
  `(tactic| rw [Prod.mk.inj_iff] at * ; obtain $pat? $[ :  $ty]? := $val)

It works on a simple example like

example (h : (x, 3) = (1, 3)) : False := by
  obtain ⟨h1, h2⟩ := h

producing the goal state

x : ℕ
h1 : x = 1
h2 : 3 = 3
⊢ False

[Heather Macbeth]

But the rw ... at * is obviously too heavy-handed. Here's an example of why:

example (h : (x, 3) = (1, 3) ∨ y = 2) (h' : (3, 4) = (z, w)): False := by
  obtain h1 | h2 := h

The current version of the macro produces the goal state

x y z w : ℕ
h' : 3 = z ∧ 4 = w
h1 : x = 1 ∧ 3 = 3
⊢ False

x y z w : ℕ
h' : 3 = z ∧ 4 = w
h2 : y = 2
⊢ False

whereas I'd like it to produce the goal state

x y z w : ℕ
h' : (3, 4) = (z, w)
h1 : (x, 3) = (1, 3)
⊢ False

x y z w : ℕ
h' : (3, 4) = (z, w)
h2 : y = 2
⊢ False

[Heather Macbeth]

Could I get some help adjusting my macro? Effectively I want it to perform

replace h := Iff.mp Prod.mk.inj_iff h
obtain ⟨h1, h2⟩ := h

if the $val in the macro is a named hypothesis h, and

have h := Iff.mp Prod.mk.inj_iff $val
obtain ⟨h1, h2⟩ := h

if the $val in the macro is some compound term.

[Kyle Miller]

Right now for simple-enough hypotheses (where the induced equalities are either between variables or between things that are defeq), it "works"

example (h : (x, 3) = (1, 3)) (h' : x = y) : False := by
  obtain ⟨h1, h2⟩ := h
/- y: ℕ
   h': 1 = y
   ⊢ False -/

though that obtain is equivalent to doing obtain ⟨⟩ := h, since these rcases patterns ignore any unused variables. Here we're asking obtain to do cases on h.

[Kyle Miller]

I wonder if it would be possible to extend rcases patterns to have another type of pattern specifically for equalities. Like maybe you could do obtain rfl h1 h2 := h, where rfl takes some number of arguments to name hypotheses for each component in the constructor injectivity lemma.

[Kyle Miller]

For your other example, it might look like

example (h : (x, 3) = (1, 3) ∨ y = 2) (h' : (3, 4) = (z, w)): False := by
  obtain rfl h1 _ | h2 := h
/- Goal 1
   x y z w: ℕ
   h': (3, 4) = (z, w)
   h1: x = 1
   ⊢ False

   Goal 2
   x y z w: ℕ
   h': (3, 4) = (z, w)
   h2: y = 2
   ⊢ False -/

(underscore in that rfl since we don't care about 3 = 3)

[Heather Macbeth]

I'm actually less interested in a principled approach with flexible syntax than in a hack that would work in this precise example, allowing me to pretend that (x, 3) = (1, 3) means x = 1 \and 3 = 3 by definition -- this is for teaching :)

[Kyle Miller]

I get that -- I just don't have any good ideas myself for getting a hack to work that won't have unexpected consequences

[Kyle Miller]

but maybe to answer your immediate question, `(tactic| obtain $pat? $[ : $ty]? := $val:ident) should let you match on the case you were asking about

[Kyle Miller]

@Heather Macbeth I haven't tested it (and I didn't adapt it to your Iff.mp ... formulation), but maybe this will help?

macro_rules
| `(tactic| obtain $pat? $[ :  $ty]? := $val) =>
  if Syntax.isIdent val then
    let h := val.raw.getId
    `(tactic| rw [Prod.mk.inj_iff] at $(mkIdent h):ident ; obtain $pat? $[ :  $ty]? := $val)
  else
    `(tactic| have h := $val; rw [Prod.mk.inj_iff] at h ; obtain $pat? $[ :  $ty]? := h)

[Kyle Miller]

(There's probably a more elegant way to handle checking whether val is an identifier and getting its name, or better, an Ident.)