I am trying to show that the following interference is unsound in terms of Separation Logic:
$$ (p_0 \implies p_1) \implies ((p_0 * q) \implies (p_1 * q)) $$
I came up with the following values for a counter example: $p_0 = true$, $p_1 = x \mapsto 1$, $q = true$. The heap contains just one mapping of $x \mapsto 1$.
The idea is that $(p_1 * q)$ cannot be true because $p_1$ already describes the whole heap and there is nothing left for $q$.
I am not sure, however, why $true * true$ would hold if there is only one element in the heap. Shouldn’t it be false as those two $true$s cannot claim that single heap element at the same time?
