Idris rewrite tactic doesn't work as expected

Question

I have this example

o : Type

Hom     : o -> o -> Type
Id      : (a : o) -> Hom a a
Comp    : Hom a b -> Hom b c -> Hom a c
IdRight : (f : Hom a b) -> Comp f (Id b) = f
IdLeft  : (f : Hom a b) -> Comp (Id a) f = f
Assoc   : (f : Hom a b) ->
          (g : Hom b c) ->
          (h : Hom c d) ->
          Comp f (Comp g h) = Comp (Comp f g) h

EqId : (f : Hom a b) ->
       (g : Hom b a) ->
       (h : Hom b a) ->
       Comp f g = Id a ->
       Comp h f = Id b ->
       g = h

EqId = ?EqIdProof

And I try to use tactics in this order to make a proof

1. intro a, b, f, g, h, fg, hf
2. rewrite IdLeft g
3. rewrite hf
4. rewrite Assoc h f g

So four step actually does nothing. Also it does nothing with sym. What I'm doing wrong? Is it possible that there is a bug in Idris itself?

Cliff Harvey Cliff Harvey · Accepted Answer · 2015-07-09T09:36:48

Your file contains only type declarations. You need to fill in some body definitions if you want to do anything with this. For example o : Type, is only a type declaration for o, and won't be usable until you write something like

o : Type
o = Bool

In order to use rewrite, you need to supply a proof of the form a = b. More specifically, you need total functions whose return type is the equality you want. (For an example type :doc multCommutative). You don't have any such proofs in this file. You also don't have any theorems that could be proved because you haven't fully defined anything yet. If you load this up in idris, it should tell you that you have a number of "metavariables" or "holes", which means parts of code that need to be filled in.

It looks like you intend to define a data type, perhaps something like

data Hom : Type -> Type -> Type where
   MkHom : (f : a -> b) -> Hom a b
   Comp  : Hom a b -> Hom b c -> Hom a c

If you want to extend the type system by introducing new types then you need to use a data declaration.

Idris rewrite tactic doesn't work as expected

1 Answers