# Strengthening

### From The Twelf Project

**Strengthening** lemmas prove that something which holds under assumptions also holds without them.

When proving type families total using %total, strengthening lemmas are sometimes necessary because Twelf estimates dependencies conservatively using the subordination relation. Specifically, for Twelf's output coverage check to succeed, the output variables of higher-order premises must mention all assumptions of subordinate types. If an assumption's type is subordinate to an output variable's type, but additional reasoning shows that the assumption cannot occur in the output variable in a particular case, you must prove a strengthening lemma expressing this reasoning.

In this tutorial, we'll show a proof where the need for strengthening arises. We'll define a language with locations, stores which map locations to terms in the language, and a notion of well-formedness with respect to a store (no dangling references and no loops). Then we'll define evaluation for the language, and prove that well-formed terms evaluate to well-formed terms; we will need strengthening for this proof.

## [edit] A little language with locations

Locations and terms:

ERROR: option 'name' deprecated or invalidloc : type. %name loc _L. loc/z : loc. loc/s : loc -> loc. tm : type. %name tm _T. tm/loc : loc -> tm. tm/lam : (tm -> tm) -> tm. tm/app : tm -> tm -> tm.

This is a silly little language; it has locations but no way to use them.

(The `%name` declarations give a prefix which Twelf uses to name unnamed variables for display; we prefix the names with `_` so that it's clear which variables Twelf named, and also because Twelf will rename your variables if they collide with the naming prefix, which can be very confusing.)

Stores and store lookup:

ERROR: option 'include' deprecated or invalidst : type. %name st _S. st/nil : st. st/cons : loc -> tm -> st -> st. st-lookup : st -> loc -> tm -> type. %name st-lookup _Dlook. st-lookup/1 : st-lookup (st/cons L T _) L T. st-lookup/2 : st-lookup (st/cons L T S) L' T' <- st-lookup S L' T'.

Stores are just lists of location/term pairs. The lookup relation might look a little strange, since both `st-lookup/1` and `st-lookup/2` apply if `L = L'`, but for our purpose it is OK and this avoids having to define disequality of locations.

Well-formedness of terms with respect to a store:

ERROR: option 'include' deprecated or invalidtm-wf : tm -> st -> type. %name tm-wf _Dwf. tm-var : tm -> type. tm-wf/var : tm-wf V S <- tm-var V. tm-wf/loc : tm-wf (tm/loc L) S <- st-lookup S L T <- tm-wf T S. tm-wf/lam : tm-wf (tm/lam ([x:tm] T x)) S <- ({v:tm}{d:tm-var v} tm-wf (T v) S). tm-wf/app : tm-wf (tm/app T1 T2) S <- tm-wf T1 S <- tm-wf T2 S.

A term is well-formed with respect to a store if its locations are all defined in the store, and if the terms bound to its locations are all well-formed with respect to the store.

How to define well-formedness of the open term that appears in the `lam` case? We assume some term, and mark it is a variable using `tm-var`, then check the well-formedness of the lambda body applied to this new term. Then we give a case saying that any term marked as a variable is well-formed.

An alternative would be to directly assume `tm-wf v S`. This example was extracted from the AML proof, where we need to prove that if we have a store `S'` which extends `S`, and a term `T` is well-formed in `S`, then `T` is also well-formed in `S'`. That proof is difficult if we assume `tm-wf v S`, because we know nothing about `v` in `S'`. With the `tm-var` approach we can just apply the `tm-wf/var` rule to get `tm-wf v S'`.

However, as we will see, this approach forces us to prove a substitution lemma, which requires the strengthening lemma.

### [edit] Evaluation and preservation

Now, some evaluation semantics, and the preservation theorem:

ERROR: option 'name' deprecated or invalidERROR: option 'include' deprecated or invalideval : tm -> tm -> type. %name eval _Deval. eval/loc : eval (tm/loc L) (tm/loc L). eval/lam : eval (tm/lam ([x:tm] T x)) (tm/lam ([x:tm] T x)). eval/app : eval (tm/app T1 T2) T' <- eval T1 (tm/lam ([x:tm] T1' x)) <- eval (T1' T2) T'. eval-pres-wf : eval T T' -> tm-wf T S -> tm-wf T' S -> type. %mode eval-pres-wf +X1 +X2 -X3. -/loc : eval-pres-wf eval/loc D D. -/lam : eval-pres-wf eval/lam D D. -/app : eval-pres-wf (eval/app Deval2 Deval1) (tm-wf/app Dwf2 Dwf1) Dwf'' <- eval-pres-wf Deval1 Dwf1 (tm-wf/lam Dwf1') <- tm-wf-subst Dwf1' Dwf2 Dwf' <- eval-pres-wf Deval2 Dwf' Dwf''. %worlds () (eval-pres-wf _ _ _). %total D (eval-pres-wf D _ _).See Twelf's output

Evaluation is just beta-reduction; we do nothing with locations.

The preservation theorem is straightforward, but we need to appeal to a substitution lemma. Let's see why: we have `Dwf1' : {v:tm}{d:tm-var v} tm-wf (T1 v) S` and `Dwf2 : tm-wf T2 S`; we need `Dwf' : tm-wf (T1 T2) S`. Now, had we defined `tm-wf/lam` to assume `d:tm-wf v S` instead of `d:tm-var v`, then we could just write `(Dwf1' T2 Dwf2)` in place of `Dwf'`. But, as previously noted, that gets us into a different kind of trouble. So we prove an explicit substitution lemma:

%block tm-bind : block {v:tm}{d:tm-var v}.ERROR: option 'name' deprecated or invalidERROR: option 'include' deprecated or invalid

tm-wf-subst : ({v:tm}{d:tm-var v} tm-wf (T1 v) S) -> tm-wf T2 S -> % tm-wf (T1 T2) S -> type. %mode tm-wf-subst +X1 +X2 -X3. -/app : tm-wf-subst ([v][d] tm-wf/app (Dwf2 v d) (Dwf1 v d)) Dwf (tm-wf/app Dwf2' Dwf1') <- tm-wf-subst Dwf1 Dwf Dwf1' <- tm-wf-subst Dwf2 Dwf Dwf2'. -/lam : tm-wf-subst ([v][d] tm-wf/lam (Dwf1 v d)) Dwf2 (tm-wf/lam Dwf1') <- ({v':tm}{d':tm-var v'} tm-wf-subst ([v][d] Dwf1 v d v' d') Dwf2 (Dwf1' v' d')). -/loc : tm-wf-subst ([v][d] tm-wf/loc (Dwf1 v d) (Dlook v)) Dwf2 (tm-wf/loc Dwf1' Dlook') <- st-lookup-strengthen Dlook Dlook' Deq <- tm-wf-strengthen Dwf1 Deq Dwf1'. -/var : tm-wf-subst ([v][d] tm-wf/var d) Dwf Dwf. -/bind : tm-wf-subst ([v][d] Dwf) _ Dwf. %worlds (tm-bind) (tm-wf-subst _ _ _). %total D (tm-wf-subst D _ _).

This lemma gives us exactly what we needed above.

The `lam` case is complicated only by the fact that we need to go under a binder; here `v` is the variable we're substituting for and `v'` is the bound variable. Since we call the lemma recursively under assumptions, we need to prove it in worlds where those assumptions are present.

In the `var` case we have found the variable we're substituting for. The `bind` case handles assumptions; there is no way to explicitly refer to them, but they are closed, so we can catch them with this case for closed terms.

The `loc` case is why we're here: Twelf determines that `Dlook` can depend on `v` and `Dwf1` on `v` and `d`, even though they can't. So we need two strengthening lemmas to get the terms we need.

Why can't `Dlook` and `Dwf1` depend on `v` and `d`? We are about to give proofs, but here is the intuition: The store `S` has no dependencies in the declaration of the lemma, and `st-lookup` just walks over the store, so `Dlook` has no dependencies; neither does the looked-up term. Now `tm-wf` just walks over the term looking up locations in the store, so it also has no dependencies.

### [edit] Strengthening lemmas

Here is the first:

ERROR: option 'name' deprecated or invalidERROR: option 'include' deprecated or invalidtm-eq : tm -> tm -> type. tm-eq_ : tm-eq T T. st-lookup-strengthen : ({v:tm} st-lookup S L (T v)) -> % st-lookup S L T' -> ({v:tm} tm-eq (T v) T') -> type. %mode st-lookup-strengthen +X1 -X2 -X3. -/1 : st-lookup-strengthen ([v] st-lookup/1) st-lookup/1 ([v] tm-eq_). -/2 : st-lookup-strengthen ([v] st-lookup/2 (Dlook v)) (st-lookup/2 Dlook') Deq <- st-lookup-strengthen Dlook Dlook' Deq. %worlds (tm-bind) (st-lookup-strengthen _ _ _). %total D (st-lookup-strengthen D _ _).

It would be nice if we could just get rid of the `v` assumption on the `st-lookup` derivation, but we have in addition that the returned term `T` can depend on `v`, so we must invent a new non-dependent `T'` and return an equality. Otherwise, this is a straightforward induction that demonstrates that we never use the assumption.

The second strengthening lemma is a little different:

ERROR: option 'name' deprecated or invalidERROR: option 'include' deprecated or invalidtm-wf-strengthen : ({v:tm}{d:tm-var v} tm-wf (T v) S) -> ({v:tm} tm-eq (T v) T') -> % tm-wf T' S -> type. %mode tm-wf-strengthen +X1 +X2 -X3. -/app : tm-wf-strengthen ([v][d] tm-wf/app (Dwf2 v d) (Dwf1 v d)) ([v] tm-eq_) (tm-wf/app Dwf2' Dwf1') <- tm-wf-strengthen Dwf2 ([v] tm-eq_) Dwf2' <- tm-wf-strengthen Dwf1 ([v] tm-eq_) Dwf1'. -/lam : tm-wf-strengthen ([v][d] tm-wf/lam (Dwf v d)) ([v:tm] tm-eq_) (tm-wf/lam Dwf') <- ({v':tm}{d':tm-var v'} tm-wf-strengthen ([v][d] Dwf v d v' d') ([v] tm-eq_) (Dwf' v' d')). -/loc : tm-wf-strengthen ([v][d] tm-wf/loc (Dwf v d) (Dlook v)) ([v] tm-eq_) (tm-wf/loc Dwf' Dlook') <- st-lookup-strengthen Dlook Dlook' Deq <- tm-wf-strengthen Dwf Deq Dwf'. -/bind : tm-wf-strengthen ([v][d] Dwf) _ Dwf. %worlds (tm-bind) (tm-wf-strengthen _ _ _). %total D (tm-wf-strengthen D _ _).

Here it is a priori possible that something of type `tm-wf (T v) S` could depend on `v` and `d` (e.g. it could be `(tm-wf/var d)`), but in conjunction with the equality it cannot. In the `loc` case we're doing essentially the same thing that we do in the substitution lemma, and must appeal to `st-lookup-strengthen` and `tm-wf-strengthen` (but we're not inducting over the well-formed term here). The coverage checker is able to rule out the `var` case since `T` does not depend on `v`.

Read more Twelf tutorials and other Twelf documentation.