exposing the structure of inductively defined terms in coq

Question

The proof that typing derivations are unique in the simply-typed lambda calculus is trivial on paper. The proof that I am familiar with proceeds by complete induction on typing derivations. However, I am having trouble proving that typing derivations, represented via the type of typing derivations, are unique. Here, the predicate dec Γ x τ is true if the variable x has type τ in environment Γ. The typing predicate J is defined as usual, simply reading off the typing rules for the simply-typed lambda calculus:

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₂) τ₂.

I am having trouble exposing the structure of a term of type J when proving that typing derivations are unique. For instance, I can induct on either d1 or d2 in the following lemma, but cannot induction on d1 then destruct d2 and conversely. The error message given by Coq (abstracting over terms leads to a term which is ill-typed) is slightly obscure, and the Coq wiki doesn't provide any help. For reference, this is the lemma that I am trying to prove:

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

I have no problems when inducting on terms, for instance, when proving that the types are unique.

EDIT: I added the the minimal number of definitions necessary to state the result that I am having trouble with. In response to huitseeker's comment, the sort of J was chosen because I wanted to reason about typing derivations as structured objects in order to perform operations like extraction and prove results like uniqueness, which I haven't done in Coq before.

In response to the first part of the comment, I can perform induction on either d1 or d2, but after performing induction I cannot use destruct, case, or induction on the remaining term. This means that I cannot expose the structure of both d1 and d2 in order to reason about both proof trees. The error that I receive when I attempt to do so, says that abstracting over the remaining terms leads to a term which is ill-typed.

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.

I've tried experimenting with dependent induction and several results from the Coq.Logic library, but without success. That derivations are unique seems like it should be an easy proposition to prove.

Answer 1

You have three problems.

One is the purely technical problem of making the induction work. You can solve the main difficulty with the dependent destruction tactic (courtesy of Matthieu Sozeau on the Coq-Club mailing list). This is an inversion tactic. I don't pretend to understand how it works under the hood.

A second difficulty is in one of the base cases, for environments. You need to prove that equality proofs in list nat are unique; this holds on all decidable domains, and the tools for that are in the Eqdep_dec module.

A third difficulty is problem-related. The unicity of derivations does not follow by a direct induction over the term or derivation structure, because your terms do not carry enough type information to reconstruct the derivation. In an application app e1 e2, there is no direct way to know the type of the argument. In the simply-typed lambda calculus, type reconstruction does hold, and is easy to prove; in larger calculi (with polymorphism or subtyping) it might not hold (for example, with ML-style polymorphism, there is a unique principal type scheme and associated derivation, but there are many derivations using base types).

Here's a quickie proof of your lemma. I omitted the proof of the unicity of environment lookups. You can induct on the term structure or on the derivation structure — this simple proof works because they're the same.

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.