Preliminaries
(Remarks on notation: To denote function application, I will use the Haskell notation $f\ x$, rather than the traditional mathematical notation $f (x)$. The expression $x^-$ denotes an involutive operation on $x$. By an intentional abuse of notation, $f^-$ denotes the inverse function of $f$.)
Let's start with the standard definition of a monoid with involution:
$$M=\langle S, \cdot, \bot, ^-\rangle$$ Laws: $$x\cdot(y\cdot z) = (x\cdot y)\cdot z = x\cdot y\cdot z\\ x\cdot\bot = \bot\cdot x = x\\ (x^-)^- = x\\ (x\cdot y)^- = y^-\cdot x^-$$
Let's also have this permutation group (where all functions in $F$ have signature $S\longrightarrow S$): $$G=\langle F, \circ,\ ^-, i\rangle$$ Laws: $$f\circ (g\circ h) = (f\circ g)\circ h = f\circ g\circ h\\ f\circ i = i\circ f = f\\ f\circ f^- = f^-\circ f = i\\ (f^-)^- = f$$
Finally, let's also have a left group action of $G$ on $S$ (the carrier set of $M$),
$$\leftarrow\ :\ ~F\times S\ \mapsto\ S$$ Laws: $$i\leftarrow x = x\\ f\leftarrow(g\leftarrow x) = (f\circ g)\leftarrow x$$
Conjectures
$$(f\ x^-)^- = f^-\ x\\ (f\leftarrow x^-)^- = f^-\leftarrow x\\ ^-\ \circ\ f\ \circ\ ^- = f^-$$
(where all left-hand occurrences of $^-$ refer to the involution operation on $S$, and all right-hand occurrences of $^-$ refer to the inversion operation on $F$.)
Question: How can you prove them?
Motivating scenario where these conjectures work
$S$ = a set of lists of symbols
$\cdot$ = list concatenation (++ in Haskell)
$\bot$ = empty list ([] in Haskell)
$^-$ = operation that inverts a list (reverse in Haskell)
$\circ$ = function composition (. in Haskell)
$\leftarrow$ = function application ($ in Haskell)
$i$ = identity function (id in Haskell)
Beyond the identity function, $F$ includes the two functions rotateRight and rotateLeft, defined as follows in the Haskell programming language (the source code is self-explanatory, but if you prefer to see it in action, copy and paste it to Replit):
--Moves the initial element (if it exists) to the final position of the list
rotateRight [] = []
rotateRight (x:xs) = xs ++ [x]
--Moves the final element (if it exists) to the initial position of the list
rotateLeft = reverse . rotateRight . reverse
--An example input
main = print $ rotateLeft [2,3,5,7]
--Output: [7,2,3,5]
Thus, our group $G$ has a single generating element, rotateRight. And rotateLeft is the inverse of rotateRight.
By looking at the definition of rotateLeft, it is clear that the 3 conjectures succeed in this particular scenario:
reverse (rotateRight (reverse x)) == rotateLeft x
reverse (rotateRight $ reverse x) == (rotateLeft $ x)
reverse . rotateRight . reverse == rotateLeft
If we chose an example list, each of the conjectures can be executed by replacing it for rotateLeft [2,3,5,7] in the previous source code, as follows:
reverse (rotateRight (reverse [2,3,5,7])) == rotateLeft [2,3,5,7]
reverse (rotateRight $ reverse [2,3,5,7]) == (rotateLeft $ [2,3,5,7])
(reverse . rotateRight . reverse) [2,3,5,7] == rotateLeft [2,3,5,7]