Calculus of Inductive Constructions¶
| Source: | https://coq.inria.fr/distrib/current/refman/cic.html |
|---|---|
| Converted by: | Clément Pit-Claudel |
\[
\newcommand{\WF}[2]{{\cal W\!F}(#1)[#2]}
\newcommand{\WFE}[1]{\WF{E}{#1}}
\newcommand{\WT}[4]{#1[#2] \vdash #3 : #4}
\newcommand{\WTE}[3]{\WT{E}{#1}{#2}{#3}}
\newcommand{\WTEG}[2]{\WTE{\Gamma}{#1}{#2}}
\newcommand{\letin}[3]{\kw{let}~#1:=#2~\kw{in}~#3}
\newcommand{\subst}[3]{#1\{#2/#3\}}
\newcommand{\mto}{.\;}
\newcommand{\kw}[1]{\textsf{#1}}
\newcommand{\lb}{\lambda}
\newcommand{\Sort}{\cal S}
\newcommand{\alors}{\textsf{then}}
\newcommand{\alter}{\textsf{alter}}
\newcommand{\bool}{\textsf{bool}}
\newcommand{\conc}{\textsf{conc}}
\newcommand{\cons}{\textsf{cons}}
\newcommand{\consf}{\textsf{consf}}
\newcommand{\emptyf}{\textsf{emptyf}}
\newcommand{\EqSt}{\textsf{EqSt}}
\newcommand{\false}{\textsf{false}}
\newcommand{\filter}{\textsf{filter}}
\newcommand{\forest}{\textsf{forest}}
\newcommand{\from}{\textsf{from}}
\newcommand{\hd}{\textsf{hd}}
\newcommand{\haslength}{\textsf{has\_length}}
\newcommand{\length}{\textsf{length}}
\newcommand{\List}{\textsf{list}}
\newcommand{\nilhl}{\textsf{nil\_hl}}
\newcommand{\conshl}{\textsf{cons\_hl}}
\newcommand{\ident}{\textsf{ident}}
\newcommand{\nat}{\textsf{nat}}
\newcommand{\nO}{\textsf{O}}
\newcommand{\nS}{\textsf{S}}
\newcommand{\node}{\textsf{node}}
\newcommand{\Nil}{\textsf{nil}}
\newcommand{\Prop}{\textsf{Prop}}
\newcommand{\Set}{\textsf{Set}}
\newcommand{\si}{\textsf{if}}
\newcommand{\sinon}{\textsf{else}}
\newcommand{\Str}{\textsf{Stream}}
\newcommand{\tl}{\textsf{tl}}
\newcommand{\tree}{\textsf{tree}}
\newcommand{\true}{\textsf{true}}
\newcommand{\Type}{\textsf{Type}}
\newcommand{\unfold}{\textsf{unfold}}
\newcommand{\zeros}{\textsf{zeros}}
\newcommand{\even}{\textsf{even}}
\newcommand{\odd}{\textsf{odd}}
\newcommand{\evenO}{\textsf{even\_O}}
\newcommand{\evenS}{\textsf{even\_S}}
\newcommand{\oddS}{\textsf{odd\_S}}
\newcommand{\Prod}{\textsf{prod}}
\newcommand{\Pair}{\textsf{pair}}
\]
A term \(t\) is well typed in a global environment \(E\) iff there exists a local context \(\Gamma\) and a term \(T\) such that the judgment \(\WTEG{t}{T}\) can be derived from the following rules.
- W-Empty\[\frac{% % }{% \WF{[]}{}% }\]
- W-Local-Assum\[\frac{% \WTEG{T}{s}% \hspace{3em}% s \in \Sort% \hspace{3em}% x \not\in \Gamma % \cup E% }{% \WFE{\Gamma::(x:T)}% }\]
- W-Local-Def\[\frac{% \WTEG{t}{T}% \hspace{3em}% x \not\in \Gamma % \cup E% }{% \WFE{\Gamma::(x:=t:T)}% }\]
- W-Global-Assum\[\frac{% \WTE{}{T}{s}% \hspace{3em}% s \in \Sort% \hspace{3em}% c \notin E% }{% \WF{E;c:T}{}% }\]
- W-Global-Def\[\frac{% \WTE{}{t}{T}% \hspace{3em}% c \notin E% }{% \WF{E;c:=t:T}{}% }\]
- Ax-Prop\[\frac{% \WFE{\Gamma}% }{% \WTEG{\Prop}{\Type(1)}% }\]
- Ax-Set\[\frac{% \WFE{\Gamma}% }{% \WTEG{\Set}{\Type(1)}% }\]
- Ax-Type\[\frac{% \WFE{\Gamma}% }{% \WTEG{\Type(i)}{\Type(i+1)}% }\]
- Var\[\frac{% \WFE{\Gamma}% \hspace{3em}% (x:T) \in \Gamma~~\mbox{or}~~(x:=t:T) \in \Gamma~\mbox{for some $t$}% }{% \WTEG{x}{T}% }\]
- Const\[\frac{% \WFE{\Gamma}% \hspace{3em}% (c:T) \in E~~\mbox{or}~~(c:=t:T) \in E~\mbox{for some $t$}% }{% \WTEG{c}{T}% }\]
- Prod-Pro\[\frac{% \WTEG{T}{s}% \hspace{3em}% s \in \Sort% \hspace{3em}% \WTE{\Gamma::(x:T)}{U}{\Prop}% }{% \WTEG{\forall~x:T,U}{\Prop}% }\]
- Prod-Set\[\frac{% \WTEG{T}{s}% \hspace{3em}% s \in \{\Prop, \Set\}% \hspace{3em}% \WTE{\Gamma::(x:T)}{U}{\Set}% }{% \WTEG{\forall~x:T,U}{\Set}% }\]
- Prod-Type\[\frac{% \WTEG{T}{\Type(i)}% \hspace{3em}% \WTE{\Gamma::(x:T)}{U}{\Type(i)}% }{% \WTEG{\forall~x:T,U}{\Type(i)}% }\]
- Lam\[\frac{% \WTEG{\forall~x:T,U}{s}% \hspace{3em}% \WTE{\Gamma::(x:T)}{t}{U}% }{% \WTEG{\lb x:T\mto t}{\forall x:T, U}% }\]
- App\[\frac{% \WTEG{t}{\forall~x:U,T}% \hspace{3em}% \WTEG{u}{U}% }{% \WTEG{(t\ u)}{\subst{T}{x}{u}}% }\]
- Let\[\frac{% \WTEG{t}{T}% \hspace{3em}% \WTE{\Gamma::(x:=t:T)}{u}{U}% }{% \WTEG{\letin{x}{t:T}{u}}{\subst{U}{x}{t}}% }\]