Идрис переписывает тактик не работает, как ожидалось

Question

У меня есть этот пример

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 

И я пытаюсь использовать тактику в таком порядке, чтобы сделать Свидетельство

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

Так четыре шага на самом деле ничего не делает. Также он ничего не делает с sym. Что я делаю неправильно? Возможно ли, что в самом Идрисе есть ошибка?

Answer 1

В файле содержатся только объявления типов. Вам нужно заполнить некоторые определения тела, если вы хотите что-то сделать с этим. Например o : Type, только тип декларации для o, и не будет использоваться до тех пор, пока написать что-то вроде

o : Type 
o = Bool 

Для того, чтобы использовать перезапись, вам нужно предоставить доказательство формы a = b. В частности, вам нужны полные функции, тип возврата которых - это необходимое вам равенство. (Пример типа :doc multCommutative). У вас нет таких доказательств в этом файле. У вас также нет никаких теорем, которые можно было бы доказать, потому что вы еще ничего не определили. Если вы загрузите это в idris, он должен сказать вам, что у вас есть несколько «метапеременных» или «дыр», что означает части кода, которые необходимо заполнить.

Похоже, вы намереваетесь определить тип данных, возможно, что-то вроде

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

Если вы хотите расширить систему типов путем введения новых типов, то вам необходимо использовать data декларацию.