2

在简单类型的 lambda 演算中类型推导是唯一的证明在纸上是微不足道的。我熟悉的证明是通过对类型推导的完全归纳来进行的。但是，我无法证明通过类型派生类型表示的类型派生是唯一的。在这里，如果变量的类型为 environment ，则谓词dec Γ x τ为真。类型谓词像往常一样定义，只需读取简单类型 lambda 演算的类型规则：xτΓJ

Inductive J (Γ : env) : term → type → Set :=
  | tvar : ∀ x τ, dec Γ x τ → J γ (var x) τ
  | tabs : ∀ τ₁ τ₂ e, J (τ₁ :: γ) e τ₂ → J γ (abs τ₁ e) (arr τ₁ τ₂)
  | tapp : ∀ τ₁ τ₂ e₁ e₂, J γ e₁ (arr τ₁ τ₂) → J γ e₂ τ₁ → J γ (app e₁ e₂) τ₂.

J在证明类型派生是唯一的时，我无法暴露类型术语的结构。例如，我可以对以下引理中的任何一个d1或d2在其中进行归纳，但不能对d1then destruct进行归纳d2，反之亦然。Coq 给出的错误消息（对术语进行抽象会导致输入错误的术语）有点模糊，并且 Coq wiki 没有提供任何帮助。作为参考，这是我试图证明的引理：

Lemma unique_derivation : ∀ Γ e τ (d₁ d₂ : J Γ e τ), d₁ = d₂.

在归纳术语时我没有问题，例如，在证明类型是唯一的时。

编辑：我添加了最少数量的定义来说明我遇到问题的结果。作为对 huitseeker 评论的回应，之所以选择这种类型J是因为我想将派生类型作为结构化对象进行推理，以便执行提取等操作并证明唯一性等结果，这是我以前在 Coq 中没有做过的。

针对评论的第一部分，我可以执行inductionor d1，d2但执行后induction我不能使用destruct, case, orinduction剩下的术语。这意味着我不能公开两者的结构，d1并且无法d2对这两个证明树进行推理。当我尝试这样做时收到的错误表明，对剩余术语进行抽象会导致术语输入错误。

Require Import Unicode.Utf8.
Require Import Utf8_core.
Require Import List.

Inductive type : Set :=
  | tau : type
  | arr : type → type → type.

Inductive term : Set :=
  | var : nat → term
  | abs : type → term → term
  | app : term → term → term.

Definition dec (Γ : list type) x τ : Prop :=
  nth_error γ x = Some τ.

Inductive J (Γ : list type) : term → type → Set :=
  | tvar : ∀ x τ, dec Γ x τ → J Γ (var x) τ
  | tabs : ∀ τ₁ τ₂ e, J (τ₁ :: Γ) e τ₂ → J Γ (abs τ₁ e) (arr τ₁ τ₂)
  | tapp : ∀ τ₁ τ₂ e₁ e₂, J Γ e₁ (arr τ₁ τ₂) → J Γ e₂ τ₁ → J Γ (app e₁ e₂) τ₂.

Lemma derivations_unique : ∀ Γ e τ (d1 d2 : J Γ e τ), d1 = d2.
Proof. admit. Qed.

我已经尝试过从库中获得dependent induction一些结果Coq.Logic，但没有成功。推导是独一无二的，这似乎是一个容易证明的命题。

4

1 回答 1

1

你有三个问题。

一个是使感应工作的纯技术问题。dependent destruction您可以使用该策略解决主要困难（由Coq-Club 邮件列表上的 Matthieu Sozeau 提供）。这是一种反转策略。我不会假装理解它是如何在幕后工作的。

第二个困难是在一个基本案例中，对于环境。你需要证明等式证明list nat是唯一的；这适用于所有可判定的域，其工具在Eqdep_dec模块中。

第三个困难与问题有关。推导的唯一性不会跟随术语或推导结构的直接归纳，因为您的术语没有携带足够的类型信息来重构推导。在应用程序app e1 e2中，没有直接的方法可以知道参数的类型。在简单类型的 lambda 演算中，类型重构确实成立，并且很容易证明；在较大的演算（具有多态性或子类型）中，它可能不成立（例如，对于 ML 风格的多态性，有一个独特的主类型方案和相关的派生，但有许多使用基本类型的派生）。

这是您的引理的快速证明。我省略了环境查找唯一性的证明。您可以对术语结构或推导结构进行归纳——这个简单的证明有效，因为它们是相同的。

Require Import Unicode.Utf8.
Require Import Utf8_core.
Require Import List.
Require Import Program.Equality.

Inductive type : Set :=
  | tau : type
  | arr : type → type → type.

Inductive term : Set :=
  | var : nat → term
  | abs : type → term → term
  | app : term → term → term.

Definition dec (Γ : list type) x τ : Prop :=
  nth_error Γ x = Some τ.

Inductive J (Γ : list type) : term → type → Set :=
  | tvar : ∀ x τ, dec Γ x τ → J Γ (var x) τ
  | tabs : ∀ τ₁ τ₂ e, J (τ₁ :: Γ) e τ₂ → J Γ (abs τ₁ e) (arr τ₁ τ₂)
  | tapp : ∀ τ₁ τ₂ e₁ e₂, J Γ e₁ (arr τ₁ τ₂) → J Γ e₂ τ₁ → J Γ (app e₁ e₂) τ₂.

Lemma unique_variable_type :
  forall G x t1 t2, dec G x t1 -> dec G x t2 -> t1 = t2.
Proof.
  unfold dec; intros.
  assert (value t1 = value t2). congruence.
  inversion H1. reflexivity.
Qed.

Axiom unique_variable_type_derivation :
  forall G x t (d1 d2 : dec G x t), d1 = d2.

Lemma unique_type : forall G e t1 t2 (d1 : J G e t1) (d2 : J G e t2), t1 = t2.
Proof.
  intros G e; generalize dependent G.
  induction e; intros.

  dependent destruction d1. dependent destruction d2.
  apply (unique_variable_type G n); assumption.

  dependent destruction d1. dependent destruction d2.
  firstorder congruence.

  dependent destruction d1. dependent destruction d2.
  assert (arr τ₁ τ₂ = arr τ₁0 τ₂0).
  firstorder congruence.
  congruence.
Qed.

Lemma unique_derivation : forall G e t (d1 d2 : J G e t), d1 = d2.
Proof.
  intros G e; generalize dependent G.
  induction e; intros.

  dependent destruction d1. dependent destruction d2.
  f_equal. solve [apply (unique_variable_type_derivation G n)].

  dependent destruction d1. dependent destruction d2.
  f_equal. solve [apply IHe].

  dependent destruction d1. dependent destruction d2.
  assert (τ₁ = τ₁0). 2: subst τ₁.
  solve [eapply unique_type; eauto].
  f_equal; solve [firstorder].
Qed.
于 2012-09-05T18:34:17.077 回答