Pattern matching on function application

Suppose we have a function f :: a -> b and a function g :: b -> a such that f . g = id. You might say that g is the "inverse" of f (and vice versa). Could we then pattern match on something like f x on the left hand side by replacing occurences of x with g x on the right hand side? For example:

-- Here, (- 3) is the "inverse" of (+ 3), or more generally, (- n) is the "inverse" of (+ n)

subtractThree (x + 3) = x
subtractThree x = (x - 3)


This just randomly came to my mind and I'm wondering if there is something fundamentally wrong with this.

Edit: This is my first post here and I'm unsure whether this is the right kind of question for this community. Please don't hesitate to close this if this doesn't belong here.

If you are given that $g(f(x))=x$ for all $x$ and $f,g$ are pure functions, then your proposed transformation works. However, the condition $f(g(x))=x$ is not sufficient: consider $f,g:\mathbb{N} \to \mathbb{N}$ given by $g(x)=2x$, $f(x)=\lfloor x/2 \rfloor$. (I'm not sure which your g . f notation was intended to capture.)

StackExchange Computer Science Q#125182, answer score: 2