destruct 战术失败，只能消除成 Prop

Question

给定一个自定义类型来表示从类型 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 returns 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}.

如果有人能提出解决该问题的建议，我将不胜感激。我熟悉 Coq 的限制，即在目标为排序 Set 或 Type i 时无法解构排序项 Prop，因此会理解精益中的类似限制，但是这似乎确实是这里的问题。我试图使 Embedding 成为归纳谓词（因此返回 Prop 而不是 Sort u），但这并没有解决错误。

我热衷于将我的 Coq 开发转化为学习精益的一种方式，所以很高兴能打破这个障碍 :)

Answer 1

问题是 Embedding 的类型是 Sort u。 Sort 0 是 Prop，所以如果 a 和 b 是 Prop，那么 Embedding 就是 Prop。当归纳类型为Prop时，其递归通常只能用于证明Prop，而不能在Type中定义任何东西。您必须确保 Embedding 不能是 Prop

解决方法是使用

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

或者

inductive Embedding (b a:Type u) : Type u

destruct 战术失败，只能消除成 Prop

destruct tactic failed, can only eliminate into Prop

lean