0

给定一个自定义类型来表示从类型 b 到 a 的嵌入：

inductive Embedding (b a:Sort u) : Sort u
| Embed : forall (j:b -> a), (forall (x y:b), j x = j y -> x = y) -> Embedding

我正在尝试定义一个restrict给定关系的函数，r:a -> a -> Prop 并且嵌入e:Embedding b a返回一个关系b

def restrict {a b:Sort u} (r:a -> a -> Prop) (e:Embedding b a) (x y: b) : Prop :=
  begin
   destruct e, -- error 
  end

我无法解构我的嵌入以访问底层注入。

 destruct tactic failed, recursor 'Embedding.cases_on' can only eliminate into Prop

在 Coq 中做同样的事情效果很好：

(* There is an injection j:b -> a, i.e. b is a subset of a                      *)
Inductive Embedding (b a:Type) : Type :=
| Embed : forall (j:b -> a), (forall (x y:b), j x = j y -> x = y) -> Embedding b a
.

Arguments Embed {b} {a}.

(* Restricting relation r on a to subset b                                      *)
Definition restrict (a b:Type) (r:a -> a -> Prop) (e:Embedding b a) (x y:b) 
    : Prop :=
        match e with
        | Embed j _ => r (j x) (j y)
        end.

Arguments restrict {a} {b}.

如果有人能提出一些解决这个问题的建议，我将不胜感激。Prop我熟悉 Coq 的限制，即当目标为 Sort Setor时无法解构 sort 的术语Type i，因此可以理解 Lean 中的类似限制，但这似乎是这里的问题。我试图做Embedding一个归纳谓词（所以返回Prop而不是Sort u），但这并没有解决错误。

我热衷于将我的 Coq 开发转化为学习精益的一种方式，因此我很乐意打破这个障碍 :)

4

1 回答 1

1

问题是Embedding有类型Sort u。Sort 0is Prop，所以 ifa和bare Prop，那么Embedding是 a Prop。当归纳类型是 时Prop，它们的递归通常只能用于证明Props 而不能用于定义Type. 你必须确保它Embedding不能成为Prop

解决方案是使用

inductive Embedding (b a:Sort u) : Sort (max 1 u)

或者

inductive Embedding (b a:Type u) : Type u
于 2020-03-08T12:56:05.080 回答