単純型付きラムダ計算で型付きラムダ計算が一意であるという証明は、紙の上では簡単です。私が精通しているという証拠は、タイピングの派生に関する完全な帰納法によって進められます。ただし、タイピング派生のタイプで表されるタイピング派生が一意であることを証明するのに苦労しています。dec Γ x τここで、変数のxタイプτがenvironmentの場合、述語はtrueですΓ。型付き述語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かで誘導することはできますが、その後破壊して逆に誘導することはできません。Coqによって表示されるエラーメッセージ（用語を抽象化すると、タイプが正しくない用語になります）は少しわかりにくく、Coqwikiは何の助けにもなりません。参考までに、これは私が証明しようとしている見出語です。d2d1d2
Lemma unique_derivation : ∀ Γ e τ (d₁ d₂ : J Γ e τ), d₁ = d₂.
タイプがユニークであることを証明するときなど、用語を導入するときに問題はありません。
編集：問題が発生した結果を示すために必要な最小限の定義を追加しました。huitseekerのコメントに応えて、J抽出などの操作を実行し、Coqでこれまで行ったことのない一意性などの結果を証明するために、派生を構造化オブジェクトとして入力することについて推論したかったので、この種が選択されました。
コメントの最初の部分に応じて、またはのinductionいずれd1かd2で実行できますが、実行後は、、、または残りの用語をinduction使用できません。これは、両方の構造を公開することはできず、両方のプルーフツリーについて推論することはできないことを意味します。私がそうしようとしたときに私が受け取るエラーは、残りの用語を抽象化すると、タイプが正しくない用語につながることを示しています。destructcaseinductiond1d2
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派生がユニークであるということは、証明するのが簡単な命題であるように思われます。