Case split tactic by "real" pattern matching

[carlostome]

Given the following (contrived but based on a real world) definition:

f : Bool → Bool → Bool
f true false = true
f x y = true

Id like to write a tactic that solves:

p :  ∀ (x y : Bool) → f x y ≡ true

Iterated case (from Tactic.Case) doesn't cut it:

p x y =  by (case x (case y (quoteTC refl >>= λ t → unifyWithGoal t)))

I suspect it is because case doesn't do real pattern-matching but instead introduces pattern lambdas. This is not enough for Agda to compute.

[WhatisRT]

IIRC case works by basically generating code of the shape case x of λ where .... Note that this is the non-depending case_of_, so it can't specialize the type in the branches of the lambda. So to fix this, it should instead generate case x returning M of λ where ..., where we need to generate the motive M ourselves by abstracting and generalizing x from the goal type.

Note that case wouldn't be able to do the regular LHS pattern matching, because it's in a term position. And (λ where ...) x is also not viable, because this always fails to infer the motive. So I don't think there's a shortcut here.