Indexed HOAS nat bijection

From The Twelf Project

Code: here
Status: %% OK %%
Output: here.

1 Bijection from indexed HOAS to natural numbers

Bijection from indexed HOAS to natural numbers

This file shows an *indexed* 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, natpair and multiset.

This file shows some of the extensions needed to handle indexed HOAS terms above and beyond those of "regular" HOAS terms (which is the topic of the [HOAS_nat_bijection] page). In the comments here, I emphasize those different aspects rather than repeat the same discussion.

Definitions

The syntax

Here we define multi-arity functions that are typed to avoid type errors (hence, no higher-order functions in the syntax -- but see "rec" which is the typed Y combinator). This syntax is rather impoverished, but it would be fairly easily to add "succ", "ifzero" terms. By "easy", I mean the addition would cause no new technical issues. It would still change al he arithmetic parts of the proofs dramatically. For this reason, I would like to implement a tool that would generate such proofs for any HOAS family of terms.

term : nat -> type.

%abbrev t = term z.


lit : nat -> t.

app : term (s N) -> t -> term N.

lam : (t -> term N) -> term (s N).

rec : (term (s N) -> term (s N)) -> term (s N).



%block blocksimple : some {n} block {v:term n}.

Equality

eq : term N1 -> term N2 -> type.


eq/ : eq T T.

Variable levels

As with the non-indexed case, a variable level is the (nonzero) natural number for a variable. But unlike before 'varlevel' is now an abbreviation for a more complex relation that permits adjustment of the index level.

varadjlevel : term N -> nat -> nat -> type.


%abbrev varlevel : term N -> nat -> type = [T] [L] varadjlevel T N L.


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

Mapping

The bijection from terms to nat is called "tonat". There is a separate mapping for each index, which makes sense becaue each index represents a different type. Unlike the non-indexed case, we need to handle an unbounded number of different types of variables, so we can't just pass one extra int, or even a fixed number of ints. Instead we need to pass a structure that represents an unbounded number of ints. We use `multiset' to represent this structure. The elements of the multiset represent the levels that came "before".

Another interesting aspect is that not all constructors for the indexed type are available for all indices. For instane `lit' is only for the 0-index and rec only for non-zero indices. On the other hand, `app' can occur for any index. Since the mapping is separate for every index, and the mapping must be one-to-one as well as onto, we must work carefully that every natural number is mapped onto exactly once. Variables are handled (as before) by reserving the first VN spots for variables, where (unlike before) VN depends on the index. Ignoring variables, `lit' takes the veen numbers and `app' takes the odd numbers for the 0-indexed terms. For the nonzero-indexed terms, app takes the odd numbers (of course) and lam and rec share the even numbers.

tonat* : {N} multiset -> term N -> nat -> type.

%abbrev tonat = tonat* _ multiset/0.


tonat/var : 
	count MS N VN ->
	varlevel V L ->
	plus M L VN ->
    tonat* N MS V M.
	
tonat/lit :
	count MS z VN ->
	times (s (s z)) M TM ->
	plus VN TM M' ->
    tonat* z MS (lit M) M'.

tonat/app :
	count MS N VN ->
	tonat* _ MS T1 M1 ->
        tonat* _ MS T2 M2 ->
        natpair`pair2nat (natpair/ M1 M2) M ->
	times (s (s z)) M TM ->
	plus VN (s TM) M' ->
    tonat* N MS (app T1 T2) M'.

tonat/lam :
	count MS (s N) VN ->
	count MS z ZN ->
	multiset`add MS z MS' ->
	({v:term z} (varlevel v (s ZN)) ->
         tonat* N MS' (F v) M) ->
	times (s (s (s (s z)))) M TM ->
	plus VN TM M' ->
    tonat* (s N) MS (lam F) M'.

tonat/rec :
	count MS (s N) VN ->
	multiset`add MS (s N) MS' ->
	({f} (varlevel f (s VN)) ->
         tonat* (s N) MS' (F f) M) ->
	times (s (s (s (s z)))) M TM ->
	plus VN (s (s TM)) M' ->
    tonat* (s N) MS (rec 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-eq :
	forall* {N1} {N2} {T1:term N1} {T2:term N2}
	forall	{F:void}
	exists	{EQ:eq T1 T2}
	true.

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


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

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


%theorem varlevel-respects-eq :
	forall* {N} {V:term N} {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} {MS} {T} {M}
	forall	{F:void}
	exists	{TN:tonat* N MS T M}
	true.

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


%theorem tonat-respects-eq :
	forall* {N1} {MS1} {T1} {M1}
		{N2} {MS2} {T2} {M2}
	forall	{TN1:tonat* N1 MS1 T1 M1}
		{EM: multiset`eq MS1 MS2}
		{ET: eq T1 T2}
		{EN: nat`eq M1 M2}
	exists	{TN2: tonat* N2 MS2 T2 M2}
	true.

- : tonat-respects-eq TN multiset`eq/ eq/ nat`eq/ TN.

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

Proof of totality of tonat

As with the non-indexed case, proving totality is surprisingly tricky. The problem is that when we get to a variable, we need to make sure that (1) the variable has a level associated with it and (2) the level is in the range 1..VN where VN is the number of variables of this index that have been seen in the context. Twelf's blocks are useful for (1) but not for (2) because there's no way to connect the context with the current nesting level.

For this proof, I generalized/extended the "case" technique to handle indexed variables. The proof is almost the same. The multisets add extra paremeters but the basic structure is the same.

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* : {N} term N -> bool -> type.

%abbrev israw = israw* _.

%abbrev rawvar = [T] israw T true.


israw/lit : israw (lit _) false.

israw/app : israw (app _ _) false.

israw/lam : israw (lam _) false.

israw/rec : israw (rec _) 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* : {N} multiset -> term N -> type.

%abbrev case = case* _.


case/lit : case _ (lit _).

case/app : case MS T1 -> case MS T2 -> case MS (app T1 T2).

case/lam :
	count MS z VN ->
	add MS z MS' ->
	({v} varlevel v (s VN) -> 
	 case MS' (F v)) -> 
    case MS (lam F).

case/rec :
	count MS (s N) VN ->
	multiset`add MS (s N) MS' ->
	({f} varlevel f (s VN) ->
	 case MS' (F f)) ->
    case* (s N) MS (rec F).

case/var : 
	count MS N VN ->
	varlevel V FL ->
	nat`ge VN FL -> 
    case* N MS V.

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

Theorems about auxiliary definitions

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

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

- : israw-total israw/lit.

- : israw-total israw/app.

- : israw-total israw/lam.

- : israw-total israw/rec.

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 : some {n} block {v:term n} {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. Unlike the one2one theorem (see later), we don't have to do extraordinary things to handle having multiple types. (Although we do need some extra lemmas to ahndle facts about multisets.)

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

- : var-gets-level ([f] [r] [i] (case/raw r)) MC GE
                   ([f] [fl] (case/var MC fl GE)).

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

- : var-gets-level ([f] [r] [i] (case/var MC VL GE)) _ _
                   ([f] [fl] (case/var MC VL GE)).

- : var-gets-level ([f] [r] [i] (case/lit: case MS (lit O))) _ _
                   ([f] [fl] (case/lit)).

- : var-gets-level ([f] [r] [i] (case/app (C1 f r i) (C2 f r i))) MC GE
                   ([f] [fl] (case/app (C1' f fl) (C2' f fl)))
    <- var-gets-level C1 MC GE C1'
    <- var-gets-level C2 MC GE C2'.

%theorem var-gets-level/L :
	forall* {MS} {N1} {FN1} {N2} {FN2} {MS'} {L1} {B}
	forall	{MC1: multiset`count MS N1 FN1}
		{MC2: multiset`count MS N2 FN2}
		{MA2: multiset`add MS N2 MS'}
		{GE: nat`ge FN1 L1}
		{EQ?: nat`eq? N1 N2 B}
	exists	{FN1'}
		{MC1': multiset`count MS' N1 FN1'}
		{GE': nat`ge FN1' L1}
	true.

- : var-gets-level/L MC _ MA FN>=L nat`eq?/yes _ MC' (ge/> FN+1>L)
    <- ge-implies-succ-gt FN>=L FN+1>L
    <- multiset`count-add-implies-count MC MA MC'.

- : var-gets-level/L MC1 _ MA2 GE (nat`eq?/no N1<>N2) _ MC1' GE
    <- multiset`add-preserves-count MC1 MA2 N1<>N2 MC1'.

%worlds () (var-gets-level/L _ _ _ _ _ _ _ _).
%total { } (var-gets-level/L _ _ _ _ _ _ _ _).

- : var-gets-level 
	([f] [r] [i] (case/lam MS^0=FN' MSU ([v] [vl] C v vl f r i))) MC GE
        ([f] [fl]    (case/lam MS^0=FN' MSU ([v] [vl] C' v vl f fl)))
    <- nat`eq?-total EQ?
    <- var-gets-level/L MC MS^0=FN' MSU GE EQ? _ MC' GE'
    <- ({v} {vl:varlevel v _} (var-gets-level (C v vl) MC' GE' (C' v vl))).

- : var-gets-level 
	([f] [r] [i] (case/rec MS^N'=FN' MSU ([f'] [fl'] (C f' fl' f r i))))
        MS^N=FN FN>=L 
        ([f] [fl] (case/rec MS^N'=FN' MSU ([f'] [fl'] (C' f' fl' f fl))))
    <- nat`eq?-total EQ?
    <- var-gets-level/L MS^N=FN MS^N'=FN' MSU FN>=L EQ? _ MS'^N=FN'' FN''>=L
    <- ({f'} {fl'} (var-gets-level (C f' fl') MS'^N=FN'' FN''>=L (C' f' fl'))).

%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 works almost the same as for non-indexed terms.

%theorem case-total* :
	forall* {N}
	forall	{T:term N}
	exists	{C:case multiset/0 T}
	true.

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

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

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

- : case-total/L _ _ (case/app C1 C2)
    <- israw-total I1
    <- case-total/L _ I1 C1
    <- israw-total I2
    <- case-total/L _ I2 C2.

- : case-total/L _ _ (case/lam MC MA ([f] [fl] (C' f fl)))
    <- multiset`count-total MC
    <- multiset`add-total MA
    <- ({v} {r:rawvar v} {i:israw-total r}
        israw-total (I v r i: israw _ B))
    <- ({v} {r:rawvar v} {i:israw-total r} 
        case-total/L _ (I v r i) (C v r i))
    <- multiset`count-add-implies-count MC MA MC'
    <- var-gets-level C MC' (nat`ge/= nat`eq/) C'.

- : case-total/L _ _ (case/rec MC MA ([f] [fl] (C' f fl)))
    <- multiset`count-total MC
    <- multiset`add-total MA
    <- ({v} {r:rawvar v} {i:israw-total r}
        israw-total (I v r i: israw _ B))
    <- ({v} {r:rawvar v} {i:israw-total r} 
        case-total/L _ (I v r i) (C v r i))
    <- multiset`count-add-implies-count MC MA MC'
    <- var-gets-level C MC' (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 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* {N}
	forall	{T:term N}
	exists	{M:nat} {D:tonat T M}
	true.

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

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

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

- : tonat-total/L (case/lit) _ (tonat/lit MC T P)
    <- count-total MC
    <- times-total T
    <- plus-total P.

- : tonat-total/L (case/app C1 C2) _ (tonat/app MC TN1 TN2 P2N T P)
    <- count-total MC
    <- tonat-total/L C1 _ TN1
    <- tonat-total/L C2 _ TN2
    <- pair2nat-total P2N
    <- times-total T
    <- plus-total P.

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

- : tonat-total/L (case/rec MC MA ([v] [vl] (C v vl))) _ 
                  (tonat/rec MC MA ([v] [vl] (TN v vl)) T P)
    <- ({v} {vl} 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

As with the non-indexed case, this aspect is easy to prove.

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* {N} {V:term N} {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* {N} {V:term N} {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* {N1} {N2} {T1:term N1} {T2:term N2} {M1} {M2}
	forall	{TN1:tonat T1 M1} 
		{TN2:tonat T2 M2}
		{E: eq T1 T2}
	exists	{E: nat`eq M1 M2}
	true.

%theorem tonat-deterministic/L :
	forall* {N} {T:term N} {MS1} {MS2} {M1} {M2}
	forall	{TN1:tonat* N MS1 T M1} 
		{TN2:tonat* N MS2 T M2}
		{E: multiset`eq MS1 MS2}
	exists	{E: nat`eq M1 M2}
	true.

- : tonat-deterministic/L (tonat/var MC1 VL1 P1) (tonat/var MC2 VL2 P2) _ N1=N2
    <- count-deterministic MC1 MC2 multiset`eq/ nat`eq/ C1=C2
    <- varlevel-deterministic VL1 VL2 L1=L2
    <- plus-right-cancels P1 P2 L1=L2 C1=C2 N1=N2.

- : tonat-deterministic/L (tonat/lit MC1 T1 P1) (tonat/lit MC2 T2 P2) _ M1'=M2'
    <- count-deterministic MC1 MC2 multiset`eq/ nat`eq/ C1=C2
    <- times-deterministic T1 T2 nat`eq/ nat`eq/ TM1=TM2
    <- plus-deterministic P1 P2 C1=C2 TM1=TM2 M1'=M2'.

- : tonat-deterministic/L (tonat/app MC1 TN1a TN1b P2N1 T1 P1) 
                          (tonat/app MC2 TN2a TN2b P2N2 T2 P2) MSE M1'=M2'
    <- count-deterministic MC1 MC2 multiset`eq/ nat`eq/ C1=C2
    <- tonat-deterministic/L TN1a TN2a MSE M1a=M2a
    <- tonat-deterministic/L TN1b TN2b MSE M1b=M2b
    <- natpair`pair-preserves-eq M1a=M2a M1b=M2b P1=P2
    <- pair2nat-deterministic P2N1 P2N2 P1=P2 M1=M2
    <- times-deterministic T1 T2 nat`eq/ M1=M2 TM1=TM2
    <- succ-deterministic TM1=TM2 TM1+1=TM2+1
    <- plus-deterministic P1 P2 C1=C2 TM1+1=TM2+1 M1'=M2'.

%theorem tonat-deterministic/L2 :
	forall* {N1} {N2} {M1} {M2} {MS} {F:term N1 -> term N2} {M}
	forall	{F1:{f:term N1} {fl:varlevel f (s M1)} 
                    tonat* N2 MS (F f) M}
		{ME: nat`eq M1 M2}
	exists	{F2:{f:term N1} {fl:varlevel f (s M2)}
		    tonat* N2 MS (F f) M}
	true.

- : tonat-deterministic/L2 F nat`eq/ F.

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

- : tonat-deterministic/L (tonat/lam MC1 MCz1 MA1 ([v] [vl] (TN1 v vl)) T1 P1)
                          (tonat/lam MC2 MCz2 MA2 ([v] [vl] (TN2 v vl)) T2 P2)
                          MS1=MS2 M1'=M2'
    <- multiset`count-deterministic MC1 MC2 MS1=MS2 nat`eq/ VN1=VN2
    <- multiset`count-deterministic MCz1 MCz2 MS1=MS2 nat`eq/ ZN1=ZN2
    <- multiset`add-deterministic MA1 MA2 MS1=MS2 nat`eq/ MS1'=MS2'
    <- tonat-deterministic/L2 TN1 ZN1=ZN2 TN1'
    <- ({v} {vl:varlevel v (s ZN2)} tonat-deterministic/L (TN1' v vl) (TN2 v vl)
                                                          MS1'=MS2' M1=M2)
    <- times-deterministic T1 T2 nat`eq/ M1=M2 TM1=TM2
    <- plus-deterministic P1 P2 VN1=VN2 TM1=TM2 M1'=M2'.

- : tonat-deterministic/L (tonat/rec MC1 MA1 ([f] [fl] (TN1 f fl)) T1 P1)
                          (tonat/rec MC2 MA2 ([f] [fl] (TN2 f fl)) T2 P2) 
                          MS1=MS2 M1'=M2'
    <- multiset`count-deterministic MC1 MC2 MS1=MS2 nat`eq/ FN1=FN2
    <- multiset`add-deterministic MA1 MA2 MS1=MS2 nat`eq/ MS1'=MS2'
    <- tonat-deterministic/L2 TN1 FN1=FN2 TN1'
    <- ({f} {fl:varlevel f (s N)} tonat-deterministic/L (TN1' f fl) (TN2 f fl)
                                                        MS1'=MS2' M1=M2)
    <- times-deterministic T1 T2 nat`eq/ M1=M2 TM1=TM2
    <- succ-deterministic TM1=TM2 TM1'=TM2'
    <- succ-deterministic TM1'=TM2' TM1''=TM2''
    <- plus-deterministic P1 P2 FN1=FN2 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 multiset`eq/ N1=N2.

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

Proving that the mapping is onto.

Again, this aspect has the same structure as with non-indexed terms.

Auxiliary definitions

We define a relation that builds on the context relation. In the non-indexed case, it took a nat, here it takes the multiset representing the levels of variables in the context.

upto : multiset -> type.


upto/0 : upto multiset/0.

upto/+ : 
	upto MS -> 
	multiset`count MS N FN ->
	varlevel (V:term N) (s FN) -> 
	multiset`add MS N MS' ->
    upto MS'.

Lemmas about regular definitions

%theorem term-inhabited :
	forall {N}
	exists {T:term N}
	true.

- : term-inhabited _ (lit z).

- : term-inhabited _ (lam ([x] T))
    <- term-inhabited _ T.

%worlds (blockvar) (term-inhabited _ _).
%total (N) (term-inhabited N _).

Theorems about auxiliary definitions

The obvious lemma that makes use of the main purpose of the relation: that a variable is always available.

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

- : upto-implies-varlevel upto/0 MC FN>L T FL
    <- count-empty-is-zero MC FN=0
    <- nat`gt-respects-eq FN>L FN=0 nat`eq/ ZERO>L 
    <- term-inhabited _ T
    <- nat`gt-contradiction ZERO>L F
    <- false-implies-varlevel F FL.

%theorem upto-implies-varlevel/L :
	forall* {MS1} {N1} {L} {FN1} {MS2} {N2} {FN2} {V1:term N1} {B}
	forall	{U: upto MS1}
		{MC1: multiset`count MS1 N1 FN1}
		{FL1: varlevel V1 (s FN1)}
		{MA: multiset`add MS1 N1 MS2}
		{MC2: multiset`count MS2 N2 FN2}
		{LT:nat`gt FN2 L}
		{EQ?: nat`eq? N1 N2 B}
	exists	{V:term N2} {VL:varlevel V (s L)}
	true.

- : upto-implies-varlevel/L _ MC1 FL1 MA MC2 (gt/1) nat`eq?/yes _ FL2
    <- count-add-implies-count MC1 MA MC2'
    <- count-deterministic MC2' MC2 multiset`eq/ nat`eq/ FN1+1=FN2+1
    <- varlevel-respects-eq FL1 FN1+1=FN2+1 FL2.

- : upto-implies-varlevel/L U MC1 FL1 MA MC2 (gt/> FN2>L) nat`eq?/yes _ FL2
    <- count-add-implies-count MC1 MA MC2'
    <- count-deterministic MC2 MC2' multiset`eq/ nat`eq/ FN2+1=FN1+1
    <- succ-cancels FN2+1=FN1+1 FN2=FN1
    <- gt-respects-eq FN2>L FN2=FN1 nat`eq/ FN1>L
    <- upto-implies-varlevel U MC1 FN1>L _ FL2.
 
- : upto-implies-varlevel/L U _ _ MA MC2 GT (nat`eq?/no N1<>N2) _ FL
    <- nat`ne-symmetric N1<>N2 N2<>N1
    <- add-preserves-count-converse MC2 MA N2<>N1 MC1
    <- upto-implies-varlevel U MC1 GT _ FL.

- : upto-implies-varlevel (upto/+ U MC1 FL1 MA) MC2 GT _ FL
    <- nat`eq?-total EQ?
    <- upto-implies-varlevel/L U MC1 FL1 MA MC2 GT EQ? _ FL.

%worlds (blockvar) (upto-implies-varlevel/L _ _ _ _ _ _ _ _ _)
                   (upto-implies-varlevel _ _ _ _ _).

%total (U V) (upto-implies-varlevel U _ _ _ _)
             (upto-implies-varlevel/L V _ _ _ _ _ _ _ _).

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}
	forall	{M:nat}
	exists	{T:term N} {TN:tonat T M}
	true.

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


%theorem tonat-onto/L :
	forall* {N} {MS:multiset}
	forall	{U:upto MS}
		{M:nat}
	exists	{T:term N} {TN:tonat* _ MS T M}
	true.

%theorem tonat-onto/L0 :
	forall* {N} {MS:multiset} {VN} {C}
	forall	{U:upto MS}
		{M:nat}
		{MC:count MS N VN}
		{CMP:nat`compare VN M C}
	exists	{T} {TN:tonat* N MS T M}
	true.

- : tonat-onto/L U M _ TN
    <- multiset`count-total MC
    <- nat`compare-total CMP
    <- tonat-onto/L0 U M MC CMP _ TN.

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

%theorem tonat-onto/L1 :
	forall*	{TM} {MS} {N} {VN}
	forall	{UF:upto MS}
		{M:nat}
		{MC:count MS N VN}
		{P:plus VN TM M}
		{Q} {R} {DR:divrem TM (s (s z)) Q R}
	exists	{T} {TN:tonat* N MS T M}
	true.

- : tonat-onto/L0 U M MC (compare/=) _ TN
    <- plus-right-identity _ P
    <- divrem-total M/2=Q,R
    <- tonat-onto/L1 U M MC P Q R M/2=Q,R _ TN.

- : tonat-onto/L0 U M MC (compare/< M>VN) _ TN
    <- gt-implies-plus M>VN _ Pc
    <- plus-commutative Pc P
    <- divrem-total M/2=Q,R
    <- tonat-onto/L1 U M MC P Q R M/2=Q,R _ TN.

- : tonat-onto/L1 _ _ _ _ _ (s (s _)) DR T TN
    <- divrem-contradiction DR (plus/s (plus/s plus/z)) F
    <- term-inhabited _ T
    <- false-implies-tonat F TN.

- : tonat-onto/L1 U M' MC VN+TM'=M' M (s z) TM'/2=M,1 
		  _ (tonat/app MC TN1 TN2 P2N TWO*M=TM VN+TM+1=M')
    <- plus-implies-ge VN+TM'=M' M'>=TM'
    <- 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
    <- plus-respects-eq VN+TM'=M' nat`eq/ TM'=TM+1 nat`eq/ VN+TM+1=M'
    <- nat2pair-total P2N
    <- quotient-of-nonzero-is-smaller TM'/2=M,1 TM'=TM+1 TM'>M
    <- nat`ge-transitive-gt M'>=TM' TM'>M M'>M
    <- nat2pair-implies-ge P2N M>=M1 M>=M2
    <- nat`gt-transitive-ge M'>M M>=M1 M'>M1
    <- nat`gt-transitive-ge M'>M M>=M2 M'>M2
    <- meta-gt _ _ M'>M1
    <- meta-gt _ _ M'>M2
    <- tonat-onto/L U M1 _ TN1
    <- tonat-onto/L U M2 _ TN2.

- : tonat-onto/L1 _ M' MC VN+TM=M' M z TM/2=M _ (tonat/lit MC TWO*M=TM VN+TM=M')
    <- div-can-be-inverted TM/2=M M*2=TM
    <- times-commutative M*2=TM TWO*M=TM.

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

- : tonat-onto/L1 U M' MC VN+FM=M' TM z FM/2=TM _ TN
    <- divrem-total TM/2=Q,R
    <- tonat-onto/L2 U M' MC VN+FM=M' FM/2=TM Q R TM/2=Q,R _ TN.

%abbrev 2*2=4 = (times/s (times/s times/z plus/z) (plus/s (plus/s plus/z))).

- : tonat-onto/L2 _ _ _ _ _ _ (s (s _)) DR T TN
    <- divrem-contradiction DR (plus/s (plus/s plus/z)) F
    <- term-inhabited _ T
    <- false-implies-tonat F TN.

- : tonat-onto/L2 U M' MC VN+FM'=M' FM'/2=TM' M (s z) TM'/2=M,1
		  _ (tonat/rec MC MA ([f] [fl] (TN f fl)) FOUR*M=FM VN+FM+2=M')
    <- divrem-can-be-inverted TM'/2=M,1 TM M*2=TM TM+ONE=TM'
    <- div-can-be-inverted FM'/2=TM' TM'*2=FM'
    <- times-total* TM (s (s z)) FM TM*2=FM 
    <- times-right-distributes-over-plus* 
	TM+ONE=TM' TM'*2=FM' TM*2=FM (times/s times/z plus/z) FM+TWO=FM'
    <- times-associative* M*2=TM TM*2=FM 2*2=4 M*4=FM
    <- times-commutative M*4=FM FOUR*M=FM
    <- plus-commutative (plus/s (plus/s plus/z)) FM+TWO=FM+2
    <- plus-deterministic FM+TWO=FM' FM+TWO=FM+2 nat`eq/ nat`eq/ FM'=FM+2
    <- plus-respects-eq VN+FM'=M' nat`eq/ FM'=FM+2 nat`eq/ VN+FM+2=M'
    <- plus-swap-succ-converse VN+FM+2=M' VN+1+FM+1=M'
    <- plus-swap-succ-converse VN+1+FM+1=M' VN+2+FM=M'
    <- multiset`add-total MA
    <- plus-implies-gt VN+2+FM=M' nat`eq/ M'>FM
    <- times-nonzero-implies-ge M*4=FM FM>=M
    <- nat`gt-transitive-ge M'>FM FM>=M M'>M
    <- meta-gt _ _ M'>M
    <- ({f} {fl} tonat-onto/L (upto/+ U MC fl MA) M _ (TN f fl)).

% 0 needs a special case for termination:

%theorem tonat-onto/0 :
	forall*	{MS}
	forall	{N} {U:upto MS} {VN}
		{MC:count MS N VN}
	exists	{T} {TN:tonat* N MS T z}
	true.

%abbrev 2*0=0 = (times/s (times/s times/z plus/z) plus/z).
%abbrev 4*0=0 = (times/s (times/s 2*0=0   plus/z) plus/z).

- : tonat-onto/0 _ U z MC _ (tonat/lit MC 2*0=0 plus/z).

- : tonat-onto/0 _ U z MC _ (tonat/lam MC MCz MA TN 4*0=0 plus/z)
    <- multiset`count-total MCz
    <- multiset`add-total MA
    <- multiset`count-total MC'
    <- ({v} {vl} (tonat-onto/0 _ (upto/+ U MCz vl MA) _ MC' _ (TN v vl))).

- : tonat-onto/0 N U (s VN-1) MC _ (tonat/var MC VL plus/z)
    <- upto-implies-varlevel U MC gt/1 _ VL.

%worlds (blockvar) (tonat-onto/0 _ _ _ _ _ _).
%total (N) (tonat-onto/0 N _ _ _ _ _).

- : tonat-onto/L2 U z MC _ _ _ _ _ _ TN
    <- tonat-onto/0 _ U _ MC _ TN.

%theorem tonat-onto/L2/L :
	forall* {M} {X} {Y} {Z} {XM}
	forall	{T:times M (s (s X)) XM}
		{P:plus Y XM (s Z)}
	exists	{G:gt (s Z) M}
	true.

- : tonat-onto/L2/L M*2=XM plus/z XM>M
    <- div-can-be-constructed M*2=XM XM/2=M
    <- quotient-of-nonzero-is-smaller XM/2=M nat`eq/ XM>M.

- : tonat-onto/L2/L M*2=XM Y+XM=X' X'>M
    <- plus-implies-gt Y+XM=X' nat`eq/ X'>MX
    <- times-nonzero-implies-ge M*2=XM XM>=M
    <- nat`gt-transitive-ge X'>MX XM>=M X'>M.

%worlds () (tonat-onto/L2/L _ _ _).
%total { } (tonat-onto/L2/L _ _ _).

- : tonat-onto/L2 U (s X) MC VN+FM=M' FM/2=TM M z TM/2=M
		  _ (tonat/lam MC MCz MA TN FOUR*M=FM VN+FM=M')
    <- div-can-be-inverted TM/2=M M*2=TM
    <- div-can-be-inverted FM/2=TM TM*2=FM
    <- times-associative* M*2=TM TM*2=FM 2*2=4 M*4=FM
    <- times-commutative M*4=FM FOUR*M=FM
    <- multiset`count-total MCz
    <- multiset`add-total MA
    <- tonat-onto/L2/L M*4=FM VN+FM=M' M'>M
    <- meta-gt (s X) M M'>M
    <- ({v} {vl} tonat-onto/L (upto/+ U MCz vl MA) _ _ (TN v vl)).

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

Proof that mapping is "one to one"

As with the simple HOAS syntax, this is the hardest of the four theorems to prove. As before, the basic structure is the same: we first show that the terms that result in the same number must be identical except that two variables may be equal just by having the same level.

As before we then 'chip' away at variables with low levels and shift the others down. We need to work at low levels because contexts cannot be parameterized by an 'N' and must be absolute. The additional problem with indexed terms is that the first variable we encounter may be of a higher-index than zero. In any case, there can be level 1 variables inside that have a different index than the one we are removing. So the context cannot simply assert that all variables will have level 2 or higher, as with did in the non-indexed case.

The basic idea is that we handle one index level at a time. But again because Twelf contexts cannot have be parameterized, we need to shift index levels down too. Of course, we cannot actually change index values. Instead, we keep a index-adjustment. Then a variable of index type (term N) has two parts to its level M L, where M+A=N and L is the original level. The multiset that keeps track of the next level is similarly shifted. We then do a shift such as we had for non-indexed terms while removing all variables of adjusted index zero (M = z). Then when these are all removed, we can adjust the indices one more step until there are no more variables of any index needing levels.

Auxiliary definitions

In this section, we use the full generality of varadjlevel because we need to recurse in two different directions: the original var level and the term level.

%block blockvaradj : some {m} {n} {l}
		      block {v:term n} {vl:varadjlevel v m (s l)}.

Equality (permitting variables with the same level).

Some variables are are bound with levels, others are not given levels. We do this in order to gradually squeeze out those that need levels. The lam1 and rec1 cases use variables that don't need levels, whereas the lam2, rec2 cases handle variables that still need level. We also take a natural number A that indicates the minimum term level that will be used. Notice that lam2 is only legal while A is still zero.

eql* : {N} {A:nat} multiset -> term N -> term N -> type.

%abbrev eql = eql* _.


eql/eq : eq T1 T2 -> eql A MS T1 T2.

eql/app : eql A MS F1 F2 -> eql A MS A1 A2 -> eql A MS (app F1 A1) (app F2 A2).

eql/lam1 : ({v} (eql A MS (F1 v) (F2 v))) -> eql A MS (lam F1) (lam F2).

eql/lam2 :
	count MS z VN -> 
	add MS z MS' -> 
	({v} {vl: varadjlevel v z (s VN)} eql z MS' (F1 v) (F2 v)) ->
    eql z MS (lam F1) (lam F2).

eql/rec1 : ({v} (eql A MS (F1 v) (F2 v))) -> eql A MS (rec F1) (rec F2).

eql/rec2 :
	plus A M (s N) ->
	count MS M VN ->
	add MS M MS' ->
	({v} {vl:varadjlevel v M (s VN)} eql A MS' (F1 v) (F2 v)) ->
    eql A MS (rec F1) (rec F2).

eql/var :
	plus A M N ->
	varadjlevel V1 M L -> 
	varadjlevel V2 M L -> 
    eql* N A MS V1 V2.

Measure of eql sizes.

We use this measure to be able to prove termination. We need eqlsize/var = eqlsize/eq, eqlsize/lam1 = eqlsize/lam2. (Less than is ok in each case but would require that we rephrase the lemmas.) We have three measures: N B M.

- N is the height of the term

- B is the minimum of any M for a varlevel (or (s z))

- M is greater than the M for any varlevel used.

The first measure is used to ensure that regular recursion through the tree terminates. We don't use normal structure recursion because everytime we change variable levels, the tree changes.

The second measure is not used for termination, but when non-zero means there are no variables with that need adjusted index zero. Once this is the case, we can adjust all levels down one notch.

The third measure is used to ensure that chipping away at indices eventually terminates: M is the maximum adjusted index used. Once M drops to zero, it means no variables need levels for equality and we can convert to an 'eq' proof easily.

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


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

eqlsize/app : 
	eqlsize E1 N1 B1 M1 ->
	eqlsize E2 N2 B2 M2 ->
	nat`max N1 N2 N ->
	nat`min B1 B2 B ->
	nat`max M1 M2 M ->
    eqlsize (eql/app E1 E2) (s N) B M.
	
eqlsize/lam1 : ({v} eqlsize (E v) N B M) -> eqlsize (eql/lam1 E) (s N) B M.

eqlsize/lam2 : 
	({v} {vl} eqlsize (E v vl) N B M) -> 
	nat`max (s z) M M' ->
    eqlsize (eql/lam2 _ _ E) (s N) z M'.

eqlsize/rec1 : ({v} eqlsize (E v) N B M) -> eqlsize (eql/rec1 E) (s N) B M.

eqlsize/rec2 : 
	({v} {vl:varadjlevel v M _} eqlsize (E v vl) N B1 M1) -> 
	nat`min M B1 B2 ->
	nat`max (s M) M1 M2 ->
    eqlsize (eql/rec2 _ _ _ E) (s N) B2 M2.

eqlsize/var : eqlsize (eql/var _ _ _) z (s z) z.

Copied definitions

As with the non-indexed case, we need to use an alternate form for levels as we shift them down or adjust them down. (Remember there are two dimensions to a level!)

varadjlevel' : term N -> nat -> nat -> type.


eql*' : {N} {A:nat} multiset -> term N -> term N -> type.

%abbrev eql' = eql*' _.


eql'/eq : eq T1 T2 -> eql' A MS T1 T2.

eql'/app : 
	eql' A MS F1 F2 -> 
	eql' A MS A1 A2 -> 
    eql' A MS (app F1 A1) (app F2 A2).

eql'/lam1 : ({v} (eql' A MS (F1 v) (F2 v))) -> eql' A MS (lam F1) (lam F2).

eql'/lam2 :
	count MS z VN -> 
	add MS z MS' -> 
	({v} {vl: varadjlevel' v z (s VN)} eql' z MS' (F1 v) (F2 v)) ->
    eql' z MS (lam F1) (lam F2).

eql'/rec1 : ({v} (eql' A MS (F1 v) (F2 v))) -> eql' A MS (rec F1) (rec F2).

eql'/rec2 :
	plus A M (s N) ->
	count MS M VN ->
	add MS M MS' ->
	({v} {vl:varadjlevel' v M (s VN)} eql' A MS' (F1 v) (F2 v)) ->
    eql' A MS (rec F1) (rec F2).

eql'/var :
	plus A M N ->
	varadjlevel' V1 M L -> 
	varadjlevel' V2 M L -> 
    eql*' N A MS V1 V2.



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


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

eqlsize'/app : 
	eqlsize' E1 N1 B1 M1 ->
	eqlsize' E2 N2 B2 M2 ->
	nat`max N1 N2 N ->
	nat`min B1 B2 B ->
	nat`max M1 M2 M ->
    eqlsize' (eql'/app E1 E2) (s N) B M.
	
eqlsize'/lam1 : ({v} eqlsize' (E v) N B M) -> eqlsize' (eql'/lam1 E) (s N) B M.

eqlsize'/lam2 : 
	({v} {vl} eqlsize' (E v vl) N B M1) -> 
	nat`max (s z) M1 M2 ->
    eqlsize' (eql'/lam2 _ _ E) (s N) z M2.

eqlsize'/rec1 : ({v} eqlsize' (E v) N B M) -> eqlsize' (eql'/rec1 E) (s N) B M.

eqlsize'/rec2 : 
	({v} {vl:varadjlevel' v M _} eqlsize' (E v vl) N B1 M1) -> 
	nat`min M B1 B2 ->
	nat`max (s M) M1 M2 ->
    eqlsize' (eql'/rec2 _ _ _ E) (s N) B2 M2.

eqlsize'/var : eqlsize' (eql'/var _ _ _) z (s z) z.

Theorems about auxiliary definitions

Some of the lemmas that would normally belong here are proved later when we have more blocks available.

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

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


%theorem false-implies-eqlsize :
	forall* {N} {A} {MS} {T1} {T2} {S} {B} {M}
		{E:eql* N A MS T1 T2}
	forall	{F:void}
	exists	{ES1:eqlsize E S B M}
	true.

%worlds (blocksimple | blockvaradj) (false-implies-eqlsize _ _).
%total { } (false-implies-eqlsize _ _).


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

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

- : eqlsize-total eqlsize/eq.

- : eqlsize-total (eqlsize/app S1 S2 M B M2)
    <- eqlsize-total S1
    <- eqlsize-total S2
    <- nat`max-total M
    <- nat`min-total B
    <- nat`max-total M2.

- : eqlsize-total (eqlsize/lam1 F)
    <- ({v} eqlsize-total (F v)).

- : eqlsize-total (eqlsize/lam2 F M)
    <- ({v} {vl} (eqlsize-total (F v vl)))
    <- nat`max-total M.

- : eqlsize-total (eqlsize/rec1 F)
    <- ({v} eqlsize-total (F v)).

- : eqlsize-total (eqlsize/rec2 F MN M)
    <- ({v} {vl} (eqlsize-total (F v vl)))
    <- nat`min-total MN
    <- nat`max-total M.

- : eqlsize-total eqlsize/var.

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

Shifting varlevels down

Now as with the non-indexed case, we shift variable levels down. As before, we need to use the alternate definitions.

The astute reader will notice that we don't have a block that just handles nonzero (adjusted) index variables being shifted over. Instead we handle a double context "noshift" that handles both directions. That's because when these lemmas are used to shift levels down, the outer context may have non-zero (adjusted) index that will need to handle being shifted in both directions.

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

%theorem varlevel-nonzero-shifts-over :
	forall* {N} {V:term N} {M} {L}
	forall	{VL:varadjlevel V (s M) (s L)}
	exists	{VL':varadjlevel' V (s M) (s L)}
	true.

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


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

%block noshift : some {l} {m} {n}
		  block {v:term n}
		  {vl:varadjlevel v (s m) (s l)}
		  {vl':varadjlevel' v (s m) (s l)}
		  {vsd:varlevel-nonzero-shifts-over vl vl'}
		  {vsd:varlevel-shifts-back vl' vl}.

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

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

%worlds (blocksimple | shiftdown | noshift) 
	(varlevel-zero-shifts-down _ _).
%worlds (blocksimple | shiftdown | noshift) 
	(varlevel-nonzero-shifts-over _ _).
%worlds (blocksimple | shiftback | noshift) 
        (varlevel-shifts-back _ _).

%total { } (varlevel-zero-shifts-down _ _).
%total { } (varlevel-nonzero-shifts-over _ _).
%total { } (varlevel-shifts-back _ _).



%theorem shift-varlevel/L1 :
	forall* {N} {A} {M0} {M1} {T1} {T2} {S} {MN} {MM}
	forall	{E: eql* N A M

Indexed HOAS nat bijection

From The Twelf Project

Contents

Bijection from indexed HOAS to natural numbers

Definitions

The syntax

Equality

Variable levels

Mapping

Utility lemmas

Proof of totality of tonat

Auxiliary definitions

raw variables

case analysis

Theorems about auxiliary definitions

Main theorem

Proof of the determinicity of the mapping

Auxiliary theorems

Main Theorem

Proving that the mapping is onto.

Auxiliary definitions

Lemmas about regular definitions

Theorems about auxiliary definitions

Main theorem

Proof that mapping is "one to one"

Auxiliary definitions

Equality (permitting variables with the same level).

Measure of eql sizes.

Copied definitions

Theorems about auxiliary definitions

Shifting varlevels down