E.W.Ayers
Appendix A
Zippers and tactics for boxes

This is a technical appendix on soundly running Lean tactics within a Box. It also provides some of the more technical background omitted from Section 2.4, such as the inference rules for the development calculus of Lean. By the end of this appendix, I will have described an 'escape-hatch' to use Lean tactics within a Box proof, meaning that we don't have to forgo using any prexisting tactic libraries by using the Box framework. The proofs here are perhaps better considered as sketches that could one day be formalised. Ultimately, these meta-level proofs are not critical to the thesis because the resulting object-level proofs produced through these moves will also be checked by the Lean kernel.

A.1. Typing of expressions containing metavariables

In this section I will provide a formal set of judgements describing how the development calculus of Lean works. I will do this by extending the presentation given by Carneiro [Car19[Car19]Carneiro, MarioLean's Type Theory (2019)] to also include typing over expressions containing metavariables. These definitions are used in the proofs soundness properties for Box in Chapter 3 and in later sections of this appendix. This section is intended to be 'complete' in the sense that it should be readable as a standalone document to understand how metavariables work in a theorem prover. I used the knowledge written in this section to implement an interfacehttps://github.com/leanprover-community/lean/pull/69 in the Lean 3 metaprogramming framework [EUR+17[EUR+17]Ebner, Gabriel; Ullrich, Sebastian; et al.A metaprogramming framework for formal verification (2017)Proceedings of the ACM on Programming Languages] for fine-grained control over the metavariable context.

The work in this section is not an original contribution, because de Moura et al (the designers of Lean 3) had to produce this theory to create the software in the first place. There are also many accounts of the theories of development calculi similar to this [SH17[SH17]Sterling, Jonathan; Harper, RobertAlgebraic Foundations of Proof Refinement (2017)arXiv preprint arXiv:1703.05215, McB00[McB00]McBride, ConorDependently typed functional programs and their proofs (2000), Spi11[Spi11]Spiwack, ArnaudVerified computing in homological algebra, a journey exploring the power and limits of dependent type theory (2011)]. The information in this section is gleaned from [EUR+17] and [MAKR15[MAKR15]de Moura, Leonardo; Avigad, Jeremy; et al.Elaboration in Dependent Type Theory (2015)CoRR], the sourcecode of the Lean 3 theorem proverhttps://github.com/leanprover/lean and through many informal chats with the community on the leanprover Zulip serverhttps://leanprover.zulipchat.com.

(A.1) recaps some definitions that were given in Section 2.4.

(A.1).

Recap of the definitions of contexts. A Name is a list of strings and numbers and acts as an identifier. In Lean 3, a distinction is made between free and bound vars, but this is simplified here. Under the hood, MvarContext is implemented as a dictionary keyed on Name instead of as a List. The sort expression represents the type of types or propositions depending on the value of the Level parameter.

Binder := Name × Expr
Context := List Binder
Expr ::=
| app : ExprExprExpr
| lam : BinderExprExpr
| pi : BinderExprExpr
| var : NameExpr
| mvar : NameExpr
| const : NameExpr
| sort : {Level}Expr
MvarDecl :=
(name : Name)
× (type : Expr)
× (ctx : Context)
× (assignment : Option Expr)
MvarContext := List MvarDecl

Let 𝑀 : MvarContext and Γ : Context. Binders are sugared as (𝑥α)Note the use of a smaller colon for typing judgements vs : for meta-level type assignments. for 𝑥, α: Binder, MvarDecls as (Γ?𝑥α) for unassigned 𝑥, α, Γ, none: MvarDecl and (Γ?𝑥α𝑡) for assigned 𝑥, α, Γ, some 𝑡: MvarDecl (Γ may be omitted if not relevant). I will use the convention that metavariable names always begin with question marks. Given 𝑥 : Name, write 𝑥Γ when 𝑥 appears in Γ.

To simplify analysis, I will assume that all contexts do not include variable clashes. That is to say, there are no two binders with the same name in Γ or 𝑀. Since there are infinitely many variable names to choose from, these kinds of variable clashes can be avoided through renaming.

Each of the definitions in (A.1) are assignable (see Section 2.4.2) as defined in (2.25). Also define the following for 𝑟 : R where R is assignable.

  • fv(𝑟) are the free variables in 𝑟.

  • mv(𝑟) are the metavariables in 𝑟.

  • umv(𝑀, 𝑟) are the unassigned metavariables in 𝑟 (according to context 𝑀).

  • amv(𝑀, 𝑟) are the assigned metavariables in 𝑟.

Recall (see Section 2.4.1) that a substitution σ is a dictionary Sub := NameExpr sending variable names to expressionsA good general account of working with substitutions can be found in [BN98].[BN98]Baader, Franz; Nipkow, TobiasTerm rewriting and all that (1998). Given σ : Sub and an 𝑟 : R where R is assignable, σ 𝑟 replaces each variable in 𝑟 with the corresponding expression in σWith the usual caveats for variable clashes as noted in Section 2.4.1. The notation for substitutions that I use is 𝑥𝑡 where 𝑥 : Name is the variable to be substituted and 𝑡 : Expr is the replacement expressionThe reader may enjoy this list of substitution notations collected by Steele [Ste17]. (link to slides)[Ste17]Steele Jr., Guy L.It's Time for a New Old Language (2017). I will extend this definition to include metavariable substitutions.

A metavariable context 𝑀 can be viewed as a substitution mapping ?𝑚 to 𝑡 for each assigned declaration ?𝑚, α, Γ, some 𝑡⟩ ∈ 𝑀. That is, 𝑀 acts by replacing each instance of an assigned metavariable with its assignment. Given an assignable 𝑒, write 𝑀 𝑒 to be the 𝑀-instantiation of 𝑒, created by performing this substitution to 𝑒. 𝑒 is 𝑀-instantiated when all of the metavariables present in 𝑒 are unassigned with respect to 𝑀.

This substitution operation on 𝑀 helps motivate the constraints that make a metavariable context well-formed. In particular, we should expect:

  • There should be no 'substitution loops': 𝑀 𝑡 should not contain any 𝑀-assigned metavariables. For example, the metavariable declaration ?𝑚, α, Γ, some ?𝑚 assigning ?𝑚 to itself would cause a loop. More perniciously, the assignment could cause an infinitely growing term as in ?𝑚?𝑚 + ?𝑚. The no-loop property depends on the entire 𝑀, as we may have a multi-declaration dependency cycle such as ?𝑚f(?𝑛), ?𝑛g(?𝑛).

  • Performing 𝑀 on an expression 𝑡 : Expr (or other assignable object) should preserve the well-formedness of 𝑡 in a context Γ. To illustrate with some examples:

    • Performing ?𝑚"hello" to ?𝑚 + 4 would produce the nonsense expression "hello" + 4, so assignments must have the same type as their metavariables.

    • Performing ?𝑚𝑥 + 2 to ?𝑚 + (λ 𝑥, 𝑥 - ?𝑚) 5 will produce (𝑥 + 2) + (λ 𝑥, 𝑥 - (𝑥 + 2)) 5. But this is badly formed because the variable 𝑥 escapes the scope of its lambda binder. Hence there needs to be a way of making sure that a metavariable assignment can't depend on variables that would cause these malformed expressions. This is why the MvarDecl definition includes a context Γ for each declaration.

These constraints will be made formal in Section A.1.3.

A.1.1. Assignment of a metavariable

Given a metavariable context 𝑀 with an unassigned metavariable ?𝑚 and a candidate expression 𝑡 : Expr, we need a way of updating 𝑀 so that ?𝑚 is assigned to 𝑡. Call this function assign : MvarContextNameExprOption MvarContext.

The procedure of assign 𝑀 ?𝑚 𝑡 is as followsThe implementation in core Lean can be found here.:

  1. Find the corresponding declaration ?𝑚, α, Γ, none⟩ ∈ 𝑀. If it doesn't exist in 𝑀 or it is already assigned, fail by returning none.

  2. Assert that there are no metavariable loops; that is, ?𝑚mv(𝑀 𝑡). (𝑀 𝑡 is the 𝑀-instantiation of 𝑡.)

  3. Assert that typings and contexts are correct with 𝑀;Γ𝑡α (to be defined in Section A.1.3).

  4. Delete ?𝑚 from 𝑀.

  5. Update 𝑀 to be ?𝑚𝑀 𝑡𝑀. That is, each occurrence of ?𝑚 in 𝑀 is replaced with the 𝑀-instantiation of 𝑡. Now ?𝑚mv(𝑀).

  6. Insert ?𝑚, α Γ, some 𝑡 into 𝑀.

Using this procedure ensures that each time a metavariable ?𝑚 is assigned, we have ?𝑚mv(assign 𝑀 ?𝑚 𝑡), which means that checking for loops only requires checking ?𝑚mv(𝑀 𝑡).

A.1.2. Dependency ordering

In this section, I will define what it means for a declaration to depend on another one and define an extension of a metavariable context.

Given an assignable 𝑟, say that 𝑟 depends on ?𝑚 when ?𝑚mv(𝑟). Given a pair of declarations 𝑑₁ =?𝑚₁, α, Γ, 𝑜₁ and 𝑑₂ =?𝑚₂, α, Γ, 𝑜₂ in 𝑀, write 𝑑₁𝑑₂ when 𝑑₂ depends on ?𝑚₁. That is 𝑑₁𝑑₂ when α or Γ or 𝑜₂ depend on ?𝑚₁.

Given the list of declarations 𝑀 : MvarContext as vertices, forms a directed graph. Assuming that this graph is acyclic (which will be enforced by the definition of a valid context given later), there exists a topological orderinghttps://en.wikipedia.org/wiki/Topological_sorting of the declarations. That is, there is an ordering of the declarations in 𝑀 such that each declaration only depends on earlier declarations.

Note that performing the assignment operation introduced in Section A.1.1 causes the dependency ordering to change: for example supposing 𝑑₁𝑑₂ in 𝑀 and then if 𝑑₁ is assigned with a term 𝑡 not containing a metavariable, then 𝑑₂ will no longer depend on ?𝑚₁ and so 𝑑₁ ▸̷ 𝑑₂. An assignment may also cause a declaration to depend on metavariables that it did not previously depend on. As such, when an assignment is performed it may be necessary to reorder the declarations in order to recover the topological ordering.

Given 𝑀 : MvarContext, we will often be adding additional declarations and assignments to 𝑀 to make a new 𝑀 + Δ : MvarContext. Let's define Δ : MvarContextExtension as in (A.2).

(A.2).

Definition of MvarContextExtension. That is, an extension is either a declaration or an assignment.

MvarContextExtension ::=
| declare (mvar_name : Name) (type : Expr) (context : Context)
| assign (mvar_name : Name) (assignment : Expr)
extend : MvarContextMvarContextExtensionMvarContext
| 𝑀declare ?𝑚 α Γ[..𝑀,?𝑚, α, Γ, none]
| 𝑀assign ?𝑚 𝑣assign 𝑀 ?𝑚 𝑣

In order for a declare ?𝑚 α Γ to be valid for 𝑀, require that 𝑀;Γα : Type and that ?𝑚𝑀. Then we have that performing a valid declaration preserves the acylicity of 𝑀 with respect to . An assignment extension also preserves acyclicity; since step 2 of the procedure in Section A.1.1 explicitly forbids dependency loops.

Hence, given a sequence of extensions to 𝑀, the relation is still acyclic and hence there exists a topological ordering of the declarations in 𝑀 for .

A.1.3. Judgements and inference rules for metavariables

Now let's define the following judgements (in the same sense as in Section 2.1.3):

  • 𝑀;Γ𝑠α
    when 𝑠 has type α under 𝑀 and Γ.

  • 𝑀;Γ𝑠𝑡
    when 𝑠 : Expr and 𝑡 : Expr are definitionally equal (see [Car19 §2.2]).

  • ok 𝑀
    when the metavariable context 𝑀 is well-formed.

  • 𝑀ok Γ
    when the given local context Γ is well-formed under 𝑀.

The inference rules for these are given in (A.3).

I'll reproduce the list of (non-inductive) typing axioms here for completeness, but please see Carneiro's thesis [Car19] for a more comprehensive version, including a full set of inference rules for let binders, reductions, definitional equality and inductive constructions among others.

(A.3).

Non-development typing rules for Lean 3 CIC. Rules relating to inductive datatypes are omitted, see [Car19 §2.6] for the full set. The rules here differ from those in [Car19] through the addition of a spectating metavariable context 𝑀. In all cases, it is assumed that there are no variable clashes, so for example writing [..Γ, (𝑥α)] implicitly assumes that 𝑥Γ. Note that in the rule sort-typing, one of the sorts is primed. This is because the presentation given here introduces a Russel-style paradox called Girard's paradox [Hur95] unless the sort expressions are parameterised by a natural number such that sort nsort (n + 1), but these are omitted here for brevity.

𝑀;Γαsort
𝑀;Γ𝑠β

Γ-widening
𝑀;[..Γ,(𝑥α)]𝑠β
𝑀;Γαsort

var-typing
𝑀;[..Γ,(𝑥α)]𝑥α

sort-typing
;∅ ⊢ sortsort'
𝑀;Γ𝑠 ∶ Π (𝑥α), β
𝑀;Γ𝑡α

app-typing
𝑀;Γ𝑠 𝑡 ∶ ⦃𝑥𝑡β
𝑀;[..Γ,(𝑥α)]𝑠β

λ-typing
𝑀;Γ(λ (𝑥α), 𝑠)(Π (𝑥α), β))
𝑀;Γαsort u
𝑀;[..Γ,(𝑥α)]βsort

Π-typing
𝑀;Γ(Π (𝑥α), β)sort
𝑀;Γ𝑒α
𝑀;Γαβ

defeq-typing
𝑀;Γ𝑒β

empty-ctx-ok
𝑀 ⊢ ∅ ok
𝑀;Γα : sort

cons-ctx-ok
𝑀[..Γ, 𝑥α] ok

[Hur95]Hurkens, Antonius JCA simplification of Girard's paradox (1995)International Conference on Typed Lambda Calculi and ApplicationsI will now extend the above analysis to include an account of the metavariable development calculus that Lean uses to represent partially constructed proofs.

(A.4).

Metavariable typing rules

𝑀;Γα : sort
𝑀;Δ𝑠 : β

𝑀-widening
[..𝑀,𝑥,α,Γ];Δ𝑠 : β
𝑀;Γ𝑡 : α
𝑀;Δ𝑠 : β

𝑀-widening
[..𝑀,𝑥,α,Γ,𝑡];Δ𝑠 : β
𝑀;Γα : sort

metavariable
[..𝑀,𝑥,α,Γ,_];Γ?𝑥 : α
𝑀;Γ𝑡 : α

assignment
[..𝑀,𝑥,α,Γ,𝑡];Γ?𝑥𝑡

empty-mctx-ok
⊢ ∅ ok
𝑀;Γα : sort

declare-ok
[..𝑀,𝑥,α,Γ] ok
𝑀;Γ𝑡α

assign-ok
[..𝑀,𝑥,α,Γ,𝑡] ok

A.1.4. Properties of the Lean development calculus

Finish this section.

In this subsection I note some regularity lemmas for the extended development calculus similarly to Carneiro [Car19 §3.2]. The first thing to note is that a judgement 𝑀;ΓJ is invariant under a reordering of the declarations of Γ or 𝑀 that preserves the dependency ordering.

Using (A.3) and some additional rules for definitional equality (, not printed here) and inductive datatypes, Carneiro proves various properties of the type system, of which the following are relevant for the analysis here:

  • (Γe : α) ⇒ ⊢ Γ ok. If the context is not well formed, then we can't make any typing judgements.

  • Γe : αfv(e)Γfv(α)Γ. If a term is well typed in Γ then all of the free variables are present.

These can be extended to include metavariables and a metavaraiable context 𝑀. do this.

  • (𝑀;Γ𝑡α)(𝑀 ok)

  • (𝑀;Γ𝑡α)(𝑀Γ ok)

  • (𝑀;Γ𝑡α)_

  • 𝑀;Γ𝑡 : απ𝑀;Γ𝑡 : α

Given 𝑀;Γ𝑡α (which I will define in Section A.1.3), we should have that performing the 𝑀 substitution should not change the validity of the results. Two things to show: 𝑀;Γ𝑡α(𝑀 + Δ);Γ𝑡α. And [..𝑀₀, (?𝑚𝑣), ..𝑀₁];Γ𝑡α[..𝑀₀, ..?𝑚𝑣𝑀₁];?𝑚𝑣Γ ⊢ ⦃?𝑚𝑣𝑡 ∶ ⦃?𝑚𝑣α. Do this in two steps, show that judgements still apply if you instantiate, and then show that you can remove an unmentioned assignment. And that reordering the 𝑀's to another -totalizer is fine. That is, 𝑀;Γ𝑀 𝑡α and 𝑀;Γ𝑡𝑀 α and 𝑀;(𝑀 Γ)𝑡 : α.

A.1.5. Metavariable dependencies

Say that ?n depends on ?m in 𝑀 when any 𝑀-instantiated expression in ?n's declaration depends on ?m. Is it possible to create an 𝑀 such that there is a dependency cycle among the metavariables? For example, can we declare a recursive pair of metavariables ?n : {i : | i?m} and ?m : {i : | i?n}? In the above theory, it is not possible to declare a pair of metavariables with this property because a metavariable context is only ok when there is an explicit ordering on the metavariables such that each does not depend on the last. This is a consequence of the 𝑀-widening and 𝑀-widening axioms. In Lean's actual implementation, it is possible to do this through the tactic.unsafe.type_context monad using an unsafe assignment, in this case an infinite-descending expression will attempt to form which will not typecheck.

A.2. Zippers on Boxes

In order to run Lean tactics at various points in the Box structure defined in Chapter 3, we need to navigate to a certain point in a Box, and build up a metavariable context 𝑀 containing all of the metavariables from the 𝒯-binders and a local context Γ comprising the variables given in the -binders above the given point in the Box. The way to implement this plan is to define a context-aware zipper [Hue97[Hue97]Huet, GérardFunctional Pearl: The Zipper (1997)Journal of functional programming] on a Box.

Let's first create a coordinate system for Box. Coordinates for functors and inductive datatypes were introduced in Section 2.3.2.

(A.5).

Coordinate type for Box. Each constructor of Coord corresponds to a recursive argument for a constructor in Box (3.9). Hence there is no 𝒭 coordinate.

Coord ::=
|| 𝒯 | 𝒱 | 𝒜₁ | 𝒜₂ | 𝒪₁ | 𝒪₂

Where here 𝒜₁ is the coordinate for the b argument of the 𝒜 constructor. That is, get 𝒜₁ (𝒜 𝑏₁ 𝑥 𝑏₂) = some 𝑏₁. Similarly for the other coordinates. A list of Coord instances can be interpreted as an address to a certain point in an expression (see Section 2.3.3).

Next, define a datastructure called a path (using the same constructor names as Boxes):

(A.6).

Type definitions for Zippers and Paths. Definition of Zipper and Path over an expression. See Figure A.9 for a visualisation. The constructors of Path are created to match the signatures of the constructors in Box (3.9). Unit is used as a placeholder.

PathItem ::=
|: BinderPathItem
| 𝒯 : BinderPathItem
| 𝒱 : BinderExprPathItem
| 𝒜₁ : UnitBinderBoxPathItem
| 𝒜₂ : BoxBinderUnitPathItem
| 𝒪₁ : UnitBoxPathItem
| 𝒪₂ : BoxUnitPathItem
Path := List PathItem
Zipper :=
(path : Path)
× (cursor : Box)
(A.7).

Helper definitions wrap and unwrap for converting between Boxes and PathItems. These follow the standard schema found in [Hue97].

unwrap : CoordBoxOption (PathItem × Box)
| ℐ ↦ ℐ (𝑥α) 𝑏some ((𝑥α) , 𝑏 )
| 𝒯 ↦ 𝒯 (?𝑚:α) 𝑏some (𝒯 ?𝑚 , 𝑏 )
| 𝒱 ↦ 𝒱 (𝑥α) 𝑣 𝑏some (𝒱 (𝑥α) 𝑣 , 𝑏 )
| 𝒜₁ ↦ 𝒜 𝑏₁ (𝑥α) 𝑏₂some (𝒜₁ () (𝑥α) 𝑏₂, 𝑏₁)
| 𝒜₂ ↦ 𝒜 𝑏₁ (𝑥α) 𝑏₂some (𝒜₂ 𝑏₁ (𝑥α) (), 𝑏₂)
| 𝒪₁ ↦ 𝒪 𝑏₁ 𝑏₂some (𝒪₁ () 𝑏₂, 𝑏₁)
| 𝒪₂ ↦ 𝒪 𝑏₁ 𝑏₂some (𝒪₂ 𝑏₁ (), 𝑏₂)
wrap : PathItemBoxBox
|(𝑥α)𝑏 ↦ ℐ (𝑥α) 𝑏
| 𝒯 ?𝑚𝑏 ↦ 𝒯 (?𝑚:α) 𝑏
| 𝒱 (𝑥α) 𝑣𝑏 ↦ 𝒱 (𝑥α) 𝑣 𝑏
| 𝒜₁ () (𝑥α) 𝑏₂𝑏₁ ↦ 𝒜 𝑏₁ (𝑥α) 𝑏₂
| 𝒜₂ 𝑏₁ (𝑥α) ()𝑏₂ ↦ 𝒜 𝑏₁ (𝑥α) 𝑏₂
| 𝒪₁ () 𝑏₂𝑏₁ ↦ 𝒪 𝑏₁ 𝑏₂
| 𝒪₂ 𝑏₁ ()𝑏₂ ↦ 𝒪 𝑏₁ 𝑏₂
(A.8).

Definitions for up, down and some helper methods for navigating Zipper. The definitions for wrap and unwrap are given in (A.7).

up : ZipperOption Zipper
|[], 𝑏⟩ ↦ none
|[..𝑝, 𝑖], 𝑏⟩ ↦ some𝑝, wrap 𝑖 𝑏
down : CoordZipperOption Zipper
| 𝑐 ↦ ⟨𝑝, 𝑏⟩ ↦ do
𝑖, 𝑏₂⟩ ← (unwrap 𝑐 𝑏)
pure[..𝑝, 𝑖], 𝑏₂
down : List CoordZipperOption Zipper
| []𝑧some 𝑧
| [𝑐, ..𝑎]𝑧down 𝑐 𝑧 >>= down 𝑎
unzip : ZipperBox
|[], 𝑏⟩ ↦ 𝑏
|[..𝑝, 𝑖], 𝑏⟩ ↦ unzip𝑝, wrap 𝑖 𝑏
zip : BoxZipper
| b ↦ ⟨∅, [], b

We can visualise the zipper as in Figure A.9: a Box is annotated with an additional blob of paint at some point in the tree. The ancestors of are in the zipper's path, and everything below is the cursor. Applying up to this zipper will move the up to the next node in the Box tree (or return none otherwise). Similarly, down 𝑐 𝑧 (A.6) will inspect the cursor of 𝑧 and move the down on its 𝑐th recursive argument. The use of a zipper datastructure is used over an address for because the zipper system allows us to modify the cursor in place and then 'unzip' the zipper to perform an operation on a sub-box.

Figure A.9.

Visualisation of a zipper. The box to the left shows an example Box with a red blob indicating the position of the zipper's cursor. The right figure shows the underlying tree of Box constructors. All blue nodes are Box constructors and all orange nodes are Path constructors.

h₁ : PR

𝑕₁ : P

?𝑡₁: R
𝑕₂ : Q

?𝑡₂: R

Motivated by Figure A.9, it may be readily verified that down 𝑐 (up 𝑧) = some 𝑧 provided 𝑧's path is not empty and if 𝑐 is the coordinate corresponding to 𝑧's rightmost path entry. With similar conditions: up (down 𝑐 𝑧) = some 𝑧.

A.2.1. Contexts of zippers

Define the context of a zipper 𝑧.ctx as:

(A.10).
ctx : PathItemContext
|𝑥[𝑥]
| 𝒜₂ 𝑏₁ 𝑥 _[𝑥]
| _[]
ctx : ZipperContext
|_,𝑝,_⟩ ↦ [..(ctx 𝑥) for 𝑥 in 𝑝]

That is, 𝑧.ctx returns the list of the variables that are bound in the path. For the example 𝑧 in Figure A.9, 𝑧.ctx = [h₁].

Similarly, define the metavariable context 𝑧.mctx of a zipper as

(A.11).

Defining the induced metavariable context 𝑀 for a zipper.

mctx : PathItemList Binder
| 𝒯 𝑚[𝑚]
| _[]
mctx : ZipperMvarContext
|_,𝑝,_⟩ ↦ {..(mctx 𝑥) for 𝑥 in 𝑝}

So 𝑧.mctx is a metavariable context containing all of the targets defined above the cursor of 𝑧.

Now, given a zipper 𝑧, write 𝑧𝑡α to mean 𝑧.mctx;𝑧.ctx𝑡α. Similarly for 𝑝 : Path, 𝑝𝑡α.

A.2.2. Zipping and unzipping is sound.

The first thing to show is that given a sound move 𝑓 : MvarContextContextBoxOption Box parametrised by the contexts 𝑀 and Γ, then given 𝑏 : Box and a valid address 𝑎 : List Coord, we get another sound move 𝑓@𝑎 defined in (A.12).

(A.12).

Operation to perform the move 𝑓 𝑀 Γ : BoxOption Box 'under' the address 𝑎 : List Coord. do notation is used.

𝑓@𝑎 : BoxOption Box
| 𝑏₁do
𝑝, 𝑏₂⟩ ← down 𝑎 𝑏₁
𝑏₃𝑓 𝑝.mctx 𝑝.ctx 𝑏₂
pure (unzip𝑝, 𝑏₃)

Suppose that 𝑏₁α, then by induction on the typing laws for Box given in Section 3.4.2, we can show 𝑝𝑏₂ζ for some ζ : Expr. Since 𝑓 is sound and assuming 𝑓(𝑏₂) doesn't fail, we also have 𝑝𝑏₃ζ. Then finally the typing laws Section 3.4.2 can be applied in reverse to recover (unzip𝑝, 𝑧)α.

Here we are working towards being able to soundly run a tactic in the context provided by a Box zipper 𝑧 by finding ways to manipulate zippers that preserve the inference rules given in (A.3) and (A.4).

A.2.3. Sound Path updates

We will also need to perform some modifications to the paths of Zippers. A path modification ρ : 𝑝𝑝' is sound on a zipper 𝑧 =𝑝, 𝑏 if 𝑀;Γunzip𝑝, 𝑏⟩ ∶ β and 𝑀;Γunzip𝑝', 𝑏⟩ ∶ β. Hence to show soundness, one simply needs to show that corresponding move unzipρ is sound.

We have the following sound path-based moves:

(A.13).

Restriction. Note that the context of ?𝑡 has changed.

: α

?𝑡 : β
...𝑏

?𝑡 : β
: α

...𝑏
provided fv(β)
(A.15).

Target swapping.


?𝑡₁ : α
?𝑡₂ : β
...𝑏

?𝑡₂ : β
?𝑡₁ : α
...𝑏
provided ?𝑡₁mv(β)
(A.15).

𝒜-target-hoisting.


[𝑥 :=]

?𝑡₁ : α
...𝑏₁
...𝑏₂

?𝑡₁ : α
[𝑥 :=]

...𝑏₁
...𝑏₂

[𝑥 :=]
...𝑏₁

?𝑡₁ : α
...𝑏₂

?𝑡₁ : α
[𝑥 :=]
...𝑏₁

...𝑏₂
provided 𝑥fv(α)

A.3. Running tactics in Boxes

Now that we have the inference rules for metavariables and a definition of a zipper over a Box, we can define how to run a tactic within a Box.

A.3.1. Hoisting 𝒪 boxes

Before defining how to make a tactic act on a Box zipper we need to define an additional operation, called 𝒪-hoisting. This is where an 𝒪-box is lifted above its parent box.

(A.16).

Definition of 𝒪-lifting.

𝒪-lift
: BoxBox
| (𝑕 (𝒪 𝑏₁ 𝑏₂)) ↦ 𝒪 (𝑕 𝑏₁) (𝑕 𝑏₂)
| (𝒯 𝑚 (𝒪 𝑏₁ 𝑏₂)) ↦ 𝒪 (𝒯 𝑚 𝑏₁) (𝒯 𝑚 𝑏₂)
| (𝒜 𝑏₀ 𝑥 (𝒪 𝑏₁ 𝑏₂)) ↦ 𝒪 (𝒜 𝑏₀ 𝑥 𝑏₁) (𝒜 𝑏₀ 𝑥 𝑏₂)
| (𝒜 (𝒪 𝑏₁ 𝑏₂) 𝑥 𝑏₀) ↦ 𝒪 (𝒜 𝑏₁ 𝑥 𝑏₀) (𝒜 𝑏₂ 𝑥 𝑏₀)
| (𝒱 𝑥 𝑣 (𝒪 𝑏₁ 𝑏₂)) ↦ 𝒪 (𝒱 𝑥 𝑣 𝑏₁) (𝒱 𝑥 𝑣 𝑏₂)
| _none
(A.17).

Diagrammatic example of 𝒪-lift acting on a 𝒯 box.


?t : α
...𝑏₁
...𝑏₂


?t : α
...𝑏₁

?t : α
...𝑏₂
(A.18).

Example of 𝒪-lift acting on an -box.

h₀ : α

...𝑏₁
...𝑏₂

h₀ : α

...𝑏₁
h₀ : α

...𝑏₂

Proposition: 𝒪-hoisting is a sound move. Proof: by compatibility (3.15) it suffices to show that the results are equal, but then this is a corollary of the WLOG proof from the compatibility lemma (3.16).

The above definition (A.16) extends to 𝒪-hoisting path entries.

The motivation behind the hoisting is that 𝒪 boxes are a form of backtracking state in a similar spirit to a logic monad [KSFS05[KSFS05]Kiselyov, Oleg; Shan, Chung-chieh; et al.Backtracking, interleaving, and terminating monad transformers: (functional pearl) (2005)ACM SIGPLAN Notices]. However by including the branching 𝒪 box on the tree, it is possible to structurally share any context that is shared among the backtracking branches. Hoisting an 𝒪 box has the effect of causing the backtracking branches to structurally share less of the context with each other. In the most extreme case, we can repeatedly apply 𝒪-hoisting to move all of the branches to the top of the box structure, at which point we arrive at something isomorphic to what would arise as a result of using the logic monad form of backtracking.

A.3.2. Updating the path to reflect a change in context

Given 𝑧 : Zipper, define 𝑧.goal to be first metavariable declared on 𝑧.path. Hence given a 𝑧 : Zipper with the cursor having shape 𝒯, we can extract a metavariable context 𝑀 = mctx 𝑧 and a special goal metavariable 𝑧.goal, from these, create 𝑡𝑠 : TacticStateSee Section 2.4.4.. We can now run a tactic 𝑡 : Tactic on 𝑡𝑠. If successful, this will return a new tactic state 𝑡𝑠'. 𝑡𝑠' will have an extension of 𝑀See (A.2)., call this 𝑀 + Δ where Δ is a list of declarations and assignments successively applied to 𝑀. The task here is to create a new 𝑧': Zipper which includes the new targets and assignments in Δ.

The crux of the task here is to use Δ to construct a new 𝑝' : Path such that unzipping 𝑝', (M + Δ) 𝑧.cursor: Zipper will result in a sound move. In general, this will mean placing new metavariable declarations from Δ as new 𝒯 entries in the path and deleting 𝒯 entries which are assigned in Δ. Additionally, it may be necessary to hoist 𝒪 boxes and re-order existing 𝒯 entries. This has to be done carefully or else we can introduce ill-formed boxes.

For example, take the zipper shown in (A.19) with metavariable context 𝑀 containing one metavariable ?𝑚 : . There is a tactic apply List.length that will act on the goal ?𝑚 by declaring a pair of new metavariables ?α : sort and ?𝑙 : List ?α and assigning ?𝑚 with List.length ?𝑙. After perfroming this tactic, the new metavariable context 𝑀 + Δ is (A.20).

(A.19).

Initial zipper.


?𝑚 :
?𝑚
(A.20).

The metavariable context after performing the apply List.length tactic at (A.19).

𝑀 + Δ = {?𝑚 := length ?𝑙, Γ
,?α, Type, Γ
,?𝑙, List ?α, Γ
}

But now if our 𝑧.path is [𝒯 (?𝑚 : )], unzipping [𝒯 (?𝑚 : )], (𝑀 + Δ) 𝑧.cursor (A.21) will not result in a valid 𝑏 : Box (i.e. one that we can derive a judgement 𝑏 : β) because the result will depend on metavariables ?α and ?𝑙 which do not have corresponding 𝒯-binders.

(A.21).

Result of applying 𝑀 + Δ from (A.20) to (A.19). This is not a well-formed Box because the metavariable ?𝑙 is not bound.


?𝑚 :
length ?𝑙

We need to make sure that the new metavariables ?α and ?𝑙 are abstracted and added to the Path as shown in (A.22), so when we unzip we end up with a well-formed Box.

(A.22).

Correct update of the zipper to reflect 𝑀 + Δ.


?α : Type
?𝑙 : List ?α
length ?𝑙

We can find additional complications if the tactic declares new metavariables in a context E other than the current local context Γ. This may happen as a result of calling intros or performing an induction step. In these cases, some additional work must be done to ensure that the newly declared metavariable is placed at the correct point in the Box such that the context produced by the path above it is the same as E. This will be tackled in the next section through the definition of a function called update.

A.3.3. Definition: update

The procedure for correctly adjusting the path to produce valid boxes as exemplified by (A.22) is as follows. Define a function update : MvarContextExtensionPathOption Path. Here, MvarContextExtension (see (A.2)) is either a metavariable assignment or a metavariable declaration for 𝑀.

update Δ 𝑝 is defined such that (update Δ 𝑝).mctx = extend Δ 𝑝.mctx where extend is defined in (A.2). To do this, update will either insert a new 𝒯 path entry or delete a 𝒯 according to whether Δ is a declaration or an assignment. Then it will reorder the 𝒯 declarations such that it respects the dependency ordering .

In general, this is not always possible since there there may be a pair of declarations 𝑑₁ 𝑑₂ : MvarDecl such that 𝑑₁𝑑₂ but 𝑑₂.context𝑑₁.context, and so there is not necessarily an ordering of the declarations which is topological on both and . This case can be handled in theory through redeclaring metavariables and using delayed abstractions as I discuss in Section A.4, however I will not analyse or implement this case because it arises rarely in practice: most of the newly declared metavariables will not be in a different context or in a subcontext of 𝑝.ctx. Furthermore most of the tactics which do cause complex declarations to appear such as intro have an equivalent Box move.

(A.23).

Pseudocode definition of update. See the remarks after this code block for more information.

update : MvarContextExtensionZipperOption Zipper
update (declare ?𝑚 α Γ)𝑝,𝑏:=
assert 𝑝.mctx;Γαsort
if (Γ𝑝.ctx):
obtain E such that [..Γ, ..E] = 𝑝.ctx
obtain [..𝑝₀, ..𝑝₁] = 𝑝 such that
𝑝₀.ctx = Γ and 𝑝₀αsort
𝑝[..𝑝₀, 𝒯 ?𝑚α, ..𝑝₁]
reorder 𝑝
return𝑝, 𝑏
else if (Γ > 𝑝.ctx):
obtain E such that [..𝑝.ctx, 𝑥₀, ..., 𝑥] = Γ
𝑝[..𝑝, 𝒜₂ (𝑥₀ $ ... $𝑥$ 𝒯 ?𝑚) 𝑦]
reassign ?𝑚 in 𝑏 with (?𝑚 𝑥₀ ... 𝑥)
reorder 𝑝
return𝑝,𝑏
else (Γ𝑝.ctx):
-- that is, Γ and 𝑝.ctx are incomparable
fail -- this case is not supported
update (assign ?𝑚 𝑣)𝑝, 𝑏:=
assert (𝑝.mctx.assign ?𝑚 𝑣) is valid
delete (𝒯 ?𝑚) from 𝑝
assign 𝑣 to ?𝑚 in 𝑝
reorder 𝑝
return 𝑝

Some remarks on (A.23):

  • reorder 𝑝 performs a reordering on the 𝒯 binders in 𝑝 to respect and contexts. As noted earlier, in certain circumstances this may not be possible, in which case fail.

  • To account for 𝒪-boxes: before performing the above reordering, liftAnalogously to (A.16). all 𝒪 items in 𝑝 so that the resulting ..𝑝₁ does not contain any 𝒪-binders.

  • In the case that Δ = declare ?𝑚 α Γ and Γ𝑝.ctx, I am making the assumption that α doesn't depend on any metavariables whose context is outside Γ. This can occur if the offending metavariable is wrapped in a delayed abstraction. I will discuss this caveat in Section A.4.

  • The case where Γ > 𝑝.ctx works by reassigning the newly declared metavariable ?𝑚 with it's skolemised version and wrapping the declaration in a series of boxes. A circumstance where this can occur is if the intros tactic was used. I will not analyse the soundness of this case in further detail because it is expected that in these cases the intro move on Boxes (3.24) should be used instead.

An example of performing the assign case of (A.23) is given in (A.24):

(A.24).

?𝑡₁ :
?𝑡₂ : P ?𝑡₁
?𝑡₃ :

Suppose that a tactic assigned ?𝑡₁ with ?𝑡₃ + 4. Then without any reordering the box would look like (A.25):

(A.25).

?𝑡₂ : P (?𝑡₃ + 4)
?𝑡₃ :

However this is not a valid box because the 𝒯-binder for ?𝑡₂ depends on a variable that is not in scope. Fortunately as discussed in Section A.1.5 a total dependency ordering of metavariables in the same context always exists, and so in update we can use the 'target-swap' (A.15) path-reordering move to rearrange the targets to obey this. This is performed in the reorder step in update (A.23).

The way that update is defined means that

  • (update (declare ?𝑚 α Γ) 𝑧).mctx = extend (declare ?𝑚 α Γ) 𝑧.mctx for a valid declaration with Γ𝑝.ctx (up to reordering of the declarations in 𝑧.mctx). As mentioned above, the other case Γ > 𝑝.ctx is not considered here. Let 𝑝', 𝑏'⟩ = update (declare ?𝑚 α Γ)𝑝, 𝑏 and 𝑝𝑏α. Then 𝑝' ⊢ 𝑏α too because 𝑝'.ctx = 𝑝.ctx and 𝑝'.mctx = extend Δ 𝑝.mctx. And we saw in Section A.1.4 that adding a declaration to a metavariable context preserves type judgements.

  • Similarly, we have (update (assign ?𝑚 𝑣) 𝑧).mctx = extend (assign ?𝑚 𝑣) 𝑧.mctx for a valid assignment. Now let 𝑝', 𝑏'⟩ = update (assign ?𝑚 𝑣)𝑝, 𝑏 and 𝑝𝑏α. Then similarly 𝑝' ⊢ ⦃?𝑚𝑣𝑏 ∶ ⦃?𝑚𝑣α. Spell out why this means that unzip 𝑧' ∶ typeof 𝑧?

A.3.4. Applying a tactic to a zipper

We can now put together the components Now let zz : ZipperZipper be some function that navigates to a certain point in a Box and let tac be a tactic, we can define the 'escape hatch' tactic procedure, depicted below in Figure A.26.

Figure A.26.

Data-flow of a Box having a tactic applied at a certain point. The Box is first zipped to produce a Path, cursor Box and metavariable context. A monad is run on this state to produce a Zipper at the required location at which point a tactic is run with the goal being the target at the cursor. The resulting metavariable context is then used to instantiate the Zipper and unzipped to produce a new Box.

A.4. A variant of 𝒜 supporting delayed abstraction

A delayed abstraction 𝑒[𝑥] is a special type of expressionLean 3 calls it a delayed abstraction macro. constructed with a local variable 𝑥 and an expression 𝑒 which may depend on 𝑥. A delayed abstraction represents an abstraction of 𝑥 on 𝑒An abstraction is when free variables are replaced with bound variables.. This is used when 𝑒 depends on a metavariable ?𝑚 whose declaration context contains 𝑥. In this case, performing the abstraction immediately would be premature because the metavariable ?𝑚 might need to depend on 𝑥.

There are a few possible variants and extensions of the design of 𝒜 boxes which I considered. The main limitation of 𝒜 boxes as detailed above is that the structure of b is inscrutable when zipped on b. So in the above example we could not infer the structure of the function through reasoning on b. In order to model this, it is necessary to invoke delayed abstractions.

To get this to work, when zipping to b, one needs to first zip to the final 𝒭 r in b, and then instantiate b with a delayed abstraction of r. Then, when performing up 𝒜₂, if a metavariable under a delayed abstraction has been assigned you need to unzip back through the entirety of b and add any new targets to the path. So a variant PathItem.𝒜₁ would change to PathExprList NameExpr.

Bibliography for this chapter

  • [BN98]Baader, Franz; Nipkow, TobiasTerm rewriting and all that (1998)publisher Cambridge University Pressisbn 978-0-521-45520-6
  • [Car19]Carneiro, MarioLean's Type Theory (2019)view online
  • [EUR+17]Ebner, Gabriel; Ullrich, Sebastian; Roesch, Jared; Avigad, Jeremy; de Moura, LeonardoA metaprogramming framework for formal verification (2017)Proceedings of the ACM on Programming Languagesvolume 1number ICFPpages 1--29publisher ACM New York, NY, USAview online
  • [Hue97]Huet, GérardFunctional Pearl: The Zipper (1997)Journal of functional programmingvolume 7number 5pages 549--554publisher Cambridge University Pressview online
  • [Hur95]Hurkens, Antonius JCA simplification of Girard's paradox (1995)International Conference on Typed Lambda Calculi and Applicationspages 266--278organization Springer
  • [KSFS05]Kiselyov, Oleg; Shan, Chung-chieh; Friedman, Daniel P; Sabry, AmrBacktracking, interleaving, and terminating monad transformers: (functional pearl) (2005)ACM SIGPLAN Noticesvolume 40number 9pages 192--203publisher ACM New York, NY, USAview online
  • [MAKR15]de Moura, Leonardo; Avigad, Jeremy; Kong, Soonho; Roux, CodyElaboration in Dependent Type Theory (2015)CoRRvolume abs/1505.04324view online
  • [McB00]McBride, ConorDependently typed functional programs and their proofs (2000)view online
  • [SH17]Sterling, Jonathan; Harper, RobertAlgebraic Foundations of Proof Refinement (2017)arXiv preprint arXiv:1703.05215view online
  • [Spi11]Spiwack, ArnaudVerified computing in homological algebra, a journey exploring the power and limits of dependent type theory (2011)view online
  • [Ste17]Steele Jr., Guy L.It's Time for a New Old Language (2017)view onlineInvited talk at Clojure/Conj 2017. Slides: http://groups.csail.mit.edu/mac/users/gjs/6.945/readings/Steele-MIT-April-2017.pdf
© 2021 E.W.Ayers. Built with Gatsby