暴露 coq 中归纳定义项的结构

Question

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

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 进行归纳，但不能对d1 进行归纳，然后破坏d2，反之亦然。 Coq 给出的错误消息（对术语进行抽象会导致输入错误的术语）有点模糊，并且 Coq wiki 没有提供任何帮助。作为参考，这是我试图证明的引理：

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

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

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

针对评论的第一部分，我可以在d1 或d2 上执行induction，但在执行induction 之后 我不能使用destruct，@ 987654339@，或induction 剩余期限。这意味着我不能同时公开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 库中的几个结果，但没有成功。推导是独一无二的，这似乎是一个容易证明的命题。

Answer 1

你有三个问题。

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

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

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

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

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.