Want to take part in these discussions? Sign in if you have an account, or apply for one below
Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.
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.
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.
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$.
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.)
I think we should give the usual rule, as in #2. Anyone who wants to fix it, please do!
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.
So the diagram next to the bad intro rule seems misleading: that $x$ arrow doesn’t have to be a context projection.
Yes, looks good. Thanks for catching this, GuiGeek, and for fixing it, Matt!
1 to 9 of 9