1

我有这个例子

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. 我做错了什么？伊德里斯本身是否可能存在错误？

4

1 回答 1

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声明。

于 2015-07-09T09:36:48.710 回答