StackOverflow2013

Note that there are some explanatory texts on larger screens.

plurals

PO
text
Body
copied!<p>You have three problems.</p> <p>One is the purely technical problem of making the induction work. You can solve the main difficulty with the <a href="http://coq.inria.fr/distrib/V8.4/refman/Reference-Manual011.html#DepInduction" rel="nofollow"><code>dependent destruction</code></a> tactic (courtesy of <a href="https://sympa.inria.fr/sympa/arc/coq-club/2008-08/msg00000.html" rel="nofollow">Matthieu Sozeau on the Coq-Club mailing list</a>). This is an inversion tactic. I don't pretend to understand how it works under the hood.</p> <p>A second difficulty is in one of the base cases, for environments. You need to prove that equality proofs in <code>list nat</code> are unique; this holds on all decidable domains, and the tools for that are in the <a href="http://coq.inria.fr/library/Coq.Logic.Eqdep_dec.html" rel="nofollow">Eqdep_dec</a> module.</p> <p>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 <code>app e1 e2</code>, 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 <em>principal</em> type scheme and associated derivation, but there are many derivations using base types).</p> <p>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.</p> <pre><code>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. </code></pre>

Querying!

Guidance

An individual column

Larger individual text columns get their own page to allow for proper reading.

SQuiL has stopped working due to an internal error.

If you are curious you may find further information in the browser console, which is accessible through the devtools (F12).

Reload