Start a new discussion

Not signed in

Want to take part in these discussions? Sign in if you have an account, or apply for one below

Site Tag Cloud

Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.

• CommentRowNumber1.
• CommentAuthorGuiGeek
• CommentTimeSep 12th 2019

In the page dependent sum type, the presented “term introduction rule” seems not really dependent, since the typing derivation of the second element is not aware of the first. I would expect $\frac{\vdash t:A\quad \vdash u:B[t/x]}{\vdash (t,u):\Sigma(x:A).B}$ which corresponds to what is presented in the text on positive and negative versions.

• CommentRowNumber2.
• CommentAuthoratmacen
• CommentTimeSep 12th 2019
• (edited Sep 12th 2019)

I guess they meant

$\frac{x:X \vdash a:A(x)}{x:X \vdash (x,a) : \sum_{x':X}A(x')}$

which I think is basically the right idea. But that’s not the usual rule either, since it doesn’t allow you to construct pairs in the empty context, unless you have a primitive substitution rule.

So the usual rule uses an arbitrary term of $X$:

$\frac{t:X \qquad a:A(t)}{(t,a) : \sum_{x:X}A(x)}$

This is the same as what you wrote, but with different notation.

• CommentRowNumber3.
• CommentAuthorGuiGeek
• CommentTimeSep 12th 2019

But what they meant looks wrong to me, since it does not allow to introduce any pair which first element is not a variable, for instance to prove $(0,Nil):\Sigma(n:Nat).Vect\,n$.

• CommentRowNumber4.
• CommentAuthoratmacen
• CommentTimeSep 12th 2019

Right, that’s why you’d need a substitution rule:

$\frac{\Gamma \vdash a\,:\,A \qquad \Gamma,x:A,\Gamma' \vdash t\,:\,T}{\Gamma,\Gamma'[a/x] \vdash t[a/x]\,:\,T[a/x]}$

So combining this with the variables-only pairing rule ($\Gamma' \coloneqq \cdot$, $a \coloneqq t$, $A \coloneqq X$, $t \coloneqq (x,a)$, $T \coloneqq \sum_{x':X}A(x')$) we get:

$\frac{\Gamma \vdash t\,:\,X \qquad \Gamma,x:X \vdash (x,a)\,:\,\sum_{x':X}A(x')}{\Gamma \vdash (t,a[t/x])\,:\,\sum_{x':X}A(x')}$

This is sufficiently general, since $x$ need not be free in $a$. (And there’s actually no reason for $x$ to be free in $a$ when you just immediately substitute, since both $t$ and $a$ are provided together. What you really want is for $x$ to be free in $A(x)$, of course.)

• CommentRowNumber5.
• CommentAuthorMike Shulman
• CommentTimeSep 12th 2019

I think we should give the usual rule, as in #2. Anyone who wants to fix it, please do!

• CommentRowNumber6.
• CommentAuthoratmacen
• CommentTimeSep 12th 2019

Now I’m not sure anymore. The argument I gave justifies:

$\frac{t:X \qquad x:X \vdash a\,:\,A(x)}{(t,a[t/x])\,:\,\sum_{x':X}A(x')}$

But having to prove $A(x)$ generically, rather than just $A(t)$ sounds harder, so maybe the rule is still too weak? Oh right, I guess it must be: what if $X$ is $bool$ and $A(x)$ is $\{true \mapsto \top,\;false \mapsto \bot\}$?

Yeah OK, it looks like requiring a variable was a red herring; the problem was that the premise isn’t depending on a specific term, like GuiGeek originally said.

• CommentRowNumber7.
• CommentAuthoratmacen
• CommentTimeSep 12th 2019

So the diagram next to the bad intro rule seems misleading: that $x$ arrow doesn’t have to be a context projection.

• CommentRowNumber8.
• CommentAuthoratmacen
• CommentTimeSep 12th 2019
Re #5: I edited the table include. Fixed?
• CommentRowNumber9.
• CommentAuthorMike Shulman
• CommentTimeSep 12th 2019

Yes, looks good. Thanks for catching this, GuiGeek, and for fixing it, Matt!