Coq 在使用强制类型定义构造函数时遇到困难

Question

定义

我正致力于在 Coq 中形式化类型化的 lambda 演算，并且为了使符号易于管理，我开始非常依赖强制转换。但是，我运行遇到了一些看起来很奇怪的困难。

现在我正在尝试使用以下类型：

类型：语言中允许类型的描述符（如函数、单元等...）
var：变量类型，定义为nat
VarSets：一组变量
判断：一对var/my_type对
ty_ctx:判断列表。
ctx_join：ty_ctx 对描述不相交的变量集

实际定义都在下面给出，除了ctx_join在下一个块中给出

(* Imports *)
Require Import lang_spec.
From Coq Require Import MSets.
Require Import List.
Import ListNotations.

Module VarSet := Make(Nat_as_OT).

Inductive Judgement : Type :=
| judge (v : var) (t : type)
.

Definition ty_ctx := (list Judgement).

Definition disj_vars (s1 s2 : VarSet.t) := VarSet.Empty (VarSet.inter s1 s2).

我经常想做类似 "this var does not appear in the set of vars bound by ty_ctx" 的陈述，为此我在下面的这些类型之间设置了一堆强制转换。


(* Functions to convert between the different types listed above *)

Fixpoint var_to_varset (v : var) : VarSet.t :=
  VarSet.singleton v.
Coercion var_to_varset : var >-> VarSet.t.

Fixpoint bound_variables (g : ty_ctx) : VarSet.t :=
  match g with
  | nil => VarSet.empty
  | cons (judge v _) g' =>VarSet.union (VarSet.singleton v) (bound_variables g')
  end.
Coercion bound_variables : ty_ctx >-> VarSet.t.

Inductive ctx_join :=
| join_single (g : ty_ctx)
| join_double (g1 g2 : ty_ctx)
              (disjoint_proof : disj_vars g1 g2)
.

Fixpoint coerce_ctx_join (dj : ctx_join) : ty_ctx :=
  match dj with
  | join_single g => g
  | join_double g1 g2 _ => g1 ++ g2
  end.
Coercion coerce_ctx_join : ctx_join >-> ty_ctx.

Fixpoint coerce_judgement_to_ty_ctx (j : Judgement) : ty_ctx :=
  cons j nil.
Coercion coerce_judgement_to_ty_ctx : Judgement >-> ty_ctx.

您会注意到 ctx_join 的定义依赖于将其参数从 ty_ctx 强制转换为 VarSet。

我制定了转换层次结构只是为了让事情更清楚

问题

我想用下面的构造函数定义一个归纳类型

Inductive expr_has_type : ty_ctx -> nat -> type -> Prop :=
(* General Expressions *)
| ty_var (g : ty_ctx) (x : var) (t : type) (xfree : disj_vars x g)
  : expr_has_type (join_double (judge x t) g xfree) x t
.

问题是当我这样做时，出现以下错误：

Error:
In environment
expr_has_type : ty_ctx -> nat -> type -> Prop
g : ty_ctx
x : var
t : type
xfree : disj_vars x g
The term "xfree" has type "disj_vars x g" while it is expected to have type
 "disj_vars (judge x t) g" (cannot unify "VarSet.In a (VarSet.inter (judge x t) g)" and
"VarSet.In a (VarSet.inter x g)").

但是，如果我将 xfree 的类型更改为 disj_vars (VarSet.singleton x) g，那么定义就可以正常工作了！这看起来很奇怪，因为 disj_vars 仅在 VarSet 上定义，因此似乎 x 应该自动转换为 VarSet.singleton x 因为这就是强制转换的设置方式.

更奇怪的是，如果我不设置从 vars 到 varsets 的强制转换，那么 Coq 会正确地抱怨将 dis_vars 应用于 var 而不是 VarSet.所以强制肯定是在做某事

有人可以向我解释为什么第一个定义失败吗？考虑到我设置的强制转换，对我来说，上面的所有定义应该是等价的

备注

将 xfree 的类型更改为 disj_vars (judge x t) g 也修复了错误。这看起来也很奇怪，因为为了能够将 disj_vars 应用到 j := (judge x t)，它首先需要通过 cons j nil 强制到 ty_ctx，然后到 VarSet 通过 bound_variables，它应该产生一个只包含 x 的 VarSet（相当于 VarSet.singleton x？）。所以这个强制链似乎很顺利，而另一个虽然更简单但失败了

Answer 1

如果您使用 Set Printing Coercions.，错误消息将提供更多有关问题的信息：

The term "xfree" has type "disj_vars (var_to_varset x) (bound_variables g)"
while it is expected to have type
 "disj_vars (bound_variables (coerce_judgement_to_ty_ctx (judge x t)))
    (bound_variables g)"

问题是 x 到 VarSet.t 的强制转换等于 Var.singleton x，而 judge 中的强制转换减少到 VarSet.union (VarSet.singleton x) VarSet.empty。虽然这两者在命题上是相等的，但在判断上它们并不相等，所以就 Coq 而言，它提出的术语是错误类型的。

Coq 在使用强制类型定义构造函数时遇到困难

Coq difficulties in defining constructors using coerced types

formal-verification

coercion

coq

定义

问题