Databases
StackOverflow2013
Postsdbo
POexposing the structure of inductively defined terms in coq
 

Note that there are some explanatory texts on larger screens.

plurals
  1. POexposing the structure of inductively defined terms in coq
    primarykey
    data
    text
    <p>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 <em>via</em> the type of typing derivations, are unique. Here, the predicate <code>dec Γ x τ</code> is true if the variable <code>x</code> has type <code>τ</code> in environment <code>Γ</code>. The typing predicate <code>J</code> is defined as usual, simply reading off the typing rules for the simply-typed lambda calculus:</p> <pre><code>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₂) τ₂. </code></pre> <p>I am having trouble exposing the structure of a term of type <code>J</code> when proving that typing derivations are unique. For instance, I can induct on either <code>d1</code> or <code>d2</code> in the following lemma, but cannot induction on <code>d1</code> then destruct <code>d2</code> 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:</p> <pre><code>Lemma unique_derivation : ∀ Γ e τ (d₁ d₂ : J Γ e τ), d₁ = d₂. </code></pre> <p>I have no problems when inducting on terms, for instance, when proving that the types are unique.</p> <p><strong>EDIT:</strong> 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 <code>J</code> 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.</p> <p>In response to the first part of the comment, I can perform <code>induction</code> on either <code>d1</code> or <code>d2</code>, but <em>after</em> performing <code>induction</code> I cannot use <code>destruct</code>, <code>case</code>, or <code>induction</code> on the remaining term. This means that I cannot expose the structure of both <code>d1</code> and <code>d2</code> 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.</p> <pre><code>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. </code></pre> <p>I've tried experimenting with <code>dependent induction</code> and several results from the <code>Coq.Logic</code> library, but without success. That derivations are unique seems like it should be an easy proposition to prove.</p>
    singulars
    1. PO
      singulars
      1. PTAnswer
    1. This table or related slice is empty.
    1. PTQuestion
    1. USdanportin
    1. USdanportin
    plurals
    1. This table or related slice is empty.
    1. This table or related slice is empty.
    1. This table or related slice is empty.
    1. PO
      singulars
      1. PTAnswer
    1. VO
      singulars
      1. POexposing the structure of inductively defined terms in coq
      1. USrks
      1. VTFavorite
    2. VO
      singulars
      1. POexposing the structure of inductively defined terms in coq
      1. This table or related slice is empty.
      1. VTUpMod
    1. COPlease be a bit more precise what you have tried ('a term which is ill-typed' can have several meanings for your particular problem - is it Coq or you that does the typing?-, you use *destruct* as a verb, but that can mean `case`, `destruct` or something else). Finally, are you sure about the sort of `J` ? Are you familiar with the notion of predicativity ?
      singulars
      1. POexposing the structure of inductively defined terms in coq
      1. UShuitseeker
    2. COI'm familiar with the notion of predicativity and that `Set` is predicative in Coq. My limited understanding indicates to me that this isn't the problem. I edited the original post to reflect the minimal development necessary to state the theorem, and tried to describe the problem that I'm having in more detail.
      singulars
      1. POexposing the structure of inductively defined terms in coq
      1. USdanportin
    3. CO@huitseeker “which is ill-typed” is recognizable as a Coq error, but a copy-paste of the actual proof attempt and exact error message would indeed have been appreciated. Having `J` in `Set` is right if you want to reason about them as first-class objects, say to prove their unicity.
      singulars
      1. POexposing the structure of inductively defined terms in coq
      1. USGilles
 

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