Databases
StackOverflow2013
Postsdbo
PO
 

Note that there are some explanatory texts on larger screens.

plurals
  1. PO
    primarykey
    data
    text
    <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 -&gt; dec G x t2 -&gt; 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>
    singulars
    1. This table or related slice is empty.
    1. POexposing the structure of inductively defined terms in coq
      singulars
      1. PTQuestion
    1. PTAnswer
    1. This table or related slice is empty.
    1. USGilles
    plurals
    1. This table or related slice is empty.
    1. This table or related slice is empty.
    1. POexposing the structure of inductively defined terms in coq
      singulars
      1. PTQuestion
    1. This table or related slice is empty.
    1. VO
      singulars
      1. PO
      1. This table or related slice is empty.
      1. VTUpMod
    2. VO
      singulars
      1. PO
      1. This table or related slice is empty.
      1. VTAcceptedByOriginator
    1. COThank you. It looks like I have some reading about dependent equality to do. Regarding your third comment: I know that typing is unique modulo a principle type scheme for lambda calculi with parametric polymorphism, and so forth. When you say that the proof only works because there is an isomorphism between type and term structure in the simply-typed lambda calculus, do you mean that the structure of the proof would be necessarily different for a calculus with a more expressive type system, even if you were working with a user-defined equivalence instead of Leibniz identity?
      singulars
      1. PO
      1. USdanportin
    2. CO@danportin The proof here works because there's an isomorphism between term and derivation (not type) structure. In general, I would expect to go through an intermediate type reconstruction lemma, which transforms terms into terms with additional type annotations (including the function and argument types on applications). Here the unique typing lemma is enough to progress, but I expect this to quickly become more complicated for “interesting” calculi. I don't have much experience with derivation uniqueness, so take this with a grain of salt.
      singulars
      1. PO
      1. USGilles
    3. COSorry, I means an isomorphism between term structure and typing derivation. Thanks for the information. I wasn't sure if you meant that the structure of the Coq proof worked because of the peculiarity of the simply-typed lambda calculus, and wouldn't work for other lambda calculi. Thank you for clarifying.
      singulars
      1. PO
      1. USdanportin
 

Querying!

 
Guidance
A row detail

Detail views are divided into sections. All the information in the data section comes from columns in the selected row. The other sections display data from other, related rows.

Related data can be related in a to-one or a to-many fashion. Captions of data related in a to-many fashion link to a list view showing a filtered view of the table.

Try moving around until you find a non-empty to-many entry and click on the label to get to one. You can move back to the root by clicking on the database name in the header.

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