Определения
Я работаю над формализацией типичного лямбда-исчисления в Coq, и чтобы сохранить нотацию управляемой, я стал полагаться на принуждения. Однако я столкнулся с некоторыми трудностями, которые кажутся странными.
Сейчас я пытаюсь работать со следующими типами:
- type: дескриптор допустимого типа на языке (например, функция, Unit, et c ...)
- 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).
Часто я хотел бы сделать такие выражения, как "этот var не появляется в наборе переменных, связанных с 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.
Я составил иерархию конверсий, чтобы прояснить ситуацию * 10 32 *
Проблема
Я бы хотел определить индуктивный тип с помощью следующего конструктора
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) сначала его нужно привести к ty_ctx через cons j nil, затем к VarSet через bound_variables, что должно привести к VarSet содержит только x (что эквивалентно VarSet.singleton x?). Так что эта цепочка принуждения, кажется, go отключается без помех, в то время как другая выходит из строя, хотя она проще