Wiki update: rearrange proving metatheorems (#42)

wiki/pages/output-factoring.elf

@@ -4,8 +4,11 @@
 %{! When checking coverage of [metatheorem](/wiki/metatheorem/)s, a common problem arises because the [output coverage](/wiki/coverage-checking/) checker only considers each rule in isolation. The proof transformation technique for addressing this problem is known as **output factoring**.
 
 The primary symptom of the problem is if Twelf fails when checking an %total declaration and gives this sort of error:
-<code>Totality: Output of subgoal not covered
-Output coverage error ...</code>
+
+```
+Totality: Output of subgoal not covered
+Output coverage error ...
+```
 
 ## Even and odd
 

wiki/pages/proving-metatheorems-proving-metatheorems-about-the-stlc.elf

@@ -1,12 +1,11 @@
 %%! title: "Proving metatheorems about the simply-typed lambda calculus"
 %%! description: "We can see that proving type preservation for the simply-typed lambda calculus is not fundamentally different from proving theorems about the natural numbers (Part of the introduction to proving metatheorems in Twelf)"
 %%! prev:
-%%!   label: "Representing the judgements of th STLC"
+%%!   label: "Representing the judgements of the STLC"
 %%!   link: /wiki/proving-metatheorems-representing-the-judgements-of-the-stlc/
 %%! next:
-%%!   label: "Proving totality assertions in non-empty contexts"
-%%!   link: /wiki/proving-metatheorems-proving-totality-assertions-in-non-empty-contexts/
-
+%%!   label: "The STLC: summary and exercises"
+%%!   link: /wiki/proving-metatheorems-summary-the-stlc/
 
 %{! 
 

wiki/pages/proving-metatheorems-proving-metatheorems-in-non-empty-contexts.elf

@@ -1,10 +1,13 @@
 %%! title: "Proving metatheorems:Proving metatheorems in non-empty contexts"
+%%! prev:
+%%!    label: "Proving totality assertions in non-empty contexts"
+%%!    link: /wiki/proving-metatheorems-proving-totality-assertions-in-non-empty-contexts/
 
-%{! \{\{proving metatheorems
-  | next = Summary: the STLC
-  | nextname = Summary
-  | prev = Proving metatheorems about the STLC
-  | prevname = Proving metatheorems\}\}
+%{! 
+
+_This page is part of the introduction to [proving metatheorems with Twelf](/wiki/proving-metatheorems-with-twelf/)._
+
+(This part of the tutorial isn't cleaned up from the transition from MediaWiki, the archived page may have better formatting)
 
 By using Twelf's ability to prove totality assertions for type families in general worlds, we can mechanize metatheorems about open LF terms.  We prove a simple metatheorem about the judgement ``size E N`` as an example. !}%
 

wiki/pages/proving-metatheorems-proving-totality-assertions-in-non-empty-contexts.elf

@@ -1,19 +1,21 @@
-%%! title: "Proving metatheorems:Proving totality assertions in non-empty contexts"
+%%! title: "Proving totality assertions in non-empty contexts"
+%%! prev:
+%%!   label: "The STLC: summary and exercises"
+%%!   link: /wiki/proving-metatheorems-summary-the-stlc/
+%%! next:
+%%!   label: Proving metatheorems in non-empty contexts
+%%!   link: /wiki/proving-metatheorems-proving-metatheorems-in-non-empty-contexts/
 
-%{! \{\{proving metatheorems
-  | next = Proving metatheorems in non-empty contexts
-  | nextname = Proving metatheorems in non-empty contexts
-  | prev = Proving metatheorems about the STLC
-  | prevname = Proving metatheorems\}\}
+%{! 
+
+_This page is part of the introduction to [proving metatheorems with Twelf](/wiki/proving-metatheorems-with-twelf/)._
 
 So far, we have only proved relations total in the empty LF context.  In this section, we discuss proving totality assertions for relations in more general contexts.  As a motivating example, we define a judgement that computes the size of a STLC term.  
 
 ## Definition of Size
 
-The definition of size uses the definitions of [natural numbers](/wiki/proving-metatheorems-representing-the-syntax-of-the-natural-numbers/), [addition judgement](/wiki/proving-metatheorems-representing-the-judgements-of-the-natural-numbers/), and [STLC term syntax](/wiki/proving-metatheorems-representing-the-syntax-of-the-stlc/) from earlier in this article. !}%
+The definition of size uses the definitions of [natural numbers](/wiki/proving-metatheorems-representing-the-syntax-of-the-natural-numbers/), [addition judgement](/wiki/proving-metatheorems-representing-the-judgements-of-the-natural-numbers/), and [STLC term syntax](/wiki/proving-metatheorems-representing-the-syntax-of-the-stlc/) from earlier in this introduction: !}%
 
-%{! (options removed from twelftag: export="syntax" hidden="true") !}%
-
 tp    : type.
 unit  : tp.
 arrow : tp -> tp -> tp.
@@ -38,14 +40,14 @@ plus-s : plus (s N1) N2 (s N3)
 %total N (plus N _ _).
 
 %{! Informally, we define the size of a term as follows:
-* <math>\mathsf\{\}|x| = 1</math>
-* <math>|\langle\rangle| = 1</math>
-* <math>|e_1 \; e_2| = 1 + |e_1| + |e_2|</math>
-* <math>\mathsf\{\}|\lambda x:\tau.e| = 1 + |e|</math>
+* <Math formula="|x| = 1"/>
+* <Math formula="|\langle\rangle| = 1"/>
+* <Math formula="|e_1 \, e_2| = 1 + |e_1| + |e_2"/>
+* <Math formula="|\lambda x{:}\tau.e| = 1 + |e|"/>
 
 We define this function in LF using the following judgement: !}%
 
-%{! (options removed from twelftag: check="true" import="syntax" export="preworld") !}%
+%{!! begin checked !!}%
 
 size       : tm -> nat -> type.
 %mode size +E -N.
@@ -60,6 +62,9 @@ size-app   : size (app E1 E2) (s N)
 		<- size E2 N2 
 		<- plus N1 N2 N.
 
+%{!! end checked !!}%
+
+
 %{! The only subtlety in this judgement is that we have recast size as a hypothetical judgement: each variable ``x:tm`` in the context is assumed to have size 1.  Correspondingly, the premise of the ``lam`` case extends the context with such an assumption for the bound variable.  
 
 ## World Declarations
@@ -73,8 +78,6 @@ We would like to assert that every term has a size.  However, because the defini
 The worlds declaration fails because ``size`` does not stay in the empty context.
 
 To give an appropriate worlds declaration for this type family, we must first specify the form of the contexts in which we consider it.  We do so with a block declaration: !}%
-
-%{! (options removed from twelftag: import="preworld" export="withworld") !}%
 
 %block size-block : block {x : tm} {_ : size x (s z)}.
 %worlds (size-block) (size _ _).
@@ -110,9 +113,9 @@ Formalizing this reasoning requires knowing when terms of one type can appear in
 
 Using subordination, we define world subsumption as follows:
 
-: **World subsumption:** A world ``W'`` subsumes a world ``W`` for a type family ``a`` iff for all contexts Γ' in ``W'``, there exists a context Γ in ``W`` such that Γ and Γ' are equal when restricted to only the declarations at types subordinate to ``a``.
+> **World subsumption:** A world ``W'`` subsumes a world ``W`` for a type family ``a`` iff for all contexts Γ' in ``W'``, there exists a context Γ in ``W`` such that Γ and Γ' are equal when restricted to only the declarations at types subordinate to ``a``.
 
-For example, ``(size-block)*`` subsumes the world containing only the empty context for ``plus``.  On the other hand, the world ``(\{x:nat\})*`` does not subsume the world containing only the empty context for ``plus``, because adding variables representing more natural numbers is relevant to ``plus``.
+For example, ``(size-block)*`` subsumes the world containing only the empty context for ``plus``.  On the other hand, the world ``({x:nat})*`` does not subsume the world containing only the empty context for ``plus``, because adding variables representing more natural numbers is relevant to ``plus``.
 
 Using world subsumption, we refine our notion of world checking as follows. A constant world checks iff
 - The world of a type family subsumes the world of each of its premises.
@@ -125,7 +128,7 @@ Under this more permissive definition, the ``plus`` premise of ``size`` is deeme
 
 We now return to the role a world declaration has in specifying totality assertions.  The above mode and world declarations for ``size`` declare the following totality assertion:
 
-: For all LF contexts Γ in ``(size-block)*``, if ``Γ \{\{vdash\}\} E : tm`` then there exist ``N`` such that ``Γ \{\{vdash\}\} N : nat`` and ``D`` such that ``Γ \{\{vdash\}\} D : size E N``.
+> For all LF contexts Γ in ``(size-block)*``, if ``Γ ⊢ E : tm`` then there exist ``N`` such that ``Γ ⊢ N : nat`` and ``D`` such that ``Γ ⊢ D : size E N``.
 
 There are two things to note about this totality assertion:
 - It generalizes those that we have seen before, where the world always contained only the empty context and consequently the assertion was about closed terms.
@@ -135,9 +138,9 @@ Twelf verifies totality assertions in non-empty contexts in the same manner as b
 
 In this case, Twelf succeeds in proving the totality of ``size``. !}%
 
-%{! (options removed from twelftag: check="true" import="withworld" export="withtotal") !}%
-
+%{!! begin checked !!}%
 %total E (size E _).
+%{!! end checked !!}%
 
 %{! ## Example world errors
 
@@ -208,8 +211,4 @@ size-app   : size (app E1 E2) (s N)
 This definition world checks because the context in ``size-lam`` is of the form specified by the world declaration.  However, the type family ``size`` does not define a total relation because it does not cover 
 variables ``x:tm`` in the LF context.  A total relation must cover both the LF constants in the signature and the LF variables in all contexts in the world.
 
------
-This page was copied from the MediaWiki version of the Twelf Wiki.
-If anything looks wrong, you can refer to the
-[wayback machine's version here](https://web.archive.org/web/20240303030303/http://twelf.org/wiki/Proving_metatheorems:Proving_totality_assertions_in_non-empty_contexts).
 !}%

wiki/pages/proving-metatheorems-stlc-answers-to-exercises.elf

@@ -1,14 +1,5 @@
 %%! title: "Proving metatheorems:STLC: Answers to exercises"
 
-%{! This page contains answers to the exercises listed [here](/wiki/proving-metatheorems-summary-the-stlc/). If you've solved an exercise that isn't answered on this page, or if you have a different solution to an exercise, please add it here.
-
-## STLC with products
-
-_Add product types (<math>\tau_1 \times \tau_2</math>) to the STLC and extend the proof of preservation to cover this new type._ !}%
-
-%{!
------
-This page was copied from the MediaWiki version of the Twelf Wiki.
-If anything looks wrong, you can refer to the
-[wayback machine's version here](https://web.archive.org/web/20240303030303/http://twelf.org/wiki/Proving_metatheorems:STLC:_Answers_to_exercises).
+%{! 
+This page has been removed, you can refer to the wayback machine's version by following the link below.
 !}%

wiki/pages/proving-metatheorems-summary-the-stlc.elf

@@ -1,9 +1,15 @@
-%%! title: "Proving metatheorems:Summary: the STLC"
+%%! title: "Summary and exercises: the simply-typed lambda calculus"
+%%! description: "In the conclusion of Part 2 of the introduction to proving metatheorems in Twelf, we summarize takeaways and present some exercises to extend the simply typed lambda calculus (Part of the introduction to proving metatheorems in Twelf)"
+%%! prev:
+%%!    label: "Proving metatheorems about the STLC"
+%%!    link: "/wiki/proving-metatheorems-proving-metatheorems-about-the-stlc/"
+%%! next:
+%%!    label: "Proving totality assertions in non-empty contexts"
+%%!    link: "/wiki/proving-metatheorems-proving-totality-assertions-in-non-empty-contexts/"
 
-%{! \{\{proving metatheorems
-  | nonext = 
-  | prev = Proving metatheorems in non-empty contexts
-  | prevname = Proving metatheorems in non-empty contexts\}\}
+%{!
+
+_This page is part of the introduction to [proving metatheorems with Twelf](/wiki/proving-metatheorems-with-twelf/)._
 
 ## Take-aways
 
@@ -19,22 +25,96 @@ Now that you've made it through this introduction, you have the basic tools you
 
 ## Test yourself
 
-_This section is under development; if you try other examples at this point, please add them here._
+Here are a few suggestions for additional explorations:
 
-Before going on to the next section, you may wish to test yourself with the following exercises.  Then see the [answers](/wiki/proving-metatheorems-stlc-answers-to-exercises/).
+### Adding features to the simply-typed lambda calculus
 
-- Add product types (<math>\tau_1 \times \tau_2</math>) to the STLC and extend the proof of preservation to cover this new type.
-- _Add your exercises here!_
+A standard extension of the simply-typed lambda calculus is _pairs_:
 
+```math
+{
+  \Gamma \vdash e_1 : \tau_1
+  \qquad
+  \Gamma \vdash e_2 : \tau_2
+  \over
+  \Gamma \vdash \langle e_1, e_2 \rangle : \tau_1 \times \tau_2
+}\mathit{of\textit{-}pair}
+```
+```math
+{
+  \Gamma \vdash e : \tau_1 \times \tau_2
+  \over
+  \Gamma \vdash \pi_1\,e : \tau_1
+}\mathit{of\textit{-}proj_1}
+\qquad
+{
+  \Gamma \vdash e : \tau_1 \times \tau_2
+  \over
+  \Gamma \vdash \pi_2\,e : \tau_1
+}\mathit{of\textit{-}proj_2}
+```
 
-\{\{proving metatheorems
-  | nonext = 
-  | prev = Proving metatheorems in non-empty contexts
-  | prevname = Proving metatheorems in non-empty contexts\}\} !}%
+The dynamic semantics of pairs have a number of rules, but they are all relatively straightforward:
+
+```math
+{
+  e_1 \, \mathtt{value}
+  \qquad
+  e_2 \, \mathtt{value}
+  \over
+  \langle e_1, e_2 \rangle \, \mathtt{value}
+}\mathit{value\textit{-}pair}
+```
+```math
+{
+  e_1 \mapsto e_1'
+  \over
+  \langle e_1 , e_2 \rangle \mapsto \langle e_1', e_2 \rangle
+}\mathit{step\textit{-}pair_1}
+\qquad
+{
+  e_1 \, \mathtt{value}
+  \qquad
+  e_2 \mapsto e_2'
+  \over
+  \langle e_1 , e_2 \rangle \mapsto \langle e_1, e_2' \rangle
+}\mathit{step\textit{-}pair_2}
+```
+```math
+{
+  e \mapsto e'
+  \over
+  \pi_1 \, e \mapsto \pi_1 \, e'
+}\mathit{step\textit{-}proj_1}
+\qquad
+{
+  e \mapsto e'
+  \over
+  \pi_2\,  e \mapsto \pi_2 \, e'
+}\mathit{step\textit{-}proj_2}
+```
+```math
+{
+  e_1 \, \mathtt{value}
+  \qquad
+  e_2 \, \mathtt{value}
+  \over
+  \pi_1 \, \langle e_1 , e_2 \rangle \mapsto e_1
+}\mathit{step\textit{-}proj\textit{-}beta_1}
+\qquad
+{
+  e_1 \, \mathtt{value}
+  \qquad
+  e_2 \, \mathtt{value}
+  \over
+  \pi_2 \, \langle e_1 , e_2 \rangle \mapsto e_2
+}\mathit{step\textit{-}proj\textit{-}beta_2}
+```
+
+Add these to your formalization of the simply-typed lambda calculus and extend the proof of preservation to cover this new type.
+
+## Next steps
+
+You now have everything you need to start proving metatheorems with Twelf! The [proof techniques covered in the tutorials](/wiki/tutorials/) are likely to be valuable as you continue. If you're interested in proving progress for the simply typed lambda calculus formulation, you'll do well to start by learning about [output factoring](/wiki/output-factoring/).
 
-%{!
------
-This page was copied from the MediaWiki version of the Twelf Wiki.
-If anything looks wrong, you can refer to the
-[wayback machine's version here](https://web.archive.org/web/20240303030303/http://twelf.org/wiki/Proving_metatheorems:Summary:_the_STLC).
 !}%

wiki/pages/proving-metatheorems-with-twelf.elf

@@ -22,6 +22,8 @@ This introduction assumes this story is somewhat familiar to you. If not, you sh
  - Her paper includes a Twelf appendix, which makes her and her readers much more confident that the theorems in the paper are actually true.  
  - When someone goes to extend the language, he has a formal, machine-checkable artifact that he can study or perhaps even reuse directly.
 
+This tutorial pays a lot of attention to the question "how do I know that what I wrote down and proved on paper, and what I wrote down and proved in Twelf, are exactly the same thing?" Checking that these two things are the same is called [adequacy](/wiki/adequacy/), and it's an important problem _whenever_ you're using a theorem proving like Twelf, Agda, or Rocq. But it definitely has the flavor of "checking lots of fiddly details," and so it's reasonable to skip discussions of adequacy in this tutorial if you're exploring Twelf for the first time. 
+
 ### First order representations: The natural numbers
 
 The first layer of this introduction uses a _very_ simple deductive system, the [natural numbers](/wiki/natural-numbers/) with addition, to introduce the Twelf methodology.
@@ -41,12 +43,13 @@ The second layer tells the same story for a programming language with variable b
  8. [Representing syntax](/wiki/proving-metatheorems-representing-the-syntax-of-the-stlc/)
  9. [Representing judgements](/wiki/proving-metatheorems-representing-the-judgements-of-the-stlc/)
  10. [Proving metatheorems](/wiki/proving-metatheorems-proving-metatheorems-about-the-stlc/)
+ 11. [Summary and exercises](/wiki/proving-metatheorems-summary-the-stlc/)
 
 ### Beyond the simply-typed lambda calculus
 
 The third layer presents some more-interesting proofs and introduces one additional feature of Twelf, the ability to do proofs about open terms. 
 
- 11. [Proving totality assertions in non-empty contexts](/wiki/proving-metatheorems-proving-totality-assertions-in-non-empty-contexts/)
- 12. [Proving metatheorems in non-empty contexts](/wiki/proving-metatheorems-proving-metatheorems-in-non-empty-contexts/)
- 13. [Summary](/wiki/proving-metatheorems-summary-the-stlc/) ([Answers to exercises](/wiki/proving-metatheorems-stlc-answers-to-exercises/)) 
+ 12. [Proving totality assertions in non-empty contexts](/wiki/proving-metatheorems-proving-totality-assertions-in-non-empty-contexts/)
+ 13. [Proving metatheorems in non-empty contexts](/wiki/proving-metatheorems-proving-metatheorems-in-non-empty-contexts/)
+
 !}%

wiki/pages/simply-typed-lambda-calculus.elf

@@ -75,8 +75,6 @@ The typing rules for the simply typed lambda calculus use a typing context <Math
 }\mathit{of\textit{-}app}
 ```
 
-
-
 This judgement is represented by the following LF signature: !}%
 
 of : tm -> tp -> type.