Term representing match

Stream: Is there code for X?

[Paul Rowe]

I'm trying to define a function using match statements. The output of the function requires me to build a term showing the equality of the two things being matched.

The example below doesn't need it, but it's enough to display my problem. I don't know how to extract (f a) = (sum.inl b) from the context. Any suggestions?

variables {α β γ : Type}

def xmpl (f : α → β ⊕ γ) (g : β → α) (h : γ → α) : α → α :=
λ a,
  match (f a) with
  | (sum.inl b) := begin
      have : (f a) = (sum.inl b), sorry,
      exact (g b),
    end
  | (sum.inr c) := h c
  end

[Kyle Miller]

There's now syntax for this in Lean 4, but to get that term in Lean 3 you have to do some tricks. Here's a link to one example

[Kyle Miller]

Another way, which isn't great, is to use tactic mode since the tactic#cases tactic has cases h : f a syntax to get that term.

[Paul Rowe]

Thanks. I'll give those a try. Tactic mode would be fine for me, but my first attempt didn't give me exactly what I wanted. I need to study the other example a little to figure out how to adapt it to my setting.

[Paul Rowe]

Following the pattern of the first link above got me there. I'm happy to hear that Lean 4 will have syntax for this.

[Junyan Xu]

The trick here seems to solve the same problem and I still don't quite get how it work ...

[Kyle Miller]

@Junyan Xu Thanks for finding that, I knew there was a way to avoid the lets but I wasn't sure what to search for.

I don't think this feature is documented in the Lean reference manual. I believe what's going on with match _, rfl : ∀ y, (f.ne_locus g).min = y → _ with is that everything after the colon is specifying the type for the match expression itself before the arguments to be matched on are passed in.

[Kyle Miller]

So the first _ corresponds to y in the forall, and rfl corresponds to (f.ne_locus g).min = y.

[Junyan Xu]

Yeah, apparently the → _ part isn't matched which is confusing. Although I didn't understand it, it didn't prevent me from working with it.

[Paul Rowe]

Huh. That's interesting. That pattern works for me too. It's certainly more streamlined, though otherwise works exactly the same inside the function definition.