paper.mng

% vim: set ft=tex:

\documentclass{jfp}
%\documentclass[a4paper]{article}
%\usepackage{a4wide}

\journaltitle{JFP}
\jnlDoiYr{2021}
\cpr{Cambridge University Press}
\doival{10.1017/xxxxx}

\newcommand{\citeinline}{\cite}
\newcommand{\citeparens}[1]{(\cite{#1})}

\usepackage{amsmath,amsfonts,amssymb,amsthm}
\tracinglostchars=2
\usepackage[utf8]{inputenc}
\usepackage[T2A]{fontenc}
%\usepackage{fontspec}
%\usepackage{unicode-math}
\usepackage{hyperref,cleveref}
\usepackage{mathtools}
\usepackage{xcolor}
\usepackage[implicitLineBreakHack]{ottalt}
\usepackage{subcaption}
\usepackage{url,natbib}
\usepackage{todonotes}
\usepackage{minted}
\usepackage[english]{babel}
\usepackage{newunicodechar}
\usepackage[toc,page]{appendix}

\newunicodechar{ℓ}{\ensuremath{\mathnormal\ell}}
\newunicodechar{ρ}{\ensuremath{\mathnormal\rho}}
\newunicodechar{σ}{\ensuremath{\mathnormal\sigma}}
\newunicodechar{ε}{\ensuremath{\mathnormal\varepsilon}}
\newunicodechar{ι}{\ensuremath{\mathnormal\iota}}

%\nonstopmode{}

\newtheorem{theorem}{Theorem}
\newtheorem{corollary}{Corollary}
\newtheorem{lemma}{Lemma}
\newtheorem{remark}{Remark}
\crefname{lemma}{lemma}{lemmas}
\crefname{remark}{remark}{remarks}
\crefname{theorem}{theorem}{theorems}

\newtheorem*{lemma*}{Lemma}
\newtheorem*{theorem*}{Theorem}

\newcommand{\unit}{\textbf{u}}
\newcommand{\Unit}{\textbf{Unit}}
\newcommand{\unitc}{\hat{\textbf{u}}}
\newcommand{\Unitc}{\widehat{\textbf{Unit}}}
\newcommand{\Basec}{\hat{B}}
\newcommand{\Int}{\textbf{Int}}
\newcommand{\ctxok}{\text{~ok}}
\newcommand{\fresh}{\text{~fresh name}}
\newcommand{\evalsto}{\rightsquigarrow}
\newcommand{\eqrefl}{\text{eq-refl~}}
\newcommand{\secondDP}{\text{second-dp~}}

\newcommand{\prooftermname}[1]{\texttt{#1}}

\begin{document}

\newNTclass{nonterm}
\newnonterm{e}{\varepsilon}
\newnonterm{es}{\varepsilon}
\newnonterm{ec}{\hat\varepsilon}
\newnonterm{r}{\rho}
\newnonterm{ts}{\tau}
\newnonterm{tc}{\hat\tau}
\newnonterm{s}{s}
\newnonterm{l}{l}
\newnonterm{B}{B}
\newnonterm{G}{\Gamma}
\newnonterm{GC}{\hat\Gamma}
\newnonterm{vs}{\varpi}
\newnonterm{vc}{\hat\varpi}
\newnonterm{f}{f}
\newnonterm{gamma}{\gamma}

\newNTclass{gterm}
\newgterm{x}{x}
\newgterm{v}{v}
\newgterm{n}{n}
\newgterm{p}{\pi}

\newcommand{\figref}[1]{Figure~\ref{fig:#1}}

\inputott{surface.ott}

\newcommand{\rae}[1]{\textcolor{magenta}{RAE: #1}}
\newcommand{\gr}[1]{\textcolor{green}{G: #1}}

\title{Compiling refinement types to dependent types}

\begin{abstract}
\end{abstract}

\maketitle

\section{Introduction}

Type systems are a powerful tool for internal specification and verification of programs,
ensuring that programs exhibit certain desirable properties and do not exhibit undesirable ones.
In particular, dependent types~\citeparens{FindSomethingForDTs} are powerful enough to encode pretty much arbitrary specifications,
going as far as encoding mathematics itself~\citeparens{FindSomethingForCurryHoward},
but this power comes at a cost: term finding (or, equivalently, proof finding) for dependent types is undecidable,
and so is type inference.
Or, practically speaking, the programmer must care about the details of the proofs,
even if the proofs lie within decidable theories
(like some flavours of arithmetic, sufficient for reasoning about array accesses and preventing out-of-bounds errors).
Even if the language supports some form of proof automation (such as proof by reflection, or Coq's tactics, or Idris' elaborator reflection),
this is still something that the programmer has to pay attention to.
Not only this consumes a part of human attention span (which is quite limited, compared to computers),
but we believe it also prevents widespread adoption of dependent types for mainstream programming.

A different point on the spectrum is represented by \emph{liquid types}~\citeparens{LiquidTypes08},
where the expressive power is limited, and the type system only allows specifying properties that can be efficiently proven (or disproven) by an SMT solver.
Liquid types are a special case of a more general concept of \emph{refinement types}~\citeparens{Constable87,Rushby98},
which are some base types endowed with a predicate, possibly dependent on other values, like \verb+{ v : Int | v >= 0 & v < len arr }+.
The logical implication on predicates
(or, equivalently, the set inclusion relation on the sets defined by predicates)
gives rise to a natural \emph{subtyping relation}:
for example, the aforementioned type is a subtype of \verb+{ v : Int | v >= -1 }+,
and the corresponding implication (which, in this case, is a tautology) is known as a \emph{verification condition} (VC).
The core idea of liquid types then is to ensure that this subtype relation is efficiently decidable by an SMT solver.

Another useful property of refinement types is that they have a natural mental model:
indeed, it feels more approachable to treat \verb+{ v : Int | v >= 0 & v < len arr }+ as just an integer that is within some array's bounds
as opposed to the typical interpretation of
``a dependent pair consisting of an integer and a pair of proofs,
one for said integer being non-negative and another one for it being less than the length of \verb+arr+''.
Thus, refinement types are arguably more accessible and more usable in mainstream programming.

The downside is that efficiently decidable refinement types are less expressive, limiting what can be specified and proven.
Even though there are new developments pushing the envelope of what can be expressed with liquid types~\citeparens{Reflection18},
the natural question is what would it take to combine full dependent types and refinement types in a single language.

Our work lays the theoretical foundation for positively answering this question, which, to the best of our knowledge, is a new contribution.
We consider a dependently typed language as some ``core'' language,
to which a ``surface'' language with just the refinement types is translated.
Moreover, we do not consider the peculiarities of a specific algorithm performing the subtyping check in the refinements language,
introducing instead the abstraction of a \emph{subtyping oracle}.
This allows plugging in not just SMT solvers but arbitrary decision procedures as long as they have certain properties we describe later.

This translation to a core dependently typed language provides several nice metatheoretical properties, most importantly:
\begin{itemize}
  \item Dependent types are a well-studied and well-understood subject,
    so taking them as the translation target automatically provides us with the existing array of metatheorems.
  \item Since we require the subtyping oracle to produce a proof of the subtyping relation,
    the result of the translation satisfies the de Bruijn criterion:
    even if the solver makes a mistake and produces an incorrect proof,
    this mistake would be caught by the type checker for the core language.
    We deem this a desirable property as it reduces the trusted code base size,
    since type checkers are typically simpler and have smaller ``error surface'' than SMT solvers,
    and, moreover, the core type checker has to be trusted anyway.
\end{itemize}

Of course, there are related developments. Perhaps the closest one is F* and, in particular, Meta-F*~\citeparens{MetaFStar} (which is also based on F* core).
(Meta-)F* also supports dependent types, but they are rather used to manipulate the VCs to turn them into an SMT-decidable form,
or discharge certain proof obligations not decidable via SMT\@.
The main difference between (Meta-)F* and our approach is that F*'s core type checker still relies on an SMT solver,
while our approach keeps the core type checker limited to a dependent type theory.

Another example of a closely related work is Hammer~\citeparens{CoqHammer}, which brings some form of automation to Coq.
Although it achieves a similar goal of producing proof terms that are then verified using the core Coq type checker,
using either a decidable fragment of Coq's logic in case of the \verb+sauto+ tactic,
or machine learning and external automated theorem provers in case of the \verb+hammer+ tactic,
it still requires the programmer to think in terms of full dependent types.

Since verification of programs for safer software is the ultimate goal of all these type systems,
it seems important to have firm foundations and verify that the type systems themselves do make sense.
Thus, we also present mechanically verified proofs in Agda of all the key theorems about our surface language and its translation procedure.
This is, as far as we are aware, also a new contribution,
and no prior papers strived to mechanically verify the metatheoretical properties of refinement types to this extent.

\rae{I was expecting to find contributions here. We need to write out the paper's
contributions.}

\section{Motivation}

Having refinement types and dependent types in a single language is useful for many reasons.

Firstly, refinement types indeed lower the cognitive load and the amount of (both keyboard and mathematical) typing the programmer has to do.
As an example, consider a function taking two non-negative numbers $x, y$ and returning $x + y + x$ along with a proof that each summand is less than or equal to the sum.
In a language with refinement types writing such a function is at most\footnote{Some implementations \citeparens{LiquidTypes08} can infer refinements automatically}
a matter of decorating its type with the right refinements, along the lines of:
\begin{minted}{idris}
funnyAdd : (x : { v : Int | v >= 0 })
         → (y : { v : Int | v >= 0 })
         → { v : Int | v >= x & v >= y }
funnyAdd x y = x + y + x
\end{minted}
Then, it's up to the SMT solver to verify that the function satisfies the refinements.

What if we wanted to write a similar function with similar guarantees in a dependently typed language with explicit proofs?

First of all, the question of representing integers in a proof-friendly way is non-obvious,
with different approaches taken in different works and ranging from
a positional representation of strictly positive integers along with a three-constructor algebraic data type for the whole range of integers~\citeparens{CoqBinNums},
to the Grothendieck group over the monoid of natural numbers.
To avoid digressing into the pros and cons of each approach,
let's give the dependently typed implementation a leg-up and assume Peano natural numbers everywhere.
Even with this allowance, the task is non-trivial, with an example Idris solution:
\begin{minted}{idris}
ltePlusLeft : (x, y : Nat) -> x `LTE` y + x
ltePlusLeft x Z = lteRefl
ltePlusLeft x (S y) = lteSuccRight (ltePlusLeft x y)

ltePlusFunny : (x, y : Nat) -> y `LTE` x + y + x
ltePlusFunny x y = rewrite plusCommutative (x + y) x
                in rewrite plusAssociative x x y
                in ltePlusLeft y (x + x)

funnyAdd : (x : Nat)
        -> (y : Nat)
        -> (v : Nat ** (x `LTE` v, y `LTE` v))
funnyAdd x y = (x + y + x ** (ltePlusLeft x (x + y), ltePlusFunny x y))
\end{minted}
Despite extensive use of library lemmas like \verb+lteRefl+, \verb+lteSuccRight+, \verb+plusCommutative+ and \verb+plusAssociative+,
the code is considerably longer and is riddled with unnecessary details.

More than that, slight variations of the pre- and post-conditions are just a matter of updating the signature with refinement types:
\begin{minted}{idris}
funnyAdd' : (x : { v : Int | v > 0 })
          → (y : { v : Int | v > 0 })
          → { v : Int | v > x & v > y }
funnyAdd' x y = x + y + x
\end{minted}
On the other hand, updating the code with explicit proofs requires more human work and is left as an exercise to the reader.

As an another example, consider the function calculating the maximum of three numbers.
Implementing it with refinement types is about as straightforward as it might get:
\begin{minted}{idris}
max3 : (x : Int) → (y : Int) → (z : Int)
     → { v : Int | v >= x & v >= y & v >= z }
max3 x y z = if x > y then
                 if x > z then x else z
             else
                 if y > z then y else z
\end{minted}

Casting integers aside and working with plain naturals again, the dependently typed solution might look a bit move involved:
\begin{minted}{idris}
notLTE : (x, y : Nat)
      -> (x `LTE` y -> Void)
      -> y `LTE` x
notLTE x Z not = LTEZero
notLTE Z (S y) not = void (not LTEZero)
notLTE (S x) (S y) notS = LTESucc (notLTE x y (\not => notS (LTESucc not)))

max3 : (x, y, z : Nat)
    -> (v : Nat ** (x `LTE` v, y `LTE` v, z `LTE` v))
max3 x y z =
  case y `isLTE` x of
       Yes y_LTE_x =>
            case z `isLTE` x of
                 Yes z_LTE_x => (x ** (lteRefl, y_LTE_x, z_LTE_x))
                 No contra => let x_LTE_z = notLTE _ _ contra
                               in (z ** (x_LTE_z,
                                         lteTransitive y_LTE_x x_LTE_z,
                                         lteRefl))
       No contra =>
            let x_LTE_y = notLTE _ _ contra
             in case z `isLTE` y of
                     Yes z_LTE_y => (y ** (x_LTE_y, lteRefl, z_LTE_y))
                     No contra => let y_LTE_z = notLTE _ _ contra
                                   in (z ** (lteTransitive x_LTE_y y_LTE_z,
                                             y_LTE_z,
                                             lteRefl))
\end{minted}

In general, refinement types are expressive enough to eliminate a fair share~\citeparens{LiquidTypes08} of run-time errors such as out-of-bounds array accesses or division by zero.

On the other hand, certain things are not expressible with refinement types.
In particular, we claim without proof that refinement types cannot affect run-time behaviour of the program
(and the reader familiar with the notion of run-time irrelevance or Coq's \verb+Prop+ universe might find those concepts useful to build the intuitive agreement with our claim).
For example, a type-safe variadic \verb+printf+ (whose arguments count, their \emph{types}, and run-time behaviour \emph{depend} on the formatting string argument \emph{value}) is not expressible with refinement types.
Although, it is worth noting that it seems to be possible to recover the full expressive power of dependent types via a \verb+Top+ type with the corresponding subtyping relation, at the cost of moving the typing checks to run-time.
\todo[inline]{Illustrate this via a Top-based printf.}

Moreover, for fundamental reasons such as Rice's theorem, there is no algorithm that decides arbitrary non-trivial semantic properties of a program,
so human assistance will always be needed for sufficiently complex programs, and this is where dependent types also come useful.
And, in practice, most existing SMT solvers do not support higher-order reasoning (in fact, it is not supported in the current SMT-LIB v2), or reasoning beyond some simple arithmetic or arrays,
so, for instance, formally proving the properties of the type system proposed in this very paper is something that, currently, a human should do.

There is also a certain synergy coming from uniting dependent types and refinement types:
for intance, since types are first-class in a dependently typed language, the refinements can also be treated as first-class.
As an example, \verb+filter+ function is conceivable which amends (arbitrary) refinements on the input, along the lines of
\begin{minted}{idris}
filter : forall Pred.
       → List { v | Pred }
       → (f : {v | Pred} → Bool)
       → List {v | Pred & f v = True}
\end{minted}

Given all of the above, it is desirable to have both refinement types and dependent types in a single language.
But having both in a single core type checker seems extravagant, and, since refinement types can be seen as a subset of dependent types,
a reasonable way to go is to have a core type checker for full dependent types, a surface language with both type systems,
and translating, respectively, refinements to dependent types and SMT decisions to proof terms.

This paper focuses on formulating the translation part and proving that the translation preserves semantics and has certain reasonable and useful properties.
We believe that the approach proposed in this paper is implementable in existing dependently typed languages such as Idris or Agda.
A language might allow both ``refinemently typed'' and dependently typed terms in a single module,
reserving a certain syntax such as \verb+foo : { v : Ty | Predicate v }+ to indicate that \verb+foo+ uses refinement types,
while also allowing to use the former in the latter and vice versa.
This enables the programmer to mostly write code with refinement types,
only resorting to the full power of dependent types when refinements are not enough.

\section{Overview}

\paragraph{Surface language}
We define a surface language with refinement types inspired by~\citeinline{LiquidTypes08,Reflection18}.
Broadly speaking, it is a simply-typed lambda calculus with several extensions,
including refinement types.
The other extensions are:
\begin{itemize}
  \item dependent arrow types, to allow subsequent refinements refer preceding arguments,
  \item a limited form of algebraic data types (ADTs) and dependent pattern matching, inspired by~\citeinline{TAPLVariants,Eisenberg16},
    to illustrate reasoning about these widely used constructs, as well as generalizing path sensitivity~\citeparens{FindSomethingForPathSensitivity}.
\end{itemize}

We also formulate and prove type safety of our language via the usual progress and preservation theorems.

One major difference between our surface language and the languages in~\citeinline{LiquidTypes08,Reflection18} is that both parametric polymorphism as well as recursion are omitted.
This simplifies the formal model of the surface language considerably, while still giving meaningful results.

\paragraph{Core language}
Our core language is a full dependently typed language based on $\lambda C$ \citeparens{Schmidt1994,Barendregt92}
and extended with a unit type and a restricted form of algebraic data types.

\paragraph{Subtyping oracle}
The refinements in our surface language may contain arbitrary terms, including function application.
In general, this makes the subtyping check undecidable: even though our surface language turns out to be strongly normalizing, in practice most languages allow potentially non-terminating terms.
We sidestep this by abstracting the subtyping checker away and introducing a notion of an oracle.
As a nice side effect, this way we also do not have to consider the specifics of the subtyping check and instead focus on compiling refinement types to dependent types.
\todo[inline]{Reword this.}
The interface of said oracle boils down to a single function:
it takes a typing context $[[ G ]]$ and two refinements $[[ r1 ]], [[ r2 ]]$ over some argument $ v $, and decides whether one is the subtype of the other.
We denote the logical context arising from the typing context $[[ G ]]$ as $[| [[ G ]] |]$, so the oracle just decides whether $[[ [| G |] => A v. (r1 => r2) ]]$ holds.

The oracle abstraction allows keeping type-checking decidable even in the presence of non-terminating terms in refinements, assuming the oracle runs in finite time.
Practically, this means that any implementation of an oracle (that always completes in finite time) will have either false negatives (deciding that some types are not in subtype relationship when, in fact, they are) or false positives.
False negatives may limit the expressive power of the language, but they do not break its type safety, and what matters is the lack of false positives.
It is also worth noting that if an implementation cannot decide a query (that is, it can neither prove nor disprove it), it might leave it as a lemma to be filled out by the user in the full dependently typed core language.

We also require the oracle to satisfy certain properties for the aforementioned surface language metatheorems to hold.
As an example, if the oracle yields a ``positive'' decision in some typing context, then it also must yield a ``positive'' decision in any bigger context,
extended with variable bindings irrelevant to the subtyping problem being considered.
All the required properties are mentioned in each individual metatheorem directly relying on them,
and those properties are listed in \cref{sect:oracle_requirements}.

It is worth noting that the work on liquid types usually assumes the subtyping checks are done via an SMT solver, which can be seen to fit our oracle abstraction.

\paragraph{Combining refinement and dependent types}
After formulating our surface and core languages, we define a translation from the former to the latter.
We also formulate two key theorems proving that the translation makes sense.
First, we prove that any well-typed surface language term has a translation to a well-typed core language term.
Then, we prove that the small-step operational semantics of the languages match and commute with the translation:
if a surface language term $[[ es ]]$ evaluates to some other term $[[ es' ]]$ in one step,
then the translation of $[[ es ]]$ to the core language evaluates into the translationof $[[ es' ]]$, although, perhaps, in several steps.

\section{Calculi definitions}

\subsection{Surface language}

The syntax of the surface language is presented in \figref{surface_syntax}.
The (small-step) operational semantics for the surface language are laid out in \figref{surface_opsem}.
That is largely the usual call-by-value evaluation model
with some extra rules for the ADTs and pattern matching.
The (restricted) type ``equivalence'' is presented in \figref{surface_tyequiv}.
The typing rules for the surface language are presented in \figref{surface_typing}.

As usual, to simplify the exposition,
all bindings in contexts are assumed to have different names, and all labels in each ADT are assumed to be different.

We also have the following concessions:
\begin{itemize}
  \item The syntax only allows refinements on base types.
    Note that this does not severely restrict the expressive power of the language.
    To see that, consider the following examples:
    \begin{description}
      \item[A functional argument.] Suppose we wish to write:
        \[
          (x : \Int) \rightarrow \{ v : \Int \rightarrow \Int | v x = 0 \} \rightarrow \Int
        \]
        With our syntax, we instead introduce a dummy parameter and write the same refinement modulo variable naming:
        \[
          (x : \Int) \rightarrow (f : \Int \rightarrow \Int) \rightarrow \{ \_ : \Unit | f x = 0 \} \rightarrow \Int.
        \]
      \item[An ADT argument] is treated similarly.
      \item[A function that is returned.] This time, suppose we wish to express
        \[
          (x : \Int) \rightarrow \{ v : \Int \rightarrow \Int | v (x + 1) = 0 \land v (x - 1) = 0 \}
        \]
        Instead, we shift the refinement to the right, refining the last value and turning the arguments into antecedents of an implication:
        \[
          (x : \Int) \rightarrow (y : \Int) \rightarrow \{ v : \Int | (y = x + 1 \Rightarrow v = 0) \land (y = x - 1 \Rightarrow v = 0) \}
        \]
      \item[An ADT that is returned.] Suppose we now wish to write, for some function $f$, the following:
        \[
          (x : \Int) \rightarrow \{ v : [[ < </ li : tsi // i /> > ]] | f x v = 0 \}
        \]
        Informally, the only way $f$ can consume a value of type $[[ < </ li : tsi // i /> > ]]$ is by pattern-matching on it.
        Thus, for each $[[ tsi ]]$ the function $f$ gives rise to a refinement $[[ ri ]]$, which is basically the right-hand side of the equation for $f$ corresponding to the constructor $[[ li ]]$.
        We push this refinement into the ADT, replacing each $[[ tsi ]]$ with $\{ v : [[ tsi ]] | [[ ri ]] \}$, recursively desugaring the refinement on $[[ tsi ]]$ as well.
    \end{description}
  \item Our algebraic data types only allow a single ``field'' in each constructor.
    One way to alleviate this is to introduce tuples,
    but doing so would complicate the exposition
    without any benefit for illustrating the main idea of this work.
\end{itemize}

\begin{remark}\label{remark:surface_base_types}
  The surface language might also have other base types (for example, $\Int$),
  elements of syntax (like numbers and operations on them)
  as well as typing rules relating those,
  but we omit them for the sake of brevity.
\rae{Brevity is good, but having only Unit makes the language trivial. Given that
the proofs are done over the language defined here, we need to add at least Int.}
\end{remark}

\begin{remark}
  Type equivalence $[[ requiv ]]$ alone is neither transitive nor reflexive,
  but those properties are regained by applying \textsc{T-RConv}, the only rule relying on $[[ requiv ]]$, enough times:
  zero for reflexivity and multiple times for transitivity.
  Delegating reflexivity and transitivity to the typing derivations, while perhaps being non-canonical,
  simplifies the proofs of the metatheoretical properties of the language.
\end{remark}

\begin{figure}[ht]
  \centering
  \begin{subfigure}{.6\textwidth}
    \nonterms{es,l,vs}
    \caption{Term level}
  \end{subfigure}

  \begin{subfigure}{.5\textwidth}
    \nonterms{G,r,B,ts}
    \caption{Type level}
  \end{subfigure}

  \caption{Surface language syntax}\label{fig:surface_syntax}
\end{figure}

\begin{figure}[ht]
  \drules[E]{$[[ es1 ~~> es2 ]]$}{term evaluation}{AppL,AppR,AppAbs,ADT,CaseScrut,CaseMatch}
  \caption{Surface language small-step operational semantics}\label{fig:surface_opsem}
\end{figure}

\begin{figure}[ht]
  \drules[RTEquiv]{$[[ ts1 requiv ts2 ]]$}{type equivalence}{Forward,Backward}
  \caption{Surface language type equivalence}\label{fig:surface_tyequiv}
\end{figure}

\begin{figure}[ht]
  \drules[TCTX]{$[[ G ok ]]$}{context well-formedness}{Empty,Bind}
  \drules[TWF]{$[[ G |- ts ]]$}{type well-formedness}{TrueRef,Base,Conj,Arr,ADT}
  \drules[T]{$[[ G |- es : ts ]]$}{term typing}{Unit,Var,Abs,App,Case,Con,Sub,RConv}
  \drules[ST]{$[[ G |- ts1 <: ts2 ]]$}{subtyping}{Base,Arr}
  \caption{Surface language typing}\label{fig:surface_typing}
\end{figure}

The translation function $[|\ |]$ maps the typing context $\nonterm G$ to some logic that the oracle can handle, and that we leave abstract.
Generally, the translation of a whole context is the conjunction of the translations of the types of the individual bindings,
and, within each refined type, the translation of the conjunction of atomic refinements is the conjunction of the translations of the atomic refinements.

\subsubsection{Requirements on the oracle}\label{sect:oracle_requirements}

Since the surface language uses the subtyping oracle in its type system, the metatheoretical properties of the language depend on the oracle satisfying certain crucial requirements.
\begin{enumerate}
  \item\label{orprop:trans}
    \emph{Transitivity}: if the oracle concludes $[[ [| G |] => A v. (r1 => r2) ]]$ and $[[ [| G |] => A v. (r2 => r3) ]]$, then it must conclude $[[ [| G |] => A v. (r1 => r3) ]]$.

  \item\label{orprop:thinning}
    \emph{Thinning}: if $[[ G ]] \subset [[ G' ]]$ and the oracle concludes $[[ [| G |] => A v. (r1 => r2) ]]$, then it must conclude $[[ [| G' |] => A v. (r1 => r2) ]]$.

    In words, if an oracle concludes that $[[ r1 ]]$ implies $[[ r2 ]]$ in some context $[[ G ]]$, then it must also conclude this implication in any bigger context $[[ G' ]]$.
    Intuitively, if the bigger context $[[ G' ]]$ does not contradict the smaller one $[[ G ]]$, then the oracle ought to be able to use just the assumptions from the subset of $[[ G' ]]$ isomorphic to $[[ G ]]$.
    Otherwise, if some bindings in $[[ G' ]]$ introduce a contradiction, then anything is derivable, including the required conclusion.

  \item\label{orprop:narrowing}
    \emph{Narrowing}: if $[[ G |- ts' <: ts ]]$, and the oracle concludes $[[ [| G, x : ts, GD |] => A v. (r1 => r2) ]]$, then it must conclude $[[ [| G, x : ts', GD |] => A v. (r1 => r2) ]]$.

    To intuitively justify this requirement, note the analogy to the chained implication in logic, and, speaking in terms of logic, $[[ G |- ts' <: ts ]]$ means that the implication $\tau' \implies \tau$ holds in $[[ G ]]$.
    But this also means that, given the derivation of $[[ [| G, x : ts, GD |] => A v. (r1 => r2) ]]$ and a context $[[ G, x : ts', GD ]]$, we could first derive an object of type $[[ ts ]]$ using just the context $[[ G ]]$,
    and then use that object in place of $x$ in the derivation of $[[ [| G, x : ts, GD |] => A v. (r1 => r2) ]]$.

  \item\label{orprop:subst}
    \emph{Substitution}: if $[[ G |- es : ts ]]$ and the oracle concludes $[[ [| G, x : ts, GD |] => A v. (r1 => r2) ]]$, then it must also conclude $[[ [| G, [ x |-> es ] GD |] => A v. ( [ x |-> es ] r1 => [ x |-> es ] r2 ) ]]$.

    To see why this is a natural requirement, consider $[[ es ]]$ to be a proof of the statement $[[ ts ]]$ in the context $[[ G ]]$.
    Then the premise $[[ [| G, x : ts, GD |] => A v. (r1 => r2) ]]$ means that $[[ A v. (r1 => r2) ]]$ holds with $[[ ts ]]$ as the assumption (among others).
    Substituting $[[ x ]]$ for $[[ es ]]$ then boils down to replacing that assumption with its proof.

  \item\label{orprop:stepping}
    \emph{Stepping}: if $[[ ts requiv ts' ]]$ and the oracle concludes $[[ [| G, x : ts, GD |] => A v. (r1 => r2) ]]$, then it must also conclude $[[ [| G, x : ts', GD |] => A v. (r1 => r2) ]]$.

    In other words, evaluation should not affect the logical interpretation of types.
\end{enumerate}

\subsubsection{Properties}

We prove the usual metatheoretical properties of the proposed language.
Some of the lemmas directly used in the subsequent exposition as well as progress and preservation theorems are formulated below.
The full (numbered and topologically sorted) list of the proven lemmas can be found in \cref{appendix:surface_props}.
The numbers of these lemmas in that list are given here in parenthesis.

We also provide machine-verified proofs of these theorems in the supplemental code,
with the corresponding proof terms referred in lemmas names.

\begin{lemma*}[Agreement I, \cref{lma:term_wf_implies_ctx_wf}, \prooftermname{T-implies-TCTX}]
  If $[[ G |- es : ts ]]$, then $[[ G ok ]]$.
\end{lemma*}

\begin{lemma*}[Agreement II, \cref{lma:type_wf_implies_ctx_wf}, \prooftermname{TWF-implies-TCTX}]
  If $[[ G |- ts ]]$, then $[[G ok]]$.
\end{lemma*}

\begin{lemma*}[Agreement III, \cref{lma:term_wf_implies_type_wf}, \prooftermname{T-implies-TWF}]
  If $[[ G |- es : ts ]]$, then $[[ G |- ts ]]$.
\end{lemma*}

\begin{theorem*}[Progress, \cref{thm:surface_progress}, \prooftermname{progress}]
  If $[[ empty |- es : ts ]]$, then either $[[ es ]]$ is a value, or there exists $[[ es' ]]$ such that $[[ es ~~> es' ]]$.
\end{theorem*}

\begin{theorem*}[Preservation, \cref{thm:surface_preservation}, \prooftermname{preservation}]
  If $[[ G |- es : ts ]]$, and $[[ es ~~> es' ]]$, then $[[ G |- es' : ts ]]$.
\end{theorem*}

\subsection{Core language}

The syntax of the core language is presented in \figref{core_syntax},
the core $\lambda C$ typing rules are defined in \figref{core_typing}
and the rules for our extensions are defined in \figref{core_typing_exts}.

We conjecture these extensions do not break the metatheoretical properties of the original $\lambda C$,
for instance, referring to~\cite{Barendregt92}:
\begin{itemize}
  \item Preservation~--- Theorem 5.2.15.
  \item Strong normalization~--- Theorem 5.3.33.
  \item Consistency, that is, $\bot$ is not derivable in the empty context~--- follows from Theorem 5.2.31 and strong normalization.
\end{itemize}

As a general convention,
core entities corresponding to the surface language are denoted by the same symbol, but with a $\widehat{\text{hat}}$.
For instance, core typing contexts are denoted as $[[ GC ]]$ and core expressions are denoted as $[[ ec ]]$.
In addition to that, we somewhat frivolously use $\hat B$
to denote the core language analogue of a surface language base type $B$,
which exists for $\Unit$ ($\hat B$ then being $\Unitc$)
and which we assume to exist for any other surface language base type
mentioned in \cref{remark:surface_base_types}.
We also assume that $\hat B$ has sort $\star$.

Although there is no separate syntactic notion of a type,
$[[ tc ]]$ is used as a metavariable where a ``type'' (an inhabitant of $\star$) or a sort ($\star$ itself or $\square$) is expected.
$[[ ec ]]$ is understood as usual, denoting any expression in the core language, be it a ``term'', a ``type'' or a sort.
The $\_$ placeholder is used where a binding name is expected but the binding is not used in the corresponding subterm,
as in $[[ Pi _ : tc1. tc2 ]]$.

Unlike the surface language,
there is no separate rules for type or context well-formedness.
Instead, when we say that a type $[[ tc ]]$ (with the above remark about what a ``type'' means) is well-formed,
we just mean that $[[ GC |- tc : sst ]]$ or $[[ GC |- tc : ssq ]]$.
To define the notion of context well-formedness,
we say that a context $[[ GC ]]$ is well-formed iff it is possible to derive $[[ GC |- ec1 : ec2 ]]$
for some $[[ ec1 ]], [[ ec2 ]]$.
Derivability of $[[ GC |- ec1 : ec2 ]]$, in turn, can be shown to imply the derivability of $[[ GC |- sst : ssq ]]$.
The latter is by no coincidence used as a premise in the \textsc{CT-UnitType} and \textsc{CT-UnitTerm} rules:
indeed, the purpose of this premise is to ensure that those rules are only applicable in a well-formed context.

The \textsc{CT-ADTCase} rule differs slightly from a typical case matching rule.
In our system, each right-hand side of a case match on a term $[[ es ]]$ has access
not only to the variable $[[ xi ]]$ under the corresponding constructor $[[ li ]]$,
but also to a proof term $[[ pi ]]$ showing that
this $[[ xi ]]$, decorated by the constructor $[[ li ]]$, is equal to the scrutinee $[[ es ]]$.
This equality is denoted by $\equiv$, which is a derived form defined later.

\begin{remark}
  One plausible way to avoid the doubt in the type safety of our core language stemming from the presence of the ADTs is to
  encode them via the Boehm-Berarducci encoding~\citeparens{Bohm85}.
  Unfortunately, this does not work in our case precisely due to the presence of the equality proof term:
  this encoding does not provide the equality witness,
  and it seemingly cannot be easily extended to account for this witness.
\end{remark}

Even though we believe that our core language enjoys the strong normalization property,
we still explicitly define the evaluation rules (\figref{core_opsem}).
Firstly, this allows fixing a specific evaluation strategy mirroring the one for the surface language,
simplifying the subsequent proofs of some key theorems.
Secondly, the rule for \textsc{CE-CaseMatch},
as well as our flavour of pattern matching in general,
deserves some special attention.
\todo[inline]{Pay said attention.}

\begin{figure}[ht]
  \nonterms{ec,s,vc}
  \caption{Core language syntax}\label{fig:core_syntax}
\end{figure}

\begin{figure}[ht]
  \drules[CT]{$[[ GC |- ec1 : ec2 ]]$}{core typing}{Sort,Var,Weaken,Form,App,Abs,Conv}
  \caption{$\lambda C$ typing rules}\label{fig:core_typing}
\end{figure}
\begin{figure}[ht]
  \drules[CT]{$[[ GC |- ec1 : ec2 ]]$}{core typing, extensions}{UnitType,UnitTerm,ADTForm,ADTCon,ADTCase}
  \caption{Typing rules for our extensions to $\lambda C$}\label{fig:core_typing_exts}
\end{figure}

\begin{figure}[ht]
  \drules[CE]{$[[ ec1 ~~> ec2 ]]$}{term evaluation}{AppL,AppR,AppAbs,ADT,CaseScrut,CaseMatch}
  \caption{Core language small-step operational semantics}\label{fig:core_opsem}
\end{figure}

\newcommand{\dast}{\ **\ }

\subsubsection{Derived forms}\label{sect:derived_forms}
We also establish some derived forms in the core language to simplify the subsequent exposition:
\begin{itemize}
  \item Simplified variable typing rule which we call \textsc{CT-VarW}:
    \[ \ottdruleCTXXVarW{} \]
    This rule unfolds into a single \textsc{CT-Var} defining $x$,
    followed by a sequence of \textsc{CT-Weaken}
    to ``move'' the $x$ into the right position in the final $[[ GC ]]$.
  \item Non-dependent function type:
    \[
      [[ tc1 -> tc2 ]] \triangleq [[ Pi _ : tc1. tc2 ]].
    \]
  \item Dependent pair type, or the $\Sigma$-type,
    with the first component being a value $x$ of type $[[ tc ]]$
    and the second component being a value of type $[[ Pred x ]]$, where $[[ Pred ]]$ is of type $[[ tc -> sst ]]$:
    \[
      [[ Sigma tc Pred ]] \triangleq [[ Pi alpha : sst. (Pi x : tc. Pred x -> alpha) -> alpha ]],
    \]
    with the corresponding constructor:
    \[
      [[ < ec : tc , p of Pred > ]] \triangleq [[ \ alpha : sst. \ f : (Pi x : tc. Pred x -> alpha). f ec p ]].
    \]

  \item Non-dependent pair type:
    \[
      [[ (tc1, tc2) ]] \triangleq [[ Pi alpha : sst. (tc1 -> tc2 -> alpha) -> alpha ]],
    \]
    with the corresponding constructor:
    \[
      [[ (ec1 : tc1, ec2 : tc2) ]] \triangleq [[ \ alpha : sst. \ f : (tc1 -> tc2 -> alpha). f ec1 ec2 ]].
    \]

    Alternatively, we could have defined non-dependent pairs via dependent pairs, along the lines of
    \[
      [[ (tc1, tc2) ]] \triangleq [[ Sigma tc1 (\ _ : tc1. tc2) ]],
    \]
    but mechanically proving this definition is well-typed (given our call-by-value operational semantics)
    requires mechanically proving that the core language is strongly normalizing,
    which is beyond the scope of this work.
  \item Equality of expressions $[[ ec1 ]], [[ ec2 ]]$ of type $[[ tc ]]$:
    \[
      [[ ec1 equal ec2 of tc ]]
        \triangleq
        [[ Pi Pred : tc -> sst. ( Pred ec1 -> Pred ec2 , Pred ec2 -> Pred ec1 ) ]]
    \]
    The reader might recognize this as the Leibniz equality~\citeparens{LeibnizEq}.

    The corresponding constructor $[[ eqrefl tc ec ]]$ of type $[[ ec equal ec of tc ]]$
    stating that $[[ ec ]]$ of type $[[ tc ]]$ is equal to itself
    is then defined as follows:
    \[
      [[ eqrefl tc ec ]] \triangleq [[ \ Pred : tc -> sst. (\ p : Pred x. p , \ p : Pred x. p) ]]
    \]
\end{itemize}

It can be shown that, for each definition,
if the entities to the left of $\triangleq$ have the naturally expected types,
then the expression to the right of it is well-typed.
We prove this in our Agda code,
and we present the statements of the corresponding lemmas in \cref{appendix:core_derived_forms}.

\section{Translation}

\newcommand{\tranty}{\mu_\tau}
\newcommand{\tranterm}{\mu_\varepsilon}
\newcommand{\transub}{\mu_{<:}}

\newcommand{\Tranctx}{\mu_{\vdash\Gamma}}
\newcommand{\Tranty}{\mu_{\vdash\tau}}
\newcommand{\Tranterm}{\mu_{\vdash\varepsilon}}
\newcommand{\Transub}{\mu_{\vdash <:}}

%FIXME ugly, but whatever
\renewcommand{\ottdrulename}[1]{}

The surface language ultimately gets translated into the core language.
What really matters for practical purposes is the translation of the terms, since
terms, not types or contexts, will eventually be compiled down to some executable code.
On the other hand, it seems desirable to ensure that the terms
that are well-typed in the surface language
are accepted by the core type checker after the translation,
providing some level of guarantee that the translation ``makes sense''.

As the oracle plays a crucial role in type checking the surface language,
it is natural to expect that it will also be used during any such translation,
for instance, to produce core language proofs that VCs hold.
The only trace of the oracle's work is in the typing derivations
(namely, in the subtyping relation check and the \textsc{T-Sub} typing rule),
so we choose to do the translation not on \emph{terms},
but rather on \emph{well-typedness derivations} for the terms.
This way the oracle has a chance to enrich the original surface language term
with proofs and witnesses of whatever it decided.

Thus the ultimate goal of this section is to define a function $\Tranterm$
taking a typing derivation in the surface language
and producing a typing derivation in the core language.
As part of its duty
this function also needs to translate the types and contexts
encountered in the source derivation,
so we also define two helper functions.
$\Tranty$ takes a surface derivation of a \emph{type} well-formedness
and produces the corresponding core derivation.
$\Tranctx$ takes a surface derivation of a \emph{context} well-formedness
and produces a core language context.

We also define two helper functions, $\tranty$ and $\tranterm$,
invoking $\Tranty$ and $\Tranterm$ and extracting just the type and term component respectively.

All in all, we define $\Tranctx$, $\Tranty$ and $\Tranterm$
with ``metatypes''
\begin{align*}
  \Tranctx  & : [[ G ok ]]         \longmapsto [[ GC ]],             \\
  \Tranty   & : [[ G |- ts ]]      \longmapsto [[ GC |- tc : sst ]], \\
  \Tranterm & : [[ G |- es : ts ]] \longmapsto [[ GC |- ec : tc ]].
\end{align*}
Our helper functions $\tranty$ and $\tranterm$ are then defined to return the $\nonterm{tc}$ and $\nonterm{ec}$
from the respective right-hand sides.
The apparent asymmetry of $\Tranctx$, which does not produce a derivation as others do,
is due to our core language not having a separate notion of a context well-formedness.

Note that, due to \cref{lma:type_wf_implies_ctx_wf} we might assume that
there is a derivation of $[[ G ok ]]$ around whenever there is a derivation of $[[ G |- ts ]]$.
Indeed, the proof of \cref{lma:type_wf_implies_ctx_wf} is constructive,
so there is a function taking a witness of $[[ G |- ts ]]$ and producing $[[ G ok ]]$.
Analogously, \cref{lma:term_wf_implies_type_wf} and \cref{lma:term_wf_implies_ctx_wf}
allow us to use a derivation of $[[ G |- ts ]]$ and $[[ G ok ]]$ respectively
whenever there is a derivation of $[[ G |- es : ts ]]$.

\paragraph{Contexts}
As a warm-up,
we start with defining $\Tranctx$,
which is the simplest of the three.
It merely maps the types of the bindings in a (well-formed) context
from the surface language into the core language.

Since $\Tranctx$ is defined on the derivations of $[[ G ok ]]$,
consider the last rule used in a derivation:
\begin{itemize}
  \item \textsc{TCTX-Empty}.
    \begin{align*}
      & \ottdruleTCTXXXEmpty{} \longmapsto \emptyset.
    \end{align*}
    The base case is trivial: the empty context is mapped to the empty context.
  \item \textsc{TCTX-Bind}.
    \begin{align*}
      & \ottdruleTCTXXXBind{}
          \longmapsto
        [[ mudG ( G ok ) , x : muT ( G |- ts ) ]].
    \end{align*}

    We recurse on the prefix $[[ G ]]$,
    which is admissible due to the $[[ G ok ]]$ premise,
    and we use $\tranty$ to get the translated type of $\gterm x$,
    which is also admissible due to the other premise.
\end{itemize}

\paragraph{Types}
Next, we define $\Tranty$. In short:
\begin{itemize}
  \item (dependent) arrow types are translated to the corresponding $\Pi$-types,
  \item refined types are translated to the corresponding $\Sigma$-types,
  \item atomic refinements, being propositions about surface language terms equality,
    are translated to propositions stating the equality of translated core language terms,
  \item conjunctions of several (atomic) refinements are represented as tuples of the corresponding atomic translations.
\end{itemize}

More formally, consider the last rule used in the derivation of $[[ G |- ts ]]$:
\begin{itemize}
  \item \textsc{TWF-TrueRef}.
    \begin{align*}
      & \ottdruleTWFXXTrueRef{} \longmapsto \ottdruleTWFTargetXXTrueRef{}, \\
      \text{where}~&[[ GC = mudG(G ok) ]].
    \end{align*}

    By \cref{lma:non_dep_pair_typing}
    $[[ (BC, unitc equal unitc of Unitc) ]]$ has type $\star$ in $[[ GC ]]$
    if $[[ BC ]]$ and $[[ unitc equal unitc of Unitc ]]$ are well-typed in $[[ GC ]]$,
    which, in turn, is easily checked.
    Thus, there exists a derivation of $[[ GC |- (BC, unitc equal unitc of Unitc) : sst ]]$,
    and it is effectively constructible, although omitted for brevity.
  \item \textsc{TWF-Base}.
    \begin{align*}
      & \ottdruleTWFXXBase{} \longmapsto \ottdruleTWFTargetXXBase{}, \\
      \text{where}~&[[ GC = mudG(G ok) ]], \\
                   &[[ ec_i = muE(G, v : { v_1 : B | top } |- es_i : { v2 : B' | r_i }) ]].
                   %TODO add tc mentioned in the equal stuff
    \end{align*}

    To see that this is well-defined, first note that
    that $[[ BC ]]$ has type $\star$ by assumption on $[[ BC ]]$.
    Then, $[[ ec_1 ]]$ and $[[ ec_2 ]]$ are well-typed in the context $[[ mudG (G, v : { v_1 : B | top } ok) ]]$ according to the premises,
    and this context coincides with the one used to type check $[[ \v : BC. ec_1 equal ec_2 of tc ]]$.
    Hence both components of the dependent pair are well-typed, so by \cref{lma:dep_pair_typing} the dependent pair itself has type $\star$.

    \todo[inline]{
      The ${ v : B | \top }$ in the $\nonterm G '$ desugars to a dependent pair, yet we use $\lambda v : \hat B$ — note the naked base type.
      Figure out how to best fix this.
    }

    Just as in the previous case, the extra derivations and premises corresponding to the considerations above
    are omitted and denoted by $\cdots$.
  \item \textsc{TWF-Conj}.
    \begin{align*}
      & \ottdruleTWFXXConj{} \longmapsto \ottdruleTWFTargetXXConj{}, \\
      \text{where}~&[[ GC = mudG(G ok)]],                                         \\
                   &P_1 \text{~s.t.~} [[ Sigma BC (\ v : BC . Pred1 v) = muT ( G |- { v : B | r1 }) ]],  \\
                   &P_2 \text{~s.t.~} [[ Sigma BC (\ v : BC . Pred2 v) = muT ( G |- { v : B | r2 }) ]].
    \end{align*}

    The proof of the right-hand side being well-defined goes similarly to the cases considered previously,
    but with an extra step.
    Namely, note that the last two ``patterns'' on the left-hand side are irrefutable:
    it can be seen by direct inspection and inductive reasoning that $\tranty$ always yields a pair
    for a derivation of the form $[[ G |- { v : B | r }]]$.
    Thus we can take the predicate components $P_1, P_2$ out from the corresponding dependent pairs
    and repack them obtaining $[[ \ v : BC . (Pred1 v, Pred2 v) ]]$.
  \item \textsc{TWF-Arr}.
    \begin{align*}
      & \ottdruleTWFXXArr{} \longmapsto \ottdruleTWFTargetXXArr{}, \\
      \text{where}~&[[ GC = mudG(G ok) ]],                \\
                   &[[ tc1 = muT(G |- ts1) ]],            \\
                   &[[ tc2 = muT(G , x : ts1 |- ts2) ]].
    \end{align*}

    The rule \textsc{CT-Form} is used on the right.
    This is admissible,
    since $[[ mudT(G |- ts1) ]]$ produces a derivation of $[[ GC |- tc1 : sst ]]$,
    and similarly there is a derivation of $[[ GC , x : tc1 |- tc2 : sst ]]$
    resulting from the other invocation of $[[ mudT ]]$.
  \item \textsc{TWF-ADT}.
    \begin{align*}
      & \ottdruleTWFXXADT{} \longmapsto \ottdruleTWFTargetXXADT{}, \\
      \text{where}~&[[ GC = mudG(G ok) ]],                \\
                   &[[ tci = muT(G |- tsi) ]].
    \end{align*}

    It can be seen that the right-hand side is well-defined
    by an argument similar to ones for the previous clauses.
\end{itemize}

\paragraph{Terms}
Finally we define $\Tranterm$.
We consider the term typing rule at the root of the derivation tree for $[[ G |- es : ts ]]$.

\begin{itemize}
  \item \textsc{T-Unit}.
    \begin{align*}
      & \ottdruleTXXUnit{} \longmapsto \ottdruleCTXXUnitTerm{}, \\
      \text{where}~&\nonterm{GC} = \Tranctx(\nonterm G \ctxok).
    \end{align*}
    Any other base type $B$ is treated similarly.

  \item \textsc{T-Var}.
    \begin{align*}
      & \ottdruleTXXVar{} \longmapsto \ottdruleTTargetXXVarW{}, \\
      \text{where}~&[[ GC = mudG(G ok) ]],       \\
                   &[[ tc = muT(G |- ts) ]].
    \end{align*}

    To show that the right-hand side is well-defined,
    first note that $x : \nonterm{tc} \in \nonterm{GC}$ holds.
    Indeed, by definition of $\Tranctx$,
    if $\nonterm G$ contains a binding for the name $x$,
    then $\nonterm{GC}$ also contains a binding for that name,
    and its type is precisely $[[ muT ( G |- ts ) ]]$.
    Secondly, $[[ G |- x : ts ]]$ implies $[[ G |- ts ]]$ by \cref{lma:term_wf_implies_type_wf},
    and $[[ mudT(G |- ts) ]]$ provides a judgement of the form $[[ GC |- tc : s ]]$.

    All in all, this shows that all the premises
    necessary for the (derived) core typing rule \textsc{CT-VarW}
    hold.

  \item \textsc{T-Abs}.
    \begin{align*}
      & \ottdruleTXXAbs{} \longmapsto \ottdruleTTargetXXAbs{}, \\
      \text{where}~&[[ GC = mudG(G ok) ]],       \\
                   &[[ tc1 = muT(G |- ts1) ]], \\
                   &[[ tc2 = muT(G , x : ts1 |- ts2) ]], \\
                   &[[ ec = muE(G , x : ts1 |- es : ts2) ]].
    \end{align*}

    The right-hand side here is well-formed.
    Firstly, $[[ mudT ( G |- (x : ts1) -> ts2 ) ]]$
    produces a derivation tree of the form $[[ GC |- Pi x : tc1. tc2 : sst ]]$,
    as can be seen by inspecting the definition of $[[ mudT ]]$ for \textsc{TWF-Arr},
    which is the only rule having $[[ G |- (x : ts1) -> ts2 ]]$ in the conclusion.
    Then, $[[ mudE ( G , x : ts1 |- es : ts2 ) ]]$
    produces a derivation of $[[ GC , x : tc1 |- ec : tc2 ]]$.
    These two derivations can then be used as premises for \textsc{CT-Abs},
    which is invoked on the right-hand side.

  \item \textsc{T-App}.
    \begin{align*}
      & \ottdruleTXXApp{} \longmapsto \ottdruleTTargetXXApp{}, \\
      \text{where}~&[[ GC = mudG(G ok) ]],       \\
                   &[[ tc2 = muT(G |- ts2) ]],       \\
                   &[[ ec1 = muE(G |- es1 : (x : ts1) -> ts2) ]], \\
                   &[[ ec2 = muE(G |- es2 : ts1) ]].
    \end{align*}

    Admissibility of the right-hand side follows from a similar argument.

  \item \textsc{T-Con}.
    \begin{align*}
      & \ottdruleTXXCon{} \longmapsto \ottdruleTTargetXXCon{}, \\
      \text{where}~&[[ GC = mudG(G ok) ]],       \\
                   &[[ tci = muT(G |- tsi) ]], \\
                   &[[ ec = muE(G |- es : tsj) ]].
    \end{align*}

    Well-formedness of the right-hand side can be shown analogously to the previous clauses.
    One extra thing to note is that,
    although $[[ G |- tsi ]]$ are not present directly in the premises of \textsc{T-Con},
    they are implied by the $[[ G |- < </ li : tsi // i /> > ]]$ premise and thus can be used.

  \item \textsc{T-Case}.
    \begin{align*}
      & \ottdruleTXXCase{} \\
      \longmapsto \quad & \ottdruleTTargetXXCase{}, \\
      \text{where}~&[[ GC = mudG(G ok) ]],       \\
                   &[[ tc' = muT(G |- ts') ]],       \\
                   &[[ ec = muE(G |- es : ts) ]],    \\
                   &[[ eci = muE(G |- esi : ts) ]],  \\
                   &[[ tci' ]] = [[ Sigma Unitc (\ _ : Unitc. ec equal ( < li = xi > as tc ) of tc) ]].
    \end{align*}

    This part of the translation is perhaps one of the most involved,
    and the main complication stems from the following.
    In \textsc{T-Case}, each (surface) $[[esi]]$ is being type checked in the context
    where $x$ (the witness of the $\mathbf{case}$ branch taken)
    has type $[[ { _ : Unit | es = (< li = xi > as ts) of ts } ]]$.
    After $[[esi]]$ gets translated into the (core) term $[[eci]]$,
    the latter is type checked in the context where $\hat x$
    has the dependent pair type $[[ Sigma Unitc (\_ : Unitc. ec equal ( < li = xi > as tc ) of tc) ]]$.
    On the other hand, the $\mathbf{proof} \pi_i$ part of the $\mathbf{case}$ branch
    provides the proof $\pi_i$ typed as $[[ ec equal ( < li = xi > as tc ) of tc ]]$,
    so it needs to be packed into the dependent pair type that $[[eci]]$ ``expects''.

    The lambda abstraction/application pair on the right-hand side of the translation
    is responsible for this extra packing.
    All the typing derivations showing that this is well-formed follow trivially
    from the typing rules, but are again omitted and replaced by $\dots$ for the sake of brevity.

  \item \textsc{T-Sub}.
    This is the only part of the translation that uses the oracle,
    and hence cannot be done as straightforwardly as the other ones.

    Our goal is to translate a typing derivation ending with \textsc{T-Sub}:
    \[
      \ottdruleTXXSub{}.
    \]

    Note that, for languages with non-trivial subtyping, uniqueness of typing does not hold,
    but it holds for the CoC modulo $\beta$-conversion
    (which is an equivalence relation unlike any non-trivial subtyping relation).
    Thus, intuitively,
    there is no general way to prescribe both the translation of $[[ ts ]]$ and $[[ ts' ]]$
    to the translation of $[[ es ]]$ simultaneously.
    Instead, we produce another term that carries along the witness of the subtyping relation.

    \todo[inline]{Should we give the intuition for producing a new term
      based on the uniqueness of typing-like considerations or
      based on VC proof witness stuff?}

    We now define yet another translation function, $\Transub$,
    mapping the derivations of $[[ G |- ts <: ts' ]]$
    into core language terms $[[gamma]]$ of type $[[ muT(G |- ts) -> muT(G |- ts') ]]$
    along with derivations of their well-typedness.
    Informally, forgetting about the distinction between surface and core types,
    a subtyping derivation is turned into a function $[[gamma]]$
    transforming any term of the subtype into a term of the supertype.

    The helper function $\transub$ is defined similarly to other helpers,
    forgetting about the derivation and yielding just the final term.

    So, consider the last (subtyping) rule in the derivation of $[[ G |- ts <: ts' ]]$:
    \begin{itemize}
      \item \textsc{ST-Base}.
        In this case $[[ts]]$ and $[[ts']]$ are
        $[[ { v : B | r1 } ]]$ and $[[ { v : B | r2 } ]]$
        respectively for some $[[B]]$, $[[r1]]$ and $[[r2]]$.
        What is needed is a function of type
        $[[ muT(G |- { v : B | r1 }) -> muT(G |- { v : B | r1 }) ]]$.

        \begin{align*}
          & \ottdruleSTXXBase{} \longmapsto \ottdruleSTTargetXXBase{}, \\
          \text{where}~&[[ GC = mudG(G ok) ]],       \\
                       &[[ tc1 ]] \text{~s.t.~} [[ (Sigma BC tc1) = muT ( G |- { v : B | r1 }) ]],  \\
                       &[[ tc2 ]] \text{~s.t.~} [[ (Sigma BC tc2) = muT ( G |- { v : B | r2 }) ]],  \\
                       &[[ ec = muE(G |- es : ts) ]].
        \end{align*}

        This is the base case for the subtyping relation,
        and this is the only case where the oracle is involved,
        so we have no choice but require the oracle to produce a core language term $\sigma$ such that
        $[[ GC |- sigma : Pi v : BC . tc1 -> tc2 ]]$,
        where $[[ GC = mudG(G ok) ]]$, and $[[tc1]]$, $[[tc2]]$ correspond to the translations
        of the refinement terms $[[r1]]$, $[[r2]]$ respectively.

        Intuitively (or, perhaps, Curry-Howard-ly),
        this $[[ sigma ]]$ witnesses the implication of the refinements $[[ A v. r1 => r2 ]]$,
        which is isomorphic to the function type $[[ Pi v : BC. tc1 -> tc2 ]]$.

        Then, this $[[ sigma ]]$ can be combined with a function $[[ seconddp ]]$
        (which maps over the second component of a dependent pair, and whose definition is omitted here for brevity),
        producing a function mapping $[[ Sigma BC tc1 ]]$ onto $[[ Sigma BC tc2 ]]$~---
        precisely what is needed in case of \textsc{ST-Base}.

      \item \textsc{ST-Arr}.
        \begin{align*}
          & \ottdruleSTXXArr{} \\
          \longmapsto \quad & \ottdruleSTTargetXXArr{}, \\
          \text{where}~&[[ GC = mudG(G ok) ]],       \\
                       &[[ gamma1 = muS(G |- ts1' <: ts1) ]],  \\
                       &[[ gamma2 = muS(G , x : ts1' |- ts2 <: ts2') ]],  \\
                       &[[ ec = muE(G |- es : ts) ]].
        \end{align*}

        Intuitively, there is a function of type $[[ (x : ts1) -> ts2 ]]$,
        and we need to produce a function of type $[[ (x : ts1') -> ts2' ]]$
        given $[[ G |- ts1' <: ts1 ]]$ and $[[ G , x : ts1' |- ts2 <: ts2' ]]$.
        Then, the first premise is used (via $[[gamma1]]$) to turn $[[x]]$ of type $[[ts1']]$
        into a value of type $[[ts1]]$ that the existing function can consume,
        producing a result of type $[[ ts2 ]]$,
        which is then similarly turned (by $[[gamma2]]$) into a value of type $[[ ts2' ]]$.

        This intuition is then formalized analogously to the previous clause.
    \end{itemize}

    With $\Transub$ defined, translation of the \textsc{T-Sub} rule is straightforward:
    \begin{align*}
      & \ottdruleTXXSub{} \longmapsto \ottdruleTTargetXXSub{}, \\
      \text{where}~&[[ GC = mudG(G ok) ]],       \\
                   &[[ ec = muE(G |- es : ts) ]], \\
                   &[[ gamma = muS(G |- ts <: ts') ]].
    \end{align*}
\end{itemize}

Having defined these functions, we formulate a simple but useful lemma:
\begin{lemma}[Translation totality]
  $\Tranctx$, $\Tranty$ and $\Tranterm$ are total.
\end{lemma}
\begin{proof}
  Firstly, each function is defined for all possible inputs.
  Then, each function recurses on structurally smaller inputs,
  and, since derivation trees are finite,
  this implies each function terminates for any input.

  The Agda implementations of these functions represent the formal proof of this statement.
\end{proof}

\subsection{Correctness}

The correctness of the translation hinges on two key theorems.
The first one claims that a well-typed program in surface language remains well-typed after the translation to the core language.

\begin{theorem}[Well-typedness preservation]\label{thm:tran_preservation}
  For any well-typed surface language term $[[ es ]]$,
  the result of the translation via $[[ muE ]]$ is typeable in the core language.
\end{theorem}
\begin{proof}
  This follows directly from the definition of $\tranterm$ via $\Tranterm$,
  the latter being total and mapping onto typing derivations in the core language.
\end{proof}

The second one claims that a well-typed surface language term evaluates to ``the same'' value as the translated one.
In other words, the translation and evaluation relations commute.

\begin{theorem}[Evaluation equivalence]
  If $[[ es ]]$ is a well-typed closed surface language term (thus $[[ empty |- es : ts ]]$) and $[[ es ~~> es' ]]$,
  then $[[ es' ]]$ also has a (well-typed) translation $[[ ec' ]]$ to the core language,
  and the translation of $[[ es ]]$ evaluates to $[[ ec' ]]$ (perhaps, in several steps).
\end{theorem}
\begin{proof}
  The existence of $[[ ec' ]]$ follows from the preservation \cref{thm:surface_preservation} for the surface language and well-typedness preservation \cref{thm:tran_preservation}.
  The rest is proven with induction on the derivation of $[[ empty |- es : ts ]]$ and $[[ es ~~> es']]$.
\end{proof}

\section{Formal proof overview}

Our formalization of the above languages is heavily inspired by~\citeinline{plfa} and~\citeinline{SystemFAgda}.

In this section we briefly outline key design decisions of our formal proof.
We use the word ``\emph{metatype}'' when discussing the (Agda) types representing the various entities in our surface and core languages.

\subsection{Formalizing surface language}

Since our surface language has a limited form of dependent typing (namely, types contain refinements, which, in turn, contain terms), typing contexts become ``non-flat''.
This is the primary factor driving the decisions behind the design of our formalization.

\paragraph{Variables} The first decision to be made is about representing variables introduced by binders (both at term level and type level).
There are multiple existing approaches, including using plain strings akin to informal human reasoning about lambda terms, or de Bruijn indices~\citeparens{FindSomethingForDeBruijn}, or locally nameless representation~\citeparens{LocallyNameless}.
In our work we choose to use de Bruijn indices, for the following reasons:
\begin{itemize}
  \item Compared to string-based approaches, there is no problem of variable shadowing.
  \item Again, compared to string-based approaches, the types of the variables (which are essentially \mintinline{agda}{Fin ℓ} for some appropriate bound \mintinline{agda}{ℓ})
    guide the development of the theorems and the proofs about the language.
  \item Compared to locally nameless representation, this is largely a matter of preference.
    We estimate the amount of work required for both LN representation and just the de Bruijn indices to be roughly equivalent, so we choose the latter.
\end{itemize}

\paragraph{Syntax} There are also several approaches to representing syntax, ranging from separate metatypes for raw terms and metatypes for typing judgements~\citeparens{FindSomethingForExtrinsicallyTyped},
to intrinsically-typed representations, where the term metatype is indexed by the metatype representing its type,
the type metatype is indexed by the metatype representing its kind, and so on for other syntactic categories~\citeparens{FindSomethingForIntrinsicallyTyped}.
Intrinsically-typed representations effectively combine syntax and typing rules, and only well-typed terms are representable.

Intrinsically-typed approach typically~\citeparens{plfa} results in much shorter metatheoretical proofs, but it becomes non-trivial for languages where types may depend on terms.
Hence we choose to use a hybrid approach, using an intrinsically well-scoped presentation~\citeparens{FindSomethingForWellScoped} with separate typing judgements.
Here, all the metatypes for language variables (\mintinline{agda}{Fin}), terms (\mintinline{agda}{STerm}), types (\mintinline{agda}{SType}) and refinements (\mintinline{agda}{Refinement})
are indexed by the \emph{length} of the typing context in which they reside.
In fact, the bound \mintinline{agda}{ℓ} in the type \mintinline{agda}{Fin ℓ} for variables mentioned above is precisely the length of the context to which the variable belongs.

It is worth noting that such light-weight (meta-)verification as having context length at type level (especially compared to intrinsically-typed representations)
is able to rule out a surprising share of incorrect (meta-)theorems before even trying to prove them.
Moreover, it also turns out to be of helpful guidance in the development of the proofs.

\paragraph{Renamings and substitutions} The formalization of substitution (and, subsequently, operational semantics and related theorems) relies on several concepts.

First, let's introduce the notion of \emph{actions}.
Note that any function \mintinline{agda}{f : Fin ℓ → Target ℓ'} from variables to some target type \mintinline{agda}{Target} (also indexed by the context length),
combined with a function \mintinline{agda}{var-action : Target ℓ → STerm ℓ},
gives rise to a family of \emph{actions} on terms, types and refinements, where the action on terms has the type \mintinline{agda}{STerm ℓ → STerm ℓ'}, and similarly for others.

Having defined that, any function \mintinline{agda}{ρ : Fin ℓ → Fin ℓ'} mapping variables from a context of length $\ell$ to a context of length $\ell'$
along with \mintinline{agda}{var-action idx = SVar idx} (where \mintinline{agda}{SVar} is the constructor of \mintinline{agda}{STerm} denoting variables),
gives rise to a family of \emph{renaming actions}, mapping terms (or types, or refinements) from a context of length $\ell$ to a context of length $\ell'$.
Renamings are used, for example, to define weakening: indeed, taking \mintinline{agda}{ρ} to be \mintinline{agda}{suc} gives the desired result.

(Simultaneous) substitutions are defined analogously, considering any function \mintinline{agda}{σ : Fin ℓ → STerm ℓ'}.
Single substitutions are then defined via a function
\begin{minted}{agda}
replace-at : (ι : Fin (suc ℓ)) → (ε : STerm ℓ) → (var : Fin (suc ℓ)) → STerm ℓ
\end{minted}
which takes an index \mintinline{agda}{ι} and a term \mintinline{agda}{ε} and substitutes \mintinline{agda}{var} for \mintinline{agda}{ε}
if \mintinline{agda}{var} is equal to \mintinline{agda}{ι}, or adjusting \mintinline{agda}{var} otherwise.
Note that the type of \mintinline{agda}{replace-at} implies that the variable being substituted vanishes from the context after substitution.

\subsection{Formalizing core language}

\section{Future work}

As we mentioned in the overview, our surface language lacks two components critical for any practically useful language:
namely, polymorphism and recursion.
Extending our language with polymorphism is straightforward, while adding general recursion is non-trivial,
since it needs to be translated to some dependently typed language, and those are typically strongly normalizing.
Investigating this is an interesting and useful direction for future work,
and one might think of the following approaches (or a combination thereof):
\begin{itemize}
  \item Require the oracle to produce a proof of termination of each recursive function.
    The oracle then can use approaches analogous to the termination checkers~\citeparens{abel1998foetus} in Idris or Agda,
    or the heuristics outlined in the works on Liquid Haskell~\citeparens{Vazou16}, or any other algorithm.
  \item Mark the recursive functions as non-terminating, propagate this property to the callers,
    and treat non-terminating functions as uninterpreted during type checking.
    It is worth noting that, in particular,
    Idris allows functions that are not provably terminating and treats them in a similar way~\citeparens{Idris13}.

    Indeed, there are two reasons why termination is so desirable for a dependently typed language:
    \begin{itemize}
      \item Termination ensures decidability of type checking, which relies on $\beta$-equivalence of terms.
        By treating functions that are not provably terminating as not having any reduction behaviour \emph{during type checking},
        we ensure type checking remains decidable, even if at a cost of rejecting some programs that otherwise would be well-typed.
        Moreover, we deem this cost insignificant for the intended uses of languages with refinement typing.
      \item Termination is crucial to the soundness of the logic that the language expresses.
        Propagating the property of ``being non-terminating'' to the callers ensures that
        $\bot$ can only be proven in contexts that are explicitly marked (by the type checker or the programmer) as non-total,
        and hence the programmer knows they have not really proven anything.
        But this is already the existing state of affairs: it is surely possible to have a term of type $\bot$, say, in Idris or Agda;
        it is just the termination checker that needs to be disabled for such a term.
    \end{itemize}
\end{itemize}

Another, practical direction for future work lies in reflecting the entities from the dependently typed language into the oracle world.
For example, suppose the programmer has defined their own \verb+Nat+ type, among with the operations on it and proofs of their properties.
What would it take to teach the oracle that type, its semantics and its operations?
Investigating how to do this in a sound and feasible way seems important to make any language combining refinement types and dependent types practically useful.

\section{Conclusions}

\bibliographystyle{jfplike}
\bibliography{biblio}

\begin{appendices}

\section{Properties of the surface language.}\label{appendix:surface_props}

\begin{lemma}[Agreement I, \prooftermname{T-implies-TCTX}]\label{lma:term_wf_implies_ctx_wf}
  If $[[ G |- es : ts ]]$, then $[[ G ok ]]$.
\end{lemma}
\begin{proof}
  Straightforward induction on the derivation of $[[ G |- es : ts ]]$.
  \textsc{T-Unit} and \textsc{T-Var} carry the witness explicitly,
  and the other rules recurse on one of their premises.
\end{proof}

\begin{lemma}[Agreement II, \prooftermname{TWF-implies-TCTX}]\label{lma:type_wf_implies_ctx_wf}
  If $[[ G |- ts ]]$, then $[[G ok]]$.
\end{lemma}
\begin{proof}
  Straightforward induction on the derivation of $[[ G |- ts ]]$.
  \textsc{TWF-TrueRef} carries the witness explicitly,
  the case for \textsc{TWF-Base} uses \cref{lma:term_wf_implies_ctx_wf} on either of its premises,
  and the other rules recurse on one of their premises.
\end{proof}

\begin{lemma}[Subtyping relation thinning, \prooftermname{st-thinning}]\label{lma:thinning_st}
  Let $[[ G ]]$, $[[ G' ]]$ be contexts such that $[[ G ]] \subset [[ G' ]]$.
  Then, $[[ G |- ts1 <: ts2 ]]$ implies $[[ G' |- ts1 <: ts2 ]]$.
\end{lemma}
\begin{proof}
  Straightforward induction on the derivation of $[[ G |- ts1 <: ts2 ]]$.
  The \textsc{ST-Base} case depends the oracle thinning property~\ref{orprop:thinning}.
\end{proof}

\begin{lemma}[Thinning]\label{lma:thinning}
  Let $[[ G ]]$, $[[ G' ]]$ be contexts such that $[[ G ]] \subset [[ G' ]]$ and $[[ G' ok ]]$.
  Given that:
  \begin{itemize}
    \item if $[[ G |- ts ]]$, then $[[ G' |- ts ]]$ (\prooftermname{twf-thinning}),
    \item if $[[ G |- es : ts ]]$, then $[[ G' |- es : ts ]]$ (\prooftermname{t-thinning}).
  \end{itemize}
\end{lemma}
\begin{proof}
  Mutual induction on the derivations of type well-formedness and term well-typedness.
  Since each clause uses the other one (and, of course, itself) only on smaller derivation trees,
  this is a well-founded proof.

  In particular, the need for mutual induction appears in the following cases:
  \begin{itemize}
    \item \textsc{TWF-Base}. Unlike other type well-formedness rules,
      its premises contain judgements about certain terms being well-typed, so this case uses thinning on types.
    \item \textsc{T-Abs}, \textsc{T-Case}, \textsc{T-Con}.
      These rules require certain judgements about type well-formedness to hold, so these cases use thinning on terms.
  \end{itemize}

  In addition to that, the \textsc{T-Sub} rule relies on the subtyping relation thinning \cref{lma:thinning_st}.
\end{proof}

\begin{lemma}[Substitution, \prooftermname{typing-substitution}]\label{lma:typing_substitution}
  Assume $[[ G |- es : ts ]]$. Given that:
  \begin{itemize}
    \item if $[[ G, x : ts, GD |- ts' ]]$, then $[[ G, [ x |-> es ] GD |- [ x |-> es ] ts' ]] $,
    \item if $[[ G, x : ts, GD |- es' : ts' ]]$, then $[[ G, [ x |-> es ] GD |- [ x |-> es ] es' : [ x |-> es ] ts' ]] $.
  \end{itemize}
\end{lemma}
\begin{proof}
  Due to the presence of a subset of dependent types the proof is a bit bulky,
  using simultaneous induction on $\Delta$ and the derivation of $[[ G, x : ts, GD |- ts' ]]$.
  We refer the interested reader to the formal proof of theorem in the supplemental code for the specific details.
\end{proof}

\begin{lemma}[Agreement III, \prooftermname{T-implies-TWF}]\label{lma:term_wf_implies_type_wf}
  If $[[ G |- es : ts ]]$, then $[[ G |- ts ]]$.
\end{lemma}
\begin{proof}
  Straightforward induction on the derivation of $[[ G |- es : ts ]]$.
  The interesting case is \textsc{T-App}, as it invokes the substitution \cref{lma:typing_substitution}.
\end{proof}

\begin{lemma}[Subtyping narrowing, \prooftermname{<:-narrowing}]\label{lma:st_narrowing}
  If $[[ G |- ts' <: ts ]]$ and $[[ G, x : ts, GD |- ts1 <: ts2 ]]$, then $[[ G, x : ts', GD |- ts1 <: ts2 ]]$.
\end{lemma}
\begin{proof}
  Straightforward induction on the derivation of $[[ G, x : ts, GD |- ts1 <: ts2 ]]$.
  The \textsc{SC-Base} case relies on the oracle narrowing property~\ref{orprop:narrowing}.
\end{proof}

\begin{lemma}[Subtyping transitivity, \prooftermname{<:-trans}]\label{lma:st_transitivity}
  If $[[ G |- ts1 <: ts2 ]]$ and $[[ G |- ts2 <: ts3 ]]$, then $[[ G |- ts1 <: ts3 ]]$.
\end{lemma}
\begin{proof}
  Simultaneous induction on both subtyping derivations, noting that they must have the same ``shape''~--- if one is \textsc{ST-Base}, then so is the other, since the $[[ ts2 ]]$ type is ``shared'' between the two.
  In particular, if both are \textsc{ST-Base}, then the oracle transitivity property~\ref{orprop:trans} is used.
  The \textsc{SC-Arr} case uses the subtyping narrowing \cref{lma:st_narrowing}.
\end{proof}

\begin{lemma}[Narrowing, \prooftermname{typing-narrowing}]\label{lma:narrowing}
  Assume that $[[ G |- ts1' <: ts1 ]]$ and $[[ G |- ts1' ]]$. Then:
  \begin{itemize}
    \item If $[[ G , x : ts1, GD ok ]]$, then $[[ G , x : ts1', GD ok ]]$.
    \item If $[[ G , x : ts1, GD |- ts ]]$, then $[[ G , x : ts1', GD |- ts ]]$.
    \item If $[[ G , x : ts1, GD |- es : ts ]]$, then $[[ G , x : ts1', GD |- es : ts ]]$.
  \end{itemize}
\end{lemma}
\begin{proof}
  Mutual induction on the derivations, using the subtyping narrowing \cref{lma:st_narrowing} in the \textsc{T-Sub} case.
\end{proof}

\begin{lemma}[Context equivalence, \prooftermname{typing-equivalence}]\label{lma:ctx_equivalence}
  Assume that $[[ ts1 requiv ts1' ]]$ and $[[ G |- ts1' ]]$. Then:
  \begin{itemize}
    \item If $[[ G , x : ts1, GD ok ]]$, then $[[ G , x : ts1', GD ok ]]$.
    \item If $[[ G , x : ts1, GD |- ts ]]$, then $[[ G , x : ts1', GD |- ts ]]$.
    \item If $[[ G , x : ts1, GD |- es : ts ]]$, then $[[ G , x : ts1', GD |- es : ts ]]$.
  \end{itemize}
\end{lemma}
\begin{proof}
  Mutual induction on the derivations.

  In the third bullet, the case of $[[ es ]]$ being the variable $[[ x ]]$ uses (and motivates the existence of) the \textsc{RTEquiv-Backward} rule.
  Indeed, if $[[ G , x : ts1, GD |- x : ts1 ]]$, then $[[ G , x : ts1', GD |- x : ts1' ]]$ according to \textsc{T-Var},
  and going back from $[[ ts1' ]]$ to $[[ ts1 ]]$ is only possible if $[[ requiv ]]$ is a symmetric relation.
  \textsc{RTEquiv-Backward} symmetrizes the \textsc{RTEquiv-Forward} rule, which is needed for the preservation \cref{thm:surface_preservation}.
\end{proof}

\begin{lemma}[Canonical forms, \prooftermname{canonical}]\label{lma:canonical_forms}
  Let $[[ empty |- es : ts ]]$ and $[[ es ]]$ be a value. In this case:
  \begin{itemize}
    \item if $[[ ts ]]$ is of the form $[[ (x : ts1) -> ts2 ]]$, then $[[ es ]]$ is of the form $[[ \ x : ts . es' ]]$,
    \item if $[[ ts ]]$ is of the form $[[ < </ li : tsi // i /> > ]]$, then $[[ es ]]$ is of the form $[[ < l = es' > as < </ li : tsi' // i /> > ]]$.
  \end{itemize}
\end{lemma}
\begin{proof}
  Straightforward induction on the derivation of $[[ empty |- es : ts ]]$, noting that some cases are ruled out by the requirement that $[[ es ]]$ is a value.
\end{proof}

\begin{lemma}[Lambda inversion, \prooftermname{SLam-inv}]\label{lma:lambda_inversion}
  If $[[ G |- \ x : ts. es : (x : ts1) -> ts2 ]]$, then $[[ G, x : ts1 |- es : ts2 ]]$.
\end{lemma}
\begin{proof}
  Induction on $[[ G |- \ x : ts. es : (x : ts1) -> ts2 ]]$.
  The following cases are possible:
  \begin{itemize}
    \item \textsc{T-Abs}: immediate.
    \item \textsc{T-Sub}: follows from applying lambda inversion to the corresponding premise of \textsc{T-Sub} and using the narrowing \cref{lma:narrowing}.
    \item \textsc{T-RConv}: follows from applying lambda inversion to the corresponding premise of \textsc{T-RConv} and using context equivalence \cref{lma:ctx_equivalence}.
  \end{itemize}
\end{proof}

\begin{theorem}[Progress, \prooftermname{progress}]\label{thm:surface_progress}
  If $[[ empty |- es : ts ]]$, then either $[[ es ]]$ is a value, or there exists $[[ es' ]]$ such that $[[ es ~~> es' ]]$.
\end{theorem}
\begin{proof}
  Straightforward induction on the derivation of $[[ empty |- es : ts ]]$.
  The canonical forms lemma~\ref{lma:canonical_forms} is used in \textsc{T-App} case if both terms are values and in \textsc{T-Case} case if the scrutinee is a value.
\end{proof}

\begin{theorem}[Preservation, \prooftermname{preservation}]\label{thm:surface_preservation}
  If $[[ G |- es : ts ]]$, and $[[ es ~~> es' ]]$, then $[[ G |- es' : ts ]]$.
\end{theorem}
\begin{proof}
  Simultaneous induction on the derivations of $[[ G |- es : ts ]]$ and $[[ es ~~> es' ]]$.
  The non-trivial cases are the ones related to the eliminators:
  \begin{itemize}
    \item \textsc{E-AppR} and \textsc{T-App}.
      Then, $[[ es ]]$ is $[[ vs1 es2 ]]$, $[[ es' ]]$ is $[[ vs1 es2' ]]$, and $[[ es2 ~~> es2' ]]$, for some $[[ vs1 ]], [[ es2 ]], [[ es2' ]]$.
      Moreover, well-typedness implies that $[[ G |- vs1 : (x : ts1) -> ts2 ]]$ and $[[ G |- es2 : ts1 ]]$.
      Then, \textsc{T-App} concludes that $[[ G |- vs1 es2 : [ x |-> es2 ] ts2 ]]$.
      Inductive hypothesis claims that $[[ G |- es2' : ts1 ]]$, and then it is easy to see that $[[ G |- vs1 es2' : [ x |-> es2' ] ts2 ]]$.
      But, the original type is $[[ [ x |-> es2 ] ts2 ]]$, so, for the preservation to hold, there needs to be a rule allowing converting $[[ [ x |-> es2' ] ts2 ]]$ to $[[ [ x |-> es2 ] ts2 ]]$,
      and this is what justifies the existence of the \textsc{T-RConv} rule along with the form of the \textsc{RTEquiv-Forward} rule.

      The substitution \cref{lma:typing_substitution} is used to ensure the new type is well-formed, as required by \textsc{T-RConv}.
    \item \textsc{E-AppAbs} and \textsc{T-App}.
      In this case $[[ es ]]$ is $[[ (\ x : ts. es1) vs2 ]]$, and well-typedness implies that $[[ G |- \ x : ts. es1 : (x : ts1) -> ts2 ]]$ and $[[ G |- vs2 : ts1 ]]$.
      What needs to be shown is that $[[ G |- [ x |-> vs2 ] es1 : [ x |-> vs2 ] ts2 ]]$.
      For this, the lambda inversion \cref{lma:lambda_inversion} is used to derive that $[[ G, x : ts1 |- es1 : ts2 ]]$, and the result follows by the substitution \cref{lma:typing_substitution}.
    \item \textsc{E-CaseMatch} and \textsc{T-Case}.
      Similarly to the previous cases, using substitution \cref{lma:typing_substitution} to show that $[[ [xj |-> vs] esj ]]$ has the expected type
      after substituting the pattern match variable $[[ xj ]]$ in the branch term $[[ esj ]]$ for the scrutinee value $[[ vs ]]$.
  \end{itemize}
\end{proof}

\section{Derived forms typing}\label{appendix:core_derived_forms}

Below is the list of lemmas stating that
our core language derived forms (\cref{sect:derived_forms})
are well-typed given the respective assumptions.
We also verify these lemmas mechanically in our Agda code,
particularly in \verb+Core/Syntax/Derived/Typing.agda+.

\begin{lemma}[\textsc{CT-VarW}]
  If $[[ GC |- ec : s ]]$ and $[[ x : ec in GC ]]$, then $[[ GC |- x : ec ]]$.
\end{lemma}

\begin{lemma}[Non-dependent functions]
  If $[[ GC |- tc1 : s1 ]]$ and $[[ GC |- tc2 : s2 ]]$, then $[[ GC |- tc1 -> tc2 : s2 ]]$.
\end{lemma}

\begin{lemma}[Dependent pair type]
  If $[[ GC |- tc : s ]]$ and $[[ GC |- Pred : tc -> sst ]]$, then $[[ GC |- Sigma tc Pred : sst ]]$.
\end{lemma}

\begin{lemma}[Dependent pair constructor]
  If
  \begin{itemize}
    \item $[[ GC |- tc : s ]]$,
    \item $[[ GC |- Pred : tc -> sst ]]$,
    \item $[[ GC |- ec : tc ]]$,
    \item $[[ GC |- pi : Pred ec ]]$,
  \end{itemize}
  then $[[ GC |- Sigma tc Pred : sst ]]$.
\end{lemma}

\begin{lemma}[Non-dependent pair type]
  If $[[ GC |- tc1 : sst ]]$ and $[[ GC |- tc2 : sst ]]$, then $[[ GC |- (tc1, tc2) : sst ]]$.
\end{lemma}

\begin{lemma}[Non-dependent pair constructor]
  If
  \begin{itemize}
    \item $[[ GC |- tc1 : sst ]]$,
    \item $[[ GC |- tc2 : sst ]]$,
    \item $[[ GC |- ec1 : tc1 ]]$,
    \item $[[ GC |- ec2 : tc2 ]]$,
  \end{itemize}
  then $[[ GC |- (ec1 : tc1, ec2 : tc2) : sst ]]$.
\end{lemma}

\begin{lemma}[Equality type]
  If
  \begin{itemize}
    \item $[[ GC |- tc : sst ]]$,
    \item $[[ GC |- ec1 : tc ]]$,
    \item $[[ GC |- ec2 : tc ]]$,
  \end{itemize}
  then $[[ GC |- ec1 equal ec2 of tc : sst ]]$.
\end{lemma}

\begin{lemma}[Equality constructor]
  If $[[ GC |- tc : sst ]]$ and $[[ GC |- ec : tc ]]$, then $[[ GC |- eqrefl tc ec : ec equal ec of tc ]]$.
\end{lemma}

\end{appendices}

\end{document}