Using rewrite for my own equality?

Question

I have the following definition of equality:

data Equal : x -> y -> Type where
    Reflexive : Equal a a

Whenever I want to use the rewrite syntax, I need something of type (a = b), so i created:

makeEquitable : Equal x y -> x = y
makeEquitable Reflexive = Refl

Now I can do makeEquitable (_ : Equal a b) which I can then use to rewrite things. I would like to simplify this and I looked into replace which I don't really understand replace : (x = y) -> P x -> P y. This P thing is a built-in Idris property I assume - how would I make such function for my own definition Equality - would it also be possible to "bake-in" something special so that rewrite would magically work for Equal a b?

Answer 1

If you set :set showimplicits in the repl, you see the implicit arguments for :t replace:

replace : {a : Type} -> {x : a} -> {y : a} -> {P : a -> Type} ->
          ((=) {A = a} {B = a} x y) -> P x -> P y

There is nothing special about P, it is just an implicit argument: a predicate P that holds over values of type a. Most types of these implicit arguments can be inferred, so your function could look like:

replaceEqual : {P : a -> Type} -> Equal x y -> P x -> P y
replaceEqual Reflexive prf = prf

But you cannot easily make your own rewrite as far as I know. However, you can use a syntax rule to prettify your approach:

syntax eqrewrite [a] "in" [b] = rewrite makeEquitable a in b;

plus_commutes_Z' : Equal m (plus m 0)
plus_commutes_Z' {m = Z} = Reflexive
plus_commutes_Z' {m = (S k)} =
  let rec = plus_commutes_Z' {m=k}
  in eqrewrite rec in Reflexive