Equation for match-case

Stream: new members

[Erika]

Is there way to fill this hole (similar to coq's match-return)

match f x with
| case1 y := g x y (_: f x = case1 y)
| ...
end

[Mario Carneiro]

It's not built in to the match syntax, but there is a tactic for this, cases

[Mario Carneiro]

cases h : f x with y,
{ -- case1 y
  exact g x y h, }

[Erika]

ooh, that's good to know, I also noticed that refine will not make goals for _ within a match arm

[Mario Carneiro]

Lean does have match-return as well, but you have to handhold it a bit to get this goal

match f x, rfl : ∀ a, f x = a → P with
| case1 y, h := g x y (h: f x = case1 y)
| ...
end

[Erika]

ah, I see, this is acceptable too

[Mario Carneiro]

I'm not sure I know what you mean by not making goals for _

[Mario Carneiro]

refine will make goals for anything it can't infer

[Mario Carneiro]

oh, maybe you mean match blocks refine because it uses the equation compiler (so it is typechecking in a different context, for a standalone definition)

[Erika]

def test (b: bool) : bool :=
begin
  refine (match b with | tt := tt | ff := _ end), -- error for _, instead of new goal
end

[Mario Carneiro]

right

[Mario Carneiro]

same happens when you use let <...> = e1 in e2

[Erika]

thanks for the help

[Mario Carneiro]

you can still use tactics in there, but you have to make a separate begin-end block

[Mario Carneiro]

def test (b: bool) : bool :=
begin
  exact (match b with | tt := tt | ff := begin
    ...
  end end),
end