How to define a property of a function that is its own inverse in Idris?
I want to say that for a function f with signature t-> t for all x in tf (f (x)) = x.
When I ran this:
%default total
-- The type of parity values - either Even or Odd
data Parity = Even | Odd
-- Even is the opposite of Odd and Odd is the opposite of Even
opposite: Parity -> Parity
opposite Even = Odd
opposite Odd = Even
-- The 'opposite' function is it own inverse
opposite_its_own_inverse : (p : Parity) -> opposite (opposite p) = p
opposite_its_own_inverse Even = Refl
opposite_its_own_inverse Odd = Refl
-- abstraction of being one own inverse
IsItsOwnInverse : {t : Type} -> (f: t->t) -> Type
IsItsOwnInverse {t} f = (x: t) -> f (f x) = x
opposite_IsItsOwnInverse : IsItsOwnInverse {t=Parity} opposite
opposite_IsItsOwnInverse = opposite_its_own_inverse
I am getting this error message:
- + Errors (1)
`-- own_inverse_example.idr line 22 col 25:
When checking right hand side of opposite_IsItsOwnInverse with expected type
IsItsOwnInverse opposite
Type mismatch between
(p : Parity) ->
opposite (opposite p) = p (Type of opposite_its_own_inverse)
and
(x : Parity) -> opposite (opposite x) = x (Expected type)
Specifically:
Type mismatch between
opposite (opposite v0)
and
opposite (opposite v0)
Am I doing something wrong, or is this just a bug?
If I replace the last "counter_its_own_inverse" with "?" I get:
Holes
This buffer displays the unsolved holes from the currently-loaded code. Press
the [P] buttons to solve the holes interactively in the prover.
- + Main.hole [P]
`-- opposite : Parity -> Parity
-------------------------------------------------------
Main.hole : (x : Parity) -> opposite (opposite x) = x
source to share
The name of this property is involution . Your type for this property is pretty good, but I like to write it like this:
Involution : (t -> t) -> t -> Type
Involution f x = f (f x) = x
The first problem with yours opposite_IsItsOwnInverse
is that you haven't fully applied Involution
so that you don't get the type yet. You also need to apply Parity
to Involution
give Type
, for example:
opposite_IsItsOwnInverse : Involution opposite p
What p
is an implicit argument. Implicit arguments are implicitly created by string identifiers in type signatures. This is similar to writing:
opposite_IsItsOwnInverse : {p : Parity} -> Involution opposite p
But this leads to another problem with the signature - opposite
it is also lowercase, so it is treated as an implicit argument! (This is why you are getting a confusing error message, Idris created another variable called opposite
). Here you have two possible solutions: qualify the identifier, or use an identifier that starts with an uppercase letter.
I am assuming that the module you are writing uses the default name Main
. The final type signature looks like this:
opposite_IsItsOwnInverse : Involution Main.opposite p
And the implementation will use the implicit argument and provide it to the function you already wrote:
opposite_IsItsOwnInverse {p} = opposite_its_own_inverse p
source to share