HOAS nat bijection

From The Twelf Project
Jump to: navigation, search
This is Literate Twelf
Code: here
Status: %% OK %%
Output: here.

Bijection from HOAS to natural numbers

Preliminaries

This file shows a simple HOAS term type and a mapping from these terms to the natural numbers. It depends on John Boyland's library signatures, in particular void, bool, nat and natpair.

Such mappings are useful so that the library signatures for set and map can be used to form sets or maps using the HOAS terms as keys.

The mapping is proved total, deterministic, onto and one2one in four separate metatheorems. (The actual relation itself is not proved total or deterministic directly.). Thus the mapping is a bijection.

This file is a proof of concept that this sort of mapping can be done and more importantly, proved correct, in Twelf. The HOAS terms themselves are uninteresting. The purpose in doing these proofs is to help me (John Boyland) write a general package to generate such mappings and their proofs.

In writing the proofs, I am greatly indebted to Rob Simmons who took up my challenge to write bijections involving HOAS terms. However, I go against his explicit advice in using the "%theorem" syntax extensively which I find much more clear that the "preferred" Twelf way of purity.


Definitions

The syntax

The HOAS defined here is uninteresting. There isn't even any way to use more than one variable (although the proofs use techniques that can handle any number of variables).

t : type.


a : t.

b : t -> t.

f : (t -> t) -> t.

%block blocksimple : block {v:t}.

Equality

eq : t -> t -> type.


eq/ : eq T T.

Variable levels

A variable level is the (nonzero) natural number for a variable. This value is used to determine the mapping for a variable.

varlevel : t -> nat -> type.

%block blockvar : some {l} block {v} {vl:varlevel v (s l)}.

Mapping

The bijection from t to nat is called "tonat". In its more general form the relation takes a natural number indicating how deep we are inside functions.

tonat* : nat -> t -> nat -> type.

%abbrev tonat = tonat* z.


tonat/v : 
	varlevel V L ->
	plus M L N ->
    tonat* N V M.

tonat/a : tonat* N a N.

tonat/b : 
	tonat* N T M ->
	times (s (s z)) M TM ->
	plus (s N) TM M' ->
    tonat* N (b T) M'.

tonat/f :
	({v} (varlevel v (s N)) ->
         tonat* (s N) (F v) M) ->
	times (s (s z)) M TM ->
	plus (s (s N)) TM M' ->
    tonat* N (f F) M'.

Utility lemmas

The following theorems prove obvious simple things about the basic relations. They following the conventions established in John Boyland's library signatures.

%theorem false-implies-varlevel :
	forall*	{V} {L}
	forall	{F:void}
	exists	{VL:varlevel V L}
	true.

%worlds (blockvar) (false-implies-varlevel _ _).
%total { } (false-implies-varlevel _ _).


%theorem varlevel-respects-eq :
	forall* {V} {L1} {L2}
	forall	{VL1:varlevel V L1}
		{E:nat`eq L1 L2}
	exists	{VL2:varlevel V L2}
	true.

- : varlevel-respects-eq VL nat`eq/ VL.

%worlds (blocksimple | blockvar) (varlevel-respects-eq _ _ _).
%total { } (varlevel-respects-eq _ _ _).


%theorem false-implies-tonat :
	forall* {N} {T} {M}
	forall	{F:void}
	exists	{TN:tonat* N T M}
	true.

%worlds (blockvar) (false-implies-tonat _ _).
%total { } (false-implies-tonat _ _).

Proof of totality of tonat

The difficulty here is that we need to prove that when we get to a variable (and exactly how we tell this in Twelf is tricky because variables can't be captured in case analysis), we need to ensure that (1) the variable has a level associated with it and (2) the level is in the range 1..N where N is the block nesting we are in. Blocks are useful for (1) but not for (2) because there's no way to connect the context with the current nesting level.

Instead we use a technique (I learn from Rob Simmons) to handle one level of variable a time in a separate lemma. This works since for each particular HOAS function we know that the variable is bound legally.

We package this approach up into an auxiliary relation that incidentally makes it easy to capture variables in case analysis. This makes for a wordy series of proofs. Perhaps we can get rid of 'case' in general.

Auxiliary definitions

raw variables

A variable is raw if we haven't verified that it has a level in range. Non variables are not raw.

israw : t -> bool -> type.

%abbrev rawvar = [T] israw T true.


israw/a : israw a false.

israw/b : israw (b _) false.

israw/f : israw (f _) false.

case analysis

We case analysis terms with two cases for variables. The raw case is used only internally and can be ignored in "clients" that don't use israw.

case : nat -> t -> type.


case/a : case _ a.

case/b : case N T -> case N (b T).

case/f : ({v} varlevel v (s N) -> case (s N) (F v)) -> case N (f F).

case/var : varlevel V L -> nat`ge N L -> case N V.

case/raw : rawvar V -> case N V.

Theorems about auxiliary definitions

What follows first is a theorem that says that in a context where all variables are raw, we can campute the rawness of all terms. In a Twelf idiom that will be seen several times in this file (and which I learned from Rob Simmons), we have to put the theorem for the the variable case in the same context that defines the variable as raw. (This is rather annoying: Twelf should be smart enough to see that the context that defines the variable has the necessary relation.) This somewhat contorted idiom falls afoul of autofreezing in Twelf 1.5r3. I consider this a bug in Twelf, but fortunately it can be worked around by defining a fake circular dependency. (Again, the idea from Rob Simmons.) For some reason, unlike Rob's examples and the later instances in this file, I need to add israw to the fake dependencies as well. The definition "fake" is never used again. It has no "meaning."

%theorem israw-total* :
	forall	{T}
	exists	{B} {I:israw T B}
	true.

%abbrev israw-total = israw-total* _ _.

- : israw-total israw/a.

- : israw-total israw/b.

- : israw-total israw/f.

fake : type.
- : fake <- {i:israw-total* T B I} israw-total* T' B' I'.
- : fake <- {i:israw-total* T B I} israw T' B'.

%block blockraw : block {v} {rv:rawvar v} {irt:israw-total rv}.

%worlds (blockraw) (israw-total* _ _ _).
%total { } (israw-total* _ _ _).

The following theorem handles one variable converting it from raw to handle a level that is in the required range. This is an important technique for handle variables in Twelf: one at a time.

%theorem var-gets-level :
	forall* {N} {T} {L}
	forall	{F: {v} {rv:rawvar v} {i:israw-total rv} case N (T v)}
		{GE: nat`ge N L}
	exists  {F': {v} (varlevel v L) -> case N (T v)}
	true.

- : var-gets-level ([v] [r] [i] (case/raw r)) N>=L
                   ([v] [vl] (case/var vl N>=L)).

- : var-gets-level ([v] [r] [i] (case/raw R)) _
                   ([v] [vl] (case/raw R)).

- : var-gets-level ([v] [c] [i] (case/var VL N>=L)) _
                   ([v] [vl] (case/var VL N>=L)).

- : var-gets-level ([v] [c] [i] case/a) _
                   ([v] [vl] case/a).

- : var-gets-level ([v] [c] [i] (case/b (C v c i))) N>=L
                   ([v] [vl] (case/b (C' v vl)))
    <- var-gets-level ([v] [c] [i] (C v c i)) N>=L ([v][vl] (C' v vl)).

- : var-gets-level ([v] [c] [i] (case/f ([v'][vl'] (C v' vl' v c i)))) N>=L
                   ([v][vl] (case/f ([v'][vl'] (C' v' vl' v vl))))
    <- ge-implies-succ-gt N>=L N+1>L
    <- ({v'} {vl':varlevel v' _} 
	var-gets-level ([v] [c] [i] (C v' vl' v c i)) (nat`ge/> N+1>L)
             ([v][vl](C' v' vl' v vl))).

%worlds (blockvar | blockraw) (var-gets-level _ _ _).
%total F (var-gets-level F _ _).

We are now ready to prove that we can always "case" a term. This code follows John Boyland's library convention of defining a "-total" metatheorem as having implicit arguments that are explicit in a "-total*" version. In the main lemma, the interesting case is when we have a "f" term: after ensuring that the subterm can be be tested for rawness, we recurse while the variable is assumed raw. Once this is done, we convert the variable into one with a level using "var-gets-level". Note that the var levels don't go into the context for this theorem.

%theorem case-total* :
	forall	{T}
	exists	{C:case z T}
	true.

%abbrev case-total = case-total* _.

%theorem case-total/L :
	forall* {B}
	forall	{N} {T} {I:israw T B}
	exists	{C:case N T}
	true.

- : case-total/L _ _ _ (case/a).

- : case-total/L _ _ _ (case/b C)
    <- israw-total I
    <- case-total/L _ _ I C.

- : case-total/L _ (f ([v] F v)) israw/f (case/f ([v] [vl] (C' v vl)))
    <- ({v} {r:rawvar v} {i:israw-total r}
        israw-total (I v r i))
    <- ({v} {r:rawvar v} {i:israw-total r} 
        case-total/L _ (F v) (I v r i : israw (F v) B) (C v r i))
    <- var-gets-level C (nat`ge/= nat`eq/) C'.

- : case-total/L _ V R (case/raw R).

%worlds (blockraw) (case-total/L _ _ _ _).
%total T (case-total/L _ T _ _).

- : case-total* T C
    <- israw-total I
    <- case-total/L z T I C.

%worlds () (case-total* _ _).
%total { } (case-total* _ _).

Main theorem

We are ready now to prove totality of the relation. We case the term first and then have everything we need to push through totality.

%theorem tonat-total* :
	forall {T:t}
	exists {M:nat} {D:tonat T M}
	true.

%abbrev tonat-total = tonat-total* _ _.

%theorem tonat-total/L :
	forall {N:nat} {T:t} {C:case N T}
	exists {M:nat} {D:tonat* N T M}
	true.

- : tonat-total/L _ _ (case/var VL GE) _ (tonat/v VL P)
    <- ge-implies-plus GE _ P.

- : tonat-total/L _ _ (case/a) _ (tonat/a).

- : tonat-total/L _ _ (case/b C) _ (tonat/b TN T P)
    <- tonat-total/L _ _ C _ TN
    <- times-total T
    <- plus-total P.

- : tonat-total/L _ _ (case/f ([v] [vl] (C v vl))) _ 
                      (tonat/f ([v] [vl] (TN v vl)) T P)
    <- ({v} {vl:varlevel v (s N)} tonat-total/L _ _ (C v vl) _ (TN v vl))
    <- times-total T
    <- plus-total P.

%worlds (blockvar) (tonat-total/L _ _ _ _ _).
%total (C) (tonat-total/L _ _ C _ _).

- : tonat-total TN
    <- case-total C
    <- tonat-total/L _ _ C _ TN.

%worlds () (tonat-total* _ _ _).
%total { } (tonat-total* _ _ _).

Proof of the determinicity of the mapping

In this section, we prove that tonat gives only one value (hence it is a function). This sort of theorem is called a "uniqueness" theorem. Here the name I use for it comes from Twelf's "%deterministic" declaration. (I find the term "unique" might refer to the "one2one" aspect, proved later.)

This aspect is much easier to prove that any of the others. That probably reflects the fact that the relation was written in a functional style.

Auxiliary theorems

We prove that variable levels are "unique" and that they are never zero. The proofs are trivial: Twelf can accept them from the context alone.

%theorem varlevel-deterministic :
	forall* {V} {L1} {L2}
	forall	{VL1:varlevel V L1}
		{VL2:varlevel V L2}
	exists	{E:nat`eq L1 L2}
	true.

- : varlevel-deterministic _ _ nat`eq/.

%worlds (blockvar) (varlevel-deterministic _ _ _).
%total { } (varlevel-deterministic _ _ _).


%theorem varlevel-contradiction :
	forall* {V} {L}
	forall	{VL:varlevel V L}
		{E:nat`eq L z}
	exists	{F:void}
	true.

%worlds (blockvar) (varlevel-contradiction _ _ _).
%total { }  (varlevel-contradiction _ _ _).

Main Theorem

%theorem tonat-deterministic :
	forall* {T1} {T2} {N1} {N2}
	forall	{TN1:tonat T1 N1} 
		{TN2:tonat T2 N2}
		{E: eq T1 T2}
	exists	{E: nat`eq N1 N2}
	true.

%theorem tonat-deterministic/L :
	forall* {T} {N} {N1} {N2}
	forall	{TN1:tonat* N T N1} 
		{TN2:tonat* N T N2}
	exists	{E: nat`eq N1 N2}
	true.

- : tonat-deterministic/L (tonat/v VL1 P1) (tonat/v VL2 P2) N1=N2
    <- varlevel-deterministic VL1 VL2 L1=L2
    <- plus-right-cancels P1 P2 L1=L2 nat`eq/ N1=N2.

- : tonat-deterministic/L (tonat/a) (tonat/a) nat`eq/.

- : tonat-deterministic/L (tonat/b TN1 T1 P1) (tonat/b TN2 T2 P2) M1'=M2'
    <- tonat-deterministic/L TN1 TN2 M1=M2
    <- times-deterministic T1 T2 nat`eq/ M1=M2 TM1=TM2
    <- plus-deterministic P1 P2 nat`eq/ TM1=TM2 M1'=M2'.

- : tonat-deterministic/L (tonat/f ([v] [vl] (TN1 v vl)) T1 P1)
                          (tonat/f ([v] [vl] (TN2 v vl)) T2 P2) M1'=M2'
    <- ({v} {vl:varlevel v (s N)} tonat-deterministic/L (TN1 v vl) (TN2 v vl)
                                                        M1=M2)
    <- times-deterministic T1 T2 nat`eq/ M1=M2 TM1=TM2
    <- plus-deterministic P1 P2 nat`eq/ TM1=TM2 M1'=M2'.

%worlds (blockvar) (tonat-deterministic/L _ _ _).
%total (T) (tonat-deterministic/L T _ _).

- : tonat-deterministic TN1 TN2 eq/ N1=N2
    <- tonat-deterministic/L TN1 TN2 N1=N2.

%worlds () (tonat-deterministic _ _ _ _).
%total { } (tonat-deterministic _ _ _ _).

Proving that the mapping is onto.

Here we use the mathematical term "onto": a function is "onto" if its range is equal to its co-domain: that is if every value in the co-domain has a value in the domain that maps to it.

The tricky aspect here is that we need to show that every level that the reverse mapping has a variable associated with it. We do this using a helper relation, as opposed to putting something in the context, since as explained earlier, the context is useless to connect variables with the nesting level.

Auxiliary definitions

We define a relation that builds on the context relation. I find this rather interesting because it uses the context relation but is not itself in the context. This is rather rare in my limited experience.

upto N says that we have a variable for all levels 1..N.

upto : nat -> type.


upto/z : upto z.

upto/s : upto N -> varlevel V (s N) -> upto (s N).

Theorems about auxiliary definitions

The obvious lemma that makes use of the main purpose of the relation:

%theorem upto-implies-varlevel :
	forall* {N} {L}
	forall	{U:upto N}
		{LT:nat`gt N L}
	exists	{V} {VL:varlevel V (s L)}
	true.

- : upto-implies-varlevel upto/z ZERO>L a VL
    <- nat`gt-contradiction ZERO>L F
    <- false-implies-varlevel F VL.

- : upto-implies-varlevel (upto/s _ VL) (gt/1) _ VL.

- : upto-implies-varlevel (upto/s U _) (gt/> G) _ VL
    <- upto-implies-varlevel U G _ VL.

%worlds (blockvar) (upto-implies-varlevel _ _ _ _).
%total (U) (upto-implies-varlevel U _ _ _).

Main theorem

We prove the main result using two lemmas that do the case analysis on the number against the nesting level and the parity. (In general, one would use a divisor counting all cases that are recursive.) The proofs are long but simply arithmetic manipulation. Proving termination uses meta-gt for strong induction over the natural numbers.

%theorem tonat-onto* :
	forall	{N:nat}
	exists	{T} {TN:tonat T N}
	true.

%abbrev tonat-onto = tonat-onto* _ _.

%theorem tonat-onto/L1 :
	forall* {C}
	forall	{N:nat} 
		{U:upto N}
		{M:nat}
		{CMP:nat`compare N M C}
	exists	{T} {TN:tonat* N T M}
	true.

%theorem tonat-onto/L2 :
	forall*	{TM}
	forall	{N:nat}
		{U:upto N}
		{M:nat}
		{P:plus N (s TM) M}
		{Q} {R} {DR:divrem TM (s (s z)) Q R}
	exists	{T} {TN:tonat* N T M}
	true.

- : tonat-onto/L1 N U M (compare/> N>M) _ (tonat/v VL M+L+1=N)
    <- nat`gt-implies-plus N>M L L+1+M=N
    <- plus-commutative L+1+M=N M+L+1=N
    <- plus-implies-ge M+L+1=N N>=L+1
    <- ge-succ-implies-gt N>=L+1 N>L
    <- upto-implies-varlevel U N>L _ VL.

- : tonat-onto/L1 N U _ (compare/=) a tonat/a.

- : tonat-onto/L1 N U M (compare/< M>N) _ TN
    <- gt-implies-plus M>N TM TM+1+N=M
    <- plus-commutative TM+1+N=M N+TM+1=M
    <- divrem-total DR
    <- tonat-onto/L2 N U M N+TM+1=M _ _ DR _ TN.

- : tonat-onto/L2 _ U M' N+TM+1=M' M z TM/2=M _ (tonat/b TN TWO*M=TM N+1+TM=M')
    <- div-can-be-inverted TM/2=M M*2=TM
    <- times-commutative M*2=TM TWO*M=TM
    <- plus-swap-succ-converse N+TM+1=M' N+1+TM=M'
    <- plus-implies-gt N+1+TM=M' nat`eq/ M'>TM
    <- times-nonzero-implies-ge M*2=TM TM>=M
    <- nat`gt-transitive-ge M'>TM TM>=M M'>M
    <- meta-gt _ _ M'>M
    <- compare-total CMP
    <- tonat-onto/L1 _ U M CMP _ TN.

- : tonat-onto/L2 N U M' (N+TM'+1=M':plus N (s TM') M') M (s z) TM'/2=M,1 
                  (f ([v] F v))
                  (tonat/f ([v] [vl] (TN v vl))
                           TWO*M=TM N+2+TM=M')
    <- divrem-can-be-inverted TM'/2=M,1 TM M*2=TM TM+ONE=TM'
    <- times-commutative M*2=TM TWO*M=TM
    <- plus-commutative (plus/s plus/z) TM+ONE=TM+1
    <- plus-deterministic TM+ONE=TM' TM+ONE=TM+1 nat`eq/ nat`eq/ TM'=TM+1
    <- succ-deterministic TM'=TM+1 (TM'+1=TM+2:nat`eq (s TM') (s (s TM)))
    <- plus-respects-eq N+TM'+1=M' nat`eq/ TM'+1=TM+2 nat`eq/ N+TM+2=M'
    <- plus-swap-succ-converse N+TM+2=M' N+1+TM+1=M'
    <- plus-swap-succ-converse N+1+TM+1=M' N+2+TM=M'
    <- plus-implies-ge N+TM'+1=M' M'>=TM'+1
    <- ge-succ-implies-gt M'>=TM'+1 M'>TM'
    <- quotient-of-nonzero-is-smaller TM'/2=M,1 TM'=TM+1 TM'>M
    <- nat`gt-transitive M'>TM' TM'>M M'>M
    <- meta-gt _ _ M'>M
    <- nat`compare-total CMP
    <- ({v} {vl:varlevel v (s N)} 
        tonat-onto/L1 (s N) (upto/s U vl) M CMP (F v) (TN v vl)).

- : tonat-onto/L2 _ _ _ _ _ (s (s _)) DR a TN
    <- divrem-implies-gt DR TWO>R+2
    <- succ-preserves-gt-converse TWO>R+2 ONE>R+1
    <- succ-preserves-gt-converse ONE>R+1 ZERO>R
    <- gt-contradiction ZERO>R F
    <- false-implies-tonat F TN.

%worlds (blockvar) (tonat-onto/L1 _ _ _ _ _ _)
                   (tonat-onto/L2 _ _ _ _ _ _ _ _ _).
%total (M1 M2) (tonat-onto/L2 _ _ M2 _ _ _ _ _ _)
               (tonat-onto/L1 _ _ M1 _ _ _).

Proof that mapping is "one to one"

This is the most involved proof. The sketch is that we first prove that two terms that reduce to the same natural number are "eql" in a way that only requires that the variables have the same level, but not that they are the same. Of course, there is only one variable for each level, which means that the terms are truly identical. But this is impossible to express in the context. Instead, we chip away at the variables from the "outside", each time reducing the level of the remaining variables.

Auxiliary definitions

Equality (permitting variables with the same level).

eql* : nat -> t -> t -> type.

%abbrev eql = eql* z.


eql/eq : eq T1 T2 -> eql* N T1 T2.

eql/b : eql* N T1 T2 -> eql* N (b T1) (b T2).

eql/f1 : ({v:t} (eql* N (F1 v) (F2 v))) -> 
	 eql* N (f F1) (f F2).

eql/f2 : ({v:t} {vl:varlevel v (s N)} (eql* (s N) (F1 v) (F2 v))) ->
	eql* N (f F1) (f F2).

eql/v : varlevel V1 L -> varlevel V2 L -> eql* N V1 V2.

Measure of eql sizes.

We use this measure to be able to prove termination. We need eqlsize/v = eqlsize/eq, eqlsize/f1 = eqlsize/f2. (Less than is ok in each case but would require that we rephrase the lemmas.)

eqlsize : (eql* N T1 T2) -> nat -> type.


eqlsize/eq : eqlsize (eql/eq _) z.

eqlsize/b : eqlsize E N -> eqlsize (eql/b E) (s N).

eqlsize/f1 : ({v} eqlsize (E v) N) ->
	eqlsize (eql/f1 ([v] (E v))) (s N).

eqlsize/f2 : ({v} {vl} eqlsize (E v vl) N) ->
	eqlsize (eql/f2 ([v] [vl] (E v vl))) (s N).

eqlsize/v : eqlsize (eql/v _ _) z.

Copied definitions

It turns out that switching variables to an earlier level will cause mixup (because we need to have both the old and new levels in the context at the same time) unless we use a different definition. For that reason, we define alternatives for varlevel, eql and eqlsize.

varlevel' : t -> nat -> type.


eql*' : nat -> t -> t -> type.

eql'/eq : eq T1 T2 -> eql*' N T1 T2.

eql'/b : eql*' N T1 T2 -> eql*' N (b T1) (b T2).

eql'/f1 : ({v:t} (eql*' N (F1 v) (F2 v))) -> 
	 eql*' N (f F1) (f F2).

eql'/f2 : ({v:t} {vl:varlevel' v (s N)} (eql*' (s N) (F1 v) (F2 v))) ->
	eql*' N (f F1) (f F2).

eql'/v : varlevel' V1 L -> varlevel' V2 L -> eql*' N V1 V2.


eqlsize' : (eql*' N T1 T2) -> nat -> type.

eqlsize'/eq : eqlsize' (eql'/eq _) z.

eqlsize'/b : eqlsize' E N -> eqlsize' (eql'/b E) (s N).

eqlsize'/f1 : ({v} eqlsize' (E v) N) ->
	eqlsize' (eql'/f1 ([v] (E v))) (s N).

eqlsize'/f2 : ({v} {vl} eqlsize' (E v vl) N) ->
	eqlsize' (eql'/f2 ([v] [vl] (E v vl))) (s N).

eqlsize'/v : eqlsize' (eql'/v _ _) z.

Theorems about auxiliary definitions

%theorem false-implies-eql :
	forall* {T1} {T2} {N}
	forall	{F:void}
	exists	{E:eql* N T1 T2}
	true.

%worlds (blockvar | blocksimple) (false-implies-eql _ _).
%total { }  (false-implies-eql _ _).


%theorem eqlsize-total* :
	forall*	{N} {T1} {T2}
	forall  {E:eql* N T1 T2}
	exists  {S} {ES:eqlsize E S}
	true.

%abbrev eqlsize-total = eqlsize-total* _ _.

- : eqlsize-total eqlsize/eq.

- : eqlsize-total (eqlsize/b ES)
    <- eqlsize-total ES.

- : eqlsize-total (eqlsize/f1 ([v] (ES v)))
    <- ({v} eqlsize-total (ES v)).

- : eqlsize-total (eqlsize/f2 ([v] [vl] (ES v vl)))
    <- ({v} {vl} eqlsize-total (ES v vl)).

- : eqlsize-total eqlsize/v.

%worlds (blocksimple | blockvar) (eqlsize-total* _ _ _).
%total (E)  (eqlsize-total* E _ _).

The following block is used when we remove the outmost variable: all other variables are at least level 2. "blockvar2" makes this context explicit.

%block blockvar2 : some {l} block {v} {vl:varlevel v (s (s l))}.


%theorem remove-one-var :
	forall* {F1} {F2} {N} {S}
	forall {E:{v} {vl:varlevel v (s z)} (eql* (s N) (F1 v) (F2 v))}
	       {ES:{v} {vl} eqlsize (E v vl) S}
	exists {E':{v} (eql* (s N) (F1 v) (F2 v))}
	       {ES':{v} eqlsize (E' v) S}
	true.

- : remove-one-var ([v] [vl] eql/eq eq/) ([v] [vl] eqlsize/eq)
                   ([v] eql/eq eq/) ([v] eqlsize/eq).

- : remove-one-var ([v] [vl] eql/b (F v vl)) ([v] [vl] eqlsize/b (FS v vl))
                   ([v] eql/b (F' v)) ([v] eqlsize/b (FS' v))
    <- remove-one-var F FS F' FS'.

- : remove-one-var ([v] [vl] eql/f1 ([v'] (F v' v vl)))
		   ([v] [vl] eqlsize/f1 ([v'] (FS v' v vl)))
                   ([v] eql/f1 ([v'] (F' v' v)))
                   ([v] eqlsize/f1 ([v'] (FS' v' v)))
    <- {v'} remove-one-var (F v') (FS v') (F' v') (FS' v').

- : remove-one-var ([v] [vl] eql/f2 ([v'] [vl'] (F v' vl' v vl)))
		   ([v] [vl] eqlsize/f2 ([v'] [vl'] (FS v' vl' v vl)))
                   ([v] eql/f2 ([v'] [vl'] (F' v' vl' v)))
                   ([v] eqlsize/f2 ([v'] [vl'] (FS' v' vl' v)))
    <- {v'} {vl'} remove-one-var (F v' vl') (FS v' vl') (F' v' vl') (FS' v' vl').
- : remove-one-var ([v] [vl] eql/v vl vl) ([v] [vl] eqlsize/v)
                   ([v] eql/eq eq/) ([v] eqlsize/eq).

- : remove-one-var ([v] [vl] eql/v VL1 VL2) ([v] [vl] eqlsize/v)
                   ([v] eql/v VL1 VL2) ([v] eqlsize/v).

%worlds (blocksimple | blockvar2) (remove-one-var _ _ _ _).
%total (E) (remove-one-var E _ _ _).

Next follows the tortuous shift down of levels: we shift down and change to use the alternative definitions, and then we go to back the normal definitions (with no shift). The context we use will have both the old and new varlevels. It order to shift from one to the other, we need theorems that let us go from one to the other. Unfortunately, Twelf is not smart enough to infer that the context has what the theorem needs, so (as explained above) we need to put the theorem in context itself and add fake dependencies.

Adding to the complexity is the fact that we need to track the size of the equality rules for termination proof (later).

%theorem varlevel-shifts-down :
	forall* {V} {L}
	forall	{VL:varlevel V (s (s L))}
	exists	{VL':varlevel' V (s L)}
	true.

%block shiftdown : some {l} block {v} {vl:varlevel v (s (s l))} 
                                      {vl':varlevel' v (s l)}
                                      {vsd:varlevel-shifts-down vl vl'}.

fake : type.
- : fake <- ({x:varlevel-shifts-down X Y} varlevel-shifts-down X' Y').

%worlds (blocksimple | shiftdown) (varlevel-shifts-down _ _).
%total { } (varlevel-shifts-down _ _).


%theorem shift-varlevel/L1 :
	forall* {N} {T1} {T2} {S}
	forall	{E: eql* (s N) T1 T2}
		{ES:eqlsize E S}
	exists	{E': eql*' N T1 T2}
		{ES':eqlsize' E' S}
	true.

- : shift-varlevel/L1 (eql/eq eq/) eqlsize/eq (eql'/eq eq/) eqlsize'/eq.

- : shift-varlevel/L1 (eql/b E) (eqlsize/b ES) (eql'/b E') (eqlsize'/b ES')
    <- shift-varlevel/L1 E ES E' ES'.

- : shift-varlevel/L1 (eql/f1 ([v] (F v))) (eqlsize/f1 FS)
                      (eql'/f1 ([v] (F' v))) (eqlsize'/f1 FS')
    <- {v} shift-varlevel/L1 (F v) (FS v) (F' v) (FS' v).

- : shift-varlevel/L1 (eql/f2 ([v] [vl:varlevel v (s (s N))] (F v vl)))
		      (eqlsize/f2 FS)
                      (eql'/f2 ([v] [vl:varlevel' v (s N)] (F' v vl)))
		      (eqlsize'/f2 FS')
    <- {v} {vl} {vl':varlevel' v (s N)} {vsd:varlevel-shifts-down vl vl'}
       shift-varlevel/L1 (F v vl) (FS v vl) (F' v vl') (FS' v vl').

- : shift-varlevel/L1 (eql/v VL1 VL2) eqlsize/v (eql'/v VL1' VL2') eqlsize'/v
    <- varlevel-shifts-down VL1 VL1'
    <- varlevel-shifts-down VL2 VL2'.

%worlds (blocksimple | shiftdown) (shift-varlevel/L1 _ _ _ _).
%total (E)  (shift-varlevel/L1 E _ _ _).


%theorem varlevel-shifts-back :
	forall* {V} {L}
	forall	{VL':varlevel' V (s L)}
	exists	{VL:varlevel V (s L)}
	true.

%block shiftback : some {l} block {v} {vl':varlevel' v (s l)} 
                                      {vl:varlevel v (s l)}
                                      {vsb:varlevel-shifts-back vl' vl}.

fake : type.
- : fake <- ({x:varlevel-shifts-back X Y} varlevel-shifts-back X' Y').

%worlds (blocksimple | shiftback) (varlevel-shifts-back _ _).
%total { } (varlevel-shifts-back _ _).


%theorem shift-varlevel/L2 :
	forall* {N} {T1} {T2} {S}
	forall	{E': eql*' N T1 T2}
		{ES': eqlsize' E' S}
	exists	{E: eql* N T1 T2}
		{ES: eqlsize E S}
	true.

- : shift-varlevel/L2 (eql'/eq eq/) eqlsize'/eq (eql/eq eq/) eqlsize/eq.

- : shift-varlevel/L2 (eql'/b E) (eqlsize'/b ES) (eql/b E') (eqlsize/b ES')
    <- shift-varlevel/L2 E ES E' ES'.

- : shift-varlevel/L2 (eql'/f1 ([v] (F v))) (eqlsize'/f1 FS)
                      (eql/f1 ([v] (F' v))) (eqlsize/f1 FS')
    <- {v} shift-varlevel/L2 (F v) (FS v) (F' v) (FS' v).

- : shift-varlevel/L2 (eql'/f2 ([v] [vl:varlevel' v (s N)] (F v vl)))
		      (eqlsize'/f2 FS)
                      (eql/f2 ([v] [vl:varlevel v (s N)] (F' v vl)))
		      (eqlsize/f2 FS')
    <- {v} {vl'} {vl} {vsb:varlevel-shifts-back vl' vl}
       shift-varlevel/L2 (F v vl') (FS v vl') (F' v vl) (FS' v vl).

- : shift-varlevel/L2 (eql'/v VL1 VL2) eqlsize'/v (eql/v VL1' VL2') eqlsize/v
    <- varlevel-shifts-back VL1 VL1'
    <- varlevel-shifts-back VL2 VL2'.

%worlds (blocksimple | shiftback) (shift-varlevel/L2 _ _ _ _).
%total (E)  (shift-varlevel/L2 E _ _ _).

Now we put these two parts in one that hides the alternative definitions.

%theorem shift-varlevel :
	forall* {N} {T1} {T2} {S}
	forall	{E: eql* (s N) T1 T2}
		{ES:eqlsize E S}
	exists	{E': eql* N T1 T2}
		{ES':eqlsize E' S}
	true.

- : shift-varlevel E1 ES1 E3 ES3
    <- shift-varlevel/L1 E1 ES1 E2 ES2
    <- shift-varlevel/L2 E2 ES2 E3 ES3.

%worlds (blocksimple) (shift-varlevel _ _ _ _).
%total { } (shift-varlevel _ _ _ _).

The following two theorems relate structural equality with identity based equality. One of them is called "Leibnitz" equality, I have heard, but apparently haven't remembered which one.

%theorem b-preserves-eq :
	forall* {T1} {T2}
	forall	{E:eq T1 T2}
	exists	{BE:eq (b T1) (b T2)}
	true.

- : b-preserves-eq eq/ eq/.

%worlds (blocksimple) (b-preserves-eq _ _).
%total { } (b-preserves-eq _ _).


%theorem f-preserves-eq :
	forall* {F1} {F2}
	forall {E:{v} eq (F1 v) (F2 v)}
	exists	{E:eq (f F1) (f F2)}
	true.

- : f-preserves-eq ([v] eq/) eq/.

%worlds (blocksimple) (f-preserves-eq _ _).
%total { } (f-preserves-eq _ _).

Next the main lemma that says we can avoid looking at varlevels in checking equality. We remove the outside variable, shift remaining variables, and then recurse (hence the need for tracking eqlsize). Note that we never put var levels in the context.

%theorem eql-implies-eq :
	forall* {T1} {T2}
	forall	{E:eql T1 T2}
	exists	{E':eq T1 T2}
	true.

%theorem eql-implies-eq/L :
	forall* {T1} {T2}
	forall	{E:eql T1 T2} 
		{S} {ES:eqlsize E S}
	exists	{E':eq T1 T2}
	true.

- : eql-implies-eq/L (eql/eq E) _ _ E.

- : eql-implies-eq/L (eql/b E1) _ (eqlsize/b ES) E'
    <- eql-implies-eq/L E1 _ ES E1'
    <- b-preserves-eq E1' E'.

- : eql-implies-eq/L (eql/f1 ([v] (E1 v))) _ (eqlsize/f1 FS) E'
    <- ({v} eql-implies-eq/L (E1 v) _ (FS v) (E1' v))
    <- f-preserves-eq E1' E'.

- : eql-implies-eq/L (eql/f2 ([v] [vl] (F1 v vl))) _ (eqlsize/f2 FS1) E'
    <- remove-one-var F1 FS1 ([v] (F2 v)) FS2
    <- ({v} shift-varlevel (F2 v) (FS2 v) (F3 v) (FS3 v))
    <- ({v} eql-implies-eq/L (F3 v) _ (FS3 v) (F4 v))
    <- f-preserves-eq F4 E'.

%worlds (blocksimple) (eql-implies-eq/L _ _ _ _).
%total (S) (eql-implies-eq/L _ S _ _).

- : eql-implies-eq E E'
    <- eqlsize-total ES
    <- eql-implies-eq/L E _ ES E'.

%worlds (blocksimple) (eql-implies-eq _ _).
%total { } (eql-implies-eq _ _).

Main Theorem

Finally the statement of the main theorem of this section. It is proved by using eql as a between station. In this case, we do have var levels in the context. This theorem (or rather its main lemma) uses reasoning-from-false extensively because the cases cannot be distinguished by Twelf's case analysis. It also uses the "divrem" part of the nat signature extensively as well as theorems about plus and times. The proofs of the cases are uninteresting arithmetic fiddling.

%theorem tonat-one2one :
	forall*	{T1} {N1} {T2} {N2}
	forall	{TN1:tonat T1 N1}
		{TN2:tonat T2 N2}
		{E:nat`eq N1 N2}
	exists	{ET:eq T1 T2}
	true.

%theorem tonat-one2one/L :
	forall*	{N} {T1} {M1} {T2} {M2}
	forall	{TN1:tonat* N T1 M1}
		{TN2:tonat* N T2 M2}
		{E:nat`eq M1 M2}
	exists	{ET:eql* N T1 T2}
	true.

- : tonat-one2one/L tonat/a tonat/a _ (eql/eq eq/).

- : tonat-one2one/L tonat/a (tonat/b _ _ N+1+TM=N) nat`eq/ E
    <- plus-swap-succ N+1+TM=N N+TM+1=N
    <- plus-commutative N+TM+1=N TM+1+N=N
    <- plus-implies-gt TM+1+N=N nat`eq/ N>N
    <- gt-anti-reflexive N>N F
    <- false-implies-eql F E.

- : tonat-one2one/L (tonat/b _ _ N+1+TM=N) tonat/a nat`eq/ E
    <- plus-swap-succ N+1+TM=N N+TM+1=N
    <- plus-commutative N+TM+1=N TM+1+N=N
    <- plus-implies-gt TM+1+N=N nat`eq/ N>N
    <- gt-anti-reflexive N>N F
    <- false-implies-eql F E.

- : tonat-one2one/L tonat/a (tonat/f _ _ N+2+TM=N) nat`eq/ E
    <- plus-swap-succ N+2+TM=N N+1+TM+1=N
    <- plus-swap-succ N+1+TM+1=N N+TM+2=N
    <- plus-commutative N+TM+2=N TM+2+N=N
    <- plus-implies-gt TM+2+N=N nat`eq/ N>N
    <- gt-anti-reflexive N>N F
    <- false-implies-eql F E.

- : tonat-one2one/L (tonat/f _ _ N+2+TM=N) tonat/a nat`eq/ E
    <- plus-swap-succ N+2+TM=N N+1+TM+1=N
    <- plus-swap-succ N+1+TM+1=N N+TM+2=N
    <- plus-commutative N+TM+2=N TM+2+N=N
    <- plus-implies-gt TM+2+N=N nat`eq/ N>N
    <- gt-anti-reflexive N>N F
    <- false-implies-eql F E.

- : tonat-one2one/L tonat/a (tonat/v VL N+L=N) nat`eq/ E
    <- plus-right-identity N N+0=N
    <- plus-left-cancels N+L=N N+0=N nat`eq/ nat`eq/ L=0
    <- varlevel-contradiction VL L=0 F
    <- false-implies-eql F E.

- : tonat-one2one/L (tonat/v VL N+L=N) tonat/a nat`eq/ E
    <- plus-right-identity N N+0=N
    <- plus-left-cancels N+L=N N+0=N nat`eq/ nat`eq/ L=0
    <- varlevel-contradiction VL L=0 F
    <- false-implies-eql F E.

- : tonat-one2one/L (tonat/b TN1 TWO*M1=TM1 N+1+TM1=M)
                    (tonat/b TN2 TWO*M2=TM2 N+1+TM2=M) nat`eq/ (eql/b E)
    <- plus-left-cancels N+1+TM1=M N+1+TM2=M nat`eq/ nat`eq/ TM1=TM2
    <- times-left-cancels TWO*M1=TM1 TWO*M2=TM2 nat`eq/ TM1=TM2 M1=M2
    <- tonat-one2one/L TN1 TN2 M1=M2 E.

- : tonat-one2one/L (tonat/b _ TWO*M1=TM1 N+1+TM1=M) 
                    (tonat/f _ TWO*M2=TM2 N+2+TM2=M)
                    nat`eq/ E
    <- plus-swap-succ N+2+TM2=M N+1+TM2+1=M
    <- plus-left-cancels N+1+TM1=M N+1+TM2+1=M nat`eq/ nat`eq/ TM1=TM2+1
    <- times-commutative TWO*M1=TM1 M1*2=TM1
    <- plus-right-identity _ TM1+0=TM1
    <- divrem-can-be-constructed M1*2=TM1 TM1+0=TM1 (gt/> gt/1) TM1/2=M1,0
    <- times-commutative TWO*M2=TM2 M2*2=TM2
    <- nat`eq-symmetric TM1=TM2+1 TM2+1=TM1
    <- plus-respects-eq (plus/s plus/z) nat`eq/ nat`eq/ TM2+1=TM1 ONE+TM2=TM1
    <- plus-commutative ONE+TM2=TM1 TM2+ONE=TM1
    <- divrem-can-be-constructed M2*2=TM2 TM2+ONE=TM1 gt/1 TM1/2=M2,1
    <- divrem-deterministic TM1/2=M1,0 TM1/2=M2,1 nat`eq/ nat`eq/ _ ZERO=ONE
    <- nat`eq-contradiction ZERO=ONE F
    <- false-implies-eql F E.

- : tonat-one2one/L (tonat/f _ TWO*M2=TM2 N+2+TM2=M)
                    (tonat/b _ TWO*M1=TM1 N+1+TM1=M) nat`eq/ E
    <- plus-swap-succ N+2+TM2=M N+1+TM2+1=M
    <- plus-left-cancels N+1+TM1=M N+1+TM2+1=M nat`eq/ nat`eq/ TM1=TM2+1
    <- times-commutative TWO*M1=TM1 M1*2=TM1
    <- plus-right-identity _ TM1+0=TM1
    <- divrem-can-be-constructed M1*2=TM1 TM1+0=TM1 (gt/> gt/1) TM1/2=M1,0
    <- times-commutative TWO*M2=TM2 M2*2=TM2
    <- nat`eq-symmetric TM1=TM2+1 TM2+1=TM1
    <- plus-respects-eq (plus/s plus/z) nat`eq/ nat`eq/ TM2+1=TM1 ONE+TM2=TM1
    <- plus-commutative ONE+TM2=TM1 TM2+ONE=TM1
    <- divrem-can-be-constructed M2*2=TM2 TM2+ONE=TM1 gt/1 TM1/2=M2,1
    <- divrem-deterministic TM1/2=M1,0 TM1/2=M2,1 nat`eq/ nat`eq/ _ ZERO=ONE
    <- nat`eq-contradiction ZERO=ONE F
    <- false-implies-eql F E.

- : tonat-one2one/L (tonat/b _ _ N+1+TM=M) (tonat/v _ M+L=N) nat`eq/ E
    <- plus-swap-succ N+1+TM=M N+TM+1=M
    <- plus-commutative N+TM+1=M TM+1+N=M
    <- plus-implies-gt TM+1+N=M nat`eq/ M>N
    <- plus-commutative M+L=N L+M=N
    <- plus-implies-ge L+M=N N>=M
    <- nat`gt-transitive-ge M>N N>=M M>M
    <- nat`gt-anti-reflexive M>M F
    <- false-implies-eql F E.

- : tonat-one2one/L (tonat/v _ M+L=N) (tonat/b _ _ N+1+TM=M) nat`eq/ E 
    <- plus-swap-succ N+1+TM=M N+TM+1=M
    <- plus-commutative N+TM+1=M TM+1+N=M
    <- plus-implies-gt TM+1+N=M nat`eq/ M>N
    <- plus-commutative M+L=N L+M=N
    <- plus-implies-ge L+M=N N>=M
    <- nat`gt-transitive-ge M>N N>=M M>M
    <- nat`gt-anti-reflexive M>M F
    <- false-implies-eql F E.

- : tonat-one2one/L (tonat/f ([v] [vl] (F1 v vl)) TWO*M1=TM1 N+2+TM1=M) 
                    (tonat/f ([v] [vl] (F2 v vl)) TWO*M2=TM2 N+2+TM2=M)
                    nat`eq/ (eql/f2 FE)
    <- plus-left-cancels N+2+TM1=M N+2+TM2=M nat`eq/ nat`eq/ TM1=TM2
    <- times-left-cancels TWO*M1=TM1 TWO*M2=TM2 nat`eq/ TM1=TM2 M1=M2
    <- ({v} {vl:varlevel v (s N)} 
        tonat-one2one/L (F1 v vl) (F2 v vl) M1=M2 (FE v vl)).

- : tonat-one2one/L (tonat/f _ _ N+2+TM=M) (tonat/v _ M+L=N) nat`eq/ E
    <- plus-swap-succ N+2+TM=M N+1+TM+1=M
    <- plus-swap-succ N+1+TM+1=M N+TM+2=M
    <- plus-commutative N+TM+2=M TM+2+N=M
    <- plus-implies-gt TM+2+N=M nat`eq/ M>N
    <- plus-commutative M+L=N L+M=N
    <- plus-implies-ge L+M=N N>=M
    <- nat`gt-transitive-ge M>N N>=M M>M
    <- nat`gt-anti-reflexive M>M F
    <- false-implies-eql F E.

- : tonat-one2one/L (tonat/v _ M+L=N) (tonat/f _ _ N+2+TM=M) nat`eq/ E 
    <- plus-swap-succ N+2+TM=M N+1+TM+1=M
    <- plus-swap-succ N+1+TM+1=M N+TM+2=M
    <- plus-commutative N+TM+2=M TM+2+N=M
    <- plus-implies-gt TM+2+N=M nat`eq/ M>N
    <- plus-commutative M+L=N L+M=N
    <- plus-implies-ge L+M=N N>=M
    <- nat`gt-transitive-ge M>N N>=M M>M
    <- nat`gt-anti-reflexive M>M F
    <- false-implies-eql F E.

- : tonat-one2one/L (tonat/v VL1 M+L1=N) (tonat/v VL2 M+L2=N) nat`eq/ 
		     (eql/v VL1' VL2)
    <- plus-left-cancels M+L1=N M+L2=N nat`eq/ nat`eq/ L1=L2
    <- varlevel-respects-eq VL1 L1=L2 VL1'.

%worlds (blockvar) (tonat-one2one/L _ _ _ _).
%total (T) (tonat-one2one/L T _ _ _).

- : tonat-one2one TN1 TN2 EQ TEQ
    <- tonat-one2one/L TN1 TN2 EQ EQL
    <- eql-implies-eq EQL TEQ.

%worlds () (tonat-one2one _ _ _ _).
%total { } (tonat-one2one _ _ _ _).