I had trouble writing a proof in Agda. So I simplified it, a lot.
ffff : bool -> bool
ffff x with x , x
ffff x | t , t = t
ffff x | f , f = t
ffff x | t , ()
ffff x | f , ()
with the compile error:
bool × bool should be empty, but the following constructor patterns
are valid:
_,_ _ _
I know this is a kind of asinine case. But it cuts to the core of what I frequently want to do in agda. How can I restructure this proof so that the last 2 cases are absurd?
The reason that your code doesn't work is that when you use the absurd pattern (), then it should hold that there are no valid instantiations of the pattern that have the correct type. In this case, that is not the case: the type is the absurd pattern is just bool and there are obvious valid instantiations f and t. The problem is that you know there to be no valid cases of the pattern for reasons other than the type of the pattern, while Agda only looks at the type of the pattern.
Therefore, what you should try to do is to change the code so that it follows from the type of some pattern that there are no valid cases for this. One pattern that can often be useful in this case is the "inspect on steroids" pattern. Essentially, you want to remember that what you pattern match on in the with block is the value (x , x). You can do this using the "inspect on steroids" pattern as follows, although that may not be precisely what you need in your actual non-simplified code:
open import Data.Bool
open import Relation.Binary.PropositionalEquality
open import Data.Product
ffff : Bool -> Bool
ffff x with (x , x) | inspect (λ x → (x , x)) x
ffff x | true , true | _ = true
ffff x | false , false | _ = true
ffff x | true , false | [ () ]
ffff x | false , true | [ () ]
Anyway, I suggest you google for a good explanation of the "inspect on steroids" pattern (or the older "inspect" pattern), study it, perhaps study the example above and try to apply it to your actual code...
