如何判断从属匹配两个nat相等

Question

我正在设计一种使用参数高阶抽象语法PHOAS的语言。在其中，我使用的是bbv library中的位向量，看起来像word : nat -> Set。

现在，以经典的PHOAS语法，我为变量创建一个内部类型，并提供该类型的符号：

Require Import bbv.Word.
Inductive type : Set :=
  | UI : nat -> type.

Definition type_denote (t : type) : Set :=
  match t with
  | UI n => word n
  end.

最终，我希望在此PHOAS之上具有一种简单的基于堆栈的语言状态概念，所以我也有“值”：

Inductive value :=
| UI_value n : word n -> value.
Definition state := (nat * (nat -> option value))%type.

转换来自值是我遇到的问题。这是我想发生的事情：

Fail Definition fromValue_pseudo := (t : type) (v : value)
  : option (type_denote t) :=
  match (t,v) as x return option (type_denote (fst x)) with
  | (UI m1, UI_value m2 n) (* and m1 = m2  *) => Some n
  | (UI m1, UI_value m2 n) (* and m1 <> m2 *) => None
  end.

如何分辨m1 = m2，然后Some n具有[[both类型word m1和word m2呢？

Answer 1

Nat.dec_eq m2 m1上的模式匹配以对m1和m2是否相等进行案例分析，并且在它们相等的情况下，将等价证明上的模式匹配“传输” n : word m2到[ C0]（下面是通过word m1完成的操作。）>

eq_rec