michael/csci8980-f21
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions
csci8980-f21/versions/19.08/Adequacy/index.html

858 lines
232 KiB
HTML
Raw Permalink Blame History

This file contains ambiguous Unicode characters

This file contains Unicode characters that might be confused with other characters. If you think that this is intentional, you can safely ignore this warning. Use the Escape button to reveal them.

<!DOCTYPE html>
<html lang="en"><head>
<meta charset="utf-8">
<meta http-equiv="X-UA-Compatible" content="IE=edge">
<meta name="viewport" content="width=device-width, initial-scale=1">
<title>Adequacy: Adequacy of denotational semantics with respect to operational semantics 🚧 | Programming Language Foundations in Agda
</title><!-- Begin Jekyll SEO tag v2.6.1 -->
<meta name="generator" content="Jekyll v3.9.0" />
<meta property="og:title" content="Adequacy: Adequacy of denotational semantics with respect to operational semantics 🚧" />
<meta property="og:locale" content="en_US" />
<meta name="description" content="Programming Language Foundations in Agda" />
<meta property="og:description" content="Programming Language Foundations in Agda" />
<link rel="canonical" href="https://plfa.github.io/19.08/Adequacy/" />
<meta property="og:url" content="https://plfa.github.io/19.08/Adequacy/" />
<meta property="og:site_name" content="Programming Language Foundations in Agda" />
<script type="application/ld+json">
{"url":"https://plfa.github.io/19.08/Adequacy/","headline":"Adequacy: Adequacy of denotational semantics with respect to operational semantics 🚧","description":"Programming Language Foundations in Agda","@type":"WebPage","@context":"https://schema.org"}</script>
<!-- End Jekyll SEO tag -->
<link rel="stylesheet" href="/19.08/assets/main.css"></head>
<body><header class="site-header" role="banner">
<div class="wrapper">
<a class="site-title" href="/19.08/">Programming Language Foundations in Agda
</a>
<nav class="site-nav">
<span class="menu-icon">
<svg viewBox="0 0 18 15" width="18px" height="15px">
<path fill="#424242" d="M18,1.484c0,0.82-0.665,1.484-1.484,1.484H1.484C0.665,2.969,0,2.304,0,1.484l0,0C0,0.665,0.665,0,1.484,0 h15.031C17.335,0,18,0.665,18,1.484L18,1.484z"/>
<path fill="#424242" d="M18,7.516C18,8.335,17.335,9,16.516,9H1.484C0.665,9,0,8.335,0,7.516l0,0c0-0.82,0.665-1.484,1.484-1.484 h15.031C17.335,6.031,18,6.696,18,7.516L18,7.516z"/>
<path fill="#424242" d="M18,13.516C18,14.335,17.335,15,16.516,15H1.484C0.665,15,0,14.335,0,13.516l0,0 c0-0.82,0.665-1.484,1.484-1.484h15.031C17.335,12.031,18,12.696,18,13.516L18,13.516z"/>
</svg>
</span>
<div class="trigger">
<a class="page-link" href="/19.08/">The Book</a>
<a class="page-link" href="/19.08/Announcements/">Announcements</a>
<a class="page-link" href="/19.08/GettingStarted/">Getting Started</a>
<a class="page-link" href="/19.08/Citing/">Citing</a>
<a class="page-link" href="https://agda-zh.github.io/PLFA-zh/">中文</a>
</div>
</nav>
</div>
</header>
<main class="page-content" aria-label="Content">
<div class="wrapper">
<article class="post">
<header class="post-header">
<h1 class="post-title">Adequacy: Adequacy of denotational semantics with respect to operational semantics 🚧</h1>
</header>
<p style="text-align:center;">
<a alt="Previous chapter" href="/19.08/Soundness/">Prev</a>
&bullet;
<a alt="Source code" href="https://github.com/plfa/plfa.github.io/blob/dev-19.08/src/plfa/part3/Adequacy.lagda.md">Source</a>
&bullet;
<a alt="Next chapter" href="/19.08/ContextualEquivalence/">Next</a>
</p>
<div class="post-content">
<pre class="Agda"><a id="213" class="Keyword">module</a> <a id="220" href="/19.08/Adequacy/" class="Module">plfa.part3.Adequacy</a> <a id="240" class="Keyword">where</a>
</pre>
<h2 id="introduction">Introduction</h2>
<p>Having proved a preservation property in the last chapter, a natural
next step would be to prove progress. That is, to prove a property
of the form</p>
<div class="language-plaintext highlighter-rouge"><div class="highlight"><pre class="highlight"><code>If γ ⊢ M ↓ v, then either M is a lambda abstraction or M —→ N for some N.
</code></pre></div></div>
<p>Such a property would tell us that having a denotation implies either
reduction to normal form or divergence. This is indeed true, but we
can prove a much stronger property! In fact, having a denotation that
is a function value (not <code class="language-plaintext highlighter-rouge">⊥</code>) implies reduction to a lambda
abstraction (no divergence).</p>
<p>This stronger property, reformulated a bit, is known as <em>adequacy</em>.
That is, if a term <code class="language-plaintext highlighter-rouge">M</code> is denotationally equal to a lambda abstraction,
then <code class="language-plaintext highlighter-rouge">M</code> reduces to a lambda abstraction.</p>
<div class="language-plaintext highlighter-rouge"><div class="highlight"><pre class="highlight"><code>ℰ M ≃ ℰ (ƛ N) implies M —↠ ƛ N' for some N'
</code></pre></div></div>
<p>Recall that <code class="language-plaintext highlighter-rouge">ℰ M ≃ ℰ (ƛ N)</code> is equivalent to saying that
<code class="language-plaintext highlighter-rouge">γ ⊢ M ↓ (v ↦ w)</code> for some <code class="language-plaintext highlighter-rouge">v</code> and <code class="language-plaintext highlighter-rouge">w</code>. We will show that
<code class="language-plaintext highlighter-rouge">γ ⊢ M ↓ (v ↦ w)</code> implies reduction a lambda abstraction.</p>
<p>It is well known that a term can reduce to a lambda abstraction using
full β reduction if and only if it can reduce to a lambda abstraction
using the call-by-name reduction strategy. So we shall prove that
<code class="language-plaintext highlighter-rouge">γ ⊢ M ↓ (v ↦ w)</code> implies that <code class="language-plaintext highlighter-rouge">M</code> halts under call-by-name evaluation,
which we define with a big-step semantics written <code class="language-plaintext highlighter-rouge">γ' ⊢ M ⇓ c</code>, where
<code class="language-plaintext highlighter-rouge">c</code> is a closure (a term paired with an environment) and <code class="language-plaintext highlighter-rouge">γ'</code> is an
environment that maps variables to closures</p>
<p>So we will show that <code class="language-plaintext highlighter-rouge">γ ⊢ M ↓ (v ↦ w)</code> implies <code class="language-plaintext highlighter-rouge">γ' ⊢ M ⇓ c</code>,
provided <code class="language-plaintext highlighter-rouge">γ</code> and <code class="language-plaintext highlighter-rouge">γ'</code> are appropriate related. The proof will
be an induction on the derivation of <code class="language-plaintext highlighter-rouge">γ ⊢ M ↓ v</code>, and to
strengthen the induction hypothesis, we will relate semantic values to
closures using a <em>logical relation</em> <code class="language-plaintext highlighter-rouge">𝕍</code>.</p>
<p>The rest of this chapter is organized as follows.</p>
<ul>
<li>
<p>We loosen the requirement that <code class="language-plaintext highlighter-rouge">M</code> result in a function value and
instead require that <code class="language-plaintext highlighter-rouge">M</code> result in a value that is greater than or
equal to a function value. We establish several properties about
being ``greater than a function’’.</p>
</li>
<li>
<p>We define the call-by-name big-step semantics of the lambda calculus
and prove that it is deterministic.</p>
</li>
<li>
<p>We define the logical relation <code class="language-plaintext highlighter-rouge">𝕍</code> that relates values and closures,
and extend it to a relation on terms <code class="language-plaintext highlighter-rouge">𝔼</code> and environments <code class="language-plaintext highlighter-rouge">𝔾</code>.</p>
</li>
<li>
<p>We prove the main lemma,
that if <code class="language-plaintext highlighter-rouge">𝔾 γ γ'</code> and <code class="language-plaintext highlighter-rouge">γ ⊢ M ↓ v</code>, then <code class="language-plaintext highlighter-rouge">𝔼 v (clos M γ')</code>.</p>
</li>
<li>
<p>We prove adequacy as a corollary to the main lemma.</p>
</li>
</ul>
<h2 id="imports">Imports</h2>
<pre class="Agda"><a id="2656" class="Keyword">import</a> <a id="2663" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Binary.PropositionalEquality.html" class="Module">Relation.Binary.PropositionalEquality</a> <a id="2701" class="Symbol">as</a> <a id="2704" class="Module">Eq</a>
<a id="2707" class="Keyword">open</a> <a id="2712" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Binary.PropositionalEquality.html" class="Module">Eq</a> <a id="2715" class="Keyword">using</a> <a id="2721" class="Symbol">(</a><a id="2722" href="Agda.Builtin.Equality.html#125" class="Datatype Operator">_≡_</a><a id="2725" class="Symbol">;</a> <a id="2727" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Binary.PropositionalEquality.Core.html#799" class="Function Operator">_≢_</a><a id="2730" class="Symbol">;</a> <a id="2732" href="Agda.Builtin.Equality.html#182" class="InductiveConstructor">refl</a><a id="2736" class="Symbol">;</a> <a id="2738" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Binary.PropositionalEquality.Core.html#984" class="Function">trans</a><a id="2743" class="Symbol">;</a> <a id="2745" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Binary.PropositionalEquality.Core.html#939" class="Function">sym</a><a id="2748" class="Symbol">;</a> <a id="2750" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Binary.PropositionalEquality.Core.html#1090" class="Function">cong</a><a id="2754" class="Symbol">;</a> <a id="2756" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Binary.PropositionalEquality.html#1436" class="Function">cong₂</a><a id="2761" class="Symbol">;</a> <a id="2763" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Binary.PropositionalEquality.html#1308" class="Function">cong-app</a><a id="2771" class="Symbol">)</a>
<a id="2773" class="Keyword">open</a> <a id="2778" class="Keyword">import</a> <a id="2785" href="https://agda.github.io/agda-stdlib/v1.1/Data.Product.html" class="Module">Data.Product</a> <a id="2798" class="Keyword">using</a> <a id="2804" class="Symbol">(</a><a id="2805" href="https://agda.github.io/agda-stdlib/v1.1/Data.Product.html#1162" class="Function Operator">_×_</a><a id="2808" class="Symbol">;</a> <a id="2810" href="Agda.Builtin.Sigma.html#139" class="Record">Σ</a><a id="2811" class="Symbol">;</a> <a id="2813" href="https://agda.github.io/agda-stdlib/v1.1/Data.Product.html#911" class="Function">Σ-syntax</a><a id="2821" class="Symbol">;</a> <a id="2823" href="https://agda.github.io/agda-stdlib/v1.1/Data.Product.html#1364" class="Function">∃</a><a id="2824" class="Symbol">;</a> <a id="2826" href="https://agda.github.io/agda-stdlib/v1.1/Data.Product.html#1783" class="Function">∃-syntax</a><a id="2834" class="Symbol">;</a> <a id="2836" href="Agda.Builtin.Sigma.html#225" class="Field">proj₁</a><a id="2841" class="Symbol">;</a> <a id="2843" href="Agda.Builtin.Sigma.html#237" class="Field">proj₂</a><a id="2848" class="Symbol">)</a>
<a id="2852" class="Keyword">renaming</a> <a id="2861" class="Symbol">(</a><a id="2862" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">_,_</a> <a id="2866" class="Symbol">to</a> <a id="2869" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟨_,_⟩</a><a id="2874" class="Symbol">)</a>
<a id="2876" class="Keyword">open</a> <a id="2881" class="Keyword">import</a> <a id="2888" href="https://agda.github.io/agda-stdlib/v1.1/Data.Sum.html" class="Module">Data.Sum</a>
<a id="2897" class="Keyword">open</a> <a id="2902" class="Keyword">import</a> <a id="2909" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Nullary.html" class="Module">Relation.Nullary</a> <a id="2926" class="Keyword">using</a> <a id="2932" class="Symbol">(</a><a id="2933" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Nullary.html#535" class="Function Operator">¬_</a><a id="2935" class="Symbol">)</a>
<a id="2937" class="Keyword">open</a> <a id="2942" class="Keyword">import</a> <a id="2949" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Nullary.Negation.html" class="Module">Relation.Nullary.Negation</a> <a id="2975" class="Keyword">using</a> <a id="2981" class="Symbol">(</a><a id="2982" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Nullary.Negation.html#809" class="Function">contradiction</a><a id="2995" class="Symbol">)</a>
<a id="2997" class="Keyword">open</a> <a id="3002" class="Keyword">import</a> <a id="3009" href="https://agda.github.io/agda-stdlib/v1.1/Data.Empty.html" class="Module">Data.Empty</a> <a id="3020" class="Keyword">using</a> <a id="3026" class="Symbol">(</a><a id="3027" href="https://agda.github.io/agda-stdlib/v1.1/Data.Empty.html#294" class="Function">⊥-elim</a><a id="3033" class="Symbol">)</a> <a id="3035" class="Keyword">renaming</a> <a id="3044" class="Symbol">(</a><a id="3045" href="https://agda.github.io/agda-stdlib/v1.1/Data.Empty.html#279" class="Datatype">⊥</a> <a id="3047" class="Symbol">to</a> <a id="3050" href="https://agda.github.io/agda-stdlib/v1.1/Data.Empty.html#279" class="Datatype">Bot</a><a id="3053" class="Symbol">)</a>
<a id="3055" class="Keyword">open</a> <a id="3060" class="Keyword">import</a> <a id="3067" href="https://agda.github.io/agda-stdlib/v1.1/Data.Unit.html" class="Module">Data.Unit</a>
<a id="3077" class="Keyword">open</a> <a id="3082" class="Keyword">import</a> <a id="3089" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Nullary.html" class="Module">Relation.Nullary</a> <a id="3106" class="Keyword">using</a> <a id="3112" class="Symbol">(</a><a id="3113" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Nullary.html#605" class="Datatype">Dec</a><a id="3116" class="Symbol">;</a> <a id="3118" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Nullary.html#641" class="InductiveConstructor">yes</a><a id="3121" class="Symbol">;</a> <a id="3123" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Nullary.html#668" class="InductiveConstructor">no</a><a id="3125" class="Symbol">)</a>
<a id="3127" class="Keyword">open</a> <a id="3132" class="Keyword">import</a> <a id="3139" href="https://agda.github.io/agda-stdlib/v1.1/Function.html" class="Module">Function</a> <a id="3148" class="Keyword">using</a> <a id="3154" class="Symbol">(</a><a id="3155" href="https://agda.github.io/agda-stdlib/v1.1/Function.html#1099" class="Function Operator">_∘_</a><a id="3158" class="Symbol">)</a>
<a id="3160" class="Keyword">open</a> <a id="3165" class="Keyword">import</a> <a id="3172" href="/19.08/Untyped/" class="Module">plfa.part2.Untyped</a>
<a id="3196" class="Keyword">using</a> <a id="3202" class="Symbol">(</a><a id="3203" href="/19.08/Untyped/#3153" class="Datatype">Context</a><a id="3210" class="Symbol">;</a> <a id="3212" href="plfa.part2.Untyped.html#4294" class="Datatype Operator">_⊢_</a><a id="3215" class="Symbol">;</a> <a id="3217" href="plfa.part2.Untyped.html#2888" class="InductiveConstructor">★</a><a id="3218" class="Symbol">;</a> <a id="3220" href="plfa.part2.Untyped.html#3521" class="Datatype Operator">_∋_</a><a id="3223" class="Symbol">;</a> <a id="3225" href="plfa.part2.Untyped.html#3175" class="InductiveConstructor">∅</a><a id="3226" class="Symbol">;</a> <a id="3228" href="plfa.part2.Untyped.html#3191" class="InductiveConstructor Operator">_,_</a><a id="3231" class="Symbol">;</a> <a id="3233" href="plfa.part2.Untyped.html#3557" class="InductiveConstructor">Z</a><a id="3234" class="Symbol">;</a> <a id="3236" href="plfa.part2.Untyped.html#3602" class="InductiveConstructor Operator">S_</a><a id="3238" class="Symbol">;</a> <a id="3240" href="plfa.part2.Untyped.html#4330" class="InductiveConstructor Operator">`_</a><a id="3242" class="Symbol">;</a> <a id="3244" href="plfa.part2.Untyped.html#4382" class="InductiveConstructor Operator">ƛ_</a><a id="3246" class="Symbol">;</a> <a id="3248" href="plfa.part2.Untyped.html#4442" class="InductiveConstructor Operator">_·_</a><a id="3251" class="Symbol">;</a>
<a id="3265" href="/19.08/Untyped/#6235" class="Function">rename</a><a id="3271" class="Symbol">;</a> <a id="3273" href="plfa.part2.Untyped.html#6963" class="Function">subst</a><a id="3278" class="Symbol">;</a> <a id="3280" href="plfa.part2.Untyped.html#5925" class="Function">ext</a><a id="3283" class="Symbol">;</a> <a id="3285" href="plfa.part2.Untyped.html#6671" class="Function">exts</a><a id="3289" class="Symbol">;</a> <a id="3291" href="plfa.part2.Untyped.html#7491" class="Function Operator">_[_]</a><a id="3295" class="Symbol">;</a> <a id="3297" href="plfa.part2.Untyped.html#7375" class="Function">subst-zero</a><a id="3307" class="Symbol">;</a>
<a id="3321" href="/19.08/Untyped/#11267" class="Datatype Operator">_—↠_</a><a id="3325" class="Symbol">;</a> <a id="3327" href="plfa.part2.Untyped.html#11373" class="InductiveConstructor Operator">_—→⟨_⟩_</a><a id="3334" class="Symbol">;</a> <a id="3336" href="plfa.part2.Untyped.html#11317" class="InductiveConstructor Operator">_∎</a><a id="3338" class="Symbol">;</a> <a id="3340" href="plfa.part2.Untyped.html#10147" class="Datatype Operator">_—→_</a><a id="3344" class="Symbol">;</a> <a id="3346" href="plfa.part2.Untyped.html#10197" class="InductiveConstructor">ξ₁</a><a id="3348" class="Symbol">;</a> <a id="3350" href="plfa.part2.Untyped.html#10287" class="InductiveConstructor">ξ₂</a><a id="3352" class="Symbol">;</a> <a id="3354" href="plfa.part2.Untyped.html#10377" class="InductiveConstructor">β</a><a id="3355" class="Symbol">;</a> <a id="3357" href="plfa.part2.Untyped.html#10485" class="InductiveConstructor">ζ</a><a id="3358" class="Symbol">)</a>
<a id="3360" class="Keyword">open</a> <a id="3365" class="Keyword">import</a> <a id="3372" href="/19.08/Substitution/" class="Module">plfa.part2.Substitution</a> <a id="3396" class="Keyword">using</a> <a id="3402" class="Symbol">(</a><a id="3403" href="plfa.part2.Substitution.html#3046" class="Function">ids</a><a id="3406" class="Symbol">;</a> <a id="3408" href="plfa.part2.Substitution.html#16986" class="Function">sub-id</a><a id="3414" class="Symbol">)</a>
<a id="3416" class="Keyword">open</a> <a id="3421" class="Keyword">import</a> <a id="3428" href="/19.08/BigStep/" class="Module">plfa.part2.BigStep</a>
<a id="3452" class="Keyword">using</a> <a id="3458" class="Symbol">(</a><a id="3459" href="/19.08/BigStep/#2470" class="Datatype">Clos</a><a id="3463" class="Symbol">;</a> <a id="3465" href="plfa.part2.BigStep.html#2489" class="InductiveConstructor">clos</a><a id="3469" class="Symbol">;</a> <a id="3471" href="plfa.part2.BigStep.html#2440" class="Function">ClosEnv</a><a id="3478" class="Symbol">;</a> <a id="3480" href="plfa.part2.BigStep.html#2653" class="Function">∅&#39;</a><a id="3482" class="Symbol">;</a> <a id="3484" href="plfa.part2.BigStep.html#2675" class="Function Operator">_,&#39;_</a><a id="3488" class="Symbol">;</a> <a id="3490" href="plfa.part2.BigStep.html#3024" class="Datatype Operator">_⊢_⇓_</a><a id="3495" class="Symbol">;</a> <a id="3497" href="plfa.part2.BigStep.html#3081" class="InductiveConstructor">⇓-var</a><a id="3502" class="Symbol">;</a> <a id="3504" href="plfa.part2.BigStep.html#3228" class="InductiveConstructor">⇓-lam</a><a id="3509" class="Symbol">;</a> <a id="3511" href="plfa.part2.BigStep.html#3303" class="InductiveConstructor">⇓-app</a><a id="3516" class="Symbol">;</a> <a id="3518" href="plfa.part2.BigStep.html#4589" class="Function">⇓-determ</a><a id="3526" class="Symbol">;</a>
<a id="3540" href="/19.08/BigStep/#12205" class="Function">cbn→reduce</a><a id="3550" class="Symbol">)</a>
<a id="3552" class="Keyword">open</a> <a id="3557" class="Keyword">import</a> <a id="3564" href="/19.08/Denotational/" class="Module">plfa.part3.Denotational</a>
<a id="3593" class="Keyword">using</a> <a id="3599" class="Symbol">(</a><a id="3600" href="/19.08/Denotational/#4070" class="Datatype">Value</a><a id="3605" class="Symbol">;</a> <a id="3607" href="plfa.part3.Denotational.html#7207" class="Function">Env</a><a id="3610" class="Symbol">;</a> <a id="3612" href="plfa.part3.Denotational.html#7331" class="Function">`∅</a><a id="3614" class="Symbol">;</a> <a id="3616" href="plfa.part3.Denotational.html#7364" class="Function Operator">_`,_</a><a id="3620" class="Symbol">;</a> <a id="3622" href="plfa.part3.Denotational.html#4102" class="InductiveConstructor Operator">_↦_</a><a id="3625" class="Symbol">;</a> <a id="3627" href="plfa.part3.Denotational.html#4427" class="Datatype Operator">_⊑_</a><a id="3630" class="Symbol">;</a> <a id="3632" href="plfa.part3.Denotational.html#9417" class="Datatype Operator">_⊢_↓_</a><a id="3637" class="Symbol">;</a> <a id="3639" href="plfa.part3.Denotational.html#4090" class="InductiveConstructor">⊥</a><a id="3640" class="Symbol">;</a> <a id="3642" href="plfa.part3.Denotational.html#30243" class="Function">all-funs∈</a><a id="3651" class="Symbol">;</a> <a id="3653" href="plfa.part3.Denotational.html#4132" class="InductiveConstructor Operator">_⊔_</a><a id="3656" class="Symbol">;</a> <a id="3658" href="plfa.part3.Denotational.html#28536" class="Function">∈→⊑</a><a id="3661" class="Symbol">;</a>
<a id="3675" href="/19.08/Denotational/#9471" class="InductiveConstructor">var</a><a id="3678" class="Symbol">;</a> <a id="3680" href="plfa.part3.Denotational.html#9546" class="InductiveConstructor">↦-elim</a><a id="3686" class="Symbol">;</a> <a id="3688" href="plfa.part3.Denotational.html#9668" class="InductiveConstructor">↦-intro</a><a id="3695" class="Symbol">;</a> <a id="3697" href="plfa.part3.Denotational.html#9847" class="InductiveConstructor">⊔-intro</a><a id="3704" class="Symbol">;</a> <a id="3706" href="plfa.part3.Denotational.html#9780" class="InductiveConstructor">⊥-intro</a><a id="3713" class="Symbol">;</a> <a id="3715" href="plfa.part3.Denotational.html#9962" class="InductiveConstructor">sub</a><a id="3718" class="Symbol">;</a> <a id="3720" href="plfa.part3.Denotational.html#17516" class="Function">ℰ</a><a id="3721" class="Symbol">;</a> <a id="3723" href="plfa.part3.Denotational.html#17698" class="Function Operator">_≃_</a><a id="3726" class="Symbol">;</a> <a id="3728" href="plfa.part3.Denotational.html#17037" class="Function Operator">_iff_</a><a id="3733" class="Symbol">;</a>
<a id="3747" href="/19.08/Denotational/#4717" class="InductiveConstructor">⊑-trans</a><a id="3754" class="Symbol">;</a> <a id="3756" href="plfa.part3.Denotational.html#4571" class="InductiveConstructor">⊑-conj-R1</a><a id="3765" class="Symbol">;</a> <a id="3767" href="plfa.part3.Denotational.html#4644" class="InductiveConstructor">⊑-conj-R2</a><a id="3776" class="Symbol">;</a> <a id="3778" href="plfa.part3.Denotational.html#4487" class="InductiveConstructor">⊑-conj-L</a><a id="3786" class="Symbol">;</a> <a id="3788" href="plfa.part3.Denotational.html#5557" class="Function">⊑-refl</a><a id="3794" class="Symbol">;</a> <a id="3796" href="plfa.part3.Denotational.html#4788" class="InductiveConstructor">⊑-fun</a><a id="3801" class="Symbol">;</a> <a id="3803" href="plfa.part3.Denotational.html#4462" class="InductiveConstructor">⊑-bot</a><a id="3808" class="Symbol">;</a> <a id="3810" href="plfa.part3.Denotational.html#4891" class="InductiveConstructor">⊑-dist</a><a id="3816" class="Symbol">;</a>
<a id="3830" href="/19.08/Denotational/#40727" class="Function">sub-inv-fun</a><a id="3841" class="Symbol">)</a>
<a id="3843" class="Keyword">open</a> <a id="3848" class="Keyword">import</a> <a id="3855" href="/19.08/Soundness/" class="Module">plfa.part3.Soundness</a> <a id="3876" class="Keyword">using</a> <a id="3882" class="Symbol">(</a><a id="3883" href="plfa.part3.Soundness.html#23426" class="Function">soundness</a><a id="3892" class="Symbol">)</a>
</pre>
<h2 id="the-property-of-being-greater-or-equal-to-a-function">The property of being greater or equal to a function</h2>
<p>We define the following short-hand for saying that a value is
greather-than or equal to a function value.</p>
<pre class="Agda"><a id="above-fun"></a><a id="4069" href="/19.08/Adequacy/#4069" class="Function">above-fun</a> <a id="4079" class="Symbol">:</a> <a id="4081" href="/19.08/Denotational/#4070" class="Datatype">Value</a> <a id="4087" class="Symbol">→</a> <a id="4089" class="PrimitiveType">Set</a>
<a id="4093" href="/19.08/Adequacy/#4069" class="Function">above-fun</a> <a id="4103" href="plfa.part3.Adequacy.html#4103" class="Bound">u</a> <a id="4105" class="Symbol">=</a> <a id="4107" href="https://agda.github.io/agda-stdlib/v1.1/Data.Product.html#911" class="Function">Σ[</a> <a id="4110" href="plfa.part3.Adequacy.html#4110" class="Bound">v</a> <a id="4112" href="https://agda.github.io/agda-stdlib/v1.1/Data.Product.html#911" class="Function">∈</a> <a id="4114" href="/19.08/Denotational/#4070" class="Datatype">Value</a> <a id="4120" href="https://agda.github.io/agda-stdlib/v1.1/Data.Product.html#911" class="Function">]</a> <a id="4122" href="https://agda.github.io/agda-stdlib/v1.1/Data.Product.html#911" class="Function">Σ[</a> <a id="4125" href="plfa.part3.Adequacy.html#4125" class="Bound">w</a> <a id="4127" href="https://agda.github.io/agda-stdlib/v1.1/Data.Product.html#911" class="Function">∈</a> <a id="4129" href="plfa.part3.Denotational.html#4070" class="Datatype">Value</a> <a id="4135" href="https://agda.github.io/agda-stdlib/v1.1/Data.Product.html#911" class="Function">]</a> <a id="4137" href="plfa.part3.Adequacy.html#4110" class="Bound">v</a> <a id="4139" href="plfa.part3.Denotational.html#4102" class="InductiveConstructor Operator">↦</a> <a id="4141" href="plfa.part3.Adequacy.html#4125" class="Bound">w</a> <a id="4143" href="plfa.part3.Denotational.html#4427" class="Datatype Operator">⊑</a> <a id="4145" href="plfa.part3.Adequacy.html#4103" class="Bound">u</a>
</pre>
<p>If a value <code class="language-plaintext highlighter-rouge">u</code> is greater than a function, then an even greater value <code class="language-plaintext highlighter-rouge">u'</code>
is too.</p>
<pre class="Agda"><a id="above-fun-⊑"></a><a id="4240" href="/19.08/Adequacy/#4240" class="Function">above-fun-⊑</a> <a id="4252" class="Symbol">:</a> <a id="4254" class="Symbol">∀{</a><a id="4256" href="plfa.part3.Adequacy.html#4256" class="Bound">u</a> <a id="4258" href="plfa.part3.Adequacy.html#4258" class="Bound">u&#39;</a> <a id="4261" class="Symbol">:</a> <a id="4263" href="/19.08/Denotational/#4070" class="Datatype">Value</a><a id="4268" class="Symbol">}</a>
<a id="4276" class="Symbol">→</a> <a id="4278" href="/19.08/Adequacy/#4069" class="Function">above-fun</a> <a id="4288" href="plfa.part3.Adequacy.html#4256" class="Bound">u</a> <a id="4290" class="Symbol">→</a> <a id="4292" href="plfa.part3.Adequacy.html#4256" class="Bound">u</a> <a id="4294" href="/19.08/Denotational/#4427" class="Datatype Operator">⊑</a> <a id="4296" href="plfa.part3.Adequacy.html#4258" class="Bound">u&#39;</a>
<a id="4307" class="Comment">-------------------</a>
<a id="4333" class="Symbol">→</a> <a id="4335" href="/19.08/Adequacy/#4069" class="Function">above-fun</a> <a id="4345" href="plfa.part3.Adequacy.html#4258" class="Bound">u&#39;</a>
<a id="4348" href="/19.08/Adequacy/#4240" class="Function">above-fun-⊑</a> <a id="4360" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟨</a> <a id="4362" href="plfa.part3.Adequacy.html#4362" class="Bound">v</a> <a id="4364" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">,</a> <a id="4366" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟨</a> <a id="4368" href="plfa.part3.Adequacy.html#4368" class="Bound">w</a> <a id="4370" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">,</a> <a id="4372" href="plfa.part3.Adequacy.html#4372" class="Bound">lt&#39;</a> <a id="4376" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟩</a> <a id="4378" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟩</a> <a id="4380" href="plfa.part3.Adequacy.html#4380" class="Bound">lt</a> <a id="4383" class="Symbol">=</a> <a id="4385" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟨</a> <a id="4387" href="plfa.part3.Adequacy.html#4362" class="Bound">v</a> <a id="4389" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">,</a> <a id="4391" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟨</a> <a id="4393" href="plfa.part3.Adequacy.html#4368" class="Bound">w</a> <a id="4395" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">,</a> <a id="4397" href="/19.08/Denotational/#4717" class="InductiveConstructor">⊑-trans</a> <a id="4405" href="plfa.part3.Adequacy.html#4372" class="Bound">lt&#39;</a> <a id="4409" href="plfa.part3.Adequacy.html#4380" class="Bound">lt</a> <a id="4412" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟩</a> <a id="4414" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟩</a>
</pre>
<p>The bottom value <code class="language-plaintext highlighter-rouge">⊥</code> is not greater than a function.</p>
<pre class="Agda"><a id="above-fun⊥"></a><a id="4479" href="/19.08/Adequacy/#4479" class="Function">above-fun⊥</a> <a id="4490" class="Symbol">:</a> <a id="4492" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Nullary.html#535" class="Function Operator">¬</a> <a id="4494" href="plfa.part3.Adequacy.html#4069" class="Function">above-fun</a> <a id="4504" href="/19.08/Denotational/#4090" class="InductiveConstructor">⊥</a>
<a id="4506" href="/19.08/Adequacy/#4479" class="Function">above-fun⊥</a> <a id="4517" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟨</a> <a id="4519" href="plfa.part3.Adequacy.html#4519" class="Bound">v</a> <a id="4521" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">,</a> <a id="4523" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟨</a> <a id="4525" href="plfa.part3.Adequacy.html#4525" class="Bound">w</a> <a id="4527" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">,</a> <a id="4529" href="plfa.part3.Adequacy.html#4529" class="Bound">lt</a> <a id="4532" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟩</a> <a id="4534" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟩</a>
<a id="4540" class="Keyword">with</a> <a id="4545" href="/19.08/Denotational/#40727" class="Function">sub-inv-fun</a> <a id="4557" href="/19.08/Adequacy/#4529" class="Bound">lt</a>
<a id="4560" class="Symbol">...</a> <a id="4564" class="Symbol">|</a> <a id="4566" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟨</a> <a id="4568" href="/19.08/Adequacy/#4568" class="Bound">Γ</a> <a id="4570" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">,</a> <a id="4572" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟨</a> <a id="4574" href="plfa.part3.Adequacy.html#4574" class="Bound">f</a> <a id="4576" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">,</a> <a id="4578" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟨</a> <a id="4580" href="plfa.part3.Adequacy.html#4580" class="Bound">Γ⊆⊥</a> <a id="4584" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">,</a> <a id="4586" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟨</a> <a id="4588" href="plfa.part3.Adequacy.html#4588" class="Bound">lt1</a> <a id="4592" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">,</a> <a id="4594" href="plfa.part3.Adequacy.html#4594" class="Bound">lt2</a> <a id="4598" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟩</a> <a id="4600" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟩</a> <a id="4602" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟩</a> <a id="4604" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟩</a>
<a id="4610" class="Keyword">with</a> <a id="4615" href="/19.08/Denotational/#30243" class="Function">all-funs∈</a> <a id="4625" href="/19.08/Adequacy/#4574" class="Bound">f</a>
<a id="4627" class="Symbol">...</a> <a id="4631" class="Symbol">|</a> <a id="4633" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟨</a> <a id="4635" href="/19.08/Adequacy/#4635" class="Bound">A</a> <a id="4637" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">,</a> <a id="4639" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟨</a> <a id="4641" href="plfa.part3.Adequacy.html#4641" class="Bound">B</a> <a id="4643" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">,</a> <a id="4645" href="plfa.part3.Adequacy.html#4645" class="Bound">m</a> <a id="4647" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟩</a> <a id="4649" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟩</a>
<a id="4655" class="Keyword">with</a> <a id="4660" class="Bound">Γ⊆⊥</a> <a id="4664" href="/19.08/Adequacy/#4645" class="Bound">m</a>
<a id="4666" class="Symbol">...</a> <a id="4670" class="Symbol">|</a> <a id="4672" class="Symbol">()</a>
</pre>
<p>If the join of two values <code class="language-plaintext highlighter-rouge">u</code> and <code class="language-plaintext highlighter-rouge">u'</code> is greater than a function, then
at least one of them is too.</p>
<pre class="Agda"><a id="above-fun-⊔"></a><a id="4786" href="/19.08/Adequacy/#4786" class="Function">above-fun-⊔</a> <a id="4798" class="Symbol">:</a> <a id="4800" class="Symbol">∀{</a><a id="4802" href="plfa.part3.Adequacy.html#4802" class="Bound">u</a> <a id="4804" href="plfa.part3.Adequacy.html#4804" class="Bound">u&#39;</a><a id="4806" class="Symbol">}</a>
<a id="4819" class="Symbol">→</a> <a id="4821" href="/19.08/Adequacy/#4069" class="Function">above-fun</a> <a id="4831" class="Symbol">(</a><a id="4832" href="plfa.part3.Adequacy.html#4802" class="Bound">u</a> <a id="4834" href="/19.08/Denotational/#4132" class="InductiveConstructor Operator">⊔</a> <a id="4836" href="plfa.part3.Adequacy.html#4804" class="Bound">u&#39;</a><a id="4838" class="Symbol">)</a>
<a id="4851" class="Symbol">→</a> <a id="4853" href="/19.08/Adequacy/#4069" class="Function">above-fun</a> <a id="4863" href="plfa.part3.Adequacy.html#4802" class="Bound">u</a> <a id="4865" href="https://agda.github.io/agda-stdlib/v1.1/Data.Sum.Base.html#612" class="Datatype Operator">⊎</a> <a id="4867" href="plfa.part3.Adequacy.html#4069" class="Function">above-fun</a> <a id="4877" href="plfa.part3.Adequacy.html#4804" class="Bound">u&#39;</a>
<a id="4880" href="/19.08/Adequacy/#4786" class="Function">above-fun-⊔</a><a id="4891" class="Symbol">{</a><a id="4892" href="plfa.part3.Adequacy.html#4892" class="Bound">u</a><a id="4893" class="Symbol">}{</a><a id="4895" href="plfa.part3.Adequacy.html#4895" class="Bound">u&#39;</a><a id="4897" class="Symbol">}</a> <a id="4899" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟨</a> <a id="4901" href="plfa.part3.Adequacy.html#4901" class="Bound">v</a> <a id="4903" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">,</a> <a id="4905" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟨</a> <a id="4907" href="plfa.part3.Adequacy.html#4907" class="Bound">w</a> <a id="4909" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">,</a> <a id="4911" href="plfa.part3.Adequacy.html#4911" class="Bound">v↦w⊑u⊔u&#39;</a> <a id="4920" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟩</a> <a id="4922" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟩</a>
<a id="4928" class="Keyword">with</a> <a id="4933" href="/19.08/Denotational/#40727" class="Function">sub-inv-fun</a> <a id="4945" href="/19.08/Adequacy/#4911" class="Bound">v↦w⊑u⊔u&#39;</a>
<a id="4954" class="Symbol">...</a> <a id="4958" class="Symbol">|</a> <a id="4960" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟨</a> <a id="4962" href="/19.08/Adequacy/#4962" class="Bound">Γ</a> <a id="4964" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">,</a> <a id="4966" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟨</a> <a id="4968" href="plfa.part3.Adequacy.html#4968" class="Bound">f</a> <a id="4970" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">,</a> <a id="4972" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟨</a> <a id="4974" href="plfa.part3.Adequacy.html#4974" class="Bound">Γ⊆u⊔u&#39;</a> <a id="4981" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">,</a> <a id="4983" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟨</a> <a id="4985" href="plfa.part3.Adequacy.html#4985" class="Bound">lt1</a> <a id="4989" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">,</a> <a id="4991" href="plfa.part3.Adequacy.html#4991" class="Bound">lt2</a> <a id="4995" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟩</a> <a id="4997" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟩</a> <a id="4999" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟩</a> <a id="5001" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟩</a>
<a id="5007" class="Keyword">with</a> <a id="5012" href="/19.08/Denotational/#30243" class="Function">all-funs∈</a> <a id="5022" href="/19.08/Adequacy/#4968" class="Bound">f</a>
<a id="5024" class="Symbol">...</a> <a id="5028" class="Symbol">|</a> <a id="5030" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟨</a> <a id="5032" href="/19.08/Adequacy/#5032" class="Bound">A</a> <a id="5034" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">,</a> <a id="5036" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟨</a> <a id="5038" href="plfa.part3.Adequacy.html#5038" class="Bound">B</a> <a id="5040" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">,</a> <a id="5042" href="plfa.part3.Adequacy.html#5042" class="Bound">m</a> <a id="5044" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟩</a> <a id="5046" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟩</a>
<a id="5052" class="Keyword">with</a> <a id="5057" class="Bound">Γ⊆u⊔u&#39;</a> <a id="5064" href="/19.08/Adequacy/#5042" class="Bound">m</a>
<a id="5066" class="Symbol">...</a> <a id="5070" class="Symbol">|</a> <a id="5072" href="https://agda.github.io/agda-stdlib/v1.1/Data.Sum.Base.html#662" class="InductiveConstructor">inj₁</a> <a id="5077" href="/19.08/Adequacy/#5077" class="Bound">x</a> <a id="5079" class="Symbol">=</a> <a id="5081" href="https://agda.github.io/agda-stdlib/v1.1/Data.Sum.Base.html#662" class="InductiveConstructor">inj₁</a> <a id="5086" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟨</a> <a id="5088" class="Bound">A</a> <a id="5090" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">,</a> <a id="5092" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟨</a> <a id="5094" class="Bound">B</a> <a id="5096" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">,</a> <a id="5098" class="Symbol">(</a><a id="5099" href="/19.08/Denotational/#28536" class="Function">∈→⊑</a> <a id="5103" href="plfa.part3.Adequacy.html#5077" class="Bound">x</a><a id="5104" class="Symbol">)</a> <a id="5106" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟩</a> <a id="5108" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟩</a>
<a id="5110" class="Symbol">...</a> <a id="5114" class="Symbol">|</a> <a id="5116" href="https://agda.github.io/agda-stdlib/v1.1/Data.Sum.Base.html#687" class="InductiveConstructor">inj₂</a> <a id="5121" href="/19.08/Adequacy/#5121" class="Bound">x</a> <a id="5123" class="Symbol">=</a> <a id="5125" href="https://agda.github.io/agda-stdlib/v1.1/Data.Sum.Base.html#687" class="InductiveConstructor">inj₂</a> <a id="5130" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟨</a> <a id="5132" class="Bound">A</a> <a id="5134" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">,</a> <a id="5136" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟨</a> <a id="5138" class="Bound">B</a> <a id="5140" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">,</a> <a id="5142" class="Symbol">(</a><a id="5143" href="/19.08/Denotational/#28536" class="Function">∈→⊑</a> <a id="5147" href="plfa.part3.Adequacy.html#5121" class="Bound">x</a><a id="5148" class="Symbol">)</a> <a id="5150" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟩</a> <a id="5152" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟩</a>
</pre>
<p>On the other hand, if neither of <code class="language-plaintext highlighter-rouge">u</code> and <code class="language-plaintext highlighter-rouge">u'</code> is greater than a function,
then their join is also not greater than a function.</p>
<pre class="Agda"><a id="not-above-fun-⊔"></a><a id="5291" href="/19.08/Adequacy/#5291" class="Function">not-above-fun-⊔</a> <a id="5307" class="Symbol">:</a> <a id="5309" class="Symbol">∀{</a><a id="5311" href="plfa.part3.Adequacy.html#5311" class="Bound">u</a> <a id="5313" href="plfa.part3.Adequacy.html#5313" class="Bound">u&#39;</a> <a id="5316" class="Symbol">:</a> <a id="5318" href="/19.08/Denotational/#4070" class="Datatype">Value</a><a id="5323" class="Symbol">}</a>
<a id="5340" class="Symbol">→</a> <a id="5342" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Nullary.html#535" class="Function Operator">¬</a> <a id="5344" href="/19.08/Adequacy/#4069" class="Function">above-fun</a> <a id="5354" href="plfa.part3.Adequacy.html#5311" class="Bound">u</a> <a id="5356" class="Symbol">→</a> <a id="5358" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Nullary.html#535" class="Function Operator">¬</a> <a id="5360" href="plfa.part3.Adequacy.html#4069" class="Function">above-fun</a> <a id="5370" href="plfa.part3.Adequacy.html#5313" class="Bound">u&#39;</a>
<a id="5388" class="Symbol">→</a> <a id="5390" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Nullary.html#535" class="Function Operator">¬</a> <a id="5392" href="/19.08/Adequacy/#4069" class="Function">above-fun</a> <a id="5402" class="Symbol">(</a><a id="5403" href="plfa.part3.Adequacy.html#5311" class="Bound">u</a> <a id="5405" href="/19.08/Denotational/#4132" class="InductiveConstructor Operator">⊔</a> <a id="5407" href="plfa.part3.Adequacy.html#5313" class="Bound">u&#39;</a><a id="5409" class="Symbol">)</a>
<a id="5411" href="/19.08/Adequacy/#5291" class="Function">not-above-fun-⊔</a> <a id="5427" href="plfa.part3.Adequacy.html#5427" class="Bound">naf1</a> <a id="5432" href="plfa.part3.Adequacy.html#5432" class="Bound">naf2</a> <a id="5437" href="plfa.part3.Adequacy.html#5437" class="Bound">af12</a>
<a id="5446" class="Keyword">with</a> <a id="5451" href="/19.08/Adequacy/#4786" class="Function">above-fun-⊔</a> <a id="5463" href="plfa.part3.Adequacy.html#5437" class="Bound">af12</a>
<a id="5468" class="Symbol">...</a> <a id="5472" class="Symbol">|</a> <a id="5474" href="https://agda.github.io/agda-stdlib/v1.1/Data.Sum.Base.html#662" class="InductiveConstructor">inj₁</a> <a id="5479" href="/19.08/Adequacy/#5479" class="Bound">af1</a> <a id="5483" class="Symbol">=</a> <a id="5485" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Nullary.Negation.html#809" class="Function">contradiction</a> <a id="5499" href="plfa.part3.Adequacy.html#5479" class="Bound">af1</a> <a id="5503" class="Bound">naf1</a>
<a id="5508" class="Symbol">...</a> <a id="5512" class="Symbol">|</a> <a id="5514" href="https://agda.github.io/agda-stdlib/v1.1/Data.Sum.Base.html#687" class="InductiveConstructor">inj₂</a> <a id="5519" href="/19.08/Adequacy/#5519" class="Bound">af2</a> <a id="5523" class="Symbol">=</a> <a id="5525" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Nullary.Negation.html#809" class="Function">contradiction</a> <a id="5539" href="plfa.part3.Adequacy.html#5519" class="Bound">af2</a> <a id="5543" class="Bound">naf2</a>
</pre>
<p>The converse is also true. If the join of two values is not above a
function, then neither of them is individually.</p>
<pre class="Agda"><a id="not-above-fun-⊔-inv"></a><a id="5674" href="/19.08/Adequacy/#5674" class="Function">not-above-fun-⊔-inv</a> <a id="5694" class="Symbol">:</a> <a id="5696" class="Symbol">∀{</a><a id="5698" href="plfa.part3.Adequacy.html#5698" class="Bound">u</a> <a id="5700" href="plfa.part3.Adequacy.html#5700" class="Bound">u&#39;</a> <a id="5703" class="Symbol">:</a> <a id="5705" href="/19.08/Denotational/#4070" class="Datatype">Value</a><a id="5710" class="Symbol">}</a> <a id="5712" class="Symbol">→</a> <a id="5714" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Nullary.html#535" class="Function Operator">¬</a> <a id="5716" href="plfa.part3.Adequacy.html#4069" class="Function">above-fun</a> <a id="5726" class="Symbol">(</a><a id="5727" href="plfa.part3.Adequacy.html#5698" class="Bound">u</a> <a id="5729" href="plfa.part3.Denotational.html#4132" class="InductiveConstructor Operator">⊔</a> <a id="5731" href="plfa.part3.Adequacy.html#5700" class="Bound">u&#39;</a><a id="5733" class="Symbol">)</a>
<a id="5749" class="Symbol">→</a> <a id="5751" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Nullary.html#535" class="Function Operator">¬</a> <a id="5753" href="/19.08/Adequacy/#4069" class="Function">above-fun</a> <a id="5763" href="plfa.part3.Adequacy.html#5698" class="Bound">u</a> <a id="5765" href="https://agda.github.io/agda-stdlib/v1.1/Data.Product.html#1162" class="Function Operator">×</a> <a id="5767" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Nullary.html#535" class="Function Operator">¬</a> <a id="5769" href="plfa.part3.Adequacy.html#4069" class="Function">above-fun</a> <a id="5779" href="plfa.part3.Adequacy.html#5700" class="Bound">u&#39;</a>
<a id="5782" href="/19.08/Adequacy/#5674" class="Function">not-above-fun-⊔-inv</a> <a id="5802" href="plfa.part3.Adequacy.html#5802" class="Bound">af</a> <a id="5805" class="Symbol">=</a> <a id="5807" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟨</a> <a id="5809" href="plfa.part3.Adequacy.html#5835" class="Function">f</a> <a id="5811" href="plfa.part3.Adequacy.html#5802" class="Bound">af</a> <a id="5814" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">,</a> <a id="5816" href="plfa.part3.Adequacy.html#5993" class="Function">g</a> <a id="5818" href="plfa.part3.Adequacy.html#5802" class="Bound">af</a> <a id="5821" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟩</a>
<a id="5825" class="Keyword">where</a>
<a id="5835" href="/19.08/Adequacy/#5835" class="Function">f</a> <a id="5837" class="Symbol">:</a> <a id="5839" class="Symbol">∀{</a><a id="5841" href="plfa.part3.Adequacy.html#5841" class="Bound">u</a> <a id="5843" href="plfa.part3.Adequacy.html#5843" class="Bound">u&#39;</a> <a id="5846" class="Symbol">:</a> <a id="5848" href="/19.08/Denotational/#4070" class="Datatype">Value</a><a id="5853" class="Symbol">}</a> <a id="5855" class="Symbol">→</a> <a id="5857" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Nullary.html#535" class="Function Operator">¬</a> <a id="5859" href="plfa.part3.Adequacy.html#4069" class="Function">above-fun</a> <a id="5869" class="Symbol">(</a><a id="5870" href="plfa.part3.Adequacy.html#5841" class="Bound">u</a> <a id="5872" href="plfa.part3.Denotational.html#4132" class="InductiveConstructor Operator">⊔</a> <a id="5874" href="plfa.part3.Adequacy.html#5843" class="Bound">u&#39;</a><a id="5876" class="Symbol">)</a> <a id="5878" class="Symbol">→</a> <a id="5880" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Nullary.html#535" class="Function Operator">¬</a> <a id="5882" href="plfa.part3.Adequacy.html#4069" class="Function">above-fun</a> <a id="5892" href="plfa.part3.Adequacy.html#5841" class="Bound">u</a>
<a id="5898" href="/19.08/Adequacy/#5835" class="Function">f</a><a id="5899" class="Symbol">{</a><a id="5900" href="plfa.part3.Adequacy.html#5900" class="Bound">u</a><a id="5901" class="Symbol">}{</a><a id="5903" href="plfa.part3.Adequacy.html#5903" class="Bound">u&#39;</a><a id="5905" class="Symbol">}</a> <a id="5907" href="plfa.part3.Adequacy.html#5907" class="Bound">af12</a> <a id="5912" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟨</a> <a id="5914" href="plfa.part3.Adequacy.html#5914" class="Bound">v</a> <a id="5916" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">,</a> <a id="5918" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟨</a> <a id="5920" href="plfa.part3.Adequacy.html#5920" class="Bound">w</a> <a id="5922" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">,</a> <a id="5924" href="plfa.part3.Adequacy.html#5924" class="Bound">lt</a> <a id="5927" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟩</a> <a id="5929" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟩</a> <a id="5931" class="Symbol">=</a>
<a id="5941" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Nullary.Negation.html#809" class="Function">contradiction</a> <a id="5955" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟨</a> <a id="5957" href="/19.08/Adequacy/#5914" class="Bound">v</a> <a id="5959" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">,</a> <a id="5961" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟨</a> <a id="5963" href="plfa.part3.Adequacy.html#5920" class="Bound">w</a> <a id="5965" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">,</a> <a id="5967" href="/19.08/Denotational/#4571" class="InductiveConstructor">⊑-conj-R1</a> <a id="5977" href="plfa.part3.Adequacy.html#5924" class="Bound">lt</a> <a id="5980" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟩</a> <a id="5982" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟩</a> <a id="5984" href="plfa.part3.Adequacy.html#5907" class="Bound">af12</a>
<a id="5993" href="/19.08/Adequacy/#5993" class="Function">g</a> <a id="5995" class="Symbol">:</a> <a id="5997" class="Symbol">∀{</a><a id="5999" href="plfa.part3.Adequacy.html#5999" class="Bound">u</a> <a id="6001" href="plfa.part3.Adequacy.html#6001" class="Bound">u&#39;</a> <a id="6004" class="Symbol">:</a> <a id="6006" href="/19.08/Denotational/#4070" class="Datatype">Value</a><a id="6011" class="Symbol">}</a> <a id="6013" class="Symbol">→</a> <a id="6015" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Nullary.html#535" class="Function Operator">¬</a> <a id="6017" href="plfa.part3.Adequacy.html#4069" class="Function">above-fun</a> <a id="6027" class="Symbol">(</a><a id="6028" href="plfa.part3.Adequacy.html#5999" class="Bound">u</a> <a id="6030" href="plfa.part3.Denotational.html#4132" class="InductiveConstructor Operator">⊔</a> <a id="6032" href="plfa.part3.Adequacy.html#6001" class="Bound">u&#39;</a><a id="6034" class="Symbol">)</a> <a id="6036" class="Symbol">→</a> <a id="6038" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Nullary.html#535" class="Function Operator">¬</a> <a id="6040" href="plfa.part3.Adequacy.html#4069" class="Function">above-fun</a> <a id="6050" href="plfa.part3.Adequacy.html#6001" class="Bound">u&#39;</a>
<a id="6057" href="/19.08/Adequacy/#5993" class="Function">g</a><a id="6058" class="Symbol">{</a><a id="6059" href="plfa.part3.Adequacy.html#6059" class="Bound">u</a><a id="6060" class="Symbol">}{</a><a id="6062" href="plfa.part3.Adequacy.html#6062" class="Bound">u&#39;</a><a id="6064" class="Symbol">}</a> <a id="6066" href="plfa.part3.Adequacy.html#6066" class="Bound">af12</a> <a id="6071" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟨</a> <a id="6073" href="plfa.part3.Adequacy.html#6073" class="Bound">v</a> <a id="6075" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">,</a> <a id="6077" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟨</a> <a id="6079" href="plfa.part3.Adequacy.html#6079" class="Bound">w</a> <a id="6081" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">,</a> <a id="6083" href="plfa.part3.Adequacy.html#6083" class="Bound">lt</a> <a id="6086" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟩</a> <a id="6088" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟩</a> <a id="6090" class="Symbol">=</a>
<a id="6100" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Nullary.Negation.html#809" class="Function">contradiction</a> <a id="6114" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟨</a> <a id="6116" href="/19.08/Adequacy/#6073" class="Bound">v</a> <a id="6118" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">,</a> <a id="6120" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟨</a> <a id="6122" href="plfa.part3.Adequacy.html#6079" class="Bound">w</a> <a id="6124" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">,</a> <a id="6126" href="/19.08/Denotational/#4644" class="InductiveConstructor">⊑-conj-R2</a> <a id="6136" href="plfa.part3.Adequacy.html#6083" class="Bound">lt</a> <a id="6139" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟩</a> <a id="6141" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟩</a> <a id="6143" href="plfa.part3.Adequacy.html#6066" class="Bound">af12</a>
</pre>
<p>The property of being greater than a function value is decidable, as
exhibited by the following function.</p>
<pre class="Agda"><a id="above-fun?"></a><a id="6264" href="/19.08/Adequacy/#6264" class="Function">above-fun?</a> <a id="6275" class="Symbol">:</a> <a id="6277" class="Symbol">(</a><a id="6278" href="plfa.part3.Adequacy.html#6278" class="Bound">v</a> <a id="6280" class="Symbol">:</a> <a id="6282" href="/19.08/Denotational/#4070" class="Datatype">Value</a><a id="6287" class="Symbol">)</a> <a id="6289" class="Symbol">→</a> <a id="6291" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Nullary.html#605" class="Datatype">Dec</a> <a id="6295" class="Symbol">(</a><a id="6296" href="plfa.part3.Adequacy.html#4069" class="Function">above-fun</a> <a id="6306" href="plfa.part3.Adequacy.html#6278" class="Bound">v</a><a id="6307" class="Symbol">)</a>
<a id="6309" href="/19.08/Adequacy/#6264" class="Function">above-fun?</a> <a id="6320" href="/19.08/Denotational/#4090" class="InductiveConstructor">⊥</a> <a id="6322" class="Symbol">=</a> <a id="6324" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Nullary.html#668" class="InductiveConstructor">no</a> <a id="6327" href="plfa.part3.Adequacy.html#4479" class="Function">above-fun⊥</a>
<a id="6338" href="/19.08/Adequacy/#6264" class="Function">above-fun?</a> <a id="6349" class="Symbol">(</a><a id="6350" href="plfa.part3.Adequacy.html#6350" class="Bound">v</a> <a id="6352" href="/19.08/Denotational/#4102" class="InductiveConstructor Operator">↦</a> <a id="6354" href="plfa.part3.Adequacy.html#6354" class="Bound">w</a><a id="6355" class="Symbol">)</a> <a id="6357" class="Symbol">=</a> <a id="6359" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Nullary.html#641" class="InductiveConstructor">yes</a> <a id="6363" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟨</a> <a id="6365" href="plfa.part3.Adequacy.html#6350" class="Bound">v</a> <a id="6367" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">,</a> <a id="6369" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟨</a> <a id="6371" href="plfa.part3.Adequacy.html#6354" class="Bound">w</a> <a id="6373" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">,</a> <a id="6375" href="plfa.part3.Denotational.html#5557" class="Function">⊑-refl</a> <a id="6382" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟩</a> <a id="6384" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟩</a>
<a id="6386" href="/19.08/Adequacy/#6264" class="Function">above-fun?</a> <a id="6397" class="Symbol">(</a><a id="6398" href="plfa.part3.Adequacy.html#6398" class="Bound">u</a> <a id="6400" href="/19.08/Denotational/#4132" class="InductiveConstructor Operator">⊔</a> <a id="6402" href="plfa.part3.Adequacy.html#6402" class="Bound">u&#39;</a><a id="6404" class="Symbol">)</a>
<a id="6410" class="Keyword">with</a> <a id="6415" href="/19.08/Adequacy/#6264" class="Function">above-fun?</a> <a id="6426" href="plfa.part3.Adequacy.html#6398" class="Bound">u</a> <a id="6428" class="Symbol">|</a> <a id="6430" href="plfa.part3.Adequacy.html#6264" class="Function">above-fun?</a> <a id="6441" href="plfa.part3.Adequacy.html#6402" class="Bound">u&#39;</a>
<a id="6444" class="Symbol">...</a> <a id="6448" class="Symbol">|</a> <a id="6450" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Nullary.html#641" class="InductiveConstructor">yes</a> <a id="6454" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟨</a> <a id="6456" href="/19.08/Adequacy/#6456" class="Bound">v</a> <a id="6458" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">,</a> <a id="6460" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟨</a> <a id="6462" href="plfa.part3.Adequacy.html#6462" class="Bound">w</a> <a id="6464" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">,</a> <a id="6466" href="plfa.part3.Adequacy.html#6466" class="Bound">lt</a> <a id="6469" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟩</a> <a id="6471" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟩</a> <a id="6473" class="Symbol">|</a> <a id="6475" class="Symbol">_</a> <a id="6477" class="Symbol">=</a> <a id="6479" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Nullary.html#641" class="InductiveConstructor">yes</a> <a id="6483" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟨</a> <a id="6485" href="plfa.part3.Adequacy.html#6456" class="Bound">v</a> <a id="6487" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">,</a> <a id="6489" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟨</a> <a id="6491" href="plfa.part3.Adequacy.html#6462" class="Bound">w</a> <a id="6493" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">,</a> <a id="6495" class="Symbol">(</a><a id="6496" href="/19.08/Denotational/#4571" class="InductiveConstructor">⊑-conj-R1</a> <a id="6506" href="plfa.part3.Adequacy.html#6466" class="Bound">lt</a><a id="6508" class="Symbol">)</a> <a id="6510" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟩</a> <a id="6512" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟩</a>
<a id="6514" class="Symbol">...</a> <a id="6518" class="Symbol">|</a> <a id="6520" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Nullary.html#668" class="InductiveConstructor">no</a> <a id="6523" class="Symbol">_</a> <a id="6525" class="Symbol">|</a> <a id="6527" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Nullary.html#641" class="InductiveConstructor">yes</a> <a id="6531" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟨</a> <a id="6533" href="/19.08/Adequacy/#6533" class="Bound">v</a> <a id="6535" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">,</a> <a id="6537" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟨</a> <a id="6539" href="plfa.part3.Adequacy.html#6539" class="Bound">w</a> <a id="6541" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">,</a> <a id="6543" href="plfa.part3.Adequacy.html#6543" class="Bound">lt</a> <a id="6546" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟩</a> <a id="6548" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟩</a> <a id="6550" class="Symbol">=</a> <a id="6552" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Nullary.html#641" class="InductiveConstructor">yes</a> <a id="6556" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟨</a> <a id="6558" href="plfa.part3.Adequacy.html#6533" class="Bound">v</a> <a id="6560" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">,</a> <a id="6562" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟨</a> <a id="6564" href="plfa.part3.Adequacy.html#6539" class="Bound">w</a> <a id="6566" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">,</a> <a id="6568" class="Symbol">(</a><a id="6569" href="/19.08/Denotational/#4644" class="InductiveConstructor">⊑-conj-R2</a> <a id="6579" href="plfa.part3.Adequacy.html#6543" class="Bound">lt</a><a id="6581" class="Symbol">)</a> <a id="6583" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟩</a> <a id="6585" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟩</a>
<a id="6587" class="Symbol">...</a> <a id="6591" class="Symbol">|</a> <a id="6593" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Nullary.html#668" class="InductiveConstructor">no</a> <a id="6596" href="/19.08/Adequacy/#6596" class="Bound">x</a> <a id="6598" class="Symbol">|</a> <a id="6600" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Nullary.html#668" class="InductiveConstructor">no</a> <a id="6603" href="plfa.part3.Adequacy.html#6603" class="Bound">y</a> <a id="6605" class="Symbol">=</a> <a id="6607" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Nullary.html#668" class="InductiveConstructor">no</a> <a id="6610" class="Symbol">(</a><a id="6611" href="plfa.part3.Adequacy.html#5291" class="Function">not-above-fun-⊔</a> <a id="6627" href="plfa.part3.Adequacy.html#6596" class="Bound">x</a> <a id="6629" href="plfa.part3.Adequacy.html#6603" class="Bound">y</a><a id="6630" class="Symbol">)</a>
</pre>
<h2 id="relating-values-to-closures">Relating values to closures</h2>
<p>Next we relate semantic values to closures. The relation <code class="language-plaintext highlighter-rouge">𝕍</code> is for
closures whose term is a lambda abstraction, i.e., in weak-head normal
form (WHNF). The relation 𝔼 is for any closure. Roughly speaking,
<code class="language-plaintext highlighter-rouge">𝔼 v c</code> will hold if, when <code class="language-plaintext highlighter-rouge">v</code> is greater than a function value, <code class="language-plaintext highlighter-rouge">c</code> evaluates
to a closure <code class="language-plaintext highlighter-rouge">c'</code> in WHNF and <code class="language-plaintext highlighter-rouge">𝕍 v c'</code>. Regarding <code class="language-plaintext highlighter-rouge">𝕍 v c</code>, it will hold when
<code class="language-plaintext highlighter-rouge">c</code> is in WHNF, and if <code class="language-plaintext highlighter-rouge">v</code> is a function, the body of <code class="language-plaintext highlighter-rouge">c</code> evaluates
according to <code class="language-plaintext highlighter-rouge">v</code>.</p>
<pre class="Agda"><a id="𝕍"></a><a id="7123" href="/19.08/Adequacy/#7123" class="Function">𝕍</a> <a id="7125" class="Symbol">:</a> <a id="7127" href="/19.08/Denotational/#4070" class="Datatype">Value</a> <a id="7133" class="Symbol">→</a> <a id="7135" href="/19.08/BigStep/#2470" class="Datatype">Clos</a> <a id="7140" class="Symbol">→</a> <a id="7142" class="PrimitiveType">Set</a>
<a id="𝔼"></a><a id="7146" href="/19.08/Adequacy/#7146" class="Function">𝔼</a> <a id="7148" class="Symbol">:</a> <a id="7150" href="/19.08/Denotational/#4070" class="Datatype">Value</a> <a id="7156" class="Symbol">→</a> <a id="7158" href="/19.08/BigStep/#2470" class="Datatype">Clos</a> <a id="7163" class="Symbol">→</a> <a id="7165" class="PrimitiveType">Set</a>
</pre>
<p>We define <code class="language-plaintext highlighter-rouge">𝕍</code> as a function from values and closures to <code class="language-plaintext highlighter-rouge">Set</code> and not as a
data type because it is mutually recursive with <code class="language-plaintext highlighter-rouge">𝔼</code> in a negative
position (to the left of an implication). We first perform case
analysis on the term in the closure. If the term is a variable or
application, then <code class="language-plaintext highlighter-rouge">𝕍</code> is false (<code class="language-plaintext highlighter-rouge">Bot</code>). If the term is a lambda
abstraction, we define <code class="language-plaintext highlighter-rouge">𝕍</code> by recursion on the value, which we
describe below.</p>
<pre class="Agda"><a id="7594" href="/19.08/Adequacy/#7123" class="Function">𝕍</a> <a id="7596" href="plfa.part3.Adequacy.html#7596" class="Bound">v</a> <a id="7598" class="Symbol">(</a><a id="7599" href="/19.08/BigStep/#2489" class="InductiveConstructor">clos</a> <a id="7604" class="Symbol">(</a><a id="7605" href="/19.08/Untyped/#4330" class="InductiveConstructor Operator">`</a> <a id="7607" href="plfa.part3.Adequacy.html#7607" class="Bound">x₁</a><a id="7609" class="Symbol">)</a> <a id="7611" href="plfa.part3.Adequacy.html#7611" class="Bound">γ</a><a id="7612" class="Symbol">)</a> <a id="7614" class="Symbol">=</a> <a id="7616" href="https://agda.github.io/agda-stdlib/v1.1/Data.Empty.html#279" class="Datatype">Bot</a>
<a id="7620" href="/19.08/Adequacy/#7123" class="Function">𝕍</a> <a id="7622" href="plfa.part3.Adequacy.html#7622" class="Bound">v</a> <a id="7624" class="Symbol">(</a><a id="7625" href="/19.08/BigStep/#2489" class="InductiveConstructor">clos</a> <a id="7630" class="Symbol">(</a><a id="7631" href="plfa.part3.Adequacy.html#7631" class="Bound">M</a> <a id="7633" href="/19.08/Untyped/#4442" class="InductiveConstructor Operator">·</a> <a id="7635" href="plfa.part3.Adequacy.html#7635" class="Bound">M₁</a><a id="7637" class="Symbol">)</a> <a id="7639" href="plfa.part3.Adequacy.html#7639" class="Bound">γ</a><a id="7640" class="Symbol">)</a> <a id="7642" class="Symbol">=</a> <a id="7644" href="https://agda.github.io/agda-stdlib/v1.1/Data.Empty.html#279" class="Datatype">Bot</a>
<a id="7648" href="/19.08/Adequacy/#7123" class="Function">𝕍</a> <a id="7650" href="/19.08/Denotational/#4090" class="InductiveConstructor">⊥</a> <a id="7652" class="Symbol">(</a><a id="7653" href="/19.08/BigStep/#2489" class="InductiveConstructor">clos</a> <a id="7658" class="Symbol">(</a><a id="7659" href="/19.08/Untyped/#4382" class="InductiveConstructor Operator">ƛ</a> <a id="7661" href="plfa.part3.Adequacy.html#7661" class="Bound">M</a><a id="7662" class="Symbol">)</a> <a id="7664" href="plfa.part3.Adequacy.html#7664" class="Bound">γ</a><a id="7665" class="Symbol">)</a> <a id="7667" class="Symbol">=</a> <a id="7669" href="Agda.Builtin.Unit.html#137" class="Record">⊤</a>
<a id="7671" href="/19.08/Adequacy/#7123" class="Function">𝕍</a> <a id="7673" class="Symbol">(</a><a id="7674" href="plfa.part3.Adequacy.html#7674" class="Bound">v</a> <a id="7676" href="/19.08/Denotational/#4102" class="InductiveConstructor Operator">↦</a> <a id="7678" href="plfa.part3.Adequacy.html#7678" class="Bound">w</a><a id="7679" class="Symbol">)</a> <a id="7681" class="Symbol">(</a><a id="7682" href="/19.08/BigStep/#2489" class="InductiveConstructor">clos</a> <a id="7687" class="Symbol">(</a><a id="7688" href="/19.08/Untyped/#4382" class="InductiveConstructor Operator">ƛ</a> <a id="7690" href="plfa.part3.Adequacy.html#7690" class="Bound">N</a><a id="7691" class="Symbol">)</a> <a id="7693" href="plfa.part3.Adequacy.html#7693" class="Bound">γ</a><a id="7694" class="Symbol">)</a> <a id="7696" class="Symbol">=</a>
<a id="7702" class="Symbol">(∀{</a><a id="7705" href="/19.08/Adequacy/#7705" class="Bound">c</a> <a id="7707" class="Symbol">:</a> <a id="7709" href="/19.08/BigStep/#2470" class="Datatype">Clos</a><a id="7713" class="Symbol">}</a> <a id="7715" class="Symbol">→</a> <a id="7717" href="plfa.part3.Adequacy.html#7146" class="Function">𝔼</a> <a id="7719" href="plfa.part3.Adequacy.html#7674" class="Bound">v</a> <a id="7721" href="plfa.part3.Adequacy.html#7705" class="Bound">c</a> <a id="7723" class="Symbol">→</a> <a id="7725" href="plfa.part3.Adequacy.html#4069" class="Function">above-fun</a> <a id="7735" href="plfa.part3.Adequacy.html#7678" class="Bound">w</a> <a id="7737" class="Symbol">→</a> <a id="7739" href="https://agda.github.io/agda-stdlib/v1.1/Data.Product.html#911" class="Function">Σ[</a> <a id="7742" href="plfa.part3.Adequacy.html#7742" class="Bound">c&#39;</a> <a id="7745" href="https://agda.github.io/agda-stdlib/v1.1/Data.Product.html#911" class="Function">∈</a> <a id="7747" href="plfa.part2.BigStep.html#2470" class="Datatype">Clos</a> <a id="7752" href="https://agda.github.io/agda-stdlib/v1.1/Data.Product.html#911" class="Function">]</a>
<a id="7762" class="Symbol">(</a><a id="7763" href="/19.08/Adequacy/#7693" class="Bound">γ</a> <a id="7765" href="/19.08/BigStep/#2675" class="Function Operator">,&#39;</a> <a id="7768" href="plfa.part3.Adequacy.html#7705" class="Bound">c</a><a id="7769" class="Symbol">)</a> <a id="7771" href="plfa.part2.BigStep.html#3024" class="Datatype Operator">⊢</a> <a id="7773" href="plfa.part3.Adequacy.html#7690" class="Bound">N</a> <a id="7775" href="plfa.part2.BigStep.html#3024" class="Datatype Operator">⇓</a> <a id="7777" href="plfa.part3.Adequacy.html#7742" class="Bound">c&#39;</a> <a id="7781" href="https://agda.github.io/agda-stdlib/v1.1/Data.Product.html#1162" class="Function Operator">×</a> <a id="7784" href="plfa.part3.Adequacy.html#7123" class="Function">𝕍</a> <a id="7786" href="plfa.part3.Adequacy.html#7678" class="Bound">w</a> <a id="7788" href="plfa.part3.Adequacy.html#7742" class="Bound">c&#39;</a><a id="7790" class="Symbol">)</a>
<a id="7792" href="/19.08/Adequacy/#7123" class="Function">𝕍</a> <a id="7794" class="Symbol">(</a><a id="7795" href="plfa.part3.Adequacy.html#7795" class="Bound">u</a> <a id="7797" href="/19.08/Denotational/#4132" class="InductiveConstructor Operator">⊔</a> <a id="7799" href="plfa.part3.Adequacy.html#7799" class="Bound">v</a><a id="7800" class="Symbol">)</a> <a id="7802" class="Symbol">(</a><a id="7803" href="/19.08/BigStep/#2489" class="InductiveConstructor">clos</a> <a id="7808" class="Symbol">(</a><a id="7809" href="/19.08/Untyped/#4382" class="InductiveConstructor Operator">ƛ</a> <a id="7811" href="plfa.part3.Adequacy.html#7811" class="Bound">N</a><a id="7812" class="Symbol">)</a> <a id="7814" href="plfa.part3.Adequacy.html#7814" class="Bound">γ</a><a id="7815" class="Symbol">)</a> <a id="7817" class="Symbol">=</a> <a id="7819" href="plfa.part3.Adequacy.html#7123" class="Function">𝕍</a> <a id="7821" href="plfa.part3.Adequacy.html#7795" class="Bound">u</a> <a id="7823" class="Symbol">(</a><a id="7824" href="plfa.part2.BigStep.html#2489" class="InductiveConstructor">clos</a> <a id="7829" class="Symbol">(</a><a id="7830" href="plfa.part2.Untyped.html#4382" class="InductiveConstructor Operator">ƛ</a> <a id="7832" href="plfa.part3.Adequacy.html#7811" class="Bound">N</a><a id="7833" class="Symbol">)</a> <a id="7835" href="plfa.part3.Adequacy.html#7814" class="Bound">γ</a><a id="7836" class="Symbol">)</a> <a id="7838" href="https://agda.github.io/agda-stdlib/v1.1/Data.Product.html#1162" class="Function Operator">×</a> <a id="7840" href="plfa.part3.Adequacy.html#7123" class="Function">𝕍</a> <a id="7842" href="plfa.part3.Adequacy.html#7799" class="Bound">v</a> <a id="7844" class="Symbol">(</a><a id="7845" href="plfa.part2.BigStep.html#2489" class="InductiveConstructor">clos</a> <a id="7850" class="Symbol">(</a><a id="7851" href="plfa.part2.Untyped.html#4382" class="InductiveConstructor Operator">ƛ</a> <a id="7853" href="plfa.part3.Adequacy.html#7811" class="Bound">N</a><a id="7854" class="Symbol">)</a> <a id="7856" href="plfa.part3.Adequacy.html#7814" class="Bound">γ</a><a id="7857" class="Symbol">)</a>
</pre>
<ul>
<li>
<p>If the value is <code class="language-plaintext highlighter-rouge">⊥</code>, then the result is true (<code class="language-plaintext highlighter-rouge">⊤</code>).</p>
</li>
<li>
<p>If the value is a join (u ⊔ v), then the result is the pair
(conjunction) of 𝕍 is true for both u and v.</p>
</li>
<li>
<p>The important case is for a function value <code class="language-plaintext highlighter-rouge">v ↦ w</code> and closure
<code class="language-plaintext highlighter-rouge">clos (ƛ N) γ</code>. Given any closure <code class="language-plaintext highlighter-rouge">c</code> such that <code class="language-plaintext highlighter-rouge">𝔼 v c</code>, if <code class="language-plaintext highlighter-rouge">w</code> is
greater than a function, then <code class="language-plaintext highlighter-rouge">N</code> evaluates (with <code class="language-plaintext highlighter-rouge">γ</code> extended with <code class="language-plaintext highlighter-rouge">c</code>)
to some closure <code class="language-plaintext highlighter-rouge">c'</code> and we have <code class="language-plaintext highlighter-rouge">𝕍 w c'</code>.</p>
</li>
</ul>
<p>The definition of <code class="language-plaintext highlighter-rouge">𝔼</code> is straightforward. If <code class="language-plaintext highlighter-rouge">v</code> is a greater than a
function, then <code class="language-plaintext highlighter-rouge">M</code> evaluates to a closure related to <code class="language-plaintext highlighter-rouge">v</code>.</p>
<pre class="Agda"><a id="8417" href="/19.08/Adequacy/#7146" class="Function">𝔼</a> <a id="8419" href="plfa.part3.Adequacy.html#8419" class="Bound">v</a> <a id="8421" class="Symbol">(</a><a id="8422" href="/19.08/BigStep/#2489" class="InductiveConstructor">clos</a> <a id="8427" href="plfa.part3.Adequacy.html#8427" class="Bound">M</a> <a id="8429" href="plfa.part3.Adequacy.html#8429" class="Bound">γ&#39;</a><a id="8431" class="Symbol">)</a> <a id="8433" class="Symbol">=</a> <a id="8435" href="plfa.part3.Adequacy.html#4069" class="Function">above-fun</a> <a id="8445" href="plfa.part3.Adequacy.html#8419" class="Bound">v</a> <a id="8447" class="Symbol">→</a> <a id="8449" href="https://agda.github.io/agda-stdlib/v1.1/Data.Product.html#911" class="Function">Σ[</a> <a id="8452" href="plfa.part3.Adequacy.html#8452" class="Bound">c</a> <a id="8454" href="https://agda.github.io/agda-stdlib/v1.1/Data.Product.html#911" class="Function">∈</a> <a id="8456" href="plfa.part2.BigStep.html#2470" class="Datatype">Clos</a> <a id="8461" href="https://agda.github.io/agda-stdlib/v1.1/Data.Product.html#911" class="Function">]</a> <a id="8463" href="plfa.part3.Adequacy.html#8429" class="Bound">γ&#39;</a> <a id="8466" href="plfa.part2.BigStep.html#3024" class="Datatype Operator">⊢</a> <a id="8468" href="plfa.part3.Adequacy.html#8427" class="Bound">M</a> <a id="8470" href="plfa.part2.BigStep.html#3024" class="Datatype Operator">⇓</a> <a id="8472" href="plfa.part3.Adequacy.html#8452" class="Bound">c</a> <a id="8474" href="https://agda.github.io/agda-stdlib/v1.1/Data.Product.html#1162" class="Function Operator">×</a> <a id="8476" href="plfa.part3.Adequacy.html#7123" class="Function">𝕍</a> <a id="8478" href="plfa.part3.Adequacy.html#8419" class="Bound">v</a> <a id="8480" href="plfa.part3.Adequacy.html#8452" class="Bound">c</a>
</pre>
<p>The proof of the main lemma is by induction on <code class="language-plaintext highlighter-rouge">γ ⊢ M ↓ v</code>, so it goes
underneath lambda abstractions and must therefore reason about open
terms (terms with variables). So we must relate environments of
semantic values to environments of closures. In the following, <code class="language-plaintext highlighter-rouge">𝔾</code>
relates <code class="language-plaintext highlighter-rouge">γ</code> to <code class="language-plaintext highlighter-rouge">γ'</code> if the corresponding values and closures are related
by <code class="language-plaintext highlighter-rouge">𝔼</code>.</p>
<pre class="Agda"><a id="𝔾"></a><a id="8844" href="/19.08/Adequacy/#8844" class="Function">𝔾</a> <a id="8846" class="Symbol">:</a> <a id="8848" class="Symbol">∀{</a><a id="8850" href="plfa.part3.Adequacy.html#8850" class="Bound">Γ</a><a id="8851" class="Symbol">}</a> <a id="8853" class="Symbol">→</a> <a id="8855" href="/19.08/Denotational/#7207" class="Function">Env</a> <a id="8859" href="plfa.part3.Adequacy.html#8850" class="Bound">Γ</a> <a id="8861" class="Symbol">→</a> <a id="8863" href="/19.08/BigStep/#2440" class="Function">ClosEnv</a> <a id="8871" href="plfa.part3.Adequacy.html#8850" class="Bound">Γ</a> <a id="8873" class="Symbol">→</a> <a id="8875" class="PrimitiveType">Set</a>
<a id="8879" href="/19.08/Adequacy/#8844" class="Function">𝔾</a> <a id="8881" class="Symbol">{</a><a id="8882" href="plfa.part3.Adequacy.html#8882" class="Bound">Γ</a><a id="8883" class="Symbol">}</a> <a id="8885" href="plfa.part3.Adequacy.html#8885" class="Bound">γ</a> <a id="8887" href="plfa.part3.Adequacy.html#8887" class="Bound">γ&#39;</a> <a id="8890" class="Symbol">=</a> <a id="8892" class="Symbol">∀{</a><a id="8894" href="plfa.part3.Adequacy.html#8894" class="Bound">x</a> <a id="8896" class="Symbol">:</a> <a id="8898" href="plfa.part3.Adequacy.html#8882" class="Bound">Γ</a> <a id="8900" href="/19.08/Untyped/#3521" class="Datatype Operator">∋</a> <a id="8902" href="plfa.part2.Untyped.html#2888" class="InductiveConstructor">★</a><a id="8903" class="Symbol">}</a> <a id="8905" class="Symbol">→</a> <a id="8907" href="plfa.part3.Adequacy.html#7146" class="Function">𝔼</a> <a id="8909" class="Symbol">(</a><a id="8910" href="plfa.part3.Adequacy.html#8885" class="Bound">γ</a> <a id="8912" href="plfa.part3.Adequacy.html#8894" class="Bound">x</a><a id="8913" class="Symbol">)</a> <a id="8915" class="Symbol">(</a><a id="8916" href="plfa.part3.Adequacy.html#8887" class="Bound">γ&#39;</a> <a id="8919" href="plfa.part3.Adequacy.html#8894" class="Bound">x</a><a id="8920" class="Symbol">)</a>
<a id="𝔾-∅"></a><a id="8923" href="/19.08/Adequacy/#8923" class="Function">𝔾-∅</a> <a id="8927" class="Symbol">:</a> <a id="8929" href="plfa.part3.Adequacy.html#8844" class="Function">𝔾</a> <a id="8931" href="/19.08/Denotational/#7331" class="Function">`∅</a> <a id="8934" href="/19.08/BigStep/#2653" class="Function">∅&#39;</a>
<a id="8937" href="/19.08/Adequacy/#8923" class="Function">𝔾-∅</a> <a id="8941" class="Symbol">{()}</a>
<a id="𝔾-ext"></a><a id="8947" href="/19.08/Adequacy/#8947" class="Function">𝔾-ext</a> <a id="8953" class="Symbol">:</a> <a id="8955" class="Symbol">∀{</a><a id="8957" href="plfa.part3.Adequacy.html#8957" class="Bound">Γ</a><a id="8958" class="Symbol">}{</a><a id="8960" href="plfa.part3.Adequacy.html#8960" class="Bound">γ</a> <a id="8962" class="Symbol">:</a> <a id="8964" href="/19.08/Denotational/#7207" class="Function">Env</a> <a id="8968" href="plfa.part3.Adequacy.html#8957" class="Bound">Γ</a><a id="8969" class="Symbol">}{</a><a id="8971" href="plfa.part3.Adequacy.html#8971" class="Bound">γ&#39;</a> <a id="8974" class="Symbol">:</a> <a id="8976" href="/19.08/BigStep/#2440" class="Function">ClosEnv</a> <a id="8984" href="plfa.part3.Adequacy.html#8957" class="Bound">Γ</a><a id="8985" class="Symbol">}{</a><a id="8987" href="plfa.part3.Adequacy.html#8987" class="Bound">v</a> <a id="8989" href="plfa.part3.Adequacy.html#8989" class="Bound">c</a><a id="8990" class="Symbol">}</a>
<a id="8998" class="Symbol">→</a> <a id="9000" href="/19.08/Adequacy/#8844" class="Function">𝔾</a> <a id="9002" href="plfa.part3.Adequacy.html#8960" class="Bound">γ</a> <a id="9004" href="plfa.part3.Adequacy.html#8971" class="Bound">γ&#39;</a> <a id="9007" class="Symbol">→</a> <a id="9009" href="plfa.part3.Adequacy.html#7146" class="Function">𝔼</a> <a id="9011" href="plfa.part3.Adequacy.html#8987" class="Bound">v</a> <a id="9013" href="plfa.part3.Adequacy.html#8989" class="Bound">c</a> <a id="9015" class="Symbol">→</a> <a id="9017" href="plfa.part3.Adequacy.html#8844" class="Function">𝔾</a> <a id="9019" class="Symbol">(</a><a id="9020" href="plfa.part3.Adequacy.html#8960" class="Bound">γ</a> <a id="9022" href="/19.08/Denotational/#7364" class="Function Operator">`,</a> <a id="9025" href="plfa.part3.Adequacy.html#8987" class="Bound">v</a><a id="9026" class="Symbol">)</a> <a id="9028" class="Symbol">(</a><a id="9029" href="plfa.part3.Adequacy.html#8971" class="Bound">γ&#39;</a> <a id="9032" href="/19.08/BigStep/#2675" class="Function Operator">,&#39;</a> <a id="9035" href="plfa.part3.Adequacy.html#8989" class="Bound">c</a><a id="9036" class="Symbol">)</a>
<a id="9038" href="/19.08/Adequacy/#8947" class="Function">𝔾-ext</a> <a id="9044" class="Symbol">{</a><a id="9045" href="plfa.part3.Adequacy.html#9045" class="Bound">Γ</a><a id="9046" class="Symbol">}</a> <a id="9048" class="Symbol">{</a><a id="9049" href="plfa.part3.Adequacy.html#9049" class="Bound">γ</a><a id="9050" class="Symbol">}</a> <a id="9052" class="Symbol">{</a><a id="9053" href="plfa.part3.Adequacy.html#9053" class="Bound">γ&#39;</a><a id="9055" class="Symbol">}</a> <a id="9057" href="plfa.part3.Adequacy.html#9057" class="Bound">g</a> <a id="9059" href="plfa.part3.Adequacy.html#9059" class="Bound">e</a> <a id="9061" class="Symbol">{</a><a id="9062" href="/19.08/Untyped/#3557" class="InductiveConstructor">Z</a><a id="9063" class="Symbol">}</a> <a id="9065" class="Symbol">=</a> <a id="9067" href="plfa.part3.Adequacy.html#9059" class="Bound">e</a>
<a id="9069" href="/19.08/Adequacy/#8947" class="Function">𝔾-ext</a> <a id="9075" class="Symbol">{</a><a id="9076" href="plfa.part3.Adequacy.html#9076" class="Bound">Γ</a><a id="9077" class="Symbol">}</a> <a id="9079" class="Symbol">{</a><a id="9080" href="plfa.part3.Adequacy.html#9080" class="Bound">γ</a><a id="9081" class="Symbol">}</a> <a id="9083" class="Symbol">{</a><a id="9084" href="plfa.part3.Adequacy.html#9084" class="Bound">γ&#39;</a><a id="9086" class="Symbol">}</a> <a id="9088" href="plfa.part3.Adequacy.html#9088" class="Bound">g</a> <a id="9090" href="plfa.part3.Adequacy.html#9090" class="Bound">e</a> <a id="9092" class="Symbol">{</a><a id="9093" href="/19.08/Untyped/#3602" class="InductiveConstructor Operator">S</a> <a id="9095" href="plfa.part3.Adequacy.html#9095" class="Bound">x</a><a id="9096" class="Symbol">}</a> <a id="9098" class="Symbol">=</a> <a id="9100" href="plfa.part3.Adequacy.html#9088" class="Bound">g</a>
</pre>
<p>We need a few properties of the <code class="language-plaintext highlighter-rouge">𝕍</code> and <code class="language-plaintext highlighter-rouge">𝔼</code> relations. The first is that
a closure in the <code class="language-plaintext highlighter-rouge">𝕍</code> relation must be in weak-head normal form. We
define WHNF has follows.</p>
<pre class="Agda"><a id="9280" class="Keyword">data</a> <a id="WHNF"></a><a id="9285" href="/19.08/Adequacy/#9285" class="Datatype">WHNF</a> <a id="9290" class="Symbol">:</a> <a id="9292" class="Symbol">∀</a> <a id="9294" class="Symbol">{</a><a id="9295" href="plfa.part3.Adequacy.html#9295" class="Bound">Γ</a> <a id="9297" href="plfa.part3.Adequacy.html#9297" class="Bound">A</a><a id="9298" class="Symbol">}</a> <a id="9300" class="Symbol">→</a> <a id="9302" href="plfa.part3.Adequacy.html#9295" class="Bound">Γ</a> <a id="9304" href="/19.08/Untyped/#4294" class="Datatype Operator">⊢</a> <a id="9306" href="plfa.part3.Adequacy.html#9297" class="Bound">A</a> <a id="9308" class="Symbol">→</a> <a id="9310" class="PrimitiveType">Set</a> <a id="9314" class="Keyword">where</a>
<a id="WHNF.ƛ_"></a><a id="9322" href="/19.08/Adequacy/#9322" class="InductiveConstructor Operator">ƛ_</a> <a id="9325" class="Symbol">:</a> <a id="9327" class="Symbol">∀</a> <a id="9329" class="Symbol">{</a><a id="9330" href="plfa.part3.Adequacy.html#9330" class="Bound">Γ</a><a id="9331" class="Symbol">}</a> <a id="9333" class="Symbol">{</a><a id="9334" href="plfa.part3.Adequacy.html#9334" class="Bound">N</a> <a id="9336" class="Symbol">:</a> <a id="9338" href="plfa.part3.Adequacy.html#9330" class="Bound">Γ</a> <a id="9340" href="/19.08/Untyped/#3191" class="InductiveConstructor Operator">,</a> <a id="9342" href="plfa.part2.Untyped.html#2888" class="InductiveConstructor">★</a> <a id="9344" href="plfa.part2.Untyped.html#4294" class="Datatype Operator">⊢</a> <a id="9346" href="plfa.part2.Untyped.html#2888" class="InductiveConstructor">★</a><a id="9347" class="Symbol">}</a>
<a id="9354" class="Symbol">→</a> <a id="9356" href="/19.08/Adequacy/#9285" class="Datatype">WHNF</a> <a id="9361" class="Symbol">(</a><a id="9362" href="/19.08/Untyped/#4382" class="InductiveConstructor Operator">ƛ</a> <a id="9364" href="plfa.part3.Adequacy.html#9334" class="Bound">N</a><a id="9365" class="Symbol">)</a>
</pre>
<p>The proof goes by cases on the term in the closure.</p>
<pre class="Agda"><a id="𝕍→WHNF"></a><a id="9429" href="/19.08/Adequacy/#9429" class="Function">𝕍→WHNF</a> <a id="9436" class="Symbol">:</a> <a id="9438" class="Symbol">∀{</a><a id="9440" href="plfa.part3.Adequacy.html#9440" class="Bound">Γ</a><a id="9441" class="Symbol">}{</a><a id="9443" href="plfa.part3.Adequacy.html#9443" class="Bound">γ</a> <a id="9445" class="Symbol">:</a> <a id="9447" href="/19.08/BigStep/#2440" class="Function">ClosEnv</a> <a id="9455" href="plfa.part3.Adequacy.html#9440" class="Bound">Γ</a><a id="9456" class="Symbol">}{</a><a id="9458" href="plfa.part3.Adequacy.html#9458" class="Bound">M</a> <a id="9460" class="Symbol">:</a> <a id="9462" href="plfa.part3.Adequacy.html#9440" class="Bound">Γ</a> <a id="9464" href="/19.08/Untyped/#4294" class="Datatype Operator">⊢</a> <a id="9466" href="plfa.part2.Untyped.html#2888" class="InductiveConstructor">★</a><a id="9467" class="Symbol">}{</a><a id="9469" href="plfa.part3.Adequacy.html#9469" class="Bound">v</a><a id="9470" class="Symbol">}</a>
<a id="9479" class="Symbol">→</a> <a id="9481" href="/19.08/Adequacy/#7123" class="Function">𝕍</a> <a id="9483" href="plfa.part3.Adequacy.html#9469" class="Bound">v</a> <a id="9485" class="Symbol">(</a><a id="9486" href="/19.08/BigStep/#2489" class="InductiveConstructor">clos</a> <a id="9491" href="plfa.part3.Adequacy.html#9458" class="Bound">M</a> <a id="9493" href="plfa.part3.Adequacy.html#9443" class="Bound">γ</a><a id="9494" class="Symbol">)</a> <a id="9496" class="Symbol">→</a> <a id="9498" href="plfa.part3.Adequacy.html#9285" class="Datatype">WHNF</a> <a id="9503" href="plfa.part3.Adequacy.html#9458" class="Bound">M</a>
<a id="9505" href="/19.08/Adequacy/#9429" class="Function">𝕍→WHNF</a> <a id="9512" class="Symbol">{</a><a id="9513" class="Argument">M</a> <a id="9515" class="Symbol">=</a> <a id="9517" href="/19.08/Untyped/#4330" class="InductiveConstructor Operator">`</a> <a id="9519" href="plfa.part3.Adequacy.html#9519" class="Bound">x</a><a id="9520" class="Symbol">}</a> <a id="9522" class="Symbol">{</a><a id="9523" href="plfa.part3.Adequacy.html#9523" class="Bound">v</a><a id="9524" class="Symbol">}</a> <a id="9526" class="Symbol">()</a>
<a id="9529" href="/19.08/Adequacy/#9429" class="Function">𝕍→WHNF</a> <a id="9536" class="Symbol">{</a><a id="9537" class="Argument">M</a> <a id="9539" class="Symbol">=</a> <a id="9541" href="/19.08/Untyped/#4382" class="InductiveConstructor Operator">ƛ</a> <a id="9543" href="plfa.part3.Adequacy.html#9543" class="Bound">N</a><a id="9544" class="Symbol">}</a> <a id="9546" class="Symbol">{</a><a id="9547" href="plfa.part3.Adequacy.html#9547" class="Bound">v</a><a id="9548" class="Symbol">}</a> <a id="9550" href="plfa.part3.Adequacy.html#9550" class="Bound">vc</a> <a id="9553" class="Symbol">=</a> <a id="9555" href="plfa.part3.Adequacy.html#9322" class="InductiveConstructor Operator">ƛ_</a>
<a id="9558" href="/19.08/Adequacy/#9429" class="Function">𝕍→WHNF</a> <a id="9565" class="Symbol">{</a><a id="9566" class="Argument">M</a> <a id="9568" class="Symbol">=</a> <a id="9570" href="plfa.part3.Adequacy.html#9570" class="Bound">L</a> <a id="9572" href="/19.08/Untyped/#4442" class="InductiveConstructor Operator">·</a> <a id="9574" href="plfa.part3.Adequacy.html#9574" class="Bound">M</a><a id="9575" class="Symbol">}</a> <a id="9577" class="Symbol">{</a><a id="9578" href="plfa.part3.Adequacy.html#9578" class="Bound">v</a><a id="9579" class="Symbol">}</a> <a id="9581" class="Symbol">()</a>
</pre>
<p>Next we have an introduction rule for <code class="language-plaintext highlighter-rouge">𝕍</code> that mimics the <code class="language-plaintext highlighter-rouge">⊔-intro</code>
rule. If both <code class="language-plaintext highlighter-rouge">u</code> and <code class="language-plaintext highlighter-rouge">v</code> are related to a closure <code class="language-plaintext highlighter-rouge">c</code>, then their join is
too.</p>
<pre class="Agda"><a id="𝕍⊔-intro"></a><a id="9742" href="/19.08/Adequacy/#9742" class="Function">𝕍⊔-intro</a> <a id="9751" class="Symbol">:</a> <a id="9753" class="Symbol">∀{</a><a id="9755" href="plfa.part3.Adequacy.html#9755" class="Bound">c</a> <a id="9757" href="plfa.part3.Adequacy.html#9757" class="Bound">u</a> <a id="9759" href="plfa.part3.Adequacy.html#9759" class="Bound">v</a><a id="9760" class="Symbol">}</a>
<a id="9771" class="Symbol">→</a> <a id="9773" href="/19.08/Adequacy/#7123" class="Function">𝕍</a> <a id="9775" href="plfa.part3.Adequacy.html#9757" class="Bound">u</a> <a id="9777" href="plfa.part3.Adequacy.html#9755" class="Bound">c</a> <a id="9779" class="Symbol">→</a> <a id="9781" href="plfa.part3.Adequacy.html#7123" class="Function">𝕍</a> <a id="9783" href="plfa.part3.Adequacy.html#9759" class="Bound">v</a> <a id="9785" href="plfa.part3.Adequacy.html#9755" class="Bound">c</a>
<a id="9798" class="Comment">---------------</a>
<a id="9823" class="Symbol">→</a> <a id="9825" href="/19.08/Adequacy/#7123" class="Function">𝕍</a> <a id="9827" class="Symbol">(</a><a id="9828" href="plfa.part3.Adequacy.html#9757" class="Bound">u</a> <a id="9830" href="/19.08/Denotational/#4132" class="InductiveConstructor Operator">⊔</a> <a id="9832" href="plfa.part3.Adequacy.html#9759" class="Bound">v</a><a id="9833" class="Symbol">)</a> <a id="9835" href="plfa.part3.Adequacy.html#9755" class="Bound">c</a>
<a id="9837" href="/19.08/Adequacy/#9742" class="Function">𝕍⊔-intro</a> <a id="9846" class="Symbol">{</a><a id="9847" href="/19.08/BigStep/#2489" class="InductiveConstructor">clos</a> <a id="9852" class="Symbol">(</a><a id="9853" href="/19.08/Untyped/#4330" class="InductiveConstructor Operator">`</a> <a id="9855" href="plfa.part3.Adequacy.html#9855" class="Bound">x</a><a id="9856" class="Symbol">)</a> <a id="9858" href="plfa.part3.Adequacy.html#9858" class="Bound">γ</a><a id="9859" class="Symbol">}</a> <a id="9861" class="Symbol">()</a> <a id="9864" href="plfa.part3.Adequacy.html#9864" class="Bound">vc</a>
<a id="9867" href="/19.08/Adequacy/#9742" class="Function">𝕍⊔-intro</a> <a id="9876" class="Symbol">{</a><a id="9877" href="/19.08/BigStep/#2489" class="InductiveConstructor">clos</a> <a id="9882" class="Symbol">(</a><a id="9883" href="/19.08/Untyped/#4382" class="InductiveConstructor Operator">ƛ</a> <a id="9885" href="plfa.part3.Adequacy.html#9885" class="Bound">N</a><a id="9886" class="Symbol">)</a> <a id="9888" href="plfa.part3.Adequacy.html#9888" class="Bound">γ</a><a id="9889" class="Symbol">}</a> <a id="9891" href="plfa.part3.Adequacy.html#9891" class="Bound">uc</a> <a id="9894" href="plfa.part3.Adequacy.html#9894" class="Bound">vc</a> <a id="9897" class="Symbol">=</a> <a id="9899" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟨</a> <a id="9901" href="plfa.part3.Adequacy.html#9891" class="Bound">uc</a> <a id="9904" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">,</a> <a id="9906" href="plfa.part3.Adequacy.html#9894" class="Bound">vc</a> <a id="9909" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟩</a>
<a id="9911" href="/19.08/Adequacy/#9742" class="Function">𝕍⊔-intro</a> <a id="9920" class="Symbol">{</a><a id="9921" href="/19.08/BigStep/#2489" class="InductiveConstructor">clos</a> <a id="9926" class="Symbol">(</a><a id="9927" href="plfa.part3.Adequacy.html#9927" class="Bound">L</a> <a id="9929" href="/19.08/Untyped/#4442" class="InductiveConstructor Operator">·</a> <a id="9931" href="plfa.part3.Adequacy.html#9931" class="Bound">M</a><a id="9932" class="Symbol">)</a> <a id="9934" href="plfa.part3.Adequacy.html#9934" class="Bound">γ</a><a id="9935" class="Symbol">}</a> <a id="9937" class="Symbol">()</a> <a id="9940" href="plfa.part3.Adequacy.html#9940" class="Bound">vc</a>
</pre>
<p>In a moment we prove that <code class="language-plaintext highlighter-rouge">𝕍</code> is preserved when going from a greater
value to a lesser value: if <code class="language-plaintext highlighter-rouge">𝕍 v c</code> and <code class="language-plaintext highlighter-rouge">v' ⊑ v</code>, then <code class="language-plaintext highlighter-rouge">𝕍 v' c</code>.
This property, named <code class="language-plaintext highlighter-rouge">𝕍-sub</code>, is needed by the main lemma in
the case for the <code class="language-plaintext highlighter-rouge">sub</code> rule.</p>
<p>To prove <code class="language-plaintext highlighter-rouge">𝕍-sub</code>, we in turn need the following property concerning
values that are not greater than a function, that is, values that are
equivalent to <code class="language-plaintext highlighter-rouge">⊥</code>. In such cases, <code class="language-plaintext highlighter-rouge">𝕍 v (clos (ƛ N) γ')</code> is trivially true.</p>
<pre class="Agda"><a id="not-above-fun-𝕍"></a><a id="10391" href="/19.08/Adequacy/#10391" class="Function">not-above-fun-𝕍</a> <a id="10407" class="Symbol">:</a> <a id="10409" class="Symbol">∀{</a><a id="10411" href="plfa.part3.Adequacy.html#10411" class="Bound">v</a> <a id="10413" class="Symbol">:</a> <a id="10415" href="/19.08/Denotational/#4070" class="Datatype">Value</a><a id="10420" class="Symbol">}{</a><a id="10422" href="plfa.part3.Adequacy.html#10422" class="Bound">Γ</a><a id="10423" class="Symbol">}{</a><a id="10425" href="plfa.part3.Adequacy.html#10425" class="Bound">γ&#39;</a> <a id="10428" class="Symbol">:</a> <a id="10430" href="/19.08/BigStep/#2440" class="Function">ClosEnv</a> <a id="10438" href="plfa.part3.Adequacy.html#10422" class="Bound">Γ</a><a id="10439" class="Symbol">}{</a><a id="10441" href="plfa.part3.Adequacy.html#10441" class="Bound">N</a> <a id="10443" class="Symbol">:</a> <a id="10445" href="plfa.part3.Adequacy.html#10422" class="Bound">Γ</a> <a id="10447" href="/19.08/Untyped/#3191" class="InductiveConstructor Operator">,</a> <a id="10449" href="plfa.part2.Untyped.html#2888" class="InductiveConstructor">★</a> <a id="10451" href="plfa.part2.Untyped.html#4294" class="Datatype Operator">⊢</a> <a id="10453" href="plfa.part2.Untyped.html#2888" class="InductiveConstructor">★</a> <a id="10455" class="Symbol">}</a>
<a id="10461" class="Symbol">→</a> <a id="10463" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Nullary.html#535" class="Function Operator">¬</a> <a id="10465" href="/19.08/Adequacy/#4069" class="Function">above-fun</a> <a id="10475" href="plfa.part3.Adequacy.html#10411" class="Bound">v</a>
<a id="10483" class="Comment">-------------------</a>
<a id="10507" class="Symbol">→</a> <a id="10509" href="/19.08/Adequacy/#7123" class="Function">𝕍</a> <a id="10511" href="plfa.part3.Adequacy.html#10411" class="Bound">v</a> <a id="10513" class="Symbol">(</a><a id="10514" href="/19.08/BigStep/#2489" class="InductiveConstructor">clos</a> <a id="10519" class="Symbol">(</a><a id="10520" href="/19.08/Untyped/#4382" class="InductiveConstructor Operator">ƛ</a> <a id="10522" href="plfa.part3.Adequacy.html#10441" class="Bound">N</a><a id="10523" class="Symbol">)</a> <a id="10525" href="plfa.part3.Adequacy.html#10425" class="Bound">γ&#39;</a><a id="10527" class="Symbol">)</a>
<a id="10529" href="/19.08/Adequacy/#10391" class="Function">not-above-fun-𝕍</a> <a id="10545" class="Symbol">{</a><a id="10546" href="/19.08/Denotational/#4090" class="InductiveConstructor">⊥</a><a id="10547" class="Symbol">}</a> <a id="10549" href="plfa.part3.Adequacy.html#10549" class="Bound">af</a> <a id="10552" class="Symbol">=</a> <a id="10554" href="Agda.Builtin.Unit.html#174" class="InductiveConstructor">tt</a>
<a id="10557" href="/19.08/Adequacy/#10391" class="Function">not-above-fun-𝕍</a> <a id="10573" class="Symbol">{</a><a id="10574" href="plfa.part3.Adequacy.html#10574" class="Bound">v</a> <a id="10576" href="/19.08/Denotational/#4102" class="InductiveConstructor Operator">↦</a> <a id="10578" href="plfa.part3.Adequacy.html#10578" class="Bound">v&#39;</a><a id="10580" class="Symbol">}</a> <a id="10582" href="plfa.part3.Adequacy.html#10582" class="Bound">af</a> <a id="10585" class="Symbol">=</a> <a id="10587" href="https://agda.github.io/agda-stdlib/v1.1/Data.Empty.html#294" class="Function">⊥-elim</a> <a id="10594" class="Symbol">(</a><a id="10595" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Nullary.Negation.html#809" class="Function">contradiction</a> <a id="10609" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟨</a> <a id="10611" href="plfa.part3.Adequacy.html#10574" class="Bound">v</a> <a id="10613" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">,</a> <a id="10615" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟨</a> <a id="10617" href="plfa.part3.Adequacy.html#10578" class="Bound">v&#39;</a> <a id="10620" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">,</a> <a id="10622" href="plfa.part3.Denotational.html#5557" class="Function">⊑-refl</a> <a id="10629" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟩</a> <a id="10631" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟩</a> <a id="10633" href="plfa.part3.Adequacy.html#10582" class="Bound">af</a><a id="10635" class="Symbol">)</a>
<a id="10637" href="/19.08/Adequacy/#10391" class="Function">not-above-fun-𝕍</a> <a id="10653" class="Symbol">{</a><a id="10654" href="plfa.part3.Adequacy.html#10654" class="Bound">v₁</a> <a id="10657" href="/19.08/Denotational/#4132" class="InductiveConstructor Operator">⊔</a> <a id="10659" href="plfa.part3.Adequacy.html#10659" class="Bound">v₂</a><a id="10661" class="Symbol">}</a> <a id="10663" href="plfa.part3.Adequacy.html#10663" class="Bound">af</a>
<a id="10670" class="Keyword">with</a> <a id="10675" href="/19.08/Adequacy/#5674" class="Function">not-above-fun-⊔-inv</a> <a id="10695" href="plfa.part3.Adequacy.html#10663" class="Bound">af</a>
<a id="10698" class="Symbol">...</a> <a id="10702" class="Symbol">|</a> <a id="10704" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟨</a> <a id="10706" href="/19.08/Adequacy/#10706" class="Bound">af1</a> <a id="10710" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">,</a> <a id="10712" href="plfa.part3.Adequacy.html#10712" class="Bound">af2</a> <a id="10716" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟩</a> <a id="10718" class="Symbol">=</a> <a id="10720" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟨</a> <a id="10722" href="plfa.part3.Adequacy.html#10391" class="Function">not-above-fun-𝕍</a> <a id="10738" href="plfa.part3.Adequacy.html#10706" class="Bound">af1</a> <a id="10742" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">,</a> <a id="10744" href="plfa.part3.Adequacy.html#10391" class="Function">not-above-fun-𝕍</a> <a id="10760" href="plfa.part3.Adequacy.html#10712" class="Bound">af2</a> <a id="10764" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟩</a>
</pre>
<p>The proofs of <code class="language-plaintext highlighter-rouge">𝕍-sub</code> and <code class="language-plaintext highlighter-rouge">𝔼-sub</code> are intertwined.</p>
<pre class="Agda"><a id="sub-𝕍"></a><a id="10827" href="/19.08/Adequacy/#10827" class="Function">sub-𝕍</a> <a id="10833" class="Symbol">:</a> <a id="10835" class="Symbol">∀{</a><a id="10837" href="plfa.part3.Adequacy.html#10837" class="Bound">c</a> <a id="10839" class="Symbol">:</a> <a id="10841" href="/19.08/BigStep/#2470" class="Datatype">Clos</a><a id="10845" class="Symbol">}{</a><a id="10847" href="plfa.part3.Adequacy.html#10847" class="Bound">v</a> <a id="10849" href="plfa.part3.Adequacy.html#10849" class="Bound">v&#39;</a><a id="10851" class="Symbol">}</a> <a id="10853" class="Symbol">→</a> <a id="10855" href="plfa.part3.Adequacy.html#7123" class="Function">𝕍</a> <a id="10857" href="plfa.part3.Adequacy.html#10847" class="Bound">v</a> <a id="10859" href="plfa.part3.Adequacy.html#10837" class="Bound">c</a> <a id="10861" class="Symbol">→</a> <a id="10863" href="plfa.part3.Adequacy.html#10849" class="Bound">v&#39;</a> <a id="10866" href="/19.08/Denotational/#4427" class="Datatype Operator">⊑</a> <a id="10868" href="plfa.part3.Adequacy.html#10847" class="Bound">v</a> <a id="10870" class="Symbol">→</a> <a id="10872" href="plfa.part3.Adequacy.html#7123" class="Function">𝕍</a> <a id="10874" href="plfa.part3.Adequacy.html#10849" class="Bound">v&#39;</a> <a id="10877" href="plfa.part3.Adequacy.html#10837" class="Bound">c</a>
<a id="sub-𝔼"></a><a id="10879" href="/19.08/Adequacy/#10879" class="Function">sub-𝔼</a> <a id="10885" class="Symbol">:</a> <a id="10887" class="Symbol">∀{</a><a id="10889" href="plfa.part3.Adequacy.html#10889" class="Bound">c</a> <a id="10891" class="Symbol">:</a> <a id="10893" href="/19.08/BigStep/#2470" class="Datatype">Clos</a><a id="10897" class="Symbol">}{</a><a id="10899" href="plfa.part3.Adequacy.html#10899" class="Bound">v</a> <a id="10901" href="plfa.part3.Adequacy.html#10901" class="Bound">v&#39;</a><a id="10903" class="Symbol">}</a> <a id="10905" class="Symbol">→</a> <a id="10907" href="plfa.part3.Adequacy.html#7146" class="Function">𝔼</a> <a id="10909" href="plfa.part3.Adequacy.html#10899" class="Bound">v</a> <a id="10911" href="plfa.part3.Adequacy.html#10889" class="Bound">c</a> <a id="10913" class="Symbol">→</a> <a id="10915" href="plfa.part3.Adequacy.html#10901" class="Bound">v&#39;</a> <a id="10918" href="/19.08/Denotational/#4427" class="Datatype Operator">⊑</a> <a id="10920" href="plfa.part3.Adequacy.html#10899" class="Bound">v</a> <a id="10922" class="Symbol">→</a> <a id="10924" href="plfa.part3.Adequacy.html#7146" class="Function">𝔼</a> <a id="10926" href="plfa.part3.Adequacy.html#10901" class="Bound">v&#39;</a> <a id="10929" href="plfa.part3.Adequacy.html#10889" class="Bound">c</a>
</pre>
<p>We prove <code class="language-plaintext highlighter-rouge">𝕍-sub</code> by case analysis on the closure’s term, to dispatch the
cases for variables and application. We then proceed by induction on
<code class="language-plaintext highlighter-rouge">v' ⊑ v</code>. We describe each case below.</p>
<pre class="Agda"><a id="11122" href="/19.08/Adequacy/#10827" class="Function">sub-𝕍</a> <a id="11128" class="Symbol">{</a><a id="11129" href="/19.08/BigStep/#2489" class="InductiveConstructor">clos</a> <a id="11134" class="Symbol">(</a><a id="11135" href="/19.08/Untyped/#4330" class="InductiveConstructor Operator">`</a> <a id="11137" href="plfa.part3.Adequacy.html#11137" class="Bound">x</a><a id="11138" class="Symbol">)</a> <a id="11140" href="plfa.part3.Adequacy.html#11140" class="Bound">γ</a><a id="11141" class="Symbol">}</a> <a id="11143" class="Symbol">{</a><a id="11144" href="plfa.part3.Adequacy.html#11144" class="Bound">v</a><a id="11145" class="Symbol">}</a> <a id="11147" class="Symbol">()</a> <a id="11150" href="plfa.part3.Adequacy.html#11150" class="Bound">lt</a>
<a id="11153" href="/19.08/Adequacy/#10827" class="Function">sub-𝕍</a> <a id="11159" class="Symbol">{</a><a id="11160" href="/19.08/BigStep/#2489" class="InductiveConstructor">clos</a> <a id="11165" class="Symbol">(</a><a id="11166" href="plfa.part3.Adequacy.html#11166" class="Bound">L</a> <a id="11168" href="/19.08/Untyped/#4442" class="InductiveConstructor Operator">·</a> <a id="11170" href="plfa.part3.Adequacy.html#11170" class="Bound">M</a><a id="11171" class="Symbol">)</a> <a id="11173" href="plfa.part3.Adequacy.html#11173" class="Bound">γ</a><a id="11174" class="Symbol">}</a> <a id="11176" class="Symbol">()</a> <a id="11179" href="plfa.part3.Adequacy.html#11179" class="Bound">lt</a>
<a id="11182" href="/19.08/Adequacy/#10827" class="Function">sub-𝕍</a> <a id="11188" class="Symbol">{</a><a id="11189" href="/19.08/BigStep/#2489" class="InductiveConstructor">clos</a> <a id="11194" class="Symbol">(</a><a id="11195" href="/19.08/Untyped/#4382" class="InductiveConstructor Operator">ƛ</a> <a id="11197" href="plfa.part3.Adequacy.html#11197" class="Bound">N</a><a id="11198" class="Symbol">)</a> <a id="11200" href="plfa.part3.Adequacy.html#11200" class="Bound">γ</a><a id="11201" class="Symbol">}</a> <a id="11203" href="plfa.part3.Adequacy.html#11203" class="Bound">vc</a> <a id="11206" href="/19.08/Denotational/#4462" class="InductiveConstructor">⊑-bot</a> <a id="11212" class="Symbol">=</a> <a id="11214" href="Agda.Builtin.Unit.html#174" class="InductiveConstructor">tt</a>
<a id="11217" href="/19.08/Adequacy/#10827" class="Function">sub-𝕍</a> <a id="11223" class="Symbol">{</a><a id="11224" href="/19.08/BigStep/#2489" class="InductiveConstructor">clos</a> <a id="11229" class="Symbol">(</a><a id="11230" href="/19.08/Untyped/#4382" class="InductiveConstructor Operator">ƛ</a> <a id="11232" href="plfa.part3.Adequacy.html#11232" class="Bound">N</a><a id="11233" class="Symbol">)</a> <a id="11235" href="plfa.part3.Adequacy.html#11235" class="Bound">γ</a><a id="11236" class="Symbol">}</a> <a id="11238" href="plfa.part3.Adequacy.html#11238" class="Bound">vc</a> <a id="11241" class="Symbol">(</a><a id="11242" href="/19.08/Denotational/#4487" class="InductiveConstructor">⊑-conj-L</a> <a id="11251" href="plfa.part3.Adequacy.html#11251" class="Bound">lt1</a> <a id="11255" href="plfa.part3.Adequacy.html#11255" class="Bound">lt2</a><a id="11258" class="Symbol">)</a> <a id="11260" class="Symbol">=</a> <a id="11262" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟨</a> <a id="11264" class="Symbol">(</a><a id="11265" href="plfa.part3.Adequacy.html#10827" class="Function">sub-𝕍</a> <a id="11271" href="plfa.part3.Adequacy.html#11238" class="Bound">vc</a> <a id="11274" href="plfa.part3.Adequacy.html#11251" class="Bound">lt1</a><a id="11277" class="Symbol">)</a> <a id="11279" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">,</a> <a id="11281" href="plfa.part3.Adequacy.html#10827" class="Function">sub-𝕍</a> <a id="11287" href="plfa.part3.Adequacy.html#11238" class="Bound">vc</a> <a id="11290" href="plfa.part3.Adequacy.html#11255" class="Bound">lt2</a> <a id="11294" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟩</a>
<a id="11296" href="/19.08/Adequacy/#10827" class="Function">sub-𝕍</a> <a id="11302" class="Symbol">{</a><a id="11303" href="/19.08/BigStep/#2489" class="InductiveConstructor">clos</a> <a id="11308" class="Symbol">(</a><a id="11309" href="/19.08/Untyped/#4382" class="InductiveConstructor Operator">ƛ</a> <a id="11311" href="plfa.part3.Adequacy.html#11311" class="Bound">N</a><a id="11312" class="Symbol">)</a> <a id="11314" href="plfa.part3.Adequacy.html#11314" class="Bound">γ</a><a id="11315" class="Symbol">}</a> <a id="11317" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟨</a> <a id="11319" href="plfa.part3.Adequacy.html#11319" class="Bound">vv1</a> <a id="11323" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">,</a> <a id="11325" href="plfa.part3.Adequacy.html#11325" class="Bound">vv2</a> <a id="11329" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟩</a> <a id="11331" class="Symbol">(</a><a id="11332" href="/19.08/Denotational/#4571" class="InductiveConstructor">⊑-conj-R1</a> <a id="11342" href="plfa.part3.Adequacy.html#11342" class="Bound">lt</a><a id="11344" class="Symbol">)</a> <a id="11346" class="Symbol">=</a> <a id="11348" href="plfa.part3.Adequacy.html#10827" class="Function">sub-𝕍</a> <a id="11354" href="plfa.part3.Adequacy.html#11319" class="Bound">vv1</a> <a id="11358" href="plfa.part3.Adequacy.html#11342" class="Bound">lt</a>
<a id="11361" href="/19.08/Adequacy/#10827" class="Function">sub-𝕍</a> <a id="11367" class="Symbol">{</a><a id="11368" href="/19.08/BigStep/#2489" class="InductiveConstructor">clos</a> <a id="11373" class="Symbol">(</a><a id="11374" href="/19.08/Untyped/#4382" class="InductiveConstructor Operator">ƛ</a> <a id="11376" href="plfa.part3.Adequacy.html#11376" class="Bound">N</a><a id="11377" class="Symbol">)</a> <a id="11379" href="plfa.part3.Adequacy.html#11379" class="Bound">γ</a><a id="11380" class="Symbol">}</a> <a id="11382" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟨</a> <a id="11384" href="plfa.part3.Adequacy.html#11384" class="Bound">vv1</a> <a id="11388" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">,</a> <a id="11390" href="plfa.part3.Adequacy.html#11390" class="Bound">vv2</a> <a id="11394" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟩</a> <a id="11396" class="Symbol">(</a><a id="11397" href="/19.08/Denotational/#4644" class="InductiveConstructor">⊑-conj-R2</a> <a id="11407" href="plfa.part3.Adequacy.html#11407" class="Bound">lt</a><a id="11409" class="Symbol">)</a> <a id="11411" class="Symbol">=</a> <a id="11413" href="plfa.part3.Adequacy.html#10827" class="Function">sub-𝕍</a> <a id="11419" href="plfa.part3.Adequacy.html#11390" class="Bound">vv2</a> <a id="11423" href="plfa.part3.Adequacy.html#11407" class="Bound">lt</a>
<a id="11426" href="/19.08/Adequacy/#10827" class="Function">sub-𝕍</a> <a id="11432" class="Symbol">{</a><a id="11433" href="/19.08/BigStep/#2489" class="InductiveConstructor">clos</a> <a id="11438" class="Symbol">(</a><a id="11439" href="/19.08/Untyped/#4382" class="InductiveConstructor Operator">ƛ</a> <a id="11441" href="plfa.part3.Adequacy.html#11441" class="Bound">N</a><a id="11442" class="Symbol">)</a> <a id="11444" href="plfa.part3.Adequacy.html#11444" class="Bound">γ</a><a id="11445" class="Symbol">}</a> <a id="11447" href="plfa.part3.Adequacy.html#11447" class="Bound">vc</a> <a id="11450" class="Symbol">(</a><a id="11451" href="/19.08/Denotational/#4717" class="InductiveConstructor">⊑-trans</a><a id="11458" class="Symbol">{</a><a id="11459" class="Argument">v</a> <a id="11461" class="Symbol">=</a> <a id="11463" href="plfa.part3.Adequacy.html#11463" class="Bound">v₂</a><a id="11465" class="Symbol">}</a> <a id="11467" href="plfa.part3.Adequacy.html#11467" class="Bound">lt1</a> <a id="11471" href="plfa.part3.Adequacy.html#11471" class="Bound">lt2</a><a id="11474" class="Symbol">)</a> <a id="11476" class="Symbol">=</a> <a id="11478" href="plfa.part3.Adequacy.html#10827" class="Function">sub-𝕍</a> <a id="11484" class="Symbol">(</a><a id="11485" href="plfa.part3.Adequacy.html#10827" class="Function">sub-𝕍</a> <a id="11491" href="plfa.part3.Adequacy.html#11447" class="Bound">vc</a> <a id="11494" href="plfa.part3.Adequacy.html#11471" class="Bound">lt2</a><a id="11497" class="Symbol">)</a> <a id="11499" href="plfa.part3.Adequacy.html#11467" class="Bound">lt1</a>
<a id="11503" href="/19.08/Adequacy/#10827" class="Function">sub-𝕍</a> <a id="11509" class="Symbol">{</a><a id="11510" href="/19.08/BigStep/#2489" class="InductiveConstructor">clos</a> <a id="11515" class="Symbol">(</a><a id="11516" href="/19.08/Untyped/#4382" class="InductiveConstructor Operator">ƛ</a> <a id="11518" href="plfa.part3.Adequacy.html#11518" class="Bound">N</a><a id="11519" class="Symbol">)</a> <a id="11521" href="plfa.part3.Adequacy.html#11521" class="Bound">γ</a><a id="11522" class="Symbol">}</a> <a id="11524" href="plfa.part3.Adequacy.html#11524" class="Bound">vc</a> <a id="11527" class="Symbol">(</a><a id="11528" href="/19.08/Denotational/#4788" class="InductiveConstructor">⊑-fun</a> <a id="11534" href="plfa.part3.Adequacy.html#11534" class="Bound">lt1</a> <a id="11538" href="plfa.part3.Adequacy.html#11538" class="Bound">lt2</a><a id="11541" class="Symbol">)</a> <a id="11543" href="plfa.part3.Adequacy.html#11543" class="Bound">ev1</a> <a id="11547" href="plfa.part3.Adequacy.html#11547" class="Bound">sf</a>
<a id="11554" class="Keyword">with</a> <a id="11559" href="/19.08/Adequacy/#11524" class="Bound">vc</a> <a id="11562" class="Symbol">(</a><a id="11563" href="plfa.part3.Adequacy.html#10879" class="Function">sub-𝔼</a> <a id="11569" href="plfa.part3.Adequacy.html#11543" class="Bound">ev1</a> <a id="11573" href="plfa.part3.Adequacy.html#11534" class="Bound">lt1</a><a id="11576" class="Symbol">)</a> <a id="11578" class="Symbol">(</a><a id="11579" href="plfa.part3.Adequacy.html#4240" class="Function">above-fun-⊑</a> <a id="11591" href="plfa.part3.Adequacy.html#11547" class="Bound">sf</a> <a id="11594" href="plfa.part3.Adequacy.html#11538" class="Bound">lt2</a><a id="11597" class="Symbol">)</a>
<a id="11599" class="Symbol">...</a> <a id="11603" class="Symbol">|</a> <a id="11605" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟨</a> <a id="11607" href="/19.08/Adequacy/#11607" class="Bound">c</a> <a id="11609" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">,</a> <a id="11611" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟨</a> <a id="11613" href="plfa.part3.Adequacy.html#11613" class="Bound">Nc</a> <a id="11616" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">,</a> <a id="11618" href="plfa.part3.Adequacy.html#11618" class="Bound">v4</a> <a id="11621" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟩</a> <a id="11623" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟩</a> <a id="11625" class="Symbol">=</a> <a id="11627" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟨</a> <a id="11629" href="plfa.part3.Adequacy.html#11607" class="Bound">c</a> <a id="11631" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">,</a> <a id="11633" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟨</a> <a id="11635" href="plfa.part3.Adequacy.html#11613" class="Bound">Nc</a> <a id="11638" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">,</a> <a id="11640" href="plfa.part3.Adequacy.html#10827" class="Function">sub-𝕍</a> <a id="11646" href="plfa.part3.Adequacy.html#11618" class="Bound">v4</a> <a id="11649" class="Bound">lt2</a> <a id="11653" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟩</a> <a id="11655" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟩</a>
<a id="11657" href="/19.08/Adequacy/#10827" class="Function">sub-𝕍</a> <a id="11663" class="Symbol">{</a><a id="11664" href="/19.08/BigStep/#2489" class="InductiveConstructor">clos</a> <a id="11669" class="Symbol">(</a><a id="11670" href="/19.08/Untyped/#4382" class="InductiveConstructor Operator">ƛ</a> <a id="11672" href="plfa.part3.Adequacy.html#11672" class="Bound">N</a><a id="11673" class="Symbol">)</a> <a id="11675" href="plfa.part3.Adequacy.html#11675" class="Bound">γ</a><a id="11676" class="Symbol">}</a> <a id="11678" class="Symbol">{</a><a id="11679" href="plfa.part3.Adequacy.html#11679" class="Bound">v</a> <a id="11681" href="/19.08/Denotational/#4102" class="InductiveConstructor Operator">↦</a> <a id="11683" href="plfa.part3.Adequacy.html#11683" class="Bound">w</a> <a id="11685" href="plfa.part3.Denotational.html#4132" class="InductiveConstructor Operator">⊔</a> <a id="11687" href="plfa.part3.Adequacy.html#11679" class="Bound">v</a> <a id="11689" href="plfa.part3.Denotational.html#4102" class="InductiveConstructor Operator">↦</a> <a id="11691" href="plfa.part3.Adequacy.html#11691" class="Bound">w&#39;</a><a id="11693" class="Symbol">}</a> <a id="11695" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟨</a> <a id="11697" href="plfa.part3.Adequacy.html#11697" class="Bound">vcw</a> <a id="11701" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">,</a> <a id="11703" href="plfa.part3.Adequacy.html#11703" class="Bound">vcw&#39;</a> <a id="11708" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟩</a> <a id="11710" href="plfa.part3.Denotational.html#4891" class="InductiveConstructor">⊑-dist</a> <a id="11717" href="plfa.part3.Adequacy.html#11717" class="Bound">ev1c</a> <a id="11722" href="plfa.part3.Adequacy.html#11722" class="Bound">sf</a>
<a id="11729" class="Keyword">with</a> <a id="11734" href="/19.08/Adequacy/#6264" class="Function">above-fun?</a> <a id="11745" href="plfa.part3.Adequacy.html#11683" class="Bound">w</a> <a id="11747" class="Symbol">|</a> <a id="11749" href="plfa.part3.Adequacy.html#6264" class="Function">above-fun?</a> <a id="11760" href="plfa.part3.Adequacy.html#11691" class="Bound">w&#39;</a>
<a id="11763" class="Symbol">...</a> <a id="11767" class="Symbol">|</a> <a id="11769" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Nullary.html#641" class="InductiveConstructor">yes</a> <a id="11773" href="/19.08/Adequacy/#11773" class="Bound">af2</a> <a id="11777" class="Symbol">|</a> <a id="11779" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Nullary.html#641" class="InductiveConstructor">yes</a> <a id="11783" href="plfa.part3.Adequacy.html#11783" class="Bound">af3</a>
<a id="11791" class="Keyword">with</a> <a id="11796" class="Bound">vcw</a> <a id="11800" class="Bound">ev1c</a> <a id="11805" href="/19.08/Adequacy/#11773" class="Bound">af2</a> <a id="11809" class="Symbol">|</a> <a id="11811" class="Bound">vcw&#39;</a> <a id="11816" class="Bound">ev1c</a> <a id="11821" href="plfa.part3.Adequacy.html#11783" class="Bound">af3</a>
<a id="11825" class="Symbol">...</a> <a id="11829" class="Symbol">|</a> <a id="11831" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟨</a> <a id="11833" href="/19.08/BigStep/#2489" class="InductiveConstructor">clos</a> <a id="11838" href="/19.08/Adequacy/#11838" class="Bound">L</a> <a id="11840" href="plfa.part3.Adequacy.html#11840" class="Bound">δ</a> <a id="11842" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">,</a> <a id="11844" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟨</a> <a id="11846" href="plfa.part3.Adequacy.html#11846" class="Bound">L⇓c₂</a> <a id="11851" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">,</a> <a id="11853" href="plfa.part3.Adequacy.html#11853" class="Bound">𝕍w</a> <a id="11856" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟩</a> <a id="11858" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟩</a>
<a id="11864" class="Symbol">|</a> <a id="11866" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟨</a> <a id="11868" href="/19.08/Adequacy/#11868" class="Bound">c₃</a> <a id="11871" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">,</a> <a id="11873" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟨</a> <a id="11875" href="plfa.part3.Adequacy.html#11875" class="Bound">L⇓c₃</a> <a id="11880" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">,</a> <a id="11882" href="plfa.part3.Adequacy.html#11882" class="Bound">𝕍w&#39;</a> <a id="11886" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟩</a> <a id="11888" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟩</a> <a id="11890" class="Keyword">rewrite</a> <a id="11898" href="/19.08/BigStep/#4589" class="Function">⇓-determ</a> <a id="11907" href="plfa.part3.Adequacy.html#11875" class="Bound">L⇓c₃</a> <a id="11912" href="plfa.part3.Adequacy.html#11846" class="Bound">L⇓c₂</a> <a id="11917" class="Keyword">with</a> <a id="11922" href="plfa.part3.Adequacy.html#9429" class="Function">𝕍→WHNF</a> <a id="11929" href="plfa.part3.Adequacy.html#11853" class="Bound">𝕍w</a>
<a id="11932" class="Symbol">...</a> <a id="11936" class="Symbol">|</a> <a id="11938" href="/19.08/Adequacy/#9322" class="InductiveConstructor Operator">ƛ_</a> <a id="11941" class="Symbol">=</a>
<a id="11949" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟨</a> <a id="11951" href="/19.08/BigStep/#2489" class="InductiveConstructor">clos</a> <a id="11956" class="Bound">L</a> <a id="11958" class="Bound">δ</a> <a id="11960" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">,</a> <a id="11962" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟨</a> <a id="11964" class="Bound">L⇓c₂</a> <a id="11969" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">,</a> <a id="11971" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟨</a> <a id="11973" class="Bound">𝕍w</a> <a id="11976" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">,</a> <a id="11978" class="Bound">𝕍w&#39;</a> <a id="11982" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟩</a> <a id="11984" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟩</a> <a id="11986" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟩</a>
<a id="11988" href="/19.08/Adequacy/#10827" class="Function">sub-𝕍</a> <a id="11994" class="Symbol">{</a><a id="11995" href="plfa.part3.Adequacy.html#11995" class="Bound">c</a><a id="11996" class="Symbol">}</a> <a id="11998" class="Symbol">{</a><a id="11999" href="plfa.part3.Adequacy.html#11999" class="Bound">v</a> <a id="12001" href="/19.08/Denotational/#4102" class="InductiveConstructor Operator">↦</a> <a id="12003" href="plfa.part3.Adequacy.html#12003" class="Bound">w</a> <a id="12005" href="plfa.part3.Denotational.html#4132" class="InductiveConstructor Operator">⊔</a> <a id="12007" href="plfa.part3.Adequacy.html#11999" class="Bound">v</a> <a id="12009" href="plfa.part3.Denotational.html#4102" class="InductiveConstructor Operator">↦</a> <a id="12011" href="plfa.part3.Adequacy.html#12011" class="Bound">w&#39;</a><a id="12013" class="Symbol">}</a> <a id="12015" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟨</a> <a id="12017" href="plfa.part3.Adequacy.html#12017" class="Bound">vcw</a> <a id="12021" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">,</a> <a id="12023" href="plfa.part3.Adequacy.html#12023" class="Bound">vcw&#39;</a> <a id="12028" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟩</a> <a id="12031" href="plfa.part3.Denotational.html#4891" class="InductiveConstructor">⊑-dist</a> <a id="12038" href="plfa.part3.Adequacy.html#12038" class="Bound">ev1c</a> <a id="12043" href="plfa.part3.Adequacy.html#12043" class="Bound">sf</a>
<a id="12050" class="Symbol">|</a> <a id="12052" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Nullary.html#641" class="InductiveConstructor">yes</a> <a id="12056" href="/19.08/Adequacy/#12056" class="Bound">af2</a> <a id="12060" class="Symbol">|</a> <a id="12062" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Nullary.html#668" class="InductiveConstructor">no</a> <a id="12065" href="plfa.part3.Adequacy.html#12065" class="Bound">naf3</a>
<a id="12074" class="Keyword">with</a> <a id="12079" href="/19.08/Adequacy/#12017" class="Bound">vcw</a> <a id="12083" href="plfa.part3.Adequacy.html#12038" class="Bound">ev1c</a> <a id="12088" href="plfa.part3.Adequacy.html#12056" class="Bound">af2</a>
<a id="12092" class="Symbol">...</a> <a id="12096" class="Symbol">|</a> <a id="12098" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟨</a> <a id="12100" href="/19.08/BigStep/#2489" class="InductiveConstructor">clos</a> <a id="12105" class="Symbol">{</a><a id="12106" href="/19.08/Adequacy/#12106" class="Bound">Γ&#39;</a><a id="12108" class="Symbol">}</a> <a id="12110" href="plfa.part3.Adequacy.html#12110" class="Bound">L</a> <a id="12112" href="plfa.part3.Adequacy.html#12112" class="Bound">γ₁</a> <a id="12115" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">,</a> <a id="12117" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟨</a> <a id="12119" href="plfa.part3.Adequacy.html#12119" class="Bound">L⇓c2</a> <a id="12124" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">,</a> <a id="12126" href="plfa.part3.Adequacy.html#12126" class="Bound">𝕍w</a> <a id="12129" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟩</a> <a id="12131" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟩</a>
<a id="12137" class="Keyword">with</a> <a id="12142" href="/19.08/Adequacy/#9429" class="Function">𝕍→WHNF</a> <a id="12149" href="plfa.part3.Adequacy.html#12126" class="Bound">𝕍w</a>
<a id="12152" class="Symbol">...</a> <a id="12156" class="Symbol">|</a> <a id="12158" href="/19.08/Adequacy/#9322" class="InductiveConstructor Operator">ƛ_</a> <a id="12161" class="Symbol">{</a><a id="12162" class="Argument">N</a> <a id="12164" class="Symbol">=</a> <a id="12166" href="plfa.part3.Adequacy.html#12166" class="Bound">N&#39;</a><a id="12168" class="Symbol">}</a> <a id="12170" class="Symbol">=</a>
<a id="12178" class="Keyword">let</a> <a id="12182" href="/19.08/Adequacy/#12182" class="Bound">𝕍w&#39;</a> <a id="12186" class="Symbol">=</a> <a id="12188" href="plfa.part3.Adequacy.html#10391" class="Function">not-above-fun-𝕍</a><a id="12203" class="Symbol">{</a><a id="12204" class="Bound">w&#39;</a><a id="12206" class="Symbol">}{</a><a id="12208" class="Bound">Γ&#39;</a><a id="12210" class="Symbol">}{</a><a id="12212" class="Bound">γ₁</a><a id="12214" class="Symbol">}{</a><a id="12216" href="plfa.part3.Adequacy.html#12166" class="Bound">N&#39;</a><a id="12218" class="Symbol">}</a> <a id="12220" class="Bound">naf3</a> <a id="12225" class="Keyword">in</a>
<a id="12234" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟨</a> <a id="12236" href="/19.08/BigStep/#2489" class="InductiveConstructor">clos</a> <a id="12241" class="Symbol">(</a><a id="12242" href="/19.08/Untyped/#4382" class="InductiveConstructor Operator">ƛ</a> <a id="12244" href="/19.08/Adequacy/#12166" class="Bound">N&#39;</a><a id="12246" class="Symbol">)</a> <a id="12248" class="Bound">γ₁</a> <a id="12251" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">,</a> <a id="12253" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟨</a> <a id="12255" class="Bound">L⇓c2</a> <a id="12260" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">,</a> <a id="12262" href="plfa.part3.Adequacy.html#9742" class="Function">𝕍⊔-intro</a> <a id="12271" class="Bound">𝕍w</a> <a id="12274" href="plfa.part3.Adequacy.html#12182" class="Bound">𝕍w&#39;</a> <a id="12278" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟩</a> <a id="12280" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟩</a>
<a id="12282" href="/19.08/Adequacy/#10827" class="Function">sub-𝕍</a> <a id="12288" class="Symbol">{</a><a id="12289" href="plfa.part3.Adequacy.html#12289" class="Bound">c</a><a id="12290" class="Symbol">}</a> <a id="12292" class="Symbol">{</a><a id="12293" href="plfa.part3.Adequacy.html#12293" class="Bound">v</a> <a id="12295" href="/19.08/Denotational/#4102" class="InductiveConstructor Operator">↦</a> <a id="12297" href="plfa.part3.Adequacy.html#12297" class="Bound">w</a> <a id="12299" href="plfa.part3.Denotational.html#4132" class="InductiveConstructor Operator">⊔</a> <a id="12301" href="plfa.part3.Adequacy.html#12293" class="Bound">v</a> <a id="12303" href="plfa.part3.Denotational.html#4102" class="InductiveConstructor Operator">↦</a> <a id="12305" href="plfa.part3.Adequacy.html#12305" class="Bound">w&#39;</a><a id="12307" class="Symbol">}</a> <a id="12309" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟨</a> <a id="12311" href="plfa.part3.Adequacy.html#12311" class="Bound">vcw</a> <a id="12315" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">,</a> <a id="12317" href="plfa.part3.Adequacy.html#12317" class="Bound">vcw&#39;</a> <a id="12322" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟩</a> <a id="12324" href="plfa.part3.Denotational.html#4891" class="InductiveConstructor">⊑-dist</a> <a id="12331" href="plfa.part3.Adequacy.html#12331" class="Bound">ev1c</a> <a id="12336" href="plfa.part3.Adequacy.html#12336" class="Bound">sf</a>
<a id="12343" class="Symbol">|</a> <a id="12345" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Nullary.html#668" class="InductiveConstructor">no</a> <a id="12348" href="/19.08/Adequacy/#12348" class="Bound">naf2</a> <a id="12353" class="Symbol">|</a> <a id="12355" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Nullary.html#641" class="InductiveConstructor">yes</a> <a id="12359" href="plfa.part3.Adequacy.html#12359" class="Bound">af3</a>
<a id="12367" class="Keyword">with</a> <a id="12372" href="/19.08/Adequacy/#12317" class="Bound">vcw&#39;</a> <a id="12377" href="plfa.part3.Adequacy.html#12331" class="Bound">ev1c</a> <a id="12382" href="plfa.part3.Adequacy.html#12359" class="Bound">af3</a>
<a id="12386" class="Symbol">...</a> <a id="12390" class="Symbol">|</a> <a id="12392" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟨</a> <a id="12394" href="/19.08/BigStep/#2489" class="InductiveConstructor">clos</a> <a id="12399" class="Symbol">{</a><a id="12400" href="/19.08/Adequacy/#12400" class="Bound">Γ&#39;</a><a id="12402" class="Symbol">}</a> <a id="12404" href="plfa.part3.Adequacy.html#12404" class="Bound">L</a> <a id="12406" href="plfa.part3.Adequacy.html#12406" class="Bound">γ₁</a> <a id="12409" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">,</a> <a id="12411" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟨</a> <a id="12413" href="plfa.part3.Adequacy.html#12413" class="Bound">L⇓c3</a> <a id="12418" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">,</a> <a id="12420" href="plfa.part3.Adequacy.html#12420" class="Bound">𝕍w&#39;c</a> <a id="12425" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟩</a> <a id="12427" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟩</a>
<a id="12433" class="Keyword">with</a> <a id="12438" href="/19.08/Adequacy/#9429" class="Function">𝕍→WHNF</a> <a id="12445" href="plfa.part3.Adequacy.html#12420" class="Bound">𝕍w&#39;c</a>
<a id="12450" class="Symbol">...</a> <a id="12454" class="Symbol">|</a> <a id="12456" href="/19.08/Adequacy/#9322" class="InductiveConstructor Operator">ƛ_</a> <a id="12459" class="Symbol">{</a><a id="12460" class="Argument">N</a> <a id="12462" class="Symbol">=</a> <a id="12464" href="plfa.part3.Adequacy.html#12464" class="Bound">N&#39;</a><a id="12466" class="Symbol">}</a> <a id="12468" class="Symbol">=</a>
<a id="12476" class="Keyword">let</a> <a id="12480" href="/19.08/Adequacy/#12480" class="Bound">𝕍wc</a> <a id="12484" class="Symbol">=</a> <a id="12486" href="plfa.part3.Adequacy.html#10391" class="Function">not-above-fun-𝕍</a><a id="12501" class="Symbol">{</a><a id="12502" class="Bound">w</a><a id="12503" class="Symbol">}{</a><a id="12505" class="Bound">Γ&#39;</a><a id="12507" class="Symbol">}{</a><a id="12509" class="Bound">γ₁</a><a id="12511" class="Symbol">}{</a><a id="12513" href="plfa.part3.Adequacy.html#12464" class="Bound">N&#39;</a><a id="12515" class="Symbol">}</a> <a id="12517" class="Bound">naf2</a> <a id="12522" class="Keyword">in</a>
<a id="12531" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟨</a> <a id="12533" href="/19.08/BigStep/#2489" class="InductiveConstructor">clos</a> <a id="12538" class="Symbol">(</a><a id="12539" href="/19.08/Untyped/#4382" class="InductiveConstructor Operator">ƛ</a> <a id="12541" href="/19.08/Adequacy/#12464" class="Bound">N&#39;</a><a id="12543" class="Symbol">)</a> <a id="12545" class="Bound">γ₁</a> <a id="12548" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">,</a> <a id="12550" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟨</a> <a id="12552" class="Bound">L⇓c3</a> <a id="12557" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">,</a> <a id="12559" href="plfa.part3.Adequacy.html#9742" class="Function">𝕍⊔-intro</a> <a id="12568" href="plfa.part3.Adequacy.html#12480" class="Bound">𝕍wc</a> <a id="12572" class="Bound">𝕍w&#39;c</a> <a id="12577" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟩</a> <a id="12579" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟩</a>
<a id="12581" href="/19.08/Adequacy/#10827" class="Function">sub-𝕍</a> <a id="12587" class="Symbol">{</a><a id="12588" href="plfa.part3.Adequacy.html#12588" class="Bound">c</a><a id="12589" class="Symbol">}</a> <a id="12591" class="Symbol">{</a><a id="12592" href="plfa.part3.Adequacy.html#12592" class="Bound">v</a> <a id="12594" href="/19.08/Denotational/#4102" class="InductiveConstructor Operator">↦</a> <a id="12596" href="plfa.part3.Adequacy.html#12596" class="Bound">w</a> <a id="12598" href="plfa.part3.Denotational.html#4132" class="InductiveConstructor Operator">⊔</a> <a id="12600" href="plfa.part3.Adequacy.html#12592" class="Bound">v</a> <a id="12602" href="plfa.part3.Denotational.html#4102" class="InductiveConstructor Operator">↦</a> <a id="12604" href="plfa.part3.Adequacy.html#12604" class="Bound">w&#39;</a><a id="12606" class="Symbol">}</a> <a id="12608" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟨</a> <a id="12610" href="plfa.part3.Adequacy.html#12610" class="Bound">vcw</a> <a id="12614" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">,</a> <a id="12616" href="plfa.part3.Adequacy.html#12616" class="Bound">vcw&#39;</a> <a id="12621" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟩</a> <a id="12623" href="plfa.part3.Denotational.html#4891" class="InductiveConstructor">⊑-dist</a> <a id="12630" href="plfa.part3.Adequacy.html#12630" class="Bound">ev1c</a> <a id="12635" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟨</a> <a id="12637" href="plfa.part3.Adequacy.html#12637" class="Bound">v&#39;</a> <a id="12640" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">,</a> <a id="12642" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟨</a> <a id="12644" href="plfa.part3.Adequacy.html#12644" class="Bound">w&#39;&#39;</a> <a id="12648" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">,</a> <a id="12650" href="plfa.part3.Adequacy.html#12650" class="Bound">lt</a> <a id="12653" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟩</a> <a id="12655" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟩</a>
<a id="12661" class="Symbol">|</a> <a id="12663" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Nullary.html#668" class="InductiveConstructor">no</a> <a id="12666" href="/19.08/Adequacy/#12666" class="Bound">naf2</a> <a id="12671" class="Symbol">|</a> <a id="12673" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Nullary.html#668" class="InductiveConstructor">no</a> <a id="12676" href="plfa.part3.Adequacy.html#12676" class="Bound">naf3</a>
<a id="12685" class="Keyword">with</a> <a id="12690" href="/19.08/Adequacy/#4786" class="Function">above-fun-⊔</a> <a id="12702" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟨</a> <a id="12704" href="plfa.part3.Adequacy.html#12637" class="Bound">v&#39;</a> <a id="12707" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">,</a> <a id="12709" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟨</a> <a id="12711" href="plfa.part3.Adequacy.html#12644" class="Bound">w&#39;&#39;</a> <a id="12715" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">,</a> <a id="12717" href="plfa.part3.Adequacy.html#12650" class="Bound">lt</a> <a id="12720" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟩</a> <a id="12722" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟩</a>
<a id="12724" class="Symbol">...</a> <a id="12728" class="Symbol">|</a> <a id="12730" href="https://agda.github.io/agda-stdlib/v1.1/Data.Sum.Base.html#662" class="InductiveConstructor">inj₁</a> <a id="12735" href="/19.08/Adequacy/#12735" class="Bound">af2</a> <a id="12739" class="Symbol">=</a> <a id="12741" href="https://agda.github.io/agda-stdlib/v1.1/Data.Empty.html#294" class="Function">⊥-elim</a> <a id="12748" class="Symbol">(</a><a id="12749" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Nullary.Negation.html#809" class="Function">contradiction</a> <a id="12763" href="plfa.part3.Adequacy.html#12735" class="Bound">af2</a> <a id="12767" class="Bound">naf2</a><a id="12771" class="Symbol">)</a>
<a id="12773" class="Symbol">...</a> <a id="12777" class="Symbol">|</a> <a id="12779" href="https://agda.github.io/agda-stdlib/v1.1/Data.Sum.Base.html#687" class="InductiveConstructor">inj₂</a> <a id="12784" href="/19.08/Adequacy/#12784" class="Bound">af3</a> <a id="12788" class="Symbol">=</a> <a id="12790" href="https://agda.github.io/agda-stdlib/v1.1/Data.Empty.html#294" class="Function">⊥-elim</a> <a id="12797" class="Symbol">(</a><a id="12798" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Nullary.Negation.html#809" class="Function">contradiction</a> <a id="12812" href="plfa.part3.Adequacy.html#12784" class="Bound">af3</a> <a id="12816" class="Bound">naf3</a><a id="12820" class="Symbol">)</a>
</pre>
<ul>
<li>
<p>Case <code class="language-plaintext highlighter-rouge">⊑-bot</code>. We immediately have <code class="language-plaintext highlighter-rouge">𝕍 ⊥ (clos (ƛ N) γ)</code>.</p>
</li>
<li>
<p>Case <code class="language-plaintext highlighter-rouge">⊑-conj-L</code>.</p>
<div class="language-plaintext highlighter-rouge"><div class="highlight"><pre class="highlight"><code> v₁' ⊑ v v₂' ⊑ v
-------------------
(v₁' ⊔ v₂') ⊑ v
</code></pre></div> </div>
<p>The induction hypotheses gives us <code class="language-plaintext highlighter-rouge">𝕍 v₁' (clos (ƛ N) γ)</code>
and <code class="language-plaintext highlighter-rouge">𝕍 v₂' (clos (ƛ N) γ)</code>, which is all we need for this case.</p>
</li>
<li>
<p>Case <code class="language-plaintext highlighter-rouge">⊑-conj-R1</code>.</p>
<div class="language-plaintext highlighter-rouge"><div class="highlight"><pre class="highlight"><code> v' ⊑ v₁
-------------
v' ⊑ (v₁ ⊔ v₂)
</code></pre></div> </div>
<p>The induction hypothesis gives us <code class="language-plaintext highlighter-rouge">𝕍 v' (clos (ƛ N) γ)</code>.</p>
</li>
<li>
<p>Case <code class="language-plaintext highlighter-rouge">⊑-conj-R2</code>.</p>
<div class="language-plaintext highlighter-rouge"><div class="highlight"><pre class="highlight"><code> v' ⊑ v₂
-------------
v' ⊑ (v₁ ⊔ v₂)
</code></pre></div> </div>
<p>Again, the induction hypothesis gives us <code class="language-plaintext highlighter-rouge">𝕍 v' (clos (ƛ N) γ)</code>.</p>
</li>
<li>
<p>Case <code class="language-plaintext highlighter-rouge">⊑-trans</code>.</p>
<div class="language-plaintext highlighter-rouge"><div class="highlight"><pre class="highlight"><code> v' ⊑ v₂ v₂ ⊑ v
-----------------
v' ⊑ v
</code></pre></div> </div>
<p>The induction hypothesis for <code class="language-plaintext highlighter-rouge">v₂ ⊑ v</code> gives us
<code class="language-plaintext highlighter-rouge">𝕍 v₂ (clos (ƛ N) γ)</code>. We apply the induction hypothesis
for <code class="language-plaintext highlighter-rouge">v' ⊑ v₂</code> to conclude that <code class="language-plaintext highlighter-rouge">𝕍 v' (clos (ƛ N) γ)</code>.</p>
</li>
<li>
<p>Case <code class="language-plaintext highlighter-rouge">⊑-dist</code>. This case is the most difficult. We have</p>
<div class="language-plaintext highlighter-rouge"><div class="highlight"><pre class="highlight"><code> 𝕍 (v ↦ w) (clos (ƛ N) γ)
𝕍 (v ↦ w') (clos (ƛ N) γ)
</code></pre></div> </div>
<p>and need to show that</p>
<div class="language-plaintext highlighter-rouge"><div class="highlight"><pre class="highlight"><code> 𝕍 (v ↦ (w ⊔ w')) (clos (ƛ N) γ)
</code></pre></div> </div>
<p>Let <code class="language-plaintext highlighter-rouge">c</code> be an arbtrary closure such that <code class="language-plaintext highlighter-rouge">𝔼 v c</code>.
Assume <code class="language-plaintext highlighter-rouge">w ⊔ w'</code> is greater than a function.
Unfortunately, this does not mean that both <code class="language-plaintext highlighter-rouge">w</code> and <code class="language-plaintext highlighter-rouge">w'</code>
are above functions. But thanks to the lemma <code class="language-plaintext highlighter-rouge">above-fun-⊔</code>,
we know that at least one of them is greater than a function.</p>
<ul>
<li>
<p>Suppose both of them are greater than a function. Then we have
<code class="language-plaintext highlighter-rouge">γ ⊢ N ⇓ clos L δ</code> and <code class="language-plaintext highlighter-rouge">𝕍 w (clos L δ)</code>. We also have <code class="language-plaintext highlighter-rouge">γ ⊢ N ⇓ c₃</code> and
<code class="language-plaintext highlighter-rouge">𝕍 w' c₃</code>. Because the big-step semantics is deterministic, we have
<code class="language-plaintext highlighter-rouge">c₃ ≡ clos L δ</code>. Also, from <code class="language-plaintext highlighter-rouge">𝕍 w (clos L δ)</code> we know that <code class="language-plaintext highlighter-rouge">L ≡ ƛ N'</code>
for some <code class="language-plaintext highlighter-rouge">N'</code>. We conclude that <code class="language-plaintext highlighter-rouge">𝕍 (w ⊔ w') (clos (ƛ N') δ)</code>.</p>
</li>
<li>
<p>Suppose one of them is greater than a function and the other is
not: say <code class="language-plaintext highlighter-rouge">above-fun w</code> and <code class="language-plaintext highlighter-rouge">¬ above-fun w'</code>. Then from
<code class="language-plaintext highlighter-rouge">𝕍 (v ↦ w) (clos (ƛ N) γ)</code>
we have <code class="language-plaintext highlighter-rouge">γ ⊢ N ⇓ clos L γ₁</code> and <code class="language-plaintext highlighter-rouge">𝕍 w (clos L γ₁)</code>. From this we have
<code class="language-plaintext highlighter-rouge">L ≡ ƛ N'</code> for some <code class="language-plaintext highlighter-rouge">N'</code>. Meanwhile, from <code class="language-plaintext highlighter-rouge">¬ above-fun w'</code> we have
<code class="language-plaintext highlighter-rouge">𝕍 w' (clos L γ₁)</code>. We conclude that
<code class="language-plaintext highlighter-rouge">𝕍 (w ⊔ w') (clos (ƛ N') γ₁)</code>.</p>
</li>
</ul>
</li>
</ul>
<p>The proof of <code class="language-plaintext highlighter-rouge">sub-𝔼</code> is direct and explained below.</p>
<pre class="Agda"><a id="14934" href="/19.08/Adequacy/#10879" class="Function">sub-𝔼</a> <a id="14940" class="Symbol">{</a><a id="14941" href="/19.08/BigStep/#2489" class="InductiveConstructor">clos</a> <a id="14946" href="plfa.part3.Adequacy.html#14946" class="Bound">M</a> <a id="14948" href="plfa.part3.Adequacy.html#14948" class="Bound">γ</a><a id="14949" class="Symbol">}</a> <a id="14951" class="Symbol">{</a><a id="14952" href="plfa.part3.Adequacy.html#14952" class="Bound">v</a><a id="14953" class="Symbol">}</a> <a id="14955" class="Symbol">{</a><a id="14956" href="plfa.part3.Adequacy.html#14956" class="Bound">v&#39;</a><a id="14958" class="Symbol">}</a> <a id="14960" href="plfa.part3.Adequacy.html#14960" class="Bound">𝔼v</a> <a id="14963" href="plfa.part3.Adequacy.html#14963" class="Bound">v&#39;⊑v</a> <a id="14968" href="plfa.part3.Adequacy.html#14968" class="Bound">fv&#39;</a>
<a id="14976" class="Keyword">with</a> <a id="14981" href="/19.08/Adequacy/#14960" class="Bound">𝔼v</a> <a id="14984" class="Symbol">(</a><a id="14985" href="plfa.part3.Adequacy.html#4240" class="Function">above-fun-⊑</a> <a id="14997" href="plfa.part3.Adequacy.html#14968" class="Bound">fv&#39;</a> <a id="15001" href="plfa.part3.Adequacy.html#14963" class="Bound">v&#39;⊑v</a><a id="15005" class="Symbol">)</a>
<a id="15007" class="Symbol">...</a> <a id="15011" class="Symbol">|</a> <a id="15013" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟨</a> <a id="15015" href="/19.08/Adequacy/#15015" class="Bound">c</a> <a id="15017" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">,</a> <a id="15019" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟨</a> <a id="15021" href="plfa.part3.Adequacy.html#15021" class="Bound">M⇓c</a> <a id="15025" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">,</a> <a id="15027" href="plfa.part3.Adequacy.html#15027" class="Bound">𝕍v</a> <a id="15030" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟩</a> <a id="15032" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟩</a> <a id="15034" class="Symbol">=</a>
<a id="15042" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟨</a> <a id="15044" href="/19.08/Adequacy/#15015" class="Bound">c</a> <a id="15046" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">,</a> <a id="15048" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟨</a> <a id="15050" href="plfa.part3.Adequacy.html#15021" class="Bound">M⇓c</a> <a id="15054" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">,</a> <a id="15056" href="plfa.part3.Adequacy.html#10827" class="Function">sub-𝕍</a> <a id="15062" href="plfa.part3.Adequacy.html#15027" class="Bound">𝕍v</a> <a id="15065" class="Bound">v&#39;⊑v</a> <a id="15070" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟩</a> <a id="15072" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟩</a>
</pre>
<p>From <code class="language-plaintext highlighter-rouge">above-fun v'</code> and <code class="language-plaintext highlighter-rouge">v' ⊑ v</code> we have <code class="language-plaintext highlighter-rouge">above-fun v</code>. Then with <code class="language-plaintext highlighter-rouge">𝔼 v c</code> we
obtain a closure <code class="language-plaintext highlighter-rouge">c</code> such that <code class="language-plaintext highlighter-rouge">γ ⊢ M ⇓ c</code> and <code class="language-plaintext highlighter-rouge">𝕍 v c</code>. We conclude with an
application of <code class="language-plaintext highlighter-rouge">sub-𝕍</code> with <code class="language-plaintext highlighter-rouge">v' ⊑ v</code> to show <code class="language-plaintext highlighter-rouge">𝕍 v' c</code>.</p>
<h2 id="programs-with-function-denotation-terminate-via-call-by-name">Programs with function denotation terminate via call-by-name</h2>
<p>The main lemma proves that if a term has a denotation that is above a
function, then it terminates via call-by-name. More formally, if
<code class="language-plaintext highlighter-rouge">γ ⊢ M ↓ v</code> and <code class="language-plaintext highlighter-rouge">𝔾 γ γ'</code>, then <code class="language-plaintext highlighter-rouge">𝔼 v (clos M γ')</code>. The proof is by
induction on the derivation of <code class="language-plaintext highlighter-rouge">γ ⊢ M ↓ v</code> we discuss each case below.</p>
<p>The following lemma, kth-x, is used in the case for the <code class="language-plaintext highlighter-rouge">var</code> rule.</p>
<pre class="Agda"><a id="kth-x"></a><a id="15701" href="/19.08/Adequacy/#15701" class="Function">kth-x</a> <a id="15707" class="Symbol">:</a> <a id="15709" class="Symbol">∀{</a><a id="15711" href="plfa.part3.Adequacy.html#15711" class="Bound">Γ</a><a id="15712" class="Symbol">}{</a><a id="15714" href="plfa.part3.Adequacy.html#15714" class="Bound">γ&#39;</a> <a id="15717" class="Symbol">:</a> <a id="15719" href="/19.08/BigStep/#2440" class="Function">ClosEnv</a> <a id="15727" href="plfa.part3.Adequacy.html#15711" class="Bound">Γ</a><a id="15728" class="Symbol">}{</a><a id="15730" href="plfa.part3.Adequacy.html#15730" class="Bound">x</a> <a id="15732" class="Symbol">:</a> <a id="15734" href="plfa.part3.Adequacy.html#15711" class="Bound">Γ</a> <a id="15736" href="/19.08/Untyped/#3521" class="Datatype Operator">∋</a> <a id="15738" href="plfa.part2.Untyped.html#2888" class="InductiveConstructor">★</a><a id="15739" class="Symbol">}</a>
<a id="15746" class="Symbol">→</a> <a id="15748" href="https://agda.github.io/agda-stdlib/v1.1/Data.Product.html#911" class="Function">Σ[</a> <a id="15751" href="/19.08/Adequacy/#15751" class="Bound">Δ</a> <a id="15753" href="https://agda.github.io/agda-stdlib/v1.1/Data.Product.html#911" class="Function">∈</a> <a id="15755" href="/19.08/Untyped/#3153" class="Datatype">Context</a> <a id="15763" href="https://agda.github.io/agda-stdlib/v1.1/Data.Product.html#911" class="Function">]</a> <a id="15765" href="https://agda.github.io/agda-stdlib/v1.1/Data.Product.html#911" class="Function">Σ[</a> <a id="15768" href="plfa.part3.Adequacy.html#15768" class="Bound">δ</a> <a id="15770" href="https://agda.github.io/agda-stdlib/v1.1/Data.Product.html#911" class="Function">∈</a> <a id="15772" href="/19.08/BigStep/#2440" class="Function">ClosEnv</a> <a id="15780" href="plfa.part3.Adequacy.html#15751" class="Bound">Δ</a> <a id="15782" href="https://agda.github.io/agda-stdlib/v1.1/Data.Product.html#911" class="Function">]</a> <a id="15784" href="https://agda.github.io/agda-stdlib/v1.1/Data.Product.html#911" class="Function">Σ[</a> <a id="15787" href="plfa.part3.Adequacy.html#15787" class="Bound">M</a> <a id="15789" href="https://agda.github.io/agda-stdlib/v1.1/Data.Product.html#911" class="Function">∈</a> <a id="15791" href="plfa.part3.Adequacy.html#15751" class="Bound">Δ</a> <a id="15793" href="plfa.part2.Untyped.html#4294" class="Datatype Operator">⊢</a> <a id="15795" href="plfa.part2.Untyped.html#2888" class="InductiveConstructor">★</a> <a id="15797" href="https://agda.github.io/agda-stdlib/v1.1/Data.Product.html#911" class="Function">]</a>
<a id="15816" href="/19.08/Adequacy/#15714" class="Bound">γ&#39;</a> <a id="15819" href="plfa.part3.Adequacy.html#15730" class="Bound">x</a> <a id="15821" href="Agda.Builtin.Equality.html#125" class="Datatype Operator">≡</a> <a id="15823" href="/19.08/BigStep/#2489" class="InductiveConstructor">clos</a> <a id="15828" href="plfa.part3.Adequacy.html#15787" class="Bound">M</a> <a id="15830" href="plfa.part3.Adequacy.html#15768" class="Bound">δ</a>
<a id="15832" href="/19.08/Adequacy/#15701" class="Function">kth-x</a><a id="15837" class="Symbol">{</a><a id="15838" class="Argument">γ&#39;</a> <a id="15841" class="Symbol">=</a> <a id="15843" href="plfa.part3.Adequacy.html#15843" class="Bound">γ&#39;</a><a id="15845" class="Symbol">}{</a><a id="15847" class="Argument">x</a> <a id="15849" class="Symbol">=</a> <a id="15851" href="plfa.part3.Adequacy.html#15851" class="Bound">x</a><a id="15852" class="Symbol">}</a> <a id="15854" class="Keyword">with</a> <a id="15859" href="plfa.part3.Adequacy.html#15843" class="Bound">γ&#39;</a> <a id="15862" href="plfa.part3.Adequacy.html#15851" class="Bound">x</a>
<a id="15864" class="Symbol">...</a> <a id="15868" class="Symbol">|</a> <a id="15870" href="/19.08/BigStep/#2489" class="InductiveConstructor">clos</a><a id="15874" class="Symbol">{</a><a id="15875" class="Argument">Γ</a> <a id="15877" class="Symbol">=</a> <a id="15879" href="/19.08/Adequacy/#15879" class="Bound">Δ</a><a id="15880" class="Symbol">}</a> <a id="15882" href="plfa.part3.Adequacy.html#15882" class="Bound">M</a> <a id="15884" href="plfa.part3.Adequacy.html#15884" class="Bound">δ</a> <a id="15886" class="Symbol">=</a> <a id="15888" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟨</a> <a id="15890" href="plfa.part3.Adequacy.html#15879" class="Bound">Δ</a> <a id="15892" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">,</a> <a id="15894" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟨</a> <a id="15896" href="plfa.part3.Adequacy.html#15884" class="Bound">δ</a> <a id="15898" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">,</a> <a id="15900" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟨</a> <a id="15902" href="plfa.part3.Adequacy.html#15882" class="Bound">M</a> <a id="15904" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">,</a> <a id="15906" href="Agda.Builtin.Equality.html#182" class="InductiveConstructor">refl</a> <a id="15911" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟩</a> <a id="15913" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟩</a> <a id="15915" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟩</a>
</pre>
<pre class="Agda"><a id="↓→𝔼"></a><a id="15926" href="/19.08/Adequacy/#15926" class="Function">↓→𝔼</a> <a id="15930" class="Symbol">:</a> <a id="15932" class="Symbol">∀{</a><a id="15934" href="plfa.part3.Adequacy.html#15934" class="Bound">Γ</a><a id="15935" class="Symbol">}{</a><a id="15937" href="plfa.part3.Adequacy.html#15937" class="Bound">γ</a> <a id="15939" class="Symbol">:</a> <a id="15941" href="/19.08/Denotational/#7207" class="Function">Env</a> <a id="15945" href="plfa.part3.Adequacy.html#15934" class="Bound">Γ</a><a id="15946" class="Symbol">}{</a><a id="15948" href="plfa.part3.Adequacy.html#15948" class="Bound">γ&#39;</a> <a id="15951" class="Symbol">:</a> <a id="15953" href="/19.08/BigStep/#2440" class="Function">ClosEnv</a> <a id="15961" href="plfa.part3.Adequacy.html#15934" class="Bound">Γ</a><a id="15962" class="Symbol">}{</a><a id="15964" href="plfa.part3.Adequacy.html#15964" class="Bound">M</a> <a id="15966" class="Symbol">:</a> <a id="15968" href="plfa.part3.Adequacy.html#15934" class="Bound">Γ</a> <a id="15970" href="/19.08/Untyped/#4294" class="Datatype Operator">⊢</a> <a id="15972" href="plfa.part2.Untyped.html#2888" class="InductiveConstructor">★</a> <a id="15974" class="Symbol">}{</a><a id="15976" href="plfa.part3.Adequacy.html#15976" class="Bound">v</a><a id="15977" class="Symbol">}</a>
<a id="15991" class="Symbol">→</a> <a id="15993" href="/19.08/Adequacy/#8844" class="Function">𝔾</a> <a id="15995" href="plfa.part3.Adequacy.html#15937" class="Bound">γ</a> <a id="15997" href="plfa.part3.Adequacy.html#15948" class="Bound">γ&#39;</a> <a id="16000" class="Symbol">→</a> <a id="16002" href="plfa.part3.Adequacy.html#15937" class="Bound">γ</a> <a id="16004" href="/19.08/Denotational/#9417" class="Datatype Operator">⊢</a> <a id="16006" href="plfa.part3.Adequacy.html#15964" class="Bound">M</a> <a id="16008" href="plfa.part3.Denotational.html#9417" class="Datatype Operator">↓</a> <a id="16010" href="plfa.part3.Adequacy.html#15976" class="Bound">v</a> <a id="16012" class="Symbol">→</a> <a id="16014" href="plfa.part3.Adequacy.html#7146" class="Function">𝔼</a> <a id="16016" href="plfa.part3.Adequacy.html#15976" class="Bound">v</a> <a id="16018" class="Symbol">(</a><a id="16019" href="/19.08/BigStep/#2489" class="InductiveConstructor">clos</a> <a id="16024" href="plfa.part3.Adequacy.html#15964" class="Bound">M</a> <a id="16026" href="plfa.part3.Adequacy.html#15948" class="Bound">γ&#39;</a><a id="16028" class="Symbol">)</a>
<a id="16030" href="/19.08/Adequacy/#15926" class="Function">↓→𝔼</a> <a id="16034" class="Symbol">{</a><a id="16035" href="plfa.part3.Adequacy.html#16035" class="Bound">Γ</a><a id="16036" class="Symbol">}</a> <a id="16038" class="Symbol">{</a><a id="16039" href="plfa.part3.Adequacy.html#16039" class="Bound">γ</a><a id="16040" class="Symbol">}</a> <a id="16042" class="Symbol">{</a><a id="16043" href="plfa.part3.Adequacy.html#16043" class="Bound">γ&#39;</a><a id="16045" class="Symbol">}</a> <a id="16047" href="plfa.part3.Adequacy.html#16047" class="Bound">𝔾γγ&#39;</a> <a id="16052" class="Symbol">(</a><a id="16053" href="/19.08/Denotational/#9471" class="InductiveConstructor">var</a><a id="16056" class="Symbol">{</a><a id="16057" class="Argument">x</a> <a id="16059" class="Symbol">=</a> <a id="16061" href="plfa.part3.Adequacy.html#16061" class="Bound">x</a><a id="16062" class="Symbol">})</a> <a id="16065" href="plfa.part3.Adequacy.html#16065" class="Bound">fγx</a>
<a id="16073" class="Keyword">with</a> <a id="16078" href="/19.08/Adequacy/#15701" class="Function">kth-x</a><a id="16083" class="Symbol">{</a><a id="16084" href="plfa.part3.Adequacy.html#16035" class="Bound">Γ</a><a id="16085" class="Symbol">}{</a><a id="16087" href="plfa.part3.Adequacy.html#16043" class="Bound">γ&#39;</a><a id="16089" class="Symbol">}{</a><a id="16091" href="plfa.part3.Adequacy.html#16061" class="Bound">x</a><a id="16092" class="Symbol">}</a> <a id="16094" class="Symbol">|</a> <a id="16096" href="plfa.part3.Adequacy.html#16047" class="Bound">𝔾γγ&#39;</a><a id="16100" class="Symbol">{</a><a id="16101" class="Argument">x</a> <a id="16103" class="Symbol">=</a> <a id="16105" href="plfa.part3.Adequacy.html#16061" class="Bound">x</a><a id="16106" class="Symbol">}</a>
<a id="16108" class="Symbol">...</a> <a id="16112" class="Symbol">|</a> <a id="16114" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟨</a> <a id="16116" href="/19.08/Adequacy/#16116" class="Bound">Δ</a> <a id="16118" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">,</a> <a id="16120" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟨</a> <a id="16122" href="plfa.part3.Adequacy.html#16122" class="Bound">δ</a> <a id="16124" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">,</a> <a id="16126" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟨</a> <a id="16128" href="plfa.part3.Adequacy.html#16128" class="Bound">M&#39;</a> <a id="16131" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">,</a> <a id="16133" href="plfa.part3.Adequacy.html#16133" class="Bound">eq</a> <a id="16136" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟩</a> <a id="16138" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟩</a> <a id="16140" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟩</a> <a id="16142" class="Symbol">|</a> <a id="16144" href="plfa.part3.Adequacy.html#16144" class="Bound">𝔾γγ&#39;x</a> <a id="16150" class="Keyword">rewrite</a> <a id="16158" href="plfa.part3.Adequacy.html#16133" class="Bound">eq</a>
<a id="16165" class="Keyword">with</a> <a id="16170" href="/19.08/Adequacy/#16144" class="Bound">𝔾γγ&#39;x</a> <a id="16176" class="Bound">fγx</a>
<a id="16180" class="Symbol">...</a> <a id="16184" class="Symbol">|</a> <a id="16186" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟨</a> <a id="16188" href="/19.08/Adequacy/#16188" class="Bound">c</a> <a id="16190" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">,</a> <a id="16192" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟨</a> <a id="16194" href="plfa.part3.Adequacy.html#16194" class="Bound">M&#39;⇓c</a> <a id="16199" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">,</a> <a id="16201" href="plfa.part3.Adequacy.html#16201" class="Bound">𝕍γx</a> <a id="16205" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟩</a> <a id="16207" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟩</a> <a id="16209" class="Symbol">=</a>
<a id="16217" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟨</a> <a id="16219" href="/19.08/Adequacy/#16188" class="Bound">c</a> <a id="16221" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">,</a> <a id="16223" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟨</a> <a id="16225" class="Symbol">(</a><a id="16226" href="/19.08/BigStep/#3081" class="InductiveConstructor">⇓-var</a> <a id="16232" class="Bound">eq</a> <a id="16235" href="plfa.part3.Adequacy.html#16194" class="Bound">M&#39;⇓c</a><a id="16239" class="Symbol">)</a> <a id="16241" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">,</a> <a id="16243" href="plfa.part3.Adequacy.html#16201" class="Bound">𝕍γx</a> <a id="16247" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟩</a> <a id="16249" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟩</a>
<a id="16251" href="/19.08/Adequacy/#15926" class="Function">↓→𝔼</a> <a id="16255" class="Symbol">{</a><a id="16256" href="plfa.part3.Adequacy.html#16256" class="Bound">Γ</a><a id="16257" class="Symbol">}</a> <a id="16259" class="Symbol">{</a><a id="16260" href="plfa.part3.Adequacy.html#16260" class="Bound">γ</a><a id="16261" class="Symbol">}</a> <a id="16263" class="Symbol">{</a><a id="16264" href="plfa.part3.Adequacy.html#16264" class="Bound">γ&#39;</a><a id="16266" class="Symbol">}</a> <a id="16268" href="plfa.part3.Adequacy.html#16268" class="Bound">𝔾γγ&#39;</a> <a id="16273" class="Symbol">(</a><a id="16274" href="/19.08/Denotational/#9546" class="InductiveConstructor">↦-elim</a><a id="16280" class="Symbol">{</a><a id="16281" class="Argument">L</a> <a id="16283" class="Symbol">=</a> <a id="16285" href="plfa.part3.Adequacy.html#16285" class="Bound">L</a><a id="16286" class="Symbol">}{</a><a id="16288" class="Argument">M</a> <a id="16290" class="Symbol">=</a> <a id="16292" href="plfa.part3.Adequacy.html#16292" class="Bound">M</a><a id="16293" class="Symbol">}{</a><a id="16295" class="Argument">v</a> <a id="16297" class="Symbol">=</a> <a id="16299" href="plfa.part3.Adequacy.html#16299" class="Bound">v₁</a><a id="16301" class="Symbol">}{</a><a id="16303" class="Argument">w</a> <a id="16305" class="Symbol">=</a> <a id="16307" href="plfa.part3.Adequacy.html#16307" class="Bound">v</a><a id="16308" class="Symbol">}</a> <a id="16310" href="plfa.part3.Adequacy.html#16310" class="Bound">d₁</a> <a id="16313" href="plfa.part3.Adequacy.html#16313" class="Bound">d₂</a><a id="16315" class="Symbol">)</a> <a id="16317" href="plfa.part3.Adequacy.html#16317" class="Bound">fv</a>
<a id="16324" class="Keyword">with</a> <a id="16329" href="/19.08/Adequacy/#15926" class="Function">↓→𝔼</a> <a id="16333" href="plfa.part3.Adequacy.html#16268" class="Bound">𝔾γγ&#39;</a> <a id="16338" href="plfa.part3.Adequacy.html#16310" class="Bound">d₁</a> <a id="16341" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟨</a> <a id="16343" href="plfa.part3.Adequacy.html#16299" class="Bound">v₁</a> <a id="16346" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">,</a> <a id="16348" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟨</a> <a id="16350" href="plfa.part3.Adequacy.html#16307" class="Bound">v</a> <a id="16352" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">,</a> <a id="16354" href="/19.08/Denotational/#5557" class="Function">⊑-refl</a> <a id="16361" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟩</a> <a id="16363" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟩</a>
<a id="16365" class="Symbol">...</a> <a id="16369" class="Symbol">|</a> <a id="16371" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟨</a> <a id="16373" href="/19.08/BigStep/#2489" class="InductiveConstructor">clos</a> <a id="16378" href="/19.08/Adequacy/#16378" class="Bound">L&#39;</a> <a id="16381" href="plfa.part3.Adequacy.html#16381" class="Bound">δ</a> <a id="16383" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">,</a> <a id="16385" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟨</a> <a id="16387" href="plfa.part3.Adequacy.html#16387" class="Bound">L⇓L&#39;</a> <a id="16392" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">,</a> <a id="16394" href="plfa.part3.Adequacy.html#16394" class="Bound">𝕍v₁↦v</a> <a id="16400" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟩</a> <a id="16402" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟩</a>
<a id="16408" class="Keyword">with</a> <a id="16413" href="/19.08/Adequacy/#9429" class="Function">𝕍→WHNF</a> <a id="16420" href="plfa.part3.Adequacy.html#16394" class="Bound">𝕍v₁↦v</a>
<a id="16426" class="Symbol">...</a> <a id="16430" class="Symbol">|</a> <a id="16432" href="/19.08/Adequacy/#9322" class="InductiveConstructor Operator">ƛ_</a> <a id="16435" class="Symbol">{</a><a id="16436" class="Argument">N</a> <a id="16438" class="Symbol">=</a> <a id="16440" href="plfa.part3.Adequacy.html#16440" class="Bound">N</a><a id="16441" class="Symbol">}</a>
<a id="16447" class="Keyword">with</a> <a id="16452" class="Bound">𝕍v₁↦v</a> <a id="16458" class="Symbol">{</a><a id="16459" href="/19.08/BigStep/#2489" class="InductiveConstructor">clos</a> <a id="16464" class="Bound">M</a> <a id="16466" class="Bound">γ&#39;</a><a id="16468" class="Symbol">}</a> <a id="16470" class="Symbol">(</a><a id="16471" href="/19.08/Adequacy/#15926" class="Function">↓→𝔼</a> <a id="16475" class="Bound">𝔾γγ&#39;</a> <a id="16480" class="Bound">d₂</a><a id="16482" class="Symbol">)</a> <a id="16484" class="Bound">fv</a>
<a id="16487" class="Symbol">...</a> <a id="16491" class="Symbol">|</a> <a id="16493" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟨</a> <a id="16495" href="/19.08/Adequacy/#16495" class="Bound">c&#39;</a> <a id="16498" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">,</a> <a id="16500" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟨</a> <a id="16502" href="plfa.part3.Adequacy.html#16502" class="Bound">N⇓c&#39;</a> <a id="16507" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">,</a> <a id="16509" href="plfa.part3.Adequacy.html#16509" class="Bound">𝕍v</a> <a id="16512" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟩</a> <a id="16514" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟩</a> <a id="16516" class="Symbol">=</a>
<a id="16522" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟨</a> <a id="16524" href="/19.08/Adequacy/#16495" class="Bound">c&#39;</a> <a id="16527" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">,</a> <a id="16529" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟨</a> <a id="16531" href="/19.08/BigStep/#3303" class="InductiveConstructor">⇓-app</a> <a id="16537" class="Bound">L⇓L&#39;</a> <a id="16542" href="plfa.part3.Adequacy.html#16502" class="Bound">N⇓c&#39;</a> <a id="16547" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">,</a> <a id="16549" href="plfa.part3.Adequacy.html#16509" class="Bound">𝕍v</a> <a id="16552" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟩</a> <a id="16554" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟩</a>
<a id="16556" href="/19.08/Adequacy/#15926" class="Function">↓→𝔼</a> <a id="16560" class="Symbol">{</a><a id="16561" href="plfa.part3.Adequacy.html#16561" class="Bound">Γ</a><a id="16562" class="Symbol">}</a> <a id="16564" class="Symbol">{</a><a id="16565" href="plfa.part3.Adequacy.html#16565" class="Bound">γ</a><a id="16566" class="Symbol">}</a> <a id="16568" class="Symbol">{</a><a id="16569" href="plfa.part3.Adequacy.html#16569" class="Bound">γ&#39;</a><a id="16571" class="Symbol">}</a> <a id="16573" href="plfa.part3.Adequacy.html#16573" class="Bound">𝔾γγ&#39;</a> <a id="16578" class="Symbol">(</a><a id="16579" href="/19.08/Denotational/#9668" class="InductiveConstructor">↦-intro</a><a id="16586" class="Symbol">{</a><a id="16587" class="Argument">N</a> <a id="16589" class="Symbol">=</a> <a id="16591" href="plfa.part3.Adequacy.html#16591" class="Bound">N</a><a id="16592" class="Symbol">}{</a><a id="16594" class="Argument">v</a> <a id="16596" class="Symbol">=</a> <a id="16598" href="plfa.part3.Adequacy.html#16598" class="Bound">v</a><a id="16599" class="Symbol">}{</a><a id="16601" class="Argument">w</a> <a id="16603" class="Symbol">=</a> <a id="16605" href="plfa.part3.Adequacy.html#16605" class="Bound">w</a><a id="16606" class="Symbol">}</a> <a id="16608" href="plfa.part3.Adequacy.html#16608" class="Bound">d</a><a id="16609" class="Symbol">)</a> <a id="16611" href="plfa.part3.Adequacy.html#16611" class="Bound">fv↦w</a> <a id="16616" class="Symbol">=</a>
<a id="16622" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟨</a> <a id="16624" href="/19.08/BigStep/#2489" class="InductiveConstructor">clos</a> <a id="16629" class="Symbol">(</a><a id="16630" href="/19.08/Untyped/#4382" class="InductiveConstructor Operator">ƛ</a> <a id="16632" href="/19.08/Adequacy/#16591" class="Bound">N</a><a id="16633" class="Symbol">)</a> <a id="16635" href="plfa.part3.Adequacy.html#16569" class="Bound">γ&#39;</a> <a id="16638" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">,</a> <a id="16640" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟨</a> <a id="16642" href="plfa.part2.BigStep.html#3228" class="InductiveConstructor">⇓-lam</a> <a id="16648" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">,</a> <a id="16650" href="plfa.part3.Adequacy.html#16666" class="Function">E</a> <a id="16652" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟩</a> <a id="16654" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟩</a>
<a id="16660" class="Keyword">where</a> <a id="16666" href="/19.08/Adequacy/#16666" class="Function">E</a> <a id="16668" class="Symbol">:</a> <a id="16670" class="Symbol">{</a><a id="16671" href="plfa.part3.Adequacy.html#16671" class="Bound">c</a> <a id="16673" class="Symbol">:</a> <a id="16675" href="/19.08/BigStep/#2470" class="Datatype">Clos</a><a id="16679" class="Symbol">}</a> <a id="16681" class="Symbol">→</a> <a id="16683" href="plfa.part3.Adequacy.html#7146" class="Function">𝔼</a> <a id="16685" href="plfa.part3.Adequacy.html#16598" class="Bound">v</a> <a id="16687" href="plfa.part3.Adequacy.html#16671" class="Bound">c</a> <a id="16689" class="Symbol">→</a> <a id="16691" href="plfa.part3.Adequacy.html#4069" class="Function">above-fun</a> <a id="16701" href="plfa.part3.Adequacy.html#16605" class="Bound">w</a>
<a id="16715" class="Symbol">→</a> <a id="16717" href="https://agda.github.io/agda-stdlib/v1.1/Data.Product.html#911" class="Function">Σ[</a> <a id="16720" href="/19.08/Adequacy/#16720" class="Bound">c&#39;</a> <a id="16723" href="https://agda.github.io/agda-stdlib/v1.1/Data.Product.html#911" class="Function">∈</a> <a id="16725" href="/19.08/BigStep/#2470" class="Datatype">Clos</a> <a id="16730" href="https://agda.github.io/agda-stdlib/v1.1/Data.Product.html#911" class="Function">]</a> <a id="16732" class="Symbol">(</a><a id="16733" href="plfa.part3.Adequacy.html#16569" class="Bound">γ&#39;</a> <a id="16736" href="plfa.part2.BigStep.html#2675" class="Function Operator">,&#39;</a> <a id="16739" href="plfa.part3.Adequacy.html#16671" class="Bound">c</a><a id="16740" class="Symbol">)</a> <a id="16742" href="plfa.part2.BigStep.html#3024" class="Datatype Operator">⊢</a> <a id="16744" href="plfa.part3.Adequacy.html#16591" class="Bound">N</a> <a id="16746" href="plfa.part2.BigStep.html#3024" class="Datatype Operator">⇓</a> <a id="16748" href="plfa.part3.Adequacy.html#16720" class="Bound">c&#39;</a> <a id="16752" href="https://agda.github.io/agda-stdlib/v1.1/Data.Product.html#1162" class="Function Operator">×</a> <a id="16755" href="plfa.part3.Adequacy.html#7123" class="Function">𝕍</a> <a id="16757" href="plfa.part3.Adequacy.html#16605" class="Bound">w</a> <a id="16759" href="plfa.part3.Adequacy.html#16720" class="Bound">c&#39;</a>
<a id="16772" href="/19.08/Adequacy/#16666" class="Function">E</a> <a id="16774" class="Symbol">{</a><a id="16775" href="plfa.part3.Adequacy.html#16775" class="Bound">c</a><a id="16776" class="Symbol">}</a> <a id="16778" href="plfa.part3.Adequacy.html#16778" class="Bound">𝔼vc</a> <a id="16782" href="plfa.part3.Adequacy.html#16782" class="Bound">fw</a> <a id="16785" class="Symbol">=</a> <a id="16787" href="plfa.part3.Adequacy.html#15926" class="Function">↓→𝔼</a> <a id="16791" class="Symbol">(λ</a> <a id="16794" class="Symbol">{</a><a id="16795" href="plfa.part3.Adequacy.html#16795" class="Bound">x</a><a id="16796" class="Symbol">}</a> <a id="16798" class="Symbol">→</a> <a id="16800" href="plfa.part3.Adequacy.html#8947" class="Function">𝔾-ext</a><a id="16805" class="Symbol">{</a><a id="16806" href="plfa.part3.Adequacy.html#16561" class="Bound">Γ</a><a id="16807" class="Symbol">}{</a><a id="16809" href="plfa.part3.Adequacy.html#16565" class="Bound">γ</a><a id="16810" class="Symbol">}{</a><a id="16812" href="plfa.part3.Adequacy.html#16569" class="Bound">γ&#39;</a><a id="16814" class="Symbol">}</a> <a id="16816" href="plfa.part3.Adequacy.html#16573" class="Bound">𝔾γγ&#39;</a> <a id="16821" href="plfa.part3.Adequacy.html#16778" class="Bound">𝔼vc</a> <a id="16825" class="Symbol">{</a><a id="16826" href="plfa.part3.Adequacy.html#16795" class="Bound">x</a><a id="16827" class="Symbol">})</a> <a id="16830" href="plfa.part3.Adequacy.html#16608" class="Bound">d</a> <a id="16832" href="plfa.part3.Adequacy.html#16782" class="Bound">fw</a>
<a id="16835" href="/19.08/Adequacy/#15926" class="Function">↓→𝔼</a> <a id="16839" href="plfa.part3.Adequacy.html#16839" class="Bound">𝔾γγ&#39;</a> <a id="16844" href="/19.08/Denotational/#9780" class="InductiveConstructor">⊥-intro</a> <a id="16852" href="plfa.part3.Adequacy.html#16852" class="Bound">f⊥</a> <a id="16855" class="Symbol">=</a> <a id="16857" href="https://agda.github.io/agda-stdlib/v1.1/Data.Empty.html#294" class="Function">⊥-elim</a> <a id="16864" class="Symbol">(</a><a id="16865" href="plfa.part3.Adequacy.html#4479" class="Function">above-fun⊥</a> <a id="16876" href="plfa.part3.Adequacy.html#16852" class="Bound">f⊥</a><a id="16878" class="Symbol">)</a>
<a id="16880" href="/19.08/Adequacy/#15926" class="Function">↓→𝔼</a> <a id="16884" href="plfa.part3.Adequacy.html#16884" class="Bound">𝔾γγ&#39;</a> <a id="16889" class="Symbol">(</a><a id="16890" href="/19.08/Denotational/#9847" class="InductiveConstructor">⊔-intro</a><a id="16897" class="Symbol">{</a><a id="16898" class="Argument">v</a> <a id="16900" class="Symbol">=</a> <a id="16902" href="plfa.part3.Adequacy.html#16902" class="Bound">v₁</a><a id="16904" class="Symbol">}{</a><a id="16906" class="Argument">w</a> <a id="16908" class="Symbol">=</a> <a id="16910" href="plfa.part3.Adequacy.html#16910" class="Bound">v₂</a><a id="16912" class="Symbol">}</a> <a id="16914" href="plfa.part3.Adequacy.html#16914" class="Bound">d₁</a> <a id="16917" href="plfa.part3.Adequacy.html#16917" class="Bound">d₂</a><a id="16919" class="Symbol">)</a> <a id="16921" href="plfa.part3.Adequacy.html#16921" class="Bound">fv12</a>
<a id="16930" class="Keyword">with</a> <a id="16935" href="/19.08/Adequacy/#6264" class="Function">above-fun?</a> <a id="16946" href="plfa.part3.Adequacy.html#16902" class="Bound">v₁</a> <a id="16949" class="Symbol">|</a> <a id="16951" href="plfa.part3.Adequacy.html#6264" class="Function">above-fun?</a> <a id="16962" href="plfa.part3.Adequacy.html#16910" class="Bound">v₂</a>
<a id="16965" class="Symbol">...</a> <a id="16969" class="Symbol">|</a> <a id="16971" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Nullary.html#641" class="InductiveConstructor">yes</a> <a id="16975" href="/19.08/Adequacy/#16975" class="Bound">fv1</a> <a id="16979" class="Symbol">|</a> <a id="16981" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Nullary.html#641" class="InductiveConstructor">yes</a> <a id="16985" href="plfa.part3.Adequacy.html#16985" class="Bound">fv2</a>
<a id="16993" class="Keyword">with</a> <a id="16998" href="/19.08/Adequacy/#15926" class="Function">↓→𝔼</a> <a id="17002" class="Bound">𝔾γγ&#39;</a> <a id="17007" class="Bound">d₁</a> <a id="17010" href="plfa.part3.Adequacy.html#16975" class="Bound">fv1</a> <a id="17014" class="Symbol">|</a> <a id="17016" href="plfa.part3.Adequacy.html#15926" class="Function">↓→𝔼</a> <a id="17020" class="Bound">𝔾γγ&#39;</a> <a id="17025" class="Bound">d₂</a> <a id="17028" href="plfa.part3.Adequacy.html#16985" class="Bound">fv2</a>
<a id="17032" class="Symbol">...</a> <a id="17036" class="Symbol">|</a> <a id="17038" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟨</a> <a id="17040" href="/19.08/Adequacy/#17040" class="Bound">c₁</a> <a id="17043" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">,</a> <a id="17045" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟨</a> <a id="17047" href="plfa.part3.Adequacy.html#17047" class="Bound">M⇓c₁</a> <a id="17052" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">,</a> <a id="17054" href="plfa.part3.Adequacy.html#17054" class="Bound">𝕍v₁</a> <a id="17058" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟩</a> <a id="17060" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟩</a> <a id="17062" class="Symbol">|</a> <a id="17064" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟨</a> <a id="17066" href="plfa.part3.Adequacy.html#17066" class="Bound">c₂</a> <a id="17069" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">,</a> <a id="17071" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟨</a> <a id="17073" href="plfa.part3.Adequacy.html#17073" class="Bound">M⇓c₂</a> <a id="17078" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">,</a> <a id="17080" href="plfa.part3.Adequacy.html#17080" class="Bound">𝕍v₂</a> <a id="17084" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟩</a> <a id="17086" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟩</a>
<a id="17092" class="Keyword">rewrite</a> <a id="17100" href="/19.08/BigStep/#4589" class="Function">⇓-determ</a> <a id="17109" href="/19.08/Adequacy/#17073" class="Bound">M⇓c₂</a> <a id="17114" href="plfa.part3.Adequacy.html#17047" class="Bound">M⇓c₁</a> <a id="17119" class="Symbol">=</a>
<a id="17125" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟨</a> <a id="17127" href="/19.08/Adequacy/#17040" class="Bound">c₁</a> <a id="17130" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">,</a> <a id="17132" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟨</a> <a id="17134" href="plfa.part3.Adequacy.html#17047" class="Bound">M⇓c₁</a> <a id="17139" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">,</a> <a id="17141" href="plfa.part3.Adequacy.html#9742" class="Function">𝕍⊔-intro</a> <a id="17150" href="plfa.part3.Adequacy.html#17054" class="Bound">𝕍v₁</a> <a id="17154" href="plfa.part3.Adequacy.html#17080" class="Bound">𝕍v₂</a> <a id="17158" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟩</a> <a id="17160" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟩</a>
<a id="17162" href="/19.08/Adequacy/#15926" class="Function">↓→𝔼</a> <a id="17166" href="plfa.part3.Adequacy.html#17166" class="Bound">𝔾γγ&#39;</a> <a id="17171" class="Symbol">(</a><a id="17172" href="/19.08/Denotational/#9847" class="InductiveConstructor">⊔-intro</a><a id="17179" class="Symbol">{</a><a id="17180" class="Argument">v</a> <a id="17182" class="Symbol">=</a> <a id="17184" href="plfa.part3.Adequacy.html#17184" class="Bound">v₁</a><a id="17186" class="Symbol">}{</a><a id="17188" class="Argument">w</a> <a id="17190" class="Symbol">=</a> <a id="17192" href="plfa.part3.Adequacy.html#17192" class="Bound">v₂</a><a id="17194" class="Symbol">}</a> <a id="17196" href="plfa.part3.Adequacy.html#17196" class="Bound">d₁</a> <a id="17199" href="plfa.part3.Adequacy.html#17199" class="Bound">d₂</a><a id="17201" class="Symbol">)</a> <a id="17203" href="plfa.part3.Adequacy.html#17203" class="Bound">fv12</a> <a id="17208" class="Symbol">|</a> <a id="17210" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Nullary.html#641" class="InductiveConstructor">yes</a> <a id="17214" href="plfa.part3.Adequacy.html#17214" class="Bound">fv1</a> <a id="17218" class="Symbol">|</a> <a id="17220" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Nullary.html#668" class="InductiveConstructor">no</a> <a id="17223" href="plfa.part3.Adequacy.html#17223" class="Bound">nfv2</a>
<a id="17232" class="Keyword">with</a> <a id="17237" href="/19.08/Adequacy/#15926" class="Function">↓→𝔼</a> <a id="17241" href="plfa.part3.Adequacy.html#17166" class="Bound">𝔾γγ&#39;</a> <a id="17246" href="plfa.part3.Adequacy.html#17196" class="Bound">d₁</a> <a id="17249" href="plfa.part3.Adequacy.html#17214" class="Bound">fv1</a>
<a id="17253" class="Symbol">...</a> <a id="17257" class="Symbol">|</a> <a id="17259" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟨</a> <a id="17261" href="/19.08/BigStep/#2489" class="InductiveConstructor">clos</a> <a id="17266" class="Symbol">{</a><a id="17267" href="/19.08/Adequacy/#17267" class="Bound">Γ&#39;</a><a id="17269" class="Symbol">}</a> <a id="17271" href="plfa.part3.Adequacy.html#17271" class="Bound">M&#39;</a> <a id="17274" href="plfa.part3.Adequacy.html#17274" class="Bound">γ₁</a> <a id="17277" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">,</a> <a id="17279" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟨</a> <a id="17281" href="plfa.part3.Adequacy.html#17281" class="Bound">M⇓c₁</a> <a id="17286" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">,</a> <a id="17288" href="plfa.part3.Adequacy.html#17288" class="Bound">𝕍v₁</a> <a id="17292" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟩</a> <a id="17294" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟩</a>
<a id="17300" class="Keyword">with</a> <a id="17305" href="/19.08/Adequacy/#9429" class="Function">𝕍→WHNF</a> <a id="17312" href="plfa.part3.Adequacy.html#17288" class="Bound">𝕍v₁</a>
<a id="17316" class="Symbol">...</a> <a id="17320" class="Symbol">|</a> <a id="17322" href="/19.08/Adequacy/#9322" class="InductiveConstructor Operator">ƛ_</a> <a id="17325" class="Symbol">{</a><a id="17326" class="Argument">N</a> <a id="17328" class="Symbol">=</a> <a id="17330" href="plfa.part3.Adequacy.html#17330" class="Bound">N</a><a id="17331" class="Symbol">}</a> <a id="17333" class="Symbol">=</a>
<a id="17339" class="Keyword">let</a> <a id="17343" href="/19.08/Adequacy/#17343" class="Bound">𝕍v₂</a> <a id="17347" class="Symbol">=</a> <a id="17349" href="plfa.part3.Adequacy.html#10391" class="Function">not-above-fun-𝕍</a><a id="17364" class="Symbol">{</a><a id="17365" class="Bound">v₂</a><a id="17367" class="Symbol">}{</a><a id="17369" class="Bound">Γ&#39;</a><a id="17371" class="Symbol">}{</a><a id="17373" class="Bound">γ₁</a><a id="17375" class="Symbol">}{</a><a id="17377" href="plfa.part3.Adequacy.html#17330" class="Bound">N</a><a id="17378" class="Symbol">}</a> <a id="17380" class="Bound">nfv2</a> <a id="17385" class="Keyword">in</a>
<a id="17392" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟨</a> <a id="17394" href="/19.08/BigStep/#2489" class="InductiveConstructor">clos</a> <a id="17399" class="Symbol">(</a><a id="17400" href="/19.08/Untyped/#4382" class="InductiveConstructor Operator">ƛ</a> <a id="17402" href="/19.08/Adequacy/#17330" class="Bound">N</a><a id="17403" class="Symbol">)</a> <a id="17405" class="Bound">γ₁</a> <a id="17408" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">,</a> <a id="17410" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟨</a> <a id="17412" class="Bound">M⇓c₁</a> <a id="17417" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">,</a> <a id="17419" href="plfa.part3.Adequacy.html#9742" class="Function">𝕍⊔-intro</a> <a id="17428" class="Bound">𝕍v₁</a> <a id="17432" href="plfa.part3.Adequacy.html#17343" class="Bound">𝕍v₂</a> <a id="17436" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟩</a> <a id="17438" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟩</a>
<a id="17440" href="/19.08/Adequacy/#15926" class="Function">↓→𝔼</a> <a id="17444" href="plfa.part3.Adequacy.html#17444" class="Bound">𝔾γγ&#39;</a> <a id="17449" class="Symbol">(</a><a id="17450" href="/19.08/Denotational/#9847" class="InductiveConstructor">⊔-intro</a><a id="17457" class="Symbol">{</a><a id="17458" class="Argument">v</a> <a id="17460" class="Symbol">=</a> <a id="17462" href="plfa.part3.Adequacy.html#17462" class="Bound">v₁</a><a id="17464" class="Symbol">}{</a><a id="17466" class="Argument">w</a> <a id="17468" class="Symbol">=</a> <a id="17470" href="plfa.part3.Adequacy.html#17470" class="Bound">v₂</a><a id="17472" class="Symbol">}</a> <a id="17474" href="plfa.part3.Adequacy.html#17474" class="Bound">d₁</a> <a id="17477" href="plfa.part3.Adequacy.html#17477" class="Bound">d₂</a><a id="17479" class="Symbol">)</a> <a id="17481" href="plfa.part3.Adequacy.html#17481" class="Bound">fv12</a> <a id="17486" class="Symbol">|</a> <a id="17488" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Nullary.html#668" class="InductiveConstructor">no</a> <a id="17491" href="plfa.part3.Adequacy.html#17491" class="Bound">nfv1</a> <a id="17497" class="Symbol">|</a> <a id="17499" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Nullary.html#641" class="InductiveConstructor">yes</a> <a id="17503" href="plfa.part3.Adequacy.html#17503" class="Bound">fv2</a>
<a id="17511" class="Keyword">with</a> <a id="17516" href="/19.08/Adequacy/#15926" class="Function">↓→𝔼</a> <a id="17520" href="plfa.part3.Adequacy.html#17444" class="Bound">𝔾γγ&#39;</a> <a id="17525" href="plfa.part3.Adequacy.html#17477" class="Bound">d₂</a> <a id="17528" href="plfa.part3.Adequacy.html#17503" class="Bound">fv2</a>
<a id="17532" class="Symbol">...</a> <a id="17536" class="Symbol">|</a> <a id="17538" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟨</a> <a id="17540" href="/19.08/BigStep/#2489" class="InductiveConstructor">clos</a> <a id="17545" class="Symbol">{</a><a id="17546" href="/19.08/Adequacy/#17546" class="Bound">Γ&#39;</a><a id="17548" class="Symbol">}</a> <a id="17550" href="plfa.part3.Adequacy.html#17550" class="Bound">M&#39;</a> <a id="17553" href="plfa.part3.Adequacy.html#17553" class="Bound">γ₁</a> <a id="17556" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">,</a> <a id="17558" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟨</a> <a id="17560" href="plfa.part3.Adequacy.html#17560" class="Bound">M&#39;⇓c₂</a> <a id="17566" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">,</a> <a id="17568" href="plfa.part3.Adequacy.html#17568" class="Bound">𝕍2c</a> <a id="17572" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟩</a> <a id="17574" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟩</a>
<a id="17580" class="Keyword">with</a> <a id="17585" href="/19.08/Adequacy/#9429" class="Function">𝕍→WHNF</a> <a id="17592" href="plfa.part3.Adequacy.html#17568" class="Bound">𝕍2c</a>
<a id="17596" class="Symbol">...</a> <a id="17600" class="Symbol">|</a> <a id="17602" href="/19.08/Adequacy/#9322" class="InductiveConstructor Operator">ƛ_</a> <a id="17605" class="Symbol">{</a><a id="17606" class="Argument">N</a> <a id="17608" class="Symbol">=</a> <a id="17610" href="plfa.part3.Adequacy.html#17610" class="Bound">N</a><a id="17611" class="Symbol">}</a> <a id="17613" class="Symbol">=</a>
<a id="17619" class="Keyword">let</a> <a id="17623" href="/19.08/Adequacy/#17623" class="Bound">𝕍1c</a> <a id="17627" class="Symbol">=</a> <a id="17629" href="plfa.part3.Adequacy.html#10391" class="Function">not-above-fun-𝕍</a><a id="17644" class="Symbol">{</a><a id="17645" class="Bound">v₁</a><a id="17647" class="Symbol">}{</a><a id="17649" class="Bound">Γ&#39;</a><a id="17651" class="Symbol">}{</a><a id="17653" class="Bound">γ₁</a><a id="17655" class="Symbol">}{</a><a id="17657" href="plfa.part3.Adequacy.html#17610" class="Bound">N</a><a id="17658" class="Symbol">}</a> <a id="17660" class="Bound">nfv1</a> <a id="17665" class="Keyword">in</a>
<a id="17672" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟨</a> <a id="17674" href="/19.08/BigStep/#2489" class="InductiveConstructor">clos</a> <a id="17679" class="Symbol">(</a><a id="17680" href="/19.08/Untyped/#4382" class="InductiveConstructor Operator">ƛ</a> <a id="17682" href="/19.08/Adequacy/#17610" class="Bound">N</a><a id="17683" class="Symbol">)</a> <a id="17685" class="Bound">γ₁</a> <a id="17688" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">,</a> <a id="17690" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟨</a> <a id="17692" class="Bound">M&#39;⇓c₂</a> <a id="17698" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">,</a> <a id="17700" href="plfa.part3.Adequacy.html#9742" class="Function">𝕍⊔-intro</a> <a id="17709" href="plfa.part3.Adequacy.html#17623" class="Bound">𝕍1c</a> <a id="17713" class="Bound">𝕍2c</a> <a id="17717" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟩</a> <a id="17719" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟩</a>
<a id="17721" href="/19.08/Adequacy/#15926" class="Function">↓→𝔼</a> <a id="17725" href="plfa.part3.Adequacy.html#17725" class="Bound">𝔾γγ&#39;</a> <a id="17730" class="Symbol">(</a><a id="17731" href="/19.08/Denotational/#9847" class="InductiveConstructor">⊔-intro</a> <a id="17739" href="plfa.part3.Adequacy.html#17739" class="Bound">d₁</a> <a id="17742" href="plfa.part3.Adequacy.html#17742" class="Bound">d₂</a><a id="17744" class="Symbol">)</a> <a id="17746" href="plfa.part3.Adequacy.html#17746" class="Bound">fv12</a> <a id="17751" class="Symbol">|</a> <a id="17753" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Nullary.html#668" class="InductiveConstructor">no</a> <a id="17756" href="plfa.part3.Adequacy.html#17756" class="Bound">nfv1</a> <a id="17762" class="Symbol">|</a> <a id="17764" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Nullary.html#668" class="InductiveConstructor">no</a> <a id="17767" href="plfa.part3.Adequacy.html#17767" class="Bound">nfv2</a>
<a id="17776" class="Keyword">with</a> <a id="17781" href="/19.08/Adequacy/#4786" class="Function">above-fun-⊔</a> <a id="17793" href="plfa.part3.Adequacy.html#17746" class="Bound">fv12</a>
<a id="17798" class="Symbol">...</a> <a id="17802" class="Symbol">|</a> <a id="17804" href="https://agda.github.io/agda-stdlib/v1.1/Data.Sum.Base.html#662" class="InductiveConstructor">inj₁</a> <a id="17809" href="/19.08/Adequacy/#17809" class="Bound">fv1</a> <a id="17813" class="Symbol">=</a> <a id="17815" href="https://agda.github.io/agda-stdlib/v1.1/Data.Empty.html#294" class="Function">⊥-elim</a> <a id="17822" class="Symbol">(</a><a id="17823" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Nullary.Negation.html#809" class="Function">contradiction</a> <a id="17837" href="plfa.part3.Adequacy.html#17809" class="Bound">fv1</a> <a id="17841" class="Bound">nfv1</a><a id="17845" class="Symbol">)</a>
<a id="17847" class="Symbol">...</a> <a id="17851" class="Symbol">|</a> <a id="17853" href="https://agda.github.io/agda-stdlib/v1.1/Data.Sum.Base.html#687" class="InductiveConstructor">inj₂</a> <a id="17858" href="/19.08/Adequacy/#17858" class="Bound">fv2</a> <a id="17862" class="Symbol">=</a> <a id="17864" href="https://agda.github.io/agda-stdlib/v1.1/Data.Empty.html#294" class="Function">⊥-elim</a> <a id="17871" class="Symbol">(</a><a id="17872" href="https://agda.github.io/agda-stdlib/v1.1/Relation.Nullary.Negation.html#809" class="Function">contradiction</a> <a id="17886" href="plfa.part3.Adequacy.html#17858" class="Bound">fv2</a> <a id="17890" class="Bound">nfv2</a><a id="17894" class="Symbol">)</a>
<a id="17896" href="/19.08/Adequacy/#15926" class="Function">↓→𝔼</a> <a id="17900" class="Symbol">{</a><a id="17901" href="plfa.part3.Adequacy.html#17901" class="Bound">Γ</a><a id="17902" class="Symbol">}</a> <a id="17904" class="Symbol">{</a><a id="17905" href="plfa.part3.Adequacy.html#17905" class="Bound">γ</a><a id="17906" class="Symbol">}</a> <a id="17908" class="Symbol">{</a><a id="17909" href="plfa.part3.Adequacy.html#17909" class="Bound">γ&#39;</a><a id="17911" class="Symbol">}</a> <a id="17913" class="Symbol">{</a><a id="17914" href="plfa.part3.Adequacy.html#17914" class="Bound">M</a><a id="17915" class="Symbol">}</a> <a id="17917" class="Symbol">{</a><a id="17918" href="plfa.part3.Adequacy.html#17918" class="Bound">v&#39;</a><a id="17920" class="Symbol">}</a> <a id="17922" href="plfa.part3.Adequacy.html#17922" class="Bound">𝔾γγ&#39;</a> <a id="17927" class="Symbol">(</a><a id="17928" href="/19.08/Denotational/#9962" class="InductiveConstructor">sub</a><a id="17931" class="Symbol">{</a><a id="17932" class="Argument">v</a> <a id="17934" class="Symbol">=</a> <a id="17936" href="plfa.part3.Adequacy.html#17936" class="Bound">v</a><a id="17937" class="Symbol">}</a> <a id="17939" href="plfa.part3.Adequacy.html#17939" class="Bound">d</a> <a id="17941" href="plfa.part3.Adequacy.html#17941" class="Bound">v&#39;⊑v</a><a id="17945" class="Symbol">)</a> <a id="17947" href="plfa.part3.Adequacy.html#17947" class="Bound">fv&#39;</a>
<a id="17955" class="Keyword">with</a> <a id="17960" href="/19.08/Adequacy/#15926" class="Function">↓→𝔼</a> <a id="17964" class="Symbol">{</a><a id="17965" href="plfa.part3.Adequacy.html#17901" class="Bound">Γ</a><a id="17966" class="Symbol">}</a> <a id="17968" class="Symbol">{</a><a id="17969" href="plfa.part3.Adequacy.html#17905" class="Bound">γ</a><a id="17970" class="Symbol">}</a> <a id="17972" class="Symbol">{</a><a id="17973" href="plfa.part3.Adequacy.html#17909" class="Bound">γ&#39;</a><a id="17975" class="Symbol">}</a> <a id="17977" class="Symbol">{</a><a id="17978" href="plfa.part3.Adequacy.html#17914" class="Bound">M</a><a id="17979" class="Symbol">}</a> <a id="17981" href="plfa.part3.Adequacy.html#17922" class="Bound">𝔾γγ&#39;</a> <a id="17986" href="plfa.part3.Adequacy.html#17939" class="Bound">d</a> <a id="17988" class="Symbol">(</a><a id="17989" href="plfa.part3.Adequacy.html#4240" class="Function">above-fun-⊑</a> <a id="18001" href="plfa.part3.Adequacy.html#17947" class="Bound">fv&#39;</a> <a id="18005" href="plfa.part3.Adequacy.html#17941" class="Bound">v&#39;⊑v</a><a id="18009" class="Symbol">)</a>
<a id="18011" class="Symbol">...</a> <a id="18015" class="Symbol">|</a> <a id="18017" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟨</a> <a id="18019" href="/19.08/Adequacy/#18019" class="Bound">c</a> <a id="18021" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">,</a> <a id="18023" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟨</a> <a id="18025" href="plfa.part3.Adequacy.html#18025" class="Bound">M⇓c</a> <a id="18029" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">,</a> <a id="18031" href="plfa.part3.Adequacy.html#18031" class="Bound">𝕍v</a> <a id="18034" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟩</a> <a id="18036" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟩</a> <a id="18038" class="Symbol">=</a>
<a id="18046" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟨</a> <a id="18048" href="/19.08/Adequacy/#18019" class="Bound">c</a> <a id="18050" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">,</a> <a id="18052" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟨</a> <a id="18054" href="plfa.part3.Adequacy.html#18025" class="Bound">M⇓c</a> <a id="18058" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">,</a> <a id="18060" href="plfa.part3.Adequacy.html#10827" class="Function">sub-𝕍</a> <a id="18066" href="plfa.part3.Adequacy.html#18031" class="Bound">𝕍v</a> <a id="18069" class="Bound">v&#39;⊑v</a> <a id="18074" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟩</a> <a id="18076" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟩</a>
</pre>
<ul>
<li>
<p>Case <code class="language-plaintext highlighter-rouge">var</code>. Looking up <code class="language-plaintext highlighter-rouge">x</code> in <code class="language-plaintext highlighter-rouge">γ'</code> yields some closure, <code class="language-plaintext highlighter-rouge">clos M' δ</code>,
and from <code class="language-plaintext highlighter-rouge">𝔾 γ γ'</code> we have <code class="language-plaintext highlighter-rouge">𝔼 (γ x) (clos M' δ)</code>. With the premise
<code class="language-plaintext highlighter-rouge">above-fun (γ x)</code>, we obtain a closure <code class="language-plaintext highlighter-rouge">c</code> such that <code class="language-plaintext highlighter-rouge">δ ⊢ M' ⇓ c</code>
and <code class="language-plaintext highlighter-rouge">𝕍 (γ x) c</code>. To conclude <code class="language-plaintext highlighter-rouge">γ' ⊢ x ⇓ c</code> via <code class="language-plaintext highlighter-rouge">⇓-var</code>, we
need <code class="language-plaintext highlighter-rouge">γ' x ≡ clos M' δ</code>, which is obvious, but it requires some
Agda shananigans via the <code class="language-plaintext highlighter-rouge">kth-x</code> lemma to get our hands on it.</p>
</li>
<li>
<p>Case <code class="language-plaintext highlighter-rouge">↦-elim</code>. We have <code class="language-plaintext highlighter-rouge">γ ⊢ L · M ↓ v</code>.
The induction hypothesis for <code class="language-plaintext highlighter-rouge">γ ⊢ L ↓ v₁ ↦ v</code>
gives us <code class="language-plaintext highlighter-rouge">γ' ⊢ L ⇓ clos L' δ</code> and <code class="language-plaintext highlighter-rouge">𝕍 v (clos L' δ)</code>.
Of course, <code class="language-plaintext highlighter-rouge">L' ≡ ƛ N</code> for some <code class="language-plaintext highlighter-rouge">N</code>.
By the induction hypothesis for <code class="language-plaintext highlighter-rouge">γ ⊢ M ↓ v₁</code>,
we have <code class="language-plaintext highlighter-rouge">𝔼 v₁ (clos M γ')</code>.
Together with the premise <code class="language-plaintext highlighter-rouge">above-fun v</code> and <code class="language-plaintext highlighter-rouge">𝕍 v (clos L' δ)</code>,
we obtain a closure <code class="language-plaintext highlighter-rouge">c'</code> such that <code class="language-plaintext highlighter-rouge">δ ⊢ N ⇓ c'</code> and <code class="language-plaintext highlighter-rouge">𝕍 v c'</code>.
We conclude that <code class="language-plaintext highlighter-rouge">γ' ⊢ L · M ⇓ c'</code> by rule <code class="language-plaintext highlighter-rouge">⇓-app</code>.</p>
</li>
<li>
<p>Case <code class="language-plaintext highlighter-rouge">↦-intro</code>. We have <code class="language-plaintext highlighter-rouge">γ ⊢ ƛ N ↓ v ↦ w</code>.
We immediately have <code class="language-plaintext highlighter-rouge">γ' ⊢ ƛ M ⇓ clos (ƛ M) γ'</code> by rule <code class="language-plaintext highlighter-rouge">⇓-lam</code>.
But we also need to prove <code class="language-plaintext highlighter-rouge">𝕍 (v ↦ w) (clos (ƛ N) γ')</code>.
Let <code class="language-plaintext highlighter-rouge">c</code> by an arbitrary closure such that <code class="language-plaintext highlighter-rouge">𝔼 v c</code>.
Suppose <code class="language-plaintext highlighter-rouge">v'</code> is greater than a function value.
We need to show that <code class="language-plaintext highlighter-rouge">γ' , c ⊢ N ⇓ c'</code> and <code class="language-plaintext highlighter-rouge">𝕍 v' c'</code> for some <code class="language-plaintext highlighter-rouge">c'</code>.
We prove this by the induction hypothesis for <code class="language-plaintext highlighter-rouge">γ , v ⊢ N ↓ v'</code>
but we must first show that <code class="language-plaintext highlighter-rouge">𝔾 (γ , v) (γ' , c)</code>. We prove
that by the lemma <code class="language-plaintext highlighter-rouge">𝔾-ext</code>, using facts <code class="language-plaintext highlighter-rouge">𝔾 γ γ'</code> and <code class="language-plaintext highlighter-rouge">𝔼 v c</code>.</p>
</li>
<li>
<p>Case <code class="language-plaintext highlighter-rouge">⊥-intro</code>. We have the premise <code class="language-plaintext highlighter-rouge">above-fun ⊥</code>, but that’s impossible.</p>
</li>
<li>
<p>Case <code class="language-plaintext highlighter-rouge">⊔-intro</code>. We have <code class="language-plaintext highlighter-rouge">γ ⊢ M ↓ (v₁ ⊔ v₂)</code> and <code class="language-plaintext highlighter-rouge">above-fun (v₁ ⊔ v₂)</code>
and need to show <code class="language-plaintext highlighter-rouge">γ' ⊢ M ↓ c</code> and <code class="language-plaintext highlighter-rouge">𝕍 (v₁ ⊔ v₂) c</code> for some <code class="language-plaintext highlighter-rouge">c</code>.
Again, by <code class="language-plaintext highlighter-rouge">above-fun-⊔</code>, at least one of <code class="language-plaintext highlighter-rouge">v₁</code> or <code class="language-plaintext highlighter-rouge">v₂</code> is greater than
a function.</p>
<ul>
<li>
<p>Suppose both <code class="language-plaintext highlighter-rouge">v₁</code> and <code class="language-plaintext highlighter-rouge">v₂</code> are greater than a function value.
By the induction hypotheses for <code class="language-plaintext highlighter-rouge">γ ⊢ M ↓ v₁</code> and <code class="language-plaintext highlighter-rouge">γ ⊢ M ↓ v₂</code>
we have <code class="language-plaintext highlighter-rouge">γ' ⊢ M ⇓ c₁</code>, <code class="language-plaintext highlighter-rouge">𝕍 v₁ c₁</code>, <code class="language-plaintext highlighter-rouge">γ' ⊢ M ⇓ c₂</code>, and <code class="language-plaintext highlighter-rouge">𝕍 v₂ c₂</code>
for some <code class="language-plaintext highlighter-rouge">c₁</code> and <code class="language-plaintext highlighter-rouge">c₂</code>. Because <code class="language-plaintext highlighter-rouge">⇓</code> is deterministic, we have <code class="language-plaintext highlighter-rouge">c₂ ≡ c₁</code>.
Then by <code class="language-plaintext highlighter-rouge">𝕍⊔-intro</code> we conclude that <code class="language-plaintext highlighter-rouge">𝕍 (v₁ ⊔ v₂) c₁</code>.</p>
</li>
<li>
<p>Without loss of generality, suppose <code class="language-plaintext highlighter-rouge">v₁</code> is greater than a function
value but <code class="language-plaintext highlighter-rouge">v₂</code> is not. By the induction hypotheses for <code class="language-plaintext highlighter-rouge">γ ⊢ M ↓ v₁</code>,
and using <code class="language-plaintext highlighter-rouge">𝕍→WHNF</code>, we have <code class="language-plaintext highlighter-rouge">γ' ⊢ M ⇓ clos (ƛ N) γ₁</code>
and <code class="language-plaintext highlighter-rouge">𝕍 v₁ (clos (ƛ N) γ₁)</code>.
Then because <code class="language-plaintext highlighter-rouge">v₂</code> is not greater than a function, we also have
<code class="language-plaintext highlighter-rouge">𝕍 v₂ (clos (ƛ N) γ₁)</code>. We conclude that <code class="language-plaintext highlighter-rouge">𝕍 (v₁ ⊔ v₂) (clos (ƛ N) γ₁)</code>.</p>
</li>
</ul>
</li>
<li>
<p>Case <code class="language-plaintext highlighter-rouge">sub</code>. We have <code class="language-plaintext highlighter-rouge">γ ⊢ M ↓ v</code>, <code class="language-plaintext highlighter-rouge">v' ⊑ v</code>, and <code class="language-plaintext highlighter-rouge">above-fun v'</code>.
We need to show that <code class="language-plaintext highlighter-rouge">γ' ⊢ M ⇓ c</code> and <code class="language-plaintext highlighter-rouge">𝕍 v' c</code> for some <code class="language-plaintext highlighter-rouge">c</code>.
We have <code class="language-plaintext highlighter-rouge">above-fun v</code> by <code class="language-plaintext highlighter-rouge">above-fun-⊑</code>,
so the induction hypothesis for <code class="language-plaintext highlighter-rouge">γ ⊢ M ↓ v</code> gives us a closure <code class="language-plaintext highlighter-rouge">c</code>
such that <code class="language-plaintext highlighter-rouge">γ' ⊢ M ⇓ c</code> and <code class="language-plaintext highlighter-rouge">𝕍 v c</code>. We conclude that <code class="language-plaintext highlighter-rouge">𝕍 v' c</code> by <code class="language-plaintext highlighter-rouge">sub-𝕍</code>.</p>
</li>
</ul>
<h2 id="proof-of-denotational-adequacy">Proof of denotational adequacy</h2>
<p>The adequacy property is a corollary of the main lemma.
We have <code class="language-plaintext highlighter-rouge">∅ ⊢ ƛ N ↓ ⊥ ↦ ⊥</code>, so <code class="language-plaintext highlighter-rouge">ℰ M ≃ ℰ (ƛ N)</code>
gives us <code class="language-plaintext highlighter-rouge">∅ ⊢ M ↓ ⊥ ↦ ⊥</code>. Then the main lemma gives us
<code class="language-plaintext highlighter-rouge">∅ ⊢ M ⇓ clos (ƛ N′) γ</code> for some <code class="language-plaintext highlighter-rouge">N′</code> and <code class="language-plaintext highlighter-rouge">γ</code>.</p>
<pre class="Agda"><a id="adequacy"></a><a id="21034" href="/19.08/Adequacy/#21034" class="Function">adequacy</a> <a id="21043" class="Symbol">:</a> <a id="21045" class="Symbol">∀{</a><a id="21047" href="plfa.part3.Adequacy.html#21047" class="Bound">M</a> <a id="21049" class="Symbol">:</a> <a id="21051" href="/19.08/Untyped/#3175" class="InductiveConstructor">∅</a> <a id="21053" href="plfa.part2.Untyped.html#4294" class="Datatype Operator">⊢</a> <a id="21055" href="plfa.part2.Untyped.html#2888" class="InductiveConstructor">★</a><a id="21056" class="Symbol">}{</a><a id="21058" href="plfa.part3.Adequacy.html#21058" class="Bound">N</a> <a id="21060" class="Symbol">:</a> <a id="21062" href="plfa.part2.Untyped.html#3175" class="InductiveConstructor">∅</a> <a id="21064" href="plfa.part2.Untyped.html#3191" class="InductiveConstructor Operator">,</a> <a id="21066" href="plfa.part2.Untyped.html#2888" class="InductiveConstructor">★</a> <a id="21068" href="plfa.part2.Untyped.html#4294" class="Datatype Operator">⊢</a> <a id="21070" href="plfa.part2.Untyped.html#2888" class="InductiveConstructor">★</a><a id="21071" class="Symbol">}</a> <a id="21074" class="Symbol">→</a> <a id="21077" href="/19.08/Denotational/#17516" class="Function">ℰ</a> <a id="21079" href="plfa.part3.Adequacy.html#21047" class="Bound">M</a> <a id="21081" href="plfa.part3.Denotational.html#17698" class="Function Operator">≃</a> <a id="21083" href="plfa.part3.Denotational.html#17516" class="Function">ℰ</a> <a id="21085" class="Symbol">(</a><a id="21086" href="plfa.part2.Untyped.html#4382" class="InductiveConstructor Operator">ƛ</a> <a id="21088" href="plfa.part3.Adequacy.html#21058" class="Bound">N</a><a id="21089" class="Symbol">)</a>
<a id="21100" class="Symbol">→</a> <a id="21103" href="https://agda.github.io/agda-stdlib/v1.1/Data.Product.html#911" class="Function">Σ[</a> <a id="21106" href="/19.08/Adequacy/#21106" class="Bound">Γ</a> <a id="21108" href="https://agda.github.io/agda-stdlib/v1.1/Data.Product.html#911" class="Function">∈</a> <a id="21110" href="/19.08/Untyped/#3153" class="Datatype">Context</a> <a id="21118" href="https://agda.github.io/agda-stdlib/v1.1/Data.Product.html#911" class="Function">]</a> <a id="21120" href="https://agda.github.io/agda-stdlib/v1.1/Data.Product.html#911" class="Function">Σ[</a> <a id="21123" href="plfa.part3.Adequacy.html#21123" class="Bound">N′</a> <a id="21126" href="https://agda.github.io/agda-stdlib/v1.1/Data.Product.html#911" class="Function">∈</a> <a id="21128" class="Symbol">(</a><a id="21129" href="plfa.part3.Adequacy.html#21106" class="Bound">Γ</a> <a id="21131" href="plfa.part2.Untyped.html#3191" class="InductiveConstructor Operator">,</a> <a id="21133" href="plfa.part2.Untyped.html#2888" class="InductiveConstructor">★</a> <a id="21135" href="plfa.part2.Untyped.html#4294" class="Datatype Operator">⊢</a> <a id="21137" href="plfa.part2.Untyped.html#2888" class="InductiveConstructor">★</a><a id="21138" class="Symbol">)</a> <a id="21140" href="https://agda.github.io/agda-stdlib/v1.1/Data.Product.html#911" class="Function">]</a> <a id="21142" href="https://agda.github.io/agda-stdlib/v1.1/Data.Product.html#911" class="Function">Σ[</a> <a id="21145" href="plfa.part3.Adequacy.html#21145" class="Bound">γ</a> <a id="21147" href="https://agda.github.io/agda-stdlib/v1.1/Data.Product.html#911" class="Function">∈</a> <a id="21149" href="/19.08/BigStep/#2440" class="Function">ClosEnv</a> <a id="21157" href="plfa.part3.Adequacy.html#21106" class="Bound">Γ</a> <a id="21159" href="https://agda.github.io/agda-stdlib/v1.1/Data.Product.html#911" class="Function">]</a>
<a id="21173" href="/19.08/BigStep/#2653" class="Function">∅&#39;</a> <a id="21176" href="plfa.part2.BigStep.html#3024" class="Datatype Operator">⊢</a> <a id="21178" href="/19.08/Adequacy/#21047" class="Bound">M</a> <a id="21180" href="plfa.part2.BigStep.html#3024" class="Datatype Operator">⇓</a> <a id="21182" href="plfa.part2.BigStep.html#2489" class="InductiveConstructor">clos</a> <a id="21187" class="Symbol">(</a><a id="21188" href="/19.08/Untyped/#4382" class="InductiveConstructor Operator">ƛ</a> <a id="21190" href="plfa.part3.Adequacy.html#21123" class="Bound">N′</a><a id="21192" class="Symbol">)</a> <a id="21194" href="plfa.part3.Adequacy.html#21145" class="Bound">γ</a>
<a id="21196" href="/19.08/Adequacy/#21034" class="Function">adequacy</a><a id="21204" class="Symbol">{</a><a id="21205" href="plfa.part3.Adequacy.html#21205" class="Bound">M</a><a id="21206" class="Symbol">}{</a><a id="21208" href="plfa.part3.Adequacy.html#21208" class="Bound">N</a><a id="21209" class="Symbol">}</a> <a id="21211" href="plfa.part3.Adequacy.html#21211" class="Bound">eq</a>
<a id="21218" class="Keyword">with</a> <a id="21223" href="/19.08/Adequacy/#15926" class="Function">↓→𝔼</a> <a id="21227" href="plfa.part3.Adequacy.html#8923" class="Function">𝔾-∅</a> <a id="21231" class="Symbol">((</a><a id="21233" href="Agda.Builtin.Sigma.html#237" class="Field">proj₂</a> <a id="21239" class="Symbol">(</a><a id="21240" href="plfa.part3.Adequacy.html#21211" class="Bound">eq</a> <a id="21243" href="/19.08/Denotational/#7331" class="Function">`∅</a> <a id="21246" class="Symbol">(</a><a id="21247" href="plfa.part3.Denotational.html#4090" class="InductiveConstructor">⊥</a> <a id="21249" href="plfa.part3.Denotational.html#4102" class="InductiveConstructor Operator">↦</a> <a id="21251" href="plfa.part3.Denotational.html#4090" class="InductiveConstructor">⊥</a><a id="21252" class="Symbol">)))</a> <a id="21256" class="Symbol">(</a><a id="21257" href="plfa.part3.Denotational.html#9668" class="InductiveConstructor">↦-intro</a> <a id="21265" href="plfa.part3.Denotational.html#9780" class="InductiveConstructor">⊥-intro</a><a id="21272" class="Symbol">))</a>
<a id="21292" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟨</a> <a id="21294" href="/19.08/Denotational/#4090" class="InductiveConstructor">⊥</a> <a id="21296" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">,</a> <a id="21298" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟨</a> <a id="21300" href="plfa.part3.Denotational.html#4090" class="InductiveConstructor">⊥</a> <a id="21302" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">,</a> <a id="21304" href="plfa.part3.Denotational.html#5557" class="Function">⊑-refl</a> <a id="21311" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟩</a> <a id="21313" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟩</a>
<a id="21315" class="Symbol">...</a> <a id="21319" class="Symbol">|</a> <a id="21321" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟨</a> <a id="21323" href="/19.08/BigStep/#2489" class="InductiveConstructor">clos</a> <a id="21328" class="Symbol">{</a><a id="21329" href="/19.08/Adequacy/#21329" class="Bound">Γ</a><a id="21330" class="Symbol">}</a> <a id="21332" href="plfa.part3.Adequacy.html#21332" class="Bound">M′</a> <a id="21335" href="plfa.part3.Adequacy.html#21335" class="Bound">γ</a> <a id="21337" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">,</a> <a id="21339" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟨</a> <a id="21341" href="plfa.part3.Adequacy.html#21341" class="Bound">M⇓c</a> <a id="21345" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">,</a> <a id="21347" href="plfa.part3.Adequacy.html#21347" class="Bound">Vc</a> <a id="21350" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟩</a> <a id="21352" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟩</a>
<a id="21358" class="Keyword">with</a> <a id="21363" href="/19.08/Adequacy/#9429" class="Function">𝕍→WHNF</a> <a id="21370" href="plfa.part3.Adequacy.html#21347" class="Bound">Vc</a>
<a id="21373" class="Symbol">...</a> <a id="21377" class="Symbol">|</a> <a id="21379" href="/19.08/Adequacy/#9322" class="InductiveConstructor Operator">ƛ_</a> <a id="21382" class="Symbol">{</a><a id="21383" class="Argument">N</a> <a id="21385" class="Symbol">=</a> <a id="21387" href="plfa.part3.Adequacy.html#21387" class="Bound">N′</a><a id="21389" class="Symbol">}</a> <a id="21391" class="Symbol">=</a>
<a id="21397" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟨</a> <a id="21399" class="Bound">Γ</a> <a id="21401" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">,</a> <a id="21403" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟨</a> <a id="21405" href="/19.08/Adequacy/#21387" class="Bound">N′</a> <a id="21408" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">,</a> <a id="21410" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟨</a> <a id="21412" class="Bound">γ</a> <a id="21414" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">,</a> <a id="21416" class="Bound">M⇓c</a> <a id="21420" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟩</a> <a id="21423" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟩</a> <a id="21425" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟩</a>
</pre>
<h2 id="call-by-name-is-equivalent-to-beta-reduction">Call-by-name is equivalent to beta reduction</h2>
<p>As promised, we return to the question of whether call-by-name
evaluation is equivalent to beta reduction. In the chapter CallByName
we established the forward direction: that if call-by-name produces a
result, then the program beta reduces to a lambda abstraction. We now
prove the backward direction of the if-and-only-if, leveraging our
results about the denotational semantics.</p>
<pre class="Agda"><a id="reduce→cbn"></a><a id="21870" href="/19.08/Adequacy/#21870" class="Function">reduce→cbn</a> <a id="21881" class="Symbol">:</a> <a id="21883" class="Symbol">∀</a> <a id="21885" class="Symbol">{</a><a id="21886" href="plfa.part3.Adequacy.html#21886" class="Bound">M</a> <a id="21888" class="Symbol">:</a> <a id="21890" href="/19.08/Untyped/#3175" class="InductiveConstructor">∅</a> <a id="21892" href="plfa.part2.Untyped.html#4294" class="Datatype Operator">⊢</a> <a id="21894" href="plfa.part2.Untyped.html#2888" class="InductiveConstructor">★</a><a id="21895" class="Symbol">}</a> <a id="21897" class="Symbol">{</a><a id="21898" href="plfa.part3.Adequacy.html#21898" class="Bound">N</a> <a id="21900" class="Symbol">:</a> <a id="21902" href="plfa.part2.Untyped.html#3175" class="InductiveConstructor">∅</a> <a id="21904" href="plfa.part2.Untyped.html#3191" class="InductiveConstructor Operator">,</a> <a id="21906" href="plfa.part2.Untyped.html#2888" class="InductiveConstructor">★</a> <a id="21908" href="plfa.part2.Untyped.html#4294" class="Datatype Operator">⊢</a> <a id="21910" href="plfa.part2.Untyped.html#2888" class="InductiveConstructor">★</a><a id="21911" class="Symbol">}</a>
<a id="21924" class="Symbol">→</a> <a id="21926" href="/19.08/Adequacy/#21886" class="Bound">M</a> <a id="21928" href="/19.08/Untyped/#11267" class="Datatype Operator">—↠</a> <a id="21931" href="plfa.part2.Untyped.html#4382" class="InductiveConstructor Operator">ƛ</a> <a id="21933" href="plfa.part3.Adequacy.html#21898" class="Bound">N</a>
<a id="21946" class="Symbol">→</a> <a id="21948" href="https://agda.github.io/agda-stdlib/v1.1/Data.Product.html#911" class="Function">Σ[</a> <a id="21951" href="/19.08/Adequacy/#21951" class="Bound">Δ</a> <a id="21953" href="https://agda.github.io/agda-stdlib/v1.1/Data.Product.html#911" class="Function">∈</a> <a id="21955" href="/19.08/Untyped/#3153" class="Datatype">Context</a> <a id="21963" href="https://agda.github.io/agda-stdlib/v1.1/Data.Product.html#911" class="Function">]</a> <a id="21965" href="https://agda.github.io/agda-stdlib/v1.1/Data.Product.html#911" class="Function">Σ[</a> <a id="21968" href="plfa.part3.Adequacy.html#21968" class="Bound">N′</a> <a id="21971" href="https://agda.github.io/agda-stdlib/v1.1/Data.Product.html#911" class="Function">∈</a> <a id="21973" href="plfa.part3.Adequacy.html#21951" class="Bound">Δ</a> <a id="21975" href="plfa.part2.Untyped.html#3191" class="InductiveConstructor Operator">,</a> <a id="21977" href="plfa.part2.Untyped.html#2888" class="InductiveConstructor">★</a> <a id="21979" href="plfa.part2.Untyped.html#4294" class="Datatype Operator">⊢</a> <a id="21981" href="plfa.part2.Untyped.html#2888" class="InductiveConstructor">★</a> <a id="21983" href="https://agda.github.io/agda-stdlib/v1.1/Data.Product.html#911" class="Function">]</a> <a id="21985" href="https://agda.github.io/agda-stdlib/v1.1/Data.Product.html#911" class="Function">Σ[</a> <a id="21988" href="plfa.part3.Adequacy.html#21988" class="Bound">δ</a> <a id="21990" href="https://agda.github.io/agda-stdlib/v1.1/Data.Product.html#911" class="Function">∈</a> <a id="21992" href="/19.08/BigStep/#2440" class="Function">ClosEnv</a> <a id="22000" href="plfa.part3.Adequacy.html#21951" class="Bound">Δ</a> <a id="22002" href="https://agda.github.io/agda-stdlib/v1.1/Data.Product.html#911" class="Function">]</a>
<a id="22017" href="/19.08/BigStep/#2653" class="Function">∅&#39;</a> <a id="22020" href="plfa.part2.BigStep.html#3024" class="Datatype Operator">⊢</a> <a id="22022" href="/19.08/Adequacy/#21886" class="Bound">M</a> <a id="22024" href="plfa.part2.BigStep.html#3024" class="Datatype Operator">⇓</a> <a id="22026" href="plfa.part2.BigStep.html#2489" class="InductiveConstructor">clos</a> <a id="22031" class="Symbol">(</a><a id="22032" href="/19.08/Untyped/#4382" class="InductiveConstructor Operator">ƛ</a> <a id="22034" href="plfa.part3.Adequacy.html#21968" class="Bound">N′</a><a id="22036" class="Symbol">)</a> <a id="22038" href="plfa.part3.Adequacy.html#21988" class="Bound">δ</a>
<a id="22040" href="/19.08/Adequacy/#21870" class="Function">reduce→cbn</a> <a id="22051" href="plfa.part3.Adequacy.html#22051" class="Bound">M—↠ƛN</a> <a id="22057" class="Symbol">=</a> <a id="22059" href="plfa.part3.Adequacy.html#21034" class="Function">adequacy</a> <a id="22068" class="Symbol">(</a><a id="22069" href="/19.08/Soundness/#23426" class="Function">soundness</a> <a id="22079" href="plfa.part3.Adequacy.html#22051" class="Bound">M—↠ƛN</a><a id="22084" class="Symbol">)</a>
</pre>
<p>Suppose <code class="language-plaintext highlighter-rouge">M —↠ ƛ N</code>. Soundness of the denotational semantics gives us
<code class="language-plaintext highlighter-rouge">ℰ M ≃ ℰ (ƛ N)</code>. Then by adequacy we conclude that
<code class="language-plaintext highlighter-rouge">∅' ⊢ M ⇓ clos (ƛ N′) δ</code> for some <code class="language-plaintext highlighter-rouge">N′</code> and <code class="language-plaintext highlighter-rouge">δ</code>.</p>
<p>Putting the two directions of the if-and-only-if together, we
establish that call-by-name evaluation is equivalent to beta reduction
in the following sense.</p>
<pre class="Agda"><a id="cbn↔reduce"></a><a id="22422" href="/19.08/Adequacy/#22422" class="Function">cbn↔reduce</a> <a id="22433" class="Symbol">:</a> <a id="22435" class="Symbol">∀</a> <a id="22437" class="Symbol">{</a><a id="22438" href="plfa.part3.Adequacy.html#22438" class="Bound">M</a> <a id="22440" class="Symbol">:</a> <a id="22442" href="/19.08/Untyped/#3175" class="InductiveConstructor">∅</a> <a id="22444" href="plfa.part2.Untyped.html#4294" class="Datatype Operator">⊢</a> <a id="22446" href="plfa.part2.Untyped.html#2888" class="InductiveConstructor">★</a><a id="22447" class="Symbol">}</a>
<a id="22460" class="Symbol">→</a> <a id="22462" class="Symbol">(</a><a id="22463" href="https://agda.github.io/agda-stdlib/v1.1/Data.Product.html#911" class="Function">Σ[</a> <a id="22466" href="/19.08/Adequacy/#22466" class="Bound">N</a> <a id="22468" href="https://agda.github.io/agda-stdlib/v1.1/Data.Product.html#911" class="Function">∈</a> <a id="22470" href="/19.08/Untyped/#3175" class="InductiveConstructor">∅</a> <a id="22472" href="plfa.part2.Untyped.html#3191" class="InductiveConstructor Operator">,</a> <a id="22474" href="plfa.part2.Untyped.html#2888" class="InductiveConstructor">★</a> <a id="22476" href="plfa.part2.Untyped.html#4294" class="Datatype Operator">⊢</a> <a id="22478" href="plfa.part2.Untyped.html#2888" class="InductiveConstructor">★</a> <a id="22480" href="https://agda.github.io/agda-stdlib/v1.1/Data.Product.html#911" class="Function">]</a> <a id="22482" class="Symbol">(</a><a id="22483" href="plfa.part3.Adequacy.html#22438" class="Bound">M</a> <a id="22485" href="plfa.part2.Untyped.html#11267" class="Datatype Operator">—↠</a> <a id="22488" href="plfa.part2.Untyped.html#4382" class="InductiveConstructor Operator">ƛ</a> <a id="22490" href="plfa.part3.Adequacy.html#22466" class="Bound">N</a><a id="22491" class="Symbol">))</a>
<a id="22507" href="/19.08/Denotational/#17037" class="Function Operator">iff</a>
<a id="22524" class="Symbol">(</a><a id="22525" href="https://agda.github.io/agda-stdlib/v1.1/Data.Product.html#911" class="Function">Σ[</a> <a id="22528" href="/19.08/Adequacy/#22528" class="Bound">Δ</a> <a id="22530" href="https://agda.github.io/agda-stdlib/v1.1/Data.Product.html#911" class="Function">∈</a> <a id="22532" href="/19.08/Untyped/#3153" class="Datatype">Context</a> <a id="22540" href="https://agda.github.io/agda-stdlib/v1.1/Data.Product.html#911" class="Function">]</a> <a id="22542" href="https://agda.github.io/agda-stdlib/v1.1/Data.Product.html#911" class="Function">Σ[</a> <a id="22545" href="plfa.part3.Adequacy.html#22545" class="Bound">N′</a> <a id="22548" href="https://agda.github.io/agda-stdlib/v1.1/Data.Product.html#911" class="Function">∈</a> <a id="22550" href="plfa.part3.Adequacy.html#22528" class="Bound">Δ</a> <a id="22552" href="plfa.part2.Untyped.html#3191" class="InductiveConstructor Operator">,</a> <a id="22554" href="plfa.part2.Untyped.html#2888" class="InductiveConstructor">★</a> <a id="22556" href="plfa.part2.Untyped.html#4294" class="Datatype Operator">⊢</a> <a id="22558" href="plfa.part2.Untyped.html#2888" class="InductiveConstructor">★</a> <a id="22560" href="https://agda.github.io/agda-stdlib/v1.1/Data.Product.html#911" class="Function">]</a> <a id="22562" href="https://agda.github.io/agda-stdlib/v1.1/Data.Product.html#911" class="Function">Σ[</a> <a id="22565" href="plfa.part3.Adequacy.html#22565" class="Bound">δ</a> <a id="22567" href="https://agda.github.io/agda-stdlib/v1.1/Data.Product.html#911" class="Function">∈</a> <a id="22569" href="/19.08/BigStep/#2440" class="Function">ClosEnv</a> <a id="22577" href="plfa.part3.Adequacy.html#22528" class="Bound">Δ</a> <a id="22579" href="https://agda.github.io/agda-stdlib/v1.1/Data.Product.html#911" class="Function">]</a>
<a id="22596" href="/19.08/BigStep/#2653" class="Function">∅&#39;</a> <a id="22599" href="plfa.part2.BigStep.html#3024" class="Datatype Operator">⊢</a> <a id="22601" href="/19.08/Adequacy/#22438" class="Bound">M</a> <a id="22603" href="plfa.part2.BigStep.html#3024" class="Datatype Operator">⇓</a> <a id="22605" href="plfa.part2.BigStep.html#2489" class="InductiveConstructor">clos</a> <a id="22610" class="Symbol">(</a><a id="22611" href="/19.08/Untyped/#4382" class="InductiveConstructor Operator">ƛ</a> <a id="22613" href="plfa.part3.Adequacy.html#22545" class="Bound">N′</a><a id="22615" class="Symbol">)</a> <a id="22617" href="plfa.part3.Adequacy.html#22565" class="Bound">δ</a><a id="22618" class="Symbol">)</a>
<a id="22620" href="/19.08/Adequacy/#22422" class="Function">cbn↔reduce</a> <a id="22631" class="Symbol">{</a><a id="22632" href="plfa.part3.Adequacy.html#22632" class="Bound">M</a><a id="22633" class="Symbol">}</a> <a id="22635" class="Symbol">=</a> <a id="22637" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟨</a> <a id="22639" class="Symbol">(λ</a> <a id="22642" href="plfa.part3.Adequacy.html#22642" class="Bound">x</a> <a id="22644" class="Symbol">→</a> <a id="22646" href="plfa.part3.Adequacy.html#21870" class="Function">reduce→cbn</a> <a id="22657" class="Symbol">(</a><a id="22658" href="Agda.Builtin.Sigma.html#237" class="Field">proj₂</a> <a id="22664" href="plfa.part3.Adequacy.html#22642" class="Bound">x</a><a id="22665" class="Symbol">))</a> <a id="22668" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">,</a>
<a id="22689" class="Symbol">(λ</a> <a id="22692" href="/19.08/Adequacy/#22692" class="Bound">x</a> <a id="22694" class="Symbol">→</a> <a id="22696" href="/19.08/BigStep/#12205" class="Function">cbn→reduce</a> <a id="22707" class="Symbol">(</a><a id="22708" href="Agda.Builtin.Sigma.html#237" class="Field">proj₂</a> <a id="22714" class="Symbol">(</a><a id="22715" href="Agda.Builtin.Sigma.html#237" class="Field">proj₂</a> <a id="22721" class="Symbol">(</a><a id="22722" href="Agda.Builtin.Sigma.html#237" class="Field">proj₂</a> <a id="22728" href="plfa.part3.Adequacy.html#22692" class="Bound">x</a><a id="22729" class="Symbol">))))</a> <a id="22734" href="Agda.Builtin.Sigma.html#209" class="InductiveConstructor Operator">⟩</a>
</pre>
<h2 id="unicode">Unicode</h2>
<p>This chapter uses the following unicode:</p>
<div class="language-plaintext highlighter-rouge"><div class="highlight"><pre class="highlight"><code>𝔼 U+1D53C MATHEMATICAL DOUBLE-STRUCK CAPITAL E (\bE)
𝔾 U+1D53E MATHEMATICAL DOUBLE-STRUCK CAPITAL G (\bG)
𝕍 U+1D53E MATHEMATICAL DOUBLE-STRUCK CAPITAL V (\bV)
</code></pre></div></div>
</div>
<p style="text-align:center;">
<a alt="Previous chapter" href="/19.08/Soundness/">Prev</a>
&bullet;
<a alt="Source code" href="https://github.com/plfa/plfa.github.io/blob/dev-19.08/src/plfa/part3/Adequacy.lagda.md">Source</a>
&bullet;
<a alt="Next chapter" href="/19.08/ContextualEquivalence/">Next</a>
</p>
</article>
</div>
</main><footer class="site-footer h-card">
<data class="u-url" href="/19.08/"></data>
<div class="wrapper">
<h2 class="footer-heading">Programming Language Foundations in Agda
</h2><div class="footer-col-wrapper">
<div class="footer-col footer-col-1">
<ul class="contact-list">
<li class="p-name">Philip Wadler</li>
<li><a class="u-email" href="mailto:wadler@inf.ed.ac.uk">wadler@inf.ed.ac.uk</a></li>
</ul>
</div>
<div class="footer-col footer-col-2"><ul class="social-media-list"><li><a href="https://github.com/wadler"><svg class="svg-icon"><use xlink:href="/19.08/assets/minima-social-icons.svg#github"></use></svg> <span class="username">wadler</span></a></li></ul>
</div>
<div class="footer-col footer-col-3"></div>
</div><div class="footer-col-wrapper">
<div class="footer-col footer-col-1">
<ul class="contact-list">
<li class="p-name">Wen Kokke</li>
<li><a class="u-email" href="mailto:wen.kokke@ed.ac.uk">wen.kokke@ed.ac.uk</a></li>
</ul>
</div>
<div class="footer-col footer-col-2"><ul class="social-media-list"><li><a href="https://github.com/wenkokke"><svg class="svg-icon"><use xlink:href="/19.08/assets/minima-social-icons.svg#github"></use></svg> <span class="username">wenkokke</span></a></li><li><a href="https://www.twitter.com/wenkokke"><svg class="svg-icon"><use xlink:href="/19.08/assets/minima-social-icons.svg#twitter"></use></svg> <span class="username">wenkokke</span></a></li></ul>
</div>
<div class="footer-col footer-col-3"></div>
</div><div class="footer-col-wrapper">
<div class="footer-col footer-col-1">
<ul class="contact-list">
<li class="p-name">Jeremy Siek</li>
<li><a class="u-email" href="mailto:jsiek@indiana.edu">jsiek@indiana.edu</a></li>
</ul>
</div>
<div class="footer-col footer-col-2"><ul class="social-media-list"><li><a href="https://github.com/jsiek"><svg class="svg-icon"><use xlink:href="/19.08/assets/minima-social-icons.svg#github"></use></svg> <span class="username">jsiek</span></a></li><li><a href="https://www.twitter.com/jeremysiek"><svg class="svg-icon"><use xlink:href="/19.08/assets/minima-social-icons.svg#twitter"></use></svg> <span class="username">jeremysiek</span></a></li></ul>
</div>
<div class="footer-col footer-col-3"></div>
</div>This work is licensed under a <a rel="license" href="https://creativecommons.org/licenses/by/4.0/">Creative Commons Attribution 4.0 International License</a>
</div>
</footer>
<!-- Import jQuery -->
<script type="text/javascript" src="/19.08/assets/jquery.js"></script>
<script type="text/javascript">
// Makes sandwhich menu works
$('.menu-icon').click(function(){
$('.trigger').toggle();
});
// Script which allows for foldable code blocks
$('div.foldable pre').each(function(){
var autoHeight = $(this).height();
var lineHeight = parseFloat($(this).css('line-height'));
var plus = $("<div></div>");
var horLine = $("<div></div>");
var verLine = $("<div></div>");
$(this).prepend(plus);
plus.css({
'position' : 'relative',
'float' : 'right',
'right' : '-' + (0.5 * lineHeight - 1.5) + 'px',
'width' : lineHeight,
'height' : lineHeight});
verLine.css({
'position' : 'relative',
'height' : lineHeight,
'width' : '3px',
'background-color' : '#C1E0FF'});
horLine.css({
'position' : 'relative',
'top' : '-' + (0.5 * lineHeight + 1.5) + 'px',
'left' : '-' + (0.5 * lineHeight - 1.5) + 'px',
'height' : '3px',
'width' : lineHeight,
'background-color' : '#C1E0FF'});
plus.append(verLine);
plus.append(horLine);
$(this).height(2.0 * lineHeight);
$(this).css('overflow','hidden');
$(this).click(function(){
if ($(this).height() == autoHeight) {
$(this).height(2.0 * lineHeight);
plus.show();
}
else {
$(this).height('auto');
plus.hide();
}
});
});
</script>
<!-- Import KaTeX -->
<script type="text/javascript" src="/19.08/assets/katex.js"></script>
<!-- Script which renders TeX using KaTeX -->
<script type="text/javascript">
$("script[type='math/tex']").replaceWith(
function(){
var tex = $(this).text();
return "<span class=\"inline-equation\">" +
katex.renderToString(tex) +
"</span>";
});
$("script[type='math/tex; mode=display']").replaceWith(
function(){
var tex = $(this).text().replace(/%.*?(\n|$)/g,"");
return "<div class=\"equation\">" +
katex.renderToString("\\displaystyle "+tex) +
"</div>";
});
</script>
</body>
</html>
Reference in a new issue View git blame Copy permalink