Skip to content
STELF

Hereditary substitution for the STLC

You may wish to read the tutorial on admissibility of cut and/or the article on verifications and uses first.

In this tutorial, we recast the proof of cut admissibility as an algorithm for normalizing terms in the simply-typed λ-calculus. This algorithm is called hereditary substitution; it is used in the definition of LF itself, as well as in many other type theories. To apply hereditary substitution, it is necessary to:

  • Define a language of canonical forms. In programming language terms, canonical forms correspond to terms that are not β-reducible (beta-normal) and then are η-expanded as much as possible (eta-long); logically, canonical forms correspond to the cut-free sequent calculus proofs.
  • Define hereditary substitution, which computes the canonical result of substituting one canonical form into another. In programming language terms, hereditary substitution is part of a normalization algorithm; logically, it is the computational content of the proof of cut admissibility.
  • Define an eta-expansion judgement. In programming language terms, eta-expansion is part of a normalization algorithm; logically, it is the computational content of the identity theorem (Γ,A⇒A)(\Gamma,A \Rightarrow A).
  • Define an external language that admits non-canonical forms by elaboration into the canonical forms. In programming language terms, this elaboration relation corresponds to a normalization algorithm; logically, it is the computational content of the proof of cut elimination.

In this article, we formalize hereditary substitution and elaboration in STELF. We prove several results:

  • It is decidable whether or not a hereditary substitution exists. (This property is proved automatically by STELF.)
  • Under the appropriate typing conditions, hereditary substitutions exist and preserve types. Moreover, hereditary substitutions compute a unique result.
  • Eta-expansions exist, preserve types, and are unique.
  • All well-typed non-canonical forms elaborate to a canonical form of the same type.

This example brings together a number of STELF proof techniques:

The canonical forms language is described on this page; the external language and elaboration are described on the next page.

Experience report (DRL): This tutorial might seem like it takes a lot of STELF code. At the time I wrote this code, I was an experienced STELF user and familiar with the basic ideas of the canonical forms approach. However, I hadn’t gone through the details of these proofs before (that’s why I wrote the code). That said, it took no more than a work-day to work out and formalize the metatheory the canonical forms approach (everything on this page), and no more than another day to do the elaboration on the next page.

Canonical forms language: syntax and judgements

Section titled “Canonical forms language: syntax and judgements”

Syntax

Section titled “Syntax”

We consider a calculus with function and pair types, as well as a single base type:

tp : type.


b : tp.
arrow : tp -> tp -> tp.
prod : tp -> tp -> tp.


rtm : type.
mtm : type.


app : rtm -> mtm -> rtm.
c : rtm.
fst : rtm -> rtm.
snd : rtm -> rtm.


asm : rtm -> mtm.
lam : (rtm -> mtm) -> mtm.
pair : mtm -> mtm -> mtm.


%block rtm_block : block {x : rtm}.
%worlds (rtm_block) (tp) (rtm) (mtm).

The syntax of types is standard. There are a few subtleties in the syntax of terms:

  • The syntax of terms is stratified into atomic terms rtm and canonical terms mtm in order to syntactically prevent β-redices. For example, pairs are canonical but the argument of a projection (fst and snd) is atomic, so we can never project from a term that is syntactically a pair.
  • We name the syntactic classes rtm and mtm after the metavariables R and M that we will use to refer to them.
  • Because variables are considered to be atomic terms, the body of a lam binds a variable of type rtm. This means that the substitution operation that we get “for free” from the encoding is only the substitution of an rtm for a variable; hereditary substitution defines the substitution of an mtm for a variable.
  • The constant asm represents an injection from rtm into mtm.

Typing judgements

Section titled “Typing judgements”
atom : rtm -> tp -> type.
%mode atom +X1 -X2.


canon : mtm -> tp -> type.
%mode canon +X1 +X2.


% atomic


atom_c : atom c b.


atom_app : atom (app R1 M2) A
            <- atom R1 (arrow A2 A)
            <- canon M2 A2.


atom_fst : atom (fst R) A1
            <- atom R (prod A1 A2).


atom_snd : atom (snd R) A2
            <- atom R (prod A1 A2).


%% canonical


canon_asm : canon (asm R) b
             <- atom R b.


canon_lam : canon (lam M) (arrow A2 A)
             <- {x : rtm} (atom x A2) ->  canon (M x) A.


canon_pair : canon (pair M1 M2) (prod A1 A2)
              <- canon M1 A1
              <- canon M2 A2.


%block atom_block : some {A:tp}
                     block {x:rtm} {dx : atom x A}.
%worlds (atom_block) (atom _ _) (canon _ _).
%terminates (R M) (atom R _) (canon M _).

We define two mutually-recursive judgements, atom R A and canon M A. The typing judgements for the two syntactic categories have a bidirectional operational interpretation: an mtm is checked against a type, whereas an rtm synthesizes a type. The rules are the standard typing rules for the λ-calculus, modified to follow the restrictions of the syntax. Additionally, the rule canon_asm applies only at base type, which forces an mtm to be η-long.

These judgements are manifestly terminating, which we verify with the %terminates.

Hereditary substitution

Section titled “Hereditary substitution”

We define three hereditary substitution judgements:

  • hsubst_m M0 A0 ([x0] M) M': compute the canonical form M' of substituting M0 for x0 in M. A0 should be the type of M0; it is used to show that hereditary substitution is decidable.
  • hsubst_r M0 A0 ([x0] R) R': compute the atomic term R' resulting from substituting M0 for x0 in R. This judgement applies when x0 is not the head variable of the atomic term R.
  • hsubst_rr M0 A0 ([x0] R) M' A': compute a new canonical form term M' resulting from substituting M0 for x0 in R. This judgement applies when x0 is the head variable of R.

The head variable of an atomic term R is the variable at the root of a series of eliminations. E.g., the head of fst (app x c) is x. When a canonical form is substituted for a head variable, hereditary substitution continues reducing. E.g., the following judgement is derivable:

hsubst_rr
 (lam ([x] (pair c c)))
 (arrow b (prod b b))
 ([x] fst (app x c))
 c
 b

Intuitively, we substitute (lam ([x] (pair c c))) to get fst (app (lam ([x] (pair c c))) c) and then reduce this to c.

hsubst_rr also computes the type of the canonical form it produces, which is needed for the termination metric for hereditary substitution.

Here are the judgements:

hsubst_m : mtm -> tp -> (rtm -> mtm) -> mtm -> type.
%mode hsubst_m +X1 +X2 +X3 -X4.


hsubst_r : mtm -> tp -> (rtm -> rtm) -> rtm -> type.
%mode hsubst_r +X1 +X2 +X3 -X4.


hsubst_rr : mtm -> tp -> (rtm -> rtm) -> mtm -> tp -> type.
%mode hsubst_rr +X1 +X2 +X3 -X4 -X5.


%% Ms


hsubst_m_r : hsubst_m M0 A0 ([x] asm (R x)) (asm R')
              <- hsubst_r M0 A0 R R'.


hsubst_m_rr : hsubst_m M0 A0 ([x] asm (R x)) M'
               <- hsubst_rr M0 A0 R M' _.


hsubst_m_lam : hsubst_m M0 A0 ([x] (lam ([y] M x y))) (lam M')
                <- ({y:rtm}
                      hsubst_m M0 A0 ([x] M x y) (M' y)).


hsubst_m_pair : hsubst_m M0 A0 ([x] (pair (M1 x) (M2 x))) (pair M1' M2')
                 <- hsubst_m M0 A0 M1 M1'
                 <- hsubst_m M0 A0 M2 M2'.


%% R not head


hsubst_r_closed : hsubst_r M0 A0 ([x] E) E.


hsubst_r_app : hsubst_r M0 A0 ([x] (app (R x) (M x))) (app R' M')
                <- hsubst_r M0 A0 R R'
                <- hsubst_m M0 A0 M M'.


hsubst_r_fst : hsubst_r M0 A0 ([x] (fst (R x))) (fst R')
                <- hsubst_r M0 A0 R R'.


hsubst_r_snd : hsubst_r M0 A0 ([x] (snd (R x))) (snd R')
                <- hsubst_r M0 A0 R R'.


%% r head


hsubst_rr_var : hsubst_rr M0 A0 ([x] x) M0 A0.


hsubst_rr_app : hsubst_rr M0 A0 ([x] app (R1 x) (M2 x)) M'' A
                 <- hsubst_rr M0 A0 R1 (lam M') (arrow A2 A)
                 <- hsubst_m M0 A0 M2 M2'
                 <- hsubst_m M2' A2 M' M''.


hsubst_rr_fst : hsubst_rr M0 A0 ([x] (fst (R x))) M1' A1'
                 <- hsubst_rr M0 A0 R (pair M1' M2') (prod A1' A2').


hsubst_rr_snd : hsubst_rr M0 A0 ([x] (snd (R x))) M2' A2'
                 <- hsubst_rr M0 A0 R (pair M1' M2') (prod A1' A2').


%worlds (rtm_block) (hsubst_m _ _ _ _) (hsubst_r _ _ _ _) (hsubst_rr _ _ _ _ _).
%reduces A' <= A0 (hsubst_rr _ A0 _ _ A').
%terminates {(A0 A0' A0'') (M R R')} (hsubst_m _ A0 M _) (hsubst_r _ A0' R _) (hsubst_rr _ A0'' R' _ _).

The rule hsubst_r_closed is similar to a catch-all case: rather than putting cases of hereditary substitution into the LF context, we give a single rule that applies whenever the variable is not free in the term we are substituting into. This covers both the variables y:rtm in the context and the constant c, as well as any series of applications or projections made up from these terms—so the downside is that we have made hereditary substitution non-deterministic. However, keeping hereditary substitution out of the context simplifies some proofs below.

Other than that, the judgements hsubst_m and hsubst_r are defined in the straightforward compositional manner. The interesting judgement is hsubst_rr, which in each case performs some reduction on the output of the recursive call in order to compute a new canonical form. The most interesting rule is hsubst_rr_app, which continues the hereditary substitution into the body of the function.

When processing the %terminates declaration, STELF proves that it is decidable whether or not a hereditary substitution exists: the hereditary substitution judgements define a terminating logic program. The auxiliary %reduces proves that the result type of hsubst_rr is always a subterm of the type of the term being substituted for. This is true because hsubst_rr only applies when the cut variable is the head of a sequence of eliminations, and applying one of these elimination forms always decreases the type of the term. With this reduces information, we check that the hereditary substitution judgements terminate by mutual lexicographic induction—mutual because we show termination for all three judgements simultaneously, and lexicographic because, in each case, the termination metric is first the type of the substituted term, and then the term being substituted into. This metric is expressed in STELF by writing {(A0 A0' A0_) (M R R')}. The curly-braces mean lexicographic induction; the parentheses mean mutual induction.

Expansion

Section titled “Expansion”

Expansion shows that we can turn an atomic term of any type into a canonical term of that type. It is a total judgement defined by induction on the structure of the type:

expand : tp -> rtm -> mtm -> type.
%mode expand +X1 +X2 -X3.


expand_b : expand b R (asm R).


expand_arrow : expand (arrow A2 A) R (lam M)
                <- ({x : rtm} expand A2 x (M2 x))
                <- ({x : rtm} expand A (app R (M2 x)) (M x)).


expand_prod : expand (prod A1 A2) R (pair M1 M2)
               <- expand A1 (fst R) M1
               <- expand A2 (snd R) M2.


%worlds (rtm_block) (expand _ _ _).
%total A (expand A _ _).

In the expand_arrow case, we first expand a variable at the argument type, and then we expand the application at the result type.

Canonical forms language: Metatheory

Section titled “Canonical forms language: Metatheory”

Hereditary substitution

Section titled “Hereditary substitution”

Existence of hereditary substitution

Section titled “Existence of hereditary substitution”

Even though we annotated hsubst_rr with a %reduces above, we will need an effectiveness lemma version of this %reduces to use that fact in the proof below.

hsubst_rr_size : {A2} {A'} hsubst_rr M2 A2 R M' A'
                    -> type.
%mode hsubst_rr_size +X1 +X2 +X3.


- : hsubst_rr_size
     A2 A2 hsubst_rr_var.


- : hsubst_rr_size
     A2 A4 (hsubst_rr_app _ _ Drr)
     <- hsubst_rr_size A2 (arrow A3 A4) Drr.


- : hsubst_rr_size
     A2 Al (hsubst_rr_fst Drr)
     <- hsubst_rr_size A2 (prod Al Ar) Drr.


- : hsubst_rr_size
     A2 Ar (hsubst_rr_snd Drr)
     <- hsubst_rr_size A2 (prod Al Ar) Drr.


%worlds (rtm_block) (hsubst_rr_size _ _ _).
%total D (hsubst_rr_size _ _ D).
%reduces A' <= A2 (hsubst_rr_size A2 A' _).


 All the terms are inputs; the only output is the `%reduces`.


The main theorem proves that under the appropriate typing conditions, hereditary substitutions exist and preserve types.  For atomic terms, this means that one of the two kinds of hereditary substitutions exists.  Thus, we define the following sum type:


hsubst_r_exists_sum : mtm -> tp -> (rtm -> rtm) -> tp -> type.
hsubst_r_exists_sum_r : hsubst_r_exists_sum M2 A2 R A
                         <- hsubst_r M2 A2 R R'
                         <- atom R' A.
hsubst_r_exists_sum_rr : hsubst_r_exists_sum M2 A2 R A'
                          <- hsubst_rr M2 A2 R M' A'
                          <- canon M' A'.


 Because we are proving a theorem that concludes a disjunction, it should not be surprising that we need some [output factoring](/wiki/output-factoring/) lemmas.  The following lemmas may be proved independently:


hsubst_m_exists_asm :  hsubst_r_exists_sum M2 A2 R b
                       -> hsubst_m M2 A2 ([x] (asm (R x))) M'
                       -> canon M' b
                       -> type.
%mode hsubst_m_exists_asm +X1 -X2 -X3.


- : hsubst_m_exists_asm
     (hsubst_r_exists_sum_r DaR' DsR)
     (hsubst_m_r DsR)
     (canon_asm DaR').


- : hsubst_m_exists_asm
     (hsubst_r_exists_sum_rr DcM' DsR)
     (hsubst_m_rr DsR)
     DcM'.


%worlds (atom_block) (hsubst_m_exists_asm _ _ _).
%total {} (hsubst_m_exists_asm _ _ _).




hsubst_r_exists_fst : hsubst_r_exists_sum M2 A2 R (prod Al Ar)
                       -> hsubst_r_exists_sum M2 A2 ([x] (fst (R x))) Al
                       -> type.
%mode hsubst_r_exists_fst +X1 -X2.


- : hsubst_r_exists_fst
     (hsubst_r_exists_sum_r DaR' DsR)
     (hsubst_r_exists_sum_r (atom_fst DaR') (hsubst_r_fst DsR)).


- : hsubst_r_exists_fst
     (hsubst_r_exists_sum_rr (canon_pair _ DcMl') DsR)
     (hsubst_r_exists_sum_rr DcMl' (hsubst_rr_fst DsR)).


%worlds (atom_block) (hsubst_r_exists_fst _ _).
%total {} (hsubst_r_exists_fst _ _).




hsubst_r_exists_snd : hsubst_r_exists_sum M2 A2 R (prod Al Ar)
                       -> hsubst_r_exists_sum M2 A2 ([x] (snd (R x))) Ar
                       -> type.
%mode hsubst_r_exists_snd +X1 -X2.


- : hsubst_r_exists_snd
     (hsubst_r_exists_sum_r DaR' DsR)
     (hsubst_r_exists_sum_r (atom_snd DaR') (hsubst_r_snd DsR)).


- : hsubst_r_exists_snd
     (hsubst_r_exists_sum_rr (canon_pair DcMr' _) DsR)
     (hsubst_r_exists_sum_rr DcMr' (hsubst_rr_snd DsR)).


%worlds (atom_block) (hsubst_r_exists_snd _ _).
%total {} (hsubst_r_exists_snd _ _).


 Next, we prove the overall theorems, as well as a factoring lemma for application.  This last factoring lemma
must be in the mutually recursive loop with the main theorems because of the final premise of `hsubst_rr_app`, which continues the hereditary substitution.


hsubst_m_exists : {A2}
                   ({y : rtm} {dy : atom y A2} canon (M y) A)
                   -> canon M2 A2
                   -> hsubst_m M2 A2 M M'
                   -> canon M' A
                   -> type.
%mode hsubst_m_exists +X0 +X1 +X2 -X3 -X4.


hsubst_r_exists : {A2}
                   ({y : rtm} {dx : atom y A2} atom (R y) A)
                   -> canon M2 A2
                   -> hsubst_r_exists_sum M2 A2 R A
                   -> type.
%mode hsubst_r_exists +X0 +X1 +X2 -X3.


hsubst_m_exists_app : {A2}
                       %% this next argument is makes the termination argument work
                       ({y : rtm} {dx : atom y A2} atom (R1 y) (arrow A3 A4))
                       -> hsubst_r_exists_sum M2 A2 R1 (arrow A3 A4)
                       -> hsubst_m M2 A2 M3 M3'
                       -> canon M3' A3
                       -> hsubst_r_exists_sum M2 A2 ([x] (app (R1 x) (M3 x))) A4
                       -> type.
%mode hsubst_m_exists_app +X-1 +X0 +X1 +X2 +X3 -X4.


%% canonical terms


- : hsubst_m_exists
     A2
     ([x] [dx] canon_asm (DaR x dx))
     DcM2
     DsR
     DcM'
     <- hsubst_r_exists A2 DaR DcM2 Dsum
     <- hsubst_m_exists_asm Dsum DsR DcM'.


- : hsubst_m_exists
     A2
     ([x] [dx] (canon_lam ([y] [dy] DcM x dx y dy)) : canon (lam (M x)) (arrow Af At))
     (DcM2 : canon M2 A2)
     (hsubst_m_lam DsM)
     (canon_lam DcM')
     <- ({y}
           {dy : atom y Af}
           hsubst_m_exists A2 ([x] [dx] (DcM x dx y dy)) DcM2 (DsM y) (DcM' y dy)).


- : hsubst_m_exists
     A2
     ([x] [dx] (canon_pair (DcMr x dx) (DcMl x dx)))
     DcM2
     (hsubst_m_pair DsMr DsMl)
     (canon_pair DcMr' DcMl')
     <- hsubst_m_exists A2 DcMl DcM2 DsMl DcMl'
     <- hsubst_m_exists A2 DcMr DcM2 DsMr DcMr'.


%% atomic terms


- : hsubst_r_exists
     A2
     ([x] [dx] D)
     _
     (hsubst_r_exists_sum_r D hsubst_r_closed).


- : hsubst_r_exists
     A2
     ([x] [dx] dx)
     DcM2
     (hsubst_r_exists_sum_rr DcM2 hsubst_rr_var).


- : hsubst_r_exists
     A2
     ([x] [dx] (atom_app (DcM x dx) (DaR x dx)))
     DcM2
     DsumApp
     <- hsubst_m_exists A2 DcM DcM2 DsM' DcM'
     <- hsubst_r_exists A2 DaR DcM2 DsumR'
     <- hsubst_m_exists_app A2 DaR DsumR' DsM' DcM' DsumApp.


- : hsubst_r_exists
     A2
     ([x] [dx] (atom_fst (DcR x dx)))
     DcM2
     DsumFst
     <- hsubst_r_exists A2 DcR DcM2 DsumR
     <- hsubst_r_exists_fst DsumR DsumFst.


- : hsubst_r_exists
     A2
     ([x] [dx] (atom_snd (DcR x dx)))
     DcM2
     DsumSnd
     <- hsubst_r_exists A2 DcR DcM2 DsumR
     <- hsubst_r_exists_snd DsumR DsumSnd.


%% app factoring lemma


- : hsubst_m_exists_app
     A2
     _
     (hsubst_r_exists_sum_r DaR1 DsR1)
     DsM3
     DcM3
     (hsubst_r_exists_sum_r (atom_app DcM3 DaR1) (hsubst_r_app DsM3 DsR1)).


- : hsubst_m_exists_app
     A2
     _
     (hsubst_r_exists_sum_rr (canon_lam DcM4') DsR1)
     DsM3
     DcM3
     (hsubst_r_exists_sum_rr DcM4'' (hsubst_rr_app DsM4' DsM3 DsR1))
     <- hsubst_rr_size A2 (arrow A3 A4) DsR1
     <- hsubst_m_exists A3 DcM4' DcM3 DsM4' DcM4''.


%worlds (atom_block)
(hsubst_m_exists_app _ _ _ _ _ _)
(hsubst_r_exists _ _ _ _)
(hsubst_m_exists _ _ _ _ _).


%total {(A2 A2' A2'') (D  D' D'')}
(hsubst_m_exists A2' D' _ _ _)
(hsubst_m_exists_app A2'' D'' _ _ _ _)
(hsubst_r_exists A2 D _ _).

As you can see, the proof is a straightforward induction, where in each case we use the appropriate factoring lemma. In the final case of the application factoring lemma, we use the hsubst_rr_size lemma for its “side effect” of justifying the recursive call back to hsubst_m_exists. The mutual lexicographic termination metric is the same as before.

Uniqueness of hereditary substitution

Section titled “Uniqueness of hereditary substitution”

As usual for a uniqueness lemma, we must begin by defining the appropriate identity types:

id/mtm : mtm -> mtm -> type.
id/mtm_refl : id/mtm M M.


id/rtm : rtm -> rtm -> type.
id/rtm_refl : id/rtm R R.


id/tp : tp -> tp -> type.
id/tp_refl : id/tp A A.


 We elide the trivial proofs of the equivalence relation, congruence, inversion, and respects lemmas; see the complete STELF code at the end for their statements.


```stelf
id/rtm_sym : id/rtm R R'
        -> id/rtm R' R
        -> type.
%mode id/rtm_sym +X1 -X2.


- : id/rtm_sym id/rtm_refl id/rtm_refl.


%worlds (rtm_block) (id/rtm_sym _ _).
%total {} (id/rtm_sym _ _).


id/tp_arrow_inv : id/tp (arrow A1 A2) (arrow A1' A2')
       -> id/tp A1 A1'
       -> id/tp A2 A2'
       -> type.
%mode id/tp_arrow_inv +X1 -X2 -X3.


- : id/tp_arrow_inv _ id/tp_refl id/tp_refl.


%worlds (rtm_block) (id/tp_arrow_inv _ _ _).
%total {} (id/tp_arrow_inv _ _ _).


id/tp_prod_inv : id/tp (prod A1 A2) (prod A1' A2')
       -> id/tp A1 A1'
       -> id/tp A2 A2'
       -> type.
%mode id/tp_prod_inv +X1 -X2 -X3.


- : id/tp_prod_inv _ id/tp_refl id/tp_refl.


%worlds (rtm_block) (id/tp_prod_inv _ _ _).
%total {} (id/tp_prod_inv _ _ _).


id/rtm_app_cong : id/rtm R R'
       -> id/mtm M M'
       -> id/rtm (app R M) (app R' M')
       -> type.
%mode id/rtm_app_cong +X1 +X2 -X3.


- : id/rtm_app_cong _ _ id/rtm_refl.


%worlds (rtm_block) (id/rtm_app_cong _ _ _).
%total {} (id/rtm_app_cong _ _ _).


id/rtm_fst_cong : id/rtm R R'
       -> id/rtm (fst R) (fst R')
       -> type.
%mode id/rtm_fst_cong +X1  -X3.


- : id/rtm_fst_cong _ id/rtm_refl.


%worlds (rtm_block) (id/rtm_fst_cong _ _).
%total {} (id/rtm_fst_cong _ _).


id/rtm_snd_cong : id/rtm R R'
       -> id/rtm (snd R) (snd R')
       -> type.
%mode id/rtm_snd_cong +X1  -X3.


- : id/rtm_snd_cong _ id/rtm_refl.


%worlds (rtm_block) (id/rtm_snd_cong _ _).
%total {} (id/rtm_snd_cong _ _).


id/mtm_lam_cong :  ({x:rtm} id/mtm (M x) (M' x))
       -> id/mtm (lam M) (lam M')
       -> type.
%mode id/mtm_lam_cong +X1 -X3.


- : id/mtm_lam_cong _ id/mtm_refl.


%worlds (rtm_block) (id/mtm_lam_cong _ _).
%total {} (id/mtm_lam_cong _ _).


id/mtm_lam_inv :  id/mtm (lam M) (lam M')
      -> ({x:rtm} id/mtm (M x) (M' x))
      -> type.
%mode id/mtm_lam_inv +X1 -X3.


- : id/mtm_lam_inv _ ([_] id/mtm_refl).


%worlds (rtm_block) (id/mtm_lam_inv _ _).
%total {} (id/mtm_lam_inv _ _).


id/mtm_pair_cong : id/mtm M1 M1'
       -> id/mtm M2 M2'
       -> id/mtm (pair M1 M2) (pair M1' M2')
       -> type.
%mode id/mtm_pair_cong +X1 +X2 -X3.


- : id/mtm_pair_cong _ _ id/mtm_refl.


%worlds (rtm_block) (id/mtm_pair_cong _ _ _).
%total {} (id/mtm_pair_cong _ _ _).


id/mtm_pair_inv : id/mtm (pair M1 M2) (pair M1' M2')
       -> id/mtm M1 M1'
       -> id/mtm M2 M2'
       -> type.
%mode id/mtm_pair_inv +X1 -X2 -X3.


- : id/mtm_pair_inv _ id/mtm_refl id/mtm_refl.


%worlds (rtm_block) (id/mtm_pair_inv _ _ _).
%total {} (id/mtm_pair_inv _ _ _).


expand_respects_id : id/rtm R R'
          -> id/mtm M M'
          -> expand A R M
          -> expand A R' M'
          -> type.
%mode expand_respects_id +X1 +X2 +X3 -X4.


- : expand_respects_id _ _ D D.


%worlds (rtm_block) (expand_respects_id _ _ _ _).
%total {} (expand_respects_id _ _ _ _).
%reduces D1 = D2 (expand_respects_id _ _ D2 D1).


canon_respects_id :  id/mtm M M'
         -> id/tp A A'
         -> canon M A
         -> canon M' A'
         -> type.
%mode canon_respects_id +X1 +X2 +X3 -X4.


- : canon_respects_id _ _ D D.


%worlds (atom_block) (canon_respects_id _ _ _ _).
%total {} (canon_respects_id _ _ _ _).
%reduces D1 = D2 (canon_respects_id _ _ D2 D1).


hsubst_m_respects_id : id/mtm M2 M2'
      -> id/tp A2 A2'
      -> ({x} id/mtm (M x) (M' x))
      -> hsubst_m M2 A2 M Ms
      -> hsubst_m M2' A2' M' Ms
      -> type.
%mode hsubst_m_respects_id +X1 +X2 +X3 +X4 -X5.


- : hsubst_m_respects_id _ _ _ D D.


%worlds (rtm_block) (hsubst_m_respects_id _ _ _ _ _).
%total {} (hsubst_m_respects_id _ _ _ _ _).
%reduces D1 = D2 (hsubst_m_respects_id _ _ _ D2 D1).


id/mtm_asm_cong : id/rtm R R'
       -> id/mtm (asm R) (asm R')
       -> type.
%mode id/mtm_asm_cong +X1  -X3.


- : id/mtm_asm_cong _ id/mtm_refl.


%worlds (rtm_block) (id/mtm_asm_cong _ _).
%total {} (id/mtm_asm_cong _ _).

The hardest part of proving uniqueness of hereditary substitution is proving that the rules hsubst_m_r and hsubst_m_rr are mutually exclusive. We do by using reasoning with contradiction.

false : type.
%freeze false.

First, we prove that hsubst_rr is never inhabited when the variable is not free in the term being substituted into:

hsubst_rr_closed_contra : hsubst_rr M2 A2 ([_] R) M' A'
                           -> false
                           -> type.
%mode hsubst_rr_closed_contra +X1 -X2.


- : hsubst_rr_closed_contra
     (hsubst_rr_app _ _ Dr)
     X
     <- hsubst_rr_closed_contra Dr X.


- : hsubst_rr_closed_contra
     (hsubst_rr_fst D)
     X
     <- hsubst_rr_closed_contra D X.


- : hsubst_rr_closed_contra
     (hsubst_rr_snd D)
     X
     <- hsubst_rr_closed_contra D X.


%worlds (rtm_block) (hsubst_rr_closed_contra _ _).
%total D (hsubst_rr_closed_contra D _).


 This is an example of deriving a contradiction by induction—the coverage checker rules out all the base cases.


Next, we show that the two atomic term judgements are exclusive.  In the only base case that is not ruled out by coverage checking, we use the previous lemma.


%% contradiction of root and non-root


hsubst_r_rr_contra : hsubst_r M2 A2 R R'
                      -> hsubst_rr M2 A2 R M' A'
                      -> false
                      -> type.
%mode hsubst_r_rr_contra +X1 +X2 -X3.


- : hsubst_r_rr_contra
     hsubst_r_closed
     Drr
     X
     <- hsubst_rr_closed_contra Drr X.


- : hsubst_r_rr_contra
     (hsubst_r_app _ DsrR)
     (hsubst_rr_app _ _ DsrrR)
     X
     <- hsubst_r_rr_contra DsrR DsrrR X.


- : hsubst_r_rr_contra
     (hsubst_r_fst DsrR)
     (hsubst_rr_fst DsrrR)
     X
     <- hsubst_r_rr_contra DsrR DsrrR X.


- : hsubst_r_rr_contra
     (hsubst_r_snd DsrR)
     (hsubst_rr_snd DsrrR)
     X
     <- hsubst_r_rr_contra DsrR DsrrR X.


%worlds (rtm_block) (hsubst_r_rr_contra _ _ _). %% bar in extra block for lemma below's future use
%total (D) (hsubst_r_rr_contra D _ _).

Next, we write a little lemma showing that false implies any identity that we need.

%% false implies id
false_implies_id/mtm : {M} {M'}
                        false
                        -> id/mtm M M'
                        -> type.
%mode false_implies_id/mtm +X1 +X2 +X3 -X4.
%worlds (rtm_block) (false_implies_id/mtm _ _ _ _). %% bar in extra block for lemma below's future use
%total {} (false_implies_id/mtm _ _ _ _).


 The cost of defining hereditary substitution in a non-deterministic manner, which we did to avoid putting cases of hereditary substitution in the context, is that we now need to prove the following lemmas.  These lemmas establish that any way of deriving a hereditary substitution for a closed term produces the same result as `hsubst_r_closed`.


hsubst_r_vacuous_id : hsubst_r M2 A2 ([_] R) R'
                     -> id/rtm R' R
                     -> type.
%mode hsubst_r_vacuous_id +X1 -X2.


hsubst_m_vacuous_id : hsubst_m M2 A2 ([_] M) M'
                     -> id/mtm M' M
                     -> type.
%mode hsubst_m_vacuous_id +X1 -X2.


%% R


- : hsubst_r_vacuous_id hsubst_r_closed id/rtm_refl.


- : hsubst_r_vacuous_id (hsubst_r_app Dm Dr) Did'
     <- hsubst_r_vacuous_id Dr DidR
     <- hsubst_m_vacuous_id Dm DidM
     <- id/rtm_app_cong DidR DidM Did'.


- : hsubst_r_vacuous_id (hsubst_r_fst D) Did'
     <- hsubst_r_vacuous_id D Did
     <- id/rtm_fst_cong Did Did'.


- : hsubst_r_vacuous_id (hsubst_r_snd D) Did'
     <- hsubst_r_vacuous_id D Did
     <- id/rtm_snd_cong Did Did'.


%% M


- : hsubst_m_vacuous_id
     (hsubst_m_r Dr)
     Did'
     <- hsubst_r_vacuous_id Dr Did
     <- id/mtm_asm_cong Did Did'.


- : hsubst_m_vacuous_id
     (hsubst_m_rr D)
     Did
     <- hsubst_rr_closed_contra D X
     <- false_implies_id/mtm _ _ X Did.


- : hsubst_m_vacuous_id
     (hsubst_m_lam D)
     Did'
     <- ({x}
           hsubst_m_vacuous_id (D x) (Did x))
     <- id/mtm_lam_cong Did Did'.


- : hsubst_m_vacuous_id
     (hsubst_m_pair D2 D1)
     Did'
     <- hsubst_m_vacuous_id D1 Did1
     <- hsubst_m_vacuous_id D2 Did2
     <- id/mtm_pair_cong Did1 Did2 Did'.


%worlds (rtm_block) (hsubst_r_vacuous_id _ _) (hsubst_m_vacuous_id _ _).
%total (D1 D2)
(hsubst_r_vacuous_id D1 _)
(hsubst_m_vacuous_id D2 _).


 Now, we prove the top-level results:


hsubst_m_unique : hsubst_m M2 A2 M M'
                   -> hsubst_m M2 A2 M M''
                   -> id/mtm M' M''
                   -> type.
%mode hsubst_m_unique +X1 +X2 -X3.


hsubst_r_unique : hsubst_r M2 A2 R R'
                   -> hsubst_r M2 A2 R R''
                   -> id/rtm R' R''
                   -> type.
%mode hsubst_r_unique +X1 +X2 -X3.


hsubst_rr_unique : hsubst_rr M2 A2 R M' A'
                    -> hsubst_rr M2 A2 R M'' A''
                    -> id/mtm M' M''
                    -> id/tp A' A''
                    -> type.
%mode hsubst_rr_unique +X1 +X2 -X3 -X4.


%% M


- : hsubst_m_unique
     (hsubst_m_r Dsr)
     (hsubst_m_r Dsr')
     DidAsm
     <- hsubst_r_unique Dsr Dsr' DidR
     <- id/mtm_asm_cong DidR DidAsm.


- : hsubst_m_unique
     (hsubst_m_rr Dsr)
     (hsubst_m_rr Dsr')
     Did
     <- hsubst_rr_unique Dsr Dsr' Did _.


%% contradict mismatch
- : hsubst_m_unique
     (hsubst_m_r Dsr)
     (hsubst_m_rr Dsrr)
     Did
     <- hsubst_r_rr_contra Dsr Dsrr X
     <- false_implies_id/mtm _ _ X Did.


%% contradict mismatch
- : hsubst_m_unique
     (hsubst_m_rr Dsrr)
     (hsubst_m_r Dsr)
     Did
     <- hsubst_r_rr_contra Dsr Dsrr X
     <- false_implies_id/mtm _ _ X Did.


- : hsubst_m_unique
     (hsubst_m_pair DsRight DsLeft)
     (hsubst_m_pair DsRight' DsLeft')
     DidPair
     <- hsubst_m_unique DsLeft DsLeft' DidLeft
     <- hsubst_m_unique DsRight DsRight' DidRight
     <- id/mtm_pair_cong DidLeft DidRight DidPair.


- : hsubst_m_unique
     (hsubst_m_lam Ds)
     (hsubst_m_lam Ds')
     DidLam
     <- ({y:rtm} hsubst_m_unique (Ds y) (Ds' y) (Did y))
     <- id/mtm_lam_cong Did DidLam.


%% R non-root


- : hsubst_r_unique D D id/rtm_refl.


- : hsubst_r_unique
     (hsubst_r_closed : hsubst_r M2 A2 ([_] R) R)
     (D : hsubst_r M2 A2 ([_] R) R')
     Did'
     <- hsubst_r_vacuous_id D Did
     <- id/rtm_sym Did Did'.


- : hsubst_r_unique
     (D : hsubst_r M2 A2 ([_] R) R')
     (hsubst_r_closed : hsubst_r M2 A2 ([_] R) R)
     Did
     <- hsubst_r_vacuous_id D Did.


- : hsubst_r_unique
     (hsubst_r_app DsM' DsR')
     (hsubst_r_app DsM'' DsR'')
     DidApp
     <- hsubst_r_unique DsR' DsR'' DidR
     <- hsubst_m_unique DsM' DsM'' DidM
     <- id/rtm_app_cong DidR DidM DidApp.


- : hsubst_r_unique
     (hsubst_r_fst DsR')
     (hsubst_r_fst DsR'')
     DidFst
     <- hsubst_r_unique DsR' DsR'' DidR
     <- id/rtm_fst_cong DidR DidFst.
- : hsubst_r_unique
     (hsubst_r_snd DsR')
     (hsubst_r_snd DsR'')
     DidSnd
     <- hsubst_r_unique DsR' DsR'' DidR
     <- id/rtm_snd_cong DidR DidSnd.


%% R root


- : hsubst_rr_unique
     hsubst_rr_var
     hsubst_rr_var
     id/mtm_refl
     id/tp_refl.


- : hsubst_rr_unique
     (hsubst_rr_app DsM4' DsM3 DsR1)
     (hsubst_rr_app DsM4'-2 DsM3-2 DsR1-2)
     DidM4''
     DidA4
     <- hsubst_rr_unique DsR1 DsR1-2 DidLam DidArrow
     <- hsubst_m_unique DsM3 DsM3-2 DidM3'
     <- id/tp_arrow_inv DidArrow DidA3 DidA4
     <- id/mtm_lam_inv DidLam DidM4'
     <- hsubst_m_respects_id DidM3' DidA3 DidM4' DsM4' DsM4'-1
     <- hsubst_m_unique DsM4'-1 DsM4'-2 DidM4''.


- : hsubst_rr_unique
     (hsubst_rr_fst DsR')
     (hsubst_rr_fst DsR'')
     DidMl
     DidAl
     <- hsubst_rr_unique DsR' DsR'' DidPair DidProd
     <- id/tp_prod_inv DidProd DidAl _
     <- id/mtm_pair_inv DidPair DidMl _.


- : hsubst_rr_unique
     (hsubst_rr_snd DsR')
     (hsubst_rr_snd DsR'')
     DidMr
     DidAr
     <- hsubst_rr_unique DsR' DsR'' DidPair DidProd
     <- id/tp_prod_inv DidProd _ DidAr
     <- id/mtm_pair_inv DidPair _ DidMr.


%worlds (rtm_block)
(hsubst_m_unique _ _ _)
(hsubst_r_unique _ _ _)
(hsubst_rr_unique _ _ _ _).


%total (D1 D2 D3)
(hsubst_r_unique D2 _ _)
(hsubst_rr_unique D3 _ _ _)
(hsubst_m_unique D1 _ _).

Expansion

Section titled “Expansion”

Existence of expansion

Section titled “Existence of expansion”

This lemma is in part an effectiveness lemma for expansion, but it also shows that expansion preserves types.

expand_exists : {A}
                 atom R A
                 -> expand A R M
                 -> canon M A
                 -> type.
%mode expand_exists +X0 +X1 -X2 -X3.


- : expand_exists
     b
     D
     expand_b
     (canon_asm D).


- : expand_exists
     (arrow A2 A)
     DaR
     (expand_arrow DeApp DeX)
     (canon_lam DcApp)
     <- ({x : rtm}
           {dx : atom x A2}
           expand_exists A2 dx (DeX x) (DcM x dx))
     <- ({x : rtm}
           {dx : atom x A2}
           expand_exists A (atom_app (DcM x dx) DaR) (DeApp x) (DcApp x dx)).


- : expand_exists
     (prod A1 A2)
     DaR
     (expand_prod DeS DeF)
     (canon_pair DcS DcF)
     <- expand_exists A1 (atom_fst DaR) DeF DcF
     <- expand_exists A2 (atom_snd DaR) DeS DcS.


%worlds (atom_block) (expand_exists _ _ _ _).
%total D (expand_exists D _ _ _).

Uniqueness of expansion

Section titled “Uniqueness of expansion”

Uniqueness is proved by a straightforward induction using some identity lemmas:

expand_unique : expand A R M
                 -> expand A R M'
                 -> id/mtm M M'
                 -> type.
%mode expand_unique +X1 +X2 -X3.


- : expand_unique
     expand_b
     expand_b
     id/mtm_refl.


- : expand_unique
     (expand_arrow
        (DeApp : {x : rtm} expand A (app R (Mx x)) (MApp x))
        (DeX : {x : rtm} expand A2 x (Mx x)))
      (expand_arrow
         (DeApp' : {x : rtm} expand A (app R (Mx' x)) (MApp' x))
         (DeX' : {x : rtm} expand A2 x (Mx' x)))
     DidLam
     <- ({x : rtm}
           expand_unique (DeX x) (DeX' x) (DidX x))
     <- ({x : rtm}
           id/rtm_app_cong (id/rtm_refl : id/rtm R R) (DidX x) (DidApp x))
     <- ({x : rtm}
           expand_respects_id (DidApp x) id/mtm_refl (DeApp x) (DeApp-2 x))
     <- ({x : rtm}
           expand_unique (DeApp-2 x) (DeApp' x) (DidAppExp x))
     <- id/mtm_lam_cong DidAppExp DidLam.


- : expand_unique
     (expand_prod DeS DeF)
     (expand_prod DeS' DeF')
     DidPair
     <- expand_unique DeF DeF' DidF
     <- expand_unique DeS DeS' DidS
     <- id/mtm_pair_cong DidF DidS DidPair.


%worlds (rtm_block) (expand_unique _ _ _).
%total D (expand_unique _ D _).

Elaboration

Section titled “Elaboration”

In part 2, we discuss elaboration.

The complete STELF code for this tutorial contains the identity lemmas that we elided above.

This is part 2 of the case study Hereditary substitution for the STLC.

tp : type.


b : tp.
arrow : tp -> tp -> tp.
prod : tp -> tp -> tp.


rtm : type.
mtm : type.


app : rtm -> mtm -> rtm.
c : rtm.
fst : rtm -> rtm.
snd : rtm -> rtm.


asm : rtm -> mtm.
lam : (rtm -> mtm) -> mtm.
pair : mtm -> mtm -> mtm.


%block rtm_block : block {x : rtm}.
%worlds (rtm_block) (tp) (rtm) (mtm).


atom : rtm -> tp -> type.
%mode atom +X1 -X2.


canon : mtm -> tp -> type.
%mode canon +X1 +X2.


% atomic


atom_c : atom c b.


atom_app : atom (app R1 M2) A
            <- atom R1 (arrow A2 A)
            <- canon M2 A2.


atom_fst : atom (fst R) A1
            <- atom R (prod A1 A2).


atom_snd : atom (snd R) A2
            <- atom R (prod A1 A2).


%% canonical


canon_asm : canon (asm R) b
             <- atom R b.


canon_lam : canon (lam M) (arrow A2 A)
             <- {x : rtm} (atom x A2) ->  canon (M x) A.


canon_pair : canon (pair M1 M2) (prod A1 A2)
              <- canon M1 A1
              <- canon M2 A2.


%block atom_block : some {A:tp}
                     block {x:rtm} {dx : atom x A}.
%worlds (atom_block) (atom _ _) (canon _ _).
%terminates (R M) (atom R _) (canon M _).


hsubst_m : mtm -> tp -> (rtm -> mtm) -> mtm -> type.
%mode hsubst_m +X1 +X2 +X3 -X4.


hsubst_r : mtm -> tp -> (rtm -> rtm) -> rtm -> type.
%mode hsubst_r +X1 +X2 +X3 -X4.


hsubst_rr : mtm -> tp -> (rtm -> rtm) -> mtm -> tp -> type.
%mode hsubst_rr +X1 +X2 +X3 -X4 -X5.


%% Ms


hsubst_m_r : hsubst_m M0 A0 ([x] asm (R x)) (asm R')
              <- hsubst_r M0 A0 R R'.


hsubst_m_rr : hsubst_m M0 A0 ([x] asm (R x)) M'
               <- hsubst_rr M0 A0 R M' _.


hsubst_m_lam : hsubst_m M0 A0 ([x] (lam ([y] M x y))) (lam M')
                <- ({y:rtm}
                      hsubst_m M0 A0 ([x] M x y) (M' y)).


hsubst_m_pair : hsubst_m M0 A0 ([x] (pair (M1 x) (M2 x))) (pair M1' M2')
                 <- hsubst_m M0 A0 M1 M1'
                 <- hsubst_m M0 A0 M2 M2'.


%% R not head


hsubst_r_closed : hsubst_r M0 A0 ([x] E) E.


hsubst_r_app : hsubst_r M0 A0 ([x] (app (R x) (M x))) (app R' M')
                <- hsubst_r M0 A0 R R'
                <- hsubst_m M0 A0 M M'.


hsubst_r_fst : hsubst_r M0 A0 ([x] (fst (R x))) (fst R')
                <- hsubst_r M0 A0 R R'.


hsubst_r_snd : hsubst_r M0 A0 ([x] (snd (R x))) (snd R')
                <- hsubst_r M0 A0 R R'.


%% r head


hsubst_rr_var : hsubst_rr M0 A0 ([x] x) M0 A0.


hsubst_rr_app : hsubst_rr M0 A0 ([x] app (R1 x) (M2 x)) M'' A
                 <- hsubst_rr M0 A0 R1 (lam M') (arrow A2 A)
                 <- hsubst_m M0 A0 M2 M2'
                 <- hsubst_m M2' A2 M' M''.


hsubst_rr_fst : hsubst_rr M0 A0 ([x] (fst (R x))) M1' A1'
                 <- hsubst_rr M0 A0 R (pair M1' M2') (prod A1' A2').


hsubst_rr_snd : hsubst_rr M0 A0 ([x] (snd (R x))) M2' A2'
                 <- hsubst_rr M0 A0 R (pair M1' M2') (prod A1' A2').


%worlds (rtm_block) (hsubst_m _ _ _ _) (hsubst_r _ _ _ _) (hsubst_rr _ _ _ _ _).
%reduces A' <= A0 (hsubst_rr _ A0 _ _ A').
%terminates {(A0 A0' A0'') (M R R')} (hsubst_m _ A0 M _) (hsubst_r _ A0' R _) (hsubst_rr _ A0'' R' _ _).


expand : tp -> rtm -> mtm -> type.
%mode expand +X1 +X2 -X3.


expand_b : expand b R (asm R).


expand_arrow : expand (arrow A2 A) R (lam M)
                <- ({x : rtm} expand A2 x (M2 x))
                <- ({x : rtm} expand A (app R (M2 x)) (M x)).


expand_prod : expand (prod A1 A2) R (pair M1 M2)
               <- expand A1 (fst R) M1
               <- expand A2 (snd R) M2.


%worlds (rtm_block) (expand _ _ _).
%total A (expand A _ _).


hsubst_rr_size : {A2} {A'} hsubst_rr M2 A2 R M' A'
                    -> type.
%mode hsubst_rr_size +X1 +X2 +X3.


- : hsubst_rr_size
     A2 A2 hsubst_rr_var.


- : hsubst_rr_size
     A2 A4 (hsubst_rr_app _ _ Drr)
     <- hsubst_rr_size A2 (arrow A3 A4) Drr.


- : hsubst_rr_size
     A2 Al (hsubst_rr_fst Drr)
     <- hsubst_rr_size A2 (prod Al Ar) Drr.


- : hsubst_rr_size
     A2 Ar (hsubst_rr_snd Drr)
     <- hsubst_rr_size A2 (prod Al Ar) Drr.


%worlds (rtm_block) (hsubst_rr_size _ _ _).
%total D (hsubst_rr_size _ _ D).
%reduces A' <= A2 (hsubst_rr_size A2 A' _).


hsubst_r_exists_sum : mtm -> tp -> (rtm -> rtm) -> tp -> type.
hsubst_r_exists_sum_r : hsubst_r_exists_sum M2 A2 R A
                         <- hsubst_r M2 A2 R R'
                         <- atom R' A.
hsubst_r_exists_sum_rr : hsubst_r_exists_sum M2 A2 R A'
                          <- hsubst_rr M2 A2 R M' A'
                          <- canon M' A'.


hsubst_m_exists_asm :  hsubst_r_exists_sum M2 A2 R b
                       -> hsubst_m M2 A2 ([x] (asm (R x))) M'
                       -> canon M' b
                       -> type.
%mode hsubst_m_exists_asm +X1 -X2 -X3.


- : hsubst_m_exists_asm
     (hsubst_r_exists_sum_r DaR' DsR)
     (hsubst_m_r DsR)
     (canon_asm DaR').


- : hsubst_m_exists_asm
     (hsubst_r_exists_sum_rr DcM' DsR)
     (hsubst_m_rr DsR)
     DcM'.


%worlds (atom_block) (hsubst_m_exists_asm _ _ _).
%total {} (hsubst_m_exists_asm _ _ _).




hsubst_r_exists_fst : hsubst_r_exists_sum M2 A2 R (prod Al Ar)
                       -> hsubst_r_exists_sum M2 A2 ([x] (fst (R x))) Al
                       -> type.
%mode hsubst_r_exists_fst +X1 -X2.


- : hsubst_r_exists_fst
     (hsubst_r_exists_sum_r DaR' DsR)
     (hsubst_r_exists_sum_r (atom_fst DaR') (hsubst_r_fst DsR)).


- : hsubst_r_exists_fst
     (hsubst_r_exists_sum_rr (canon_pair _ DcMl') DsR)
     (hsubst_r_exists_sum_rr DcMl' (hsubst_rr_fst DsR)).


%worlds (atom_block) (hsubst_r_exists_fst _ _).
%total {} (hsubst_r_exists_fst _ _).




hsubst_r_exists_snd : hsubst_r_exists_sum M2 A2 R (prod Al Ar)
                       -> hsubst_r_exists_sum M2 A2 ([x] (snd (R x))) Ar
                       -> type.
%mode hsubst_r_exists_snd +X1 -X2.


- : hsubst_r_exists_snd
     (hsubst_r_exists_sum_r DaR' DsR)
     (hsubst_r_exists_sum_r (atom_snd DaR') (hsubst_r_snd DsR)).


- : hsubst_r_exists_snd
     (hsubst_r_exists_sum_rr (canon_pair DcMr' _) DsR)
     (hsubst_r_exists_sum_rr DcMr' (hsubst_rr_snd DsR)).


%worlds (atom_block) (hsubst_r_exists_snd _ _).
%total {} (hsubst_r_exists_snd _ _).


hsubst_m_exists : {A2}
                   ({y : rtm} {dy : atom y A2} canon (M y) A)
                   -> canon M2 A2
                   -> hsubst_m M2 A2 M M'
                   -> canon M' A
                   -> type.
%mode hsubst_m_exists +X0 +X1 +X2 -X3 -X4.


hsubst_r_exists : {A2}
                   ({y : rtm} {dx : atom y A2} atom (R y) A)
                   -> canon M2 A2
                   -> hsubst_r_exists_sum M2 A2 R A
                   -> type.
%mode hsubst_r_exists +X0 +X1 +X2 -X3.


hsubst_m_exists_app : {A2}
                       %% this next argument is makes the termination argument work
                       ({y : rtm} {dx : atom y A2} atom (R1 y) (arrow A3 A4))
                       -> hsubst_r_exists_sum M2 A2 R1 (arrow A3 A4)
                       -> hsubst_m M2 A2 M3 M3'
                       -> canon M3' A3
                       -> hsubst_r_exists_sum M2 A2 ([x] (app (R1 x) (M3 x))) A4
                       -> type.
%mode hsubst_m_exists_app +X-1 +X0 +X1 +X2 +X3 -X4.


%% canonical terms


- : hsubst_m_exists
     A2
     ([x] [dx] canon_asm (DaR x dx))
     DcM2
     DsR
     DcM'
     <- hsubst_r_exists A2 DaR DcM2 Dsum
     <- hsubst_m_exists_asm Dsum DsR DcM'.


- : hsubst_m_exists
     A2
     ([x] [dx] (canon_lam ([y] [dy] DcM x dx y dy)) : canon (lam (M x)) (arrow Af At))
     (DcM2 : canon M2 A2)
     (hsubst_m_lam DsM)
     (canon_lam DcM')
     <- ({y}
           {dy : atom y Af}
           hsubst_m_exists A2 ([x] [dx] (DcM x dx y dy)) DcM2 (DsM y) (DcM' y dy)).


- : hsubst_m_exists
     A2
     ([x] [dx] (canon_pair (DcMr x dx) (DcMl x dx)))
     DcM2
     (hsubst_m_pair DsMr DsMl)
     (canon_pair DcMr' DcMl')
     <- hsubst_m_exists A2 DcMl DcM2 DsMl DcMl'
     <- hsubst_m_exists A2 DcMr DcM2 DsMr DcMr'.


%% atomic terms


- : hsubst_r_exists
     A2
     ([x] [dx] D)
     _
     (hsubst_r_exists_sum_r D hsubst_r_closed).


- : hsubst_r_exists
     A2
     ([x] [dx] dx)
     DcM2
     (hsubst_r_exists_sum_rr DcM2 hsubst_rr_var).


- : hsubst_r_exists
     A2
     ([x] [dx] (atom_app (DcM x dx) (DaR x dx)))
     DcM2
     DsumApp
     <- hsubst_m_exists A2 DcM DcM2 DsM' DcM'
     <- hsubst_r_exists A2 DaR DcM2 DsumR'
     <- hsubst_m_exists_app A2 DaR DsumR' DsM' DcM' DsumApp.


- : hsubst_r_exists
     A2
     ([x] [dx] (atom_fst (DcR x dx)))
     DcM2
     DsumFst
     <- hsubst_r_exists A2 DcR DcM2 DsumR
     <- hsubst_r_exists_fst DsumR DsumFst.


- : hsubst_r_exists
     A2
     ([x] [dx] (atom_snd (DcR x dx)))
     DcM2
     DsumSnd
     <- hsubst_r_exists A2 DcR DcM2 DsumR
     <- hsubst_r_exists_snd DsumR DsumSnd.


%% app factoring lemma


- : hsubst_m_exists_app
     A2
     _
     (hsubst_r_exists_sum_r DaR1 DsR1)
     DsM3
     DcM3
     (hsubst_r_exists_sum_r (atom_app DcM3 DaR1) (hsubst_r_app DsM3 DsR1)).


- : hsubst_m_exists_app
     A2
     _
     (hsubst_r_exists_sum_rr (canon_lam DcM4') DsR1)
     DsM3
     DcM3
     (hsubst_r_exists_sum_rr DcM4'' (hsubst_rr_app DsM4' DsM3 DsR1))
     <- hsubst_rr_size A2 (arrow A3 A4) DsR1
     <- hsubst_m_exists A3 DcM4' DcM3 DsM4' DcM4''.


%worlds (atom_block)
(hsubst_m_exists_app _ _ _ _ _ _)
(hsubst_r_exists _ _ _ _)
(hsubst_m_exists _ _ _ _ _).


%total {(A2 A2' A2'') (D  D' D'')}
(hsubst_m_exists A2' D' _ _ _)
(hsubst_m_exists_app A2'' D'' _ _ _ _)
(hsubst_r_exists A2 D _ _).


id/mtm : mtm -> mtm -> type.
id/mtm_refl : id/mtm M M.


id/rtm : rtm -> rtm -> type.
id/rtm_refl : id/rtm R R.


id/tp : tp -> tp -> type.
id/tp_refl : id/tp A A.


id/rtm_sym : id/rtm R R'
        -> id/rtm R' R
        -> type.
%mode id/rtm_sym +X1 -X2.


- : id/rtm_sym id/rtm_refl id/rtm_refl.


%worlds (rtm_block) (id/rtm_sym _ _).
%total {} (id/rtm_sym _ _).


id/tp_arrow_inv : id/tp (arrow A1 A2) (arrow A1' A2')
       -> id/tp A1 A1'
       -> id/tp A2 A2'
       -> type.
%mode id/tp_arrow_inv +X1 -X2 -X3.


- : id/tp_arrow_inv _ id/tp_refl id/tp_refl.


%worlds (rtm_block) (id/tp_arrow_inv _ _ _).
%total {} (id/tp_arrow_inv _ _ _).


id/tp_prod_inv : id/tp (prod A1 A2) (prod A1' A2')
       -> id/tp A1 A1'
       -> id/tp A2 A2'
       -> type.
%mode id/tp_prod_inv +X1 -X2 -X3.


- : id/tp_prod_inv _ id/tp_refl id/tp_refl.


%worlds (rtm_block) (id/tp_prod_inv _ _ _).
%total {} (id/tp_prod_inv _ _ _).


id/rtm_app_cong : id/rtm R R'
       -> id/mtm M M'
       -> id/rtm (app R M) (app R' M')
       -> type.
%mode id/rtm_app_cong +X1 +X2 -X3.


- : id/rtm_app_cong _ _ id/rtm_refl.


%worlds (rtm_block) (id/rtm_app_cong _ _ _).
%total {} (id/rtm_app_cong _ _ _).


id/rtm_fst_cong : id/rtm R R'
       -> id/rtm (fst R) (fst R')
       -> type.
%mode id/rtm_fst_cong +X1  -X3.


- : id/rtm_fst_cong _ id/rtm_refl.


%worlds (rtm_block) (id/rtm_fst_cong _ _).
%total {} (id/rtm_fst_cong _ _).


id/rtm_snd_cong : id/rtm R R'
       -> id/rtm (snd R) (snd R')
       -> type.
%mode id/rtm_snd_cong +X1  -X3.


- : id/rtm_snd_cong _ id/rtm_refl.


%worlds (rtm_block) (id/rtm_snd_cong _ _).
%total {} (id/rtm_snd_cong _ _).


id/mtm_lam_cong :  ({x:rtm} id/mtm (M x) (M' x))
       -> id/mtm (lam M) (lam M')
       -> type.
%mode id/mtm_lam_cong +X1 -X3.


- : id/mtm_lam_cong _ id/mtm_refl.


%worlds (rtm_block) (id/mtm_lam_cong _ _).
%total {} (id/mtm_lam_cong _ _).


id/mtm_lam_inv :  id/mtm (lam M) (lam M')
      -> ({x:rtm} id/mtm (M x) (M' x))
      -> type.
%mode id/mtm_lam_inv +X1 -X3.


- : id/mtm_lam_inv _ ([_] id/mtm_refl).


%worlds (rtm_block) (id/mtm_lam_inv _ _).
%total {} (id/mtm_lam_inv _ _).


id/mtm_pair_cong : id/mtm M1 M1'
       -> id/mtm M2 M2'
       -> id/mtm (pair M1 M2) (pair M1' M2')
       -> type.
%mode id/mtm_pair_cong +X1 +X2 -X3.


- : id/mtm_pair_cong _ _ id/mtm_refl.


%worlds (rtm_block) (id/mtm_pair_cong _ _ _).
%total {} (id/mtm_pair_cong _ _ _).


id/mtm_pair_inv : id/mtm (pair M1 M2) (pair M1' M2')
       -> id/mtm M1 M1'
       -> id/mtm M2 M2'
       -> type.
%mode id/mtm_pair_inv +X1 -X2 -X3.


- : id/mtm_pair_inv _ id/mtm_refl id/mtm_refl.


%worlds (rtm_block) (id/mtm_pair_inv _ _ _).
%total {} (id/mtm_pair_inv _ _ _).


expand_respects_id : id/rtm R R'
          -> id/mtm M M'
          -> expand A R M
          -> expand A R' M'
          -> type.
%mode expand_respects_id +X1 +X2 +X3 -X4.


- : expand_respects_id _ _ D D.


%worlds (rtm_block) (expand_respects_id _ _ _ _).
%total {} (expand_respects_id _ _ _ _).
%reduces D1 = D2 (expand_respects_id _ _ D2 D1).


canon_respects_id :  id/mtm M M'
         -> id/tp A A'
         -> canon M A
         -> canon M' A'
         -> type.
%mode canon_respects_id +X1 +X2 +X3 -X4.


- : canon_respects_id _ _ D D.


%worlds (atom_block) (canon_respects_id _ _ _ _).
%total {} (canon_respects_id _ _ _ _).
%reduces D1 = D2 (canon_respects_id _ _ D2 D1).


hsubst_m_respects_id : id/mtm M2 M2'
      -> id/tp A2 A2'
      -> ({x} id/mtm (M x) (M' x))
      -> hsubst_m M2 A2 M Ms
      -> hsubst_m M2' A2' M' Ms
      -> type.
%mode hsubst_m_respects_id +X1 +X2 +X3 +X4 -X5.


- : hsubst_m_respects_id _ _ _ D D.


%worlds (rtm_block) (hsubst_m_respects_id _ _ _ _ _).
%total {} (hsubst_m_respects_id _ _ _ _ _).
%reduces D1 = D2 (hsubst_m_respects_id _ _ _ D2 D1).


id/mtm_asm_cong : id/rtm R R'
       -> id/mtm (asm R) (asm R')
       -> type.
%mode id/mtm_asm_cong +X1  -X3.


- : id/mtm_asm_cong _ id/mtm_refl.


%worlds (rtm_block) (id/mtm_asm_cong _ _).
%total {} (id/mtm_asm_cong _ _).


false : type.
%freeze false.


hsubst_rr_closed_contra : hsubst_rr M2 A2 ([_] R) M' A'
                           -> false
                           -> type.
%mode hsubst_rr_closed_contra +X1 -X2.


- : hsubst_rr_closed_contra
     (hsubst_rr_app _ _ Dr)
     X
     <- hsubst_rr_closed_contra Dr X.


- : hsubst_rr_closed_contra
     (hsubst_rr_fst D)
     X
     <- hsubst_rr_closed_contra D X.


- : hsubst_rr_closed_contra
     (hsubst_rr_snd D)
     X
     <- hsubst_rr_closed_contra D X.


%worlds (rtm_block) (hsubst_rr_closed_contra _ _).
%total D (hsubst_rr_closed_contra D _).


%% contradiction of root and non-root


hsubst_r_rr_contra : hsubst_r M2 A2 R R'
                      -> hsubst_rr M2 A2 R M' A'
                      -> false
                      -> type.
%mode hsubst_r_rr_contra +X1 +X2 -X3.


- : hsubst_r_rr_contra
     hsubst_r_closed
     Drr
     X
     <- hsubst_rr_closed_contra Drr X.


- : hsubst_r_rr_contra
     (hsubst_r_app _ DsrR)
     (hsubst_rr_app _ _ DsrrR)
     X
     <- hsubst_r_rr_contra DsrR DsrrR X.


- : hsubst_r_rr_contra
     (hsubst_r_fst DsrR)
     (hsubst_rr_fst DsrrR)
     X
     <- hsubst_r_rr_contra DsrR DsrrR X.


- : hsubst_r_rr_contra
     (hsubst_r_snd DsrR)
     (hsubst_rr_snd DsrrR)
     X
     <- hsubst_r_rr_contra DsrR DsrrR X.


%worlds (rtm_block) (hsubst_r_rr_contra _ _ _). %% bar in extra block for lemma below's future use
%total (D) (hsubst_r_rr_contra D _ _).


%% false implies id
false_implies_id/mtm : {M} {M'}
                        false
                        -> id/mtm M M'
                        -> type.
%mode false_implies_id/mtm +X1 +X2 +X3 -X4.
%worlds (rtm_block) (false_implies_id/mtm _ _ _ _). %% bar in extra block for lemma below's future use
%total {} (false_implies_id/mtm _ _ _ _).


hsubst_r_vacuous_id : hsubst_r M2 A2 ([_] R) R'
                     -> id/rtm R' R
                     -> type.
%mode hsubst_r_vacuous_id +X1 -X2.


hsubst_m_vacuous_id : hsubst_m M2 A2 ([_] M) M'
                     -> id/mtm M' M
                     -> type.
%mode hsubst_m_vacuous_id +X1 -X2.


%% R


- : hsubst_r_vacuous_id hsubst_r_closed id/rtm_refl.


- : hsubst_r_vacuous_id (hsubst_r_app Dm Dr) Did'
     <- hsubst_r_vacuous_id Dr DidR
     <- hsubst_m_vacuous_id Dm DidM
     <- id/rtm_app_cong DidR DidM Did'.


- : hsubst_r_vacuous_id (hsubst_r_fst D) Did'
     <- hsubst_r_vacuous_id D Did
     <- id/rtm_fst_cong Did Did'.


- : hsubst_r_vacuous_id (hsubst_r_snd D) Did'
     <- hsubst_r_vacuous_id D Did
     <- id/rtm_snd_cong Did Did'.


%% M


- : hsubst_m_vacuous_id
     (hsubst_m_r Dr)
     Did'
     <- hsubst_r_vacuous_id Dr Did
     <- id/mtm_asm_cong Did Did'.


- : hsubst_m_vacuous_id
     (hsubst_m_rr D)
     Did
     <- hsubst_rr_closed_contra D X
     <- false_implies_id/mtm _ _ X Did.


- : hsubst_m_vacuous_id
     (hsubst_m_lam D)
     Did'
     <- ({x}
           hsubst_m_vacuous_id (D x) (Did x))
     <- id/mtm_lam_cong Did Did'.


- : hsubst_m_vacuous_id
     (hsubst_m_pair D2 D1)
     Did'
     <- hsubst_m_vacuous_id D1 Did1
     <- hsubst_m_vacuous_id D2 Did2
     <- id/mtm_pair_cong Did1 Did2 Did'.


%worlds (rtm_block) (hsubst_r_vacuous_id _ _) (hsubst_m_vacuous_id _ _).
%total (D1 D2)
(hsubst_r_vacuous_id D1 _)
(hsubst_m_vacuous_id D2 _).


hsubst_m_unique : hsubst_m M2 A2 M M'
                   -> hsubst_m M2 A2 M M''
                   -> id/mtm M' M''
                   -> type.
%mode hsubst_m_unique +X1 +X2 -X3.


hsubst_r_unique : hsubst_r M2 A2 R R'
                   -> hsubst_r M2 A2 R R''
                   -> id/rtm R' R''
                   -> type.
%mode hsubst_r_unique +X1 +X2 -X3.


hsubst_rr_unique : hsubst_rr M2 A2 R M' A'
                    -> hsubst_rr M2 A2 R M'' A''
                    -> id/mtm M' M''
                    -> id/tp A' A''
                    -> type.
%mode hsubst_rr_unique +X1 +X2 -X3 -X4.


%% M


- : hsubst_m_unique
     (hsubst_m_r Dsr)
     (hsubst_m_r Dsr')
     DidAsm
     <- hsubst_r_unique Dsr Dsr' DidR
     <- id/mtm_asm_cong DidR DidAsm.


- : hsubst_m_unique
     (hsubst_m_rr Dsr)
     (hsubst_m_rr Dsr')
     Did
     <- hsubst_rr_unique Dsr Dsr' Did _.


%% contradict mismatch
- : hsubst_m_unique
     (hsubst_m_r Dsr)
     (hsubst_m_rr Dsrr)
     Did
     <- hsubst_r_rr_contra Dsr Dsrr X
     <- false_implies_id/mtm _ _ X Did.


%% contradict mismatch
- : hsubst_m_unique
     (hsubst_m_rr Dsrr)
     (hsubst_m_r Dsr)
     Did
     <- hsubst_r_rr_contra Dsr Dsrr X
     <- false_implies_id/mtm _ _ X Did.


- : hsubst_m_unique
     (hsubst_m_pair DsRight DsLeft)
     (hsubst_m_pair DsRight' DsLeft')
     DidPair
     <- hsubst_m_unique DsLeft DsLeft' DidLeft
     <- hsubst_m_unique DsRight DsRight' DidRight
     <- id/mtm_pair_cong DidLeft DidRight DidPair.


- : hsubst_m_unique
     (hsubst_m_lam Ds)
     (hsubst_m_lam Ds')
     DidLam
     <- ({y:rtm} hsubst_m_unique (Ds y) (Ds' y) (Did y))
     <- id/mtm_lam_cong Did DidLam.


%% R non-root


- : hsubst_r_unique D D id/rtm_refl.


- : hsubst_r_unique
     (hsubst_r_closed : hsubst_r M2 A2 ([_] R) R)
     (D : hsubst_r M2 A2 ([_] R) R')
     Did'
     <- hsubst_r_vacuous_id D Did
     <- id/rtm_sym Did Did'.


- : hsubst_r_unique
     (D : hsubst_r M2 A2 ([_] R) R')
     (hsubst_r_closed : hsubst_r M2 A2 ([_] R) R)
     Did
     <- hsubst_r_vacuous_id D Did.


- : hsubst_r_unique
     (hsubst_r_app DsM' DsR')
     (hsubst_r_app DsM'' DsR'')
     DidApp
     <- hsubst_r_unique DsR' DsR'' DidR
     <- hsubst_m_unique DsM' DsM'' DidM
     <- id/rtm_app_cong DidR DidM DidApp.


- : hsubst_r_unique
     (hsubst_r_fst DsR')
     (hsubst_r_fst DsR'')
     DidFst
     <- hsubst_r_unique DsR' DsR'' DidR
     <- id/rtm_fst_cong DidR DidFst.
- : hsubst_r_unique
     (hsubst_r_snd DsR')
     (hsubst_r_snd DsR'')
     DidSnd
     <- hsubst_r_unique DsR' DsR'' DidR
     <- id/rtm_snd_cong DidR DidSnd.


%% R root


- : hsubst_rr_unique
     hsubst_rr_var
     hsubst_rr_var
     id/mtm_refl
     id/tp_refl.


- : hsubst_rr_unique
     (hsubst_rr_app DsM4' DsM3 DsR1)
     (hsubst_rr_app DsM4'-2 DsM3-2 DsR1-2)
     DidM4''
     DidA4
     <- hsubst_rr_unique DsR1 DsR1-2 DidLam DidArrow
     <- hsubst_m_unique DsM3 DsM3-2 DidM3'
     <- id/tp_arrow_inv DidArrow DidA3 DidA4
     <- id/mtm_lam_inv DidLam DidM4'
     <- hsubst_m_respects_id DidM3' DidA3 DidM4' DsM4' DsM4'-1
     <- hsubst_m_unique DsM4'-1 DsM4'-2 DidM4''.


- : hsubst_rr_unique
     (hsubst_rr_fst DsR')
     (hsubst_rr_fst DsR'')
     DidMl
     DidAl
     <- hsubst_rr_unique DsR' DsR'' DidPair DidProd
     <- id/tp_prod_inv DidProd DidAl _
     <- id/mtm_pair_inv DidPair DidMl _.


- : hsubst_rr_unique
     (hsubst_rr_snd DsR')
     (hsubst_rr_snd DsR'')
     DidMr
     DidAr
     <- hsubst_rr_unique DsR' DsR'' DidPair DidProd
     <- id/tp_prod_inv DidProd _ DidAr
     <- id/mtm_pair_inv DidPair _ DidMr.


%worlds (rtm_block)
(hsubst_m_unique _ _ _)
(hsubst_r_unique _ _ _)
(hsubst_rr_unique _ _ _ _).


%total (D1 D2 D3)
(hsubst_r_unique D2 _ _)
(hsubst_rr_unique D3 _ _ _)
(hsubst_m_unique D1 _ _).


expand_exists : {A}
                 atom R A
                 -> expand A R M
                 -> canon M A
                 -> type.
%mode expand_exists +X0 +X1 -X2 -X3.


- : expand_exists
     b
     D
     expand_b
     (canon_asm D).


- : expand_exists
     (arrow A2 A)
     DaR
     (expand_arrow DeApp DeX)
     (canon_lam DcApp)
     <- ({x : rtm}
           {dx : atom x A2}
           expand_exists A2 dx (DeX x) (DcM x dx))
     <- ({x : rtm}
           {dx : atom x A2}
           expand_exists A (atom_app (DcM x dx) DaR) (DeApp x) (DcApp x dx)).


- : expand_exists
     (prod A1 A2)
     DaR
     (expand_prod DeS DeF)
     (canon_pair DcS DcF)
     <- expand_exists A1 (atom_fst DaR) DeF DcF
     <- expand_exists A2 (atom_snd DaR) DeS DcS.


%worlds (atom_block) (expand_exists _ _ _ _).
%total D (expand_exists D _ _ _).


expand_unique : expand A R M
                 -> expand A R M'
                 -> id/mtm M M'
                 -> type.
%mode expand_unique +X1 +X2 -X3.


- : expand_unique
     expand_b
     expand_b
     id/mtm_refl.


- : expand_unique
     (expand_arrow
        (DeApp : {x : rtm} expand A (app R (Mx x)) (MApp x))
        (DeX : {x : rtm} expand A2 x (Mx x)))
      (expand_arrow
         (DeApp' : {x : rtm} expand A (app R (Mx' x)) (MApp' x))
         (DeX' : {x : rtm} expand A2 x (Mx' x)))
     DidLam
     <- ({x : rtm}
           expand_unique (DeX x) (DeX' x) (DidX x))
     <- ({x : rtm}
           id/rtm_app_cong (id/rtm_refl : id/rtm R R) (DidX x) (DidApp x))
     <- ({x : rtm}
           expand_respects_id (DidApp x) id/mtm_refl (DeApp x) (DeApp-2 x))
     <- ({x : rtm}
           expand_unique (DeApp-2 x) (DeApp' x) (DidAppExp x))
     <- id/mtm_lam_cong DidAppExp DidLam.


- : expand_unique
     (expand_prod DeS DeF)
     (expand_prod DeS' DeF')
     DidPair
     <- expand_unique DeF DeF' DidF
     <- expand_unique DeS DeS' DidS
     <- id/mtm_pair_cong DidF DidS DidPair.


%worlds (rtm_block) (expand_unique _ _ _).
%total D (expand_unique _ D _).


tp : type.


b : tp.
arrow : tp -> tp -> tp.
prod : tp -> tp -> tp.


rtm : type.
mtm : type.


app : rtm -> mtm -> rtm.
c : rtm.
fst : rtm -> rtm.
snd : rtm -> rtm.


asm : rtm -> mtm.
lam : (rtm -> mtm) -> mtm.
pair : mtm -> mtm -> mtm.


%block rtm_block : block {x : rtm}.
%worlds (rtm_block) (tp) (rtm) (mtm).


atom : rtm -> tp -> type.
%mode atom +X1 -X2.


canon : mtm -> tp -> type.
%mode canon +X1 +X2.


% atomic


atom_c : atom c b.


atom_app : atom (app R1 M2) A
            <- atom R1 (arrow A2 A)
            <- canon M2 A2.


atom_fst : atom (fst R) A1
            <- atom R (prod A1 A2).


atom_snd : atom (snd R) A2
            <- atom R (prod A1 A2).


%% canonical


canon_asm : canon (asm R) b
             <- atom R b.


canon_lam : canon (lam M) (arrow A2 A)
             <- {x : rtm} (atom x A2) ->  canon (M x) A.


canon_pair : canon (pair M1 M2) (prod A1 A2)
              <- canon M1 A1
              <- canon M2 A2.


%block atom_block : some {A:tp}
                     block {x:rtm} {dx : atom x A}.
%worlds (atom_block) (atom _ _) (canon _ _).
%terminates (R M) (atom R _) (canon M _).


hsubst_m : mtm -> tp -> (rtm -> mtm) -> mtm -> type.
%mode hsubst_m +X1 +X2 +X3 -X4.


hsubst_r : mtm -> tp -> (rtm -> rtm) -> rtm -> type.
%mode hsubst_r +X1 +X2 +X3 -X4.


hsubst_rr : mtm -> tp -> (rtm -> rtm) -> mtm -> tp -> type.
%mode hsubst_rr +X1 +X2 +X3 -X4 -X5.


%% Ms


hsubst_m_r : hsubst_m M0 A0 ([x] asm (R x)) (asm R')
              <- hsubst_r M0 A0 R R'.


hsubst_m_rr : hsubst_m M0 A0 ([x] asm (R x)) M'
               <- hsubst_rr M0 A0 R M' _.


hsubst_m_lam : hsubst_m M0 A0 ([x] (lam ([y] M x y))) (lam M')
                <- ({y:rtm}
                      hsubst_m M0 A0 ([x] M x y) (M' y)).


hsubst_m_pair : hsubst_m M0 A0 ([x] (pair (M1 x) (M2 x))) (pair M1' M2')
                 <- hsubst_m M0 A0 M1 M1'
                 <- hsubst_m M0 A0 M2 M2'.


%% R not head


hsubst_r_closed : hsubst_r M0 A0 ([x] E) E.


hsubst_r_app : hsubst_r M0 A0 ([x] (app (R x) (M x))) (app R' M')
                <- hsubst_r M0 A0 R R'
                <- hsubst_m M0 A0 M M'.


hsubst_r_fst : hsubst_r M0 A0 ([x] (fst (R x))) (fst R')
                <- hsubst_r M0 A0 R R'.


hsubst_r_snd : hsubst_r M0 A0 ([x] (snd (R x))) (snd R')
                <- hsubst_r M0 A0 R R'.


%% r head


hsubst_rr_var : hsubst_rr M0 A0 ([x] x) M0 A0.


hsubst_rr_app : hsubst_rr M0 A0 ([x] app (R1 x) (M2 x)) M'' A
                 <- hsubst_rr M0 A0 R1 (lam M') (arrow A2 A)
                 <- hsubst_m M0 A0 M2 M2'
                 <- hsubst_m M2' A2 M' M''.


hsubst_rr_fst : hsubst_rr M0 A0 ([x] (fst (R x))) M1' A1'
                 <- hsubst_rr M0 A0 R (pair M1' M2') (prod A1' A2').


hsubst_rr_snd : hsubst_rr M0 A0 ([x] (snd (R x))) M2' A2'
                 <- hsubst_rr M0 A0 R (pair M1' M2') (prod A1' A2').


%worlds (rtm_block) (hsubst_m _ _ _ _) (hsubst_r _ _ _ _) (hsubst_rr _ _ _ _ _).
%reduces A' <= A0 (hsubst_rr _ A0 _ _ A').
%terminates {(A0 A0' A0'') (M R R')} (hsubst_m _ A0 M _) (hsubst_r _ A0' R _) (hsubst_rr _ A0'' R' _ _).


expand : tp -> rtm -> mtm -> type.
%mode expand +X1 +X2 -X3.


expand_b : expand b R (asm R).


expand_arrow : expand (arrow A2 A) R (lam M)
                <- ({x : rtm} expand A2 x (M2 x))
                <- ({x : rtm} expand A (app R (M2 x)) (M x)).


expand_prod : expand (prod A1 A2) R (pair M1 M2)
               <- expand A1 (fst R) M1
               <- expand A2 (snd R) M2.


%worlds (rtm_block) (expand _ _ _).
%total A (expand A _ _).


hsubst_rr_size : {A2} {A'} hsubst_rr M2 A2 R M' A'
                    -> type.
%mode hsubst_rr_size +X1 +X2 +X3.


- : hsubst_rr_size
     A2 A2 hsubst_rr_var.


- : hsubst_rr_size
     A2 A4 (hsubst_rr_app _ _ Drr)
     <- hsubst_rr_size A2 (arrow A3 A4) Drr.


- : hsubst_rr_size
     A2 Al (hsubst_rr_fst Drr)
     <- hsubst_rr_size A2 (prod Al Ar) Drr.


- : hsubst_rr_size
     A2 Ar (hsubst_rr_snd Drr)
     <- hsubst_rr_size A2 (prod Al Ar) Drr.


%worlds (rtm_block) (hsubst_rr_size _ _ _).
%total D (hsubst_rr_size _ _ D).
%reduces A' <= A2 (hsubst_rr_size A2 A' _).


hsubst_r_exists_sum : mtm -> tp -> (rtm -> rtm) -> tp -> type.
hsubst_r_exists_sum_r : hsubst_r_exists_sum M2 A2 R A
                         <- hsubst_r M2 A2 R R'
                         <- atom R' A.
hsubst_r_exists_sum_rr : hsubst_r_exists_sum M2 A2 R A'
                          <- hsubst_rr M2 A2 R M' A'
                          <- canon M' A'.


hsubst_m_exists_asm :  hsubst_r_exists_sum M2 A2 R b
                       -> hsubst_m M2 A2 ([x] (asm (R x))) M'
                       -> canon M' b
                       -> type.
%mode hsubst_m_exists_asm +X1 -X2 -X3.


- : hsubst_m_exists_asm
     (hsubst_r_exists_sum_r DaR' DsR)
     (hsubst_m_r DsR)
     (canon_asm DaR').


- : hsubst_m_exists_asm
     (hsubst_r_exists_sum_rr DcM' DsR)
     (hsubst_m_rr DsR)
     DcM'.


%worlds (atom_block) (hsubst_m_exists_asm _ _ _).
%total {} (hsubst_m_exists_asm _ _ _).




hsubst_r_exists_fst : hsubst_r_exists_sum M2 A2 R (prod Al Ar)
                       -> hsubst_r_exists_sum M2 A2 ([x] (fst (R x))) Al
                       -> type.
%mode hsubst_r_exists_fst +X1 -X2.


- : hsubst_r_exists_fst
     (hsubst_r_exists_sum_r DaR' DsR)
     (hsubst_r_exists_sum_r (atom_fst DaR') (hsubst_r_fst DsR)).


- : hsubst_r_exists_fst
     (hsubst_r_exists_sum_rr (canon_pair _ DcMl') DsR)
     (hsubst_r_exists_sum_rr DcMl' (hsubst_rr_fst DsR)).


%worlds (atom_block) (hsubst_r_exists_fst _ _).
%total {} (hsubst_r_exists_fst _ _).




hsubst_r_exists_snd : hsubst_r_exists_sum M2 A2 R (prod Al Ar)
                       -> hsubst_r_exists_sum M2 A2 ([x] (snd (R x))) Ar
                       -> type.
%mode hsubst_r_exists_snd +X1 -X2.


- : hsubst_r_exists_snd
     (hsubst_r_exists_sum_r DaR' DsR)
     (hsubst_r_exists_sum_r (atom_snd DaR') (hsubst_r_snd DsR)).


- : hsubst_r_exists_snd
     (hsubst_r_exists_sum_rr (canon_pair DcMr' _) DsR)
     (hsubst_r_exists_sum_rr DcMr' (hsubst_rr_snd DsR)).


%worlds (atom_block) (hsubst_r_exists_snd _ _).
%total {} (hsubst_r_exists_snd _ _).


hsubst_m_exists : {A2}
                   ({y : rtm} {dy : atom y A2} canon (M y) A)
                   -> canon M2 A2
                   -> hsubst_m M2 A2 M M'
                   -> canon M' A
                   -> type.
%mode hsubst_m_exists +X0 +X1 +X2 -X3 -X4.


hsubst_r_exists : {A2}
                   ({y : rtm} {dx : atom y A2} atom (R y) A)
                   -> canon M2 A2
                   -> hsubst_r_exists_sum M2 A2 R A
                   -> type.
%mode hsubst_r_exists +X0 +X1 +X2 -X3.


hsubst_m_exists_app : {A2}
                       %% this next argument is makes the termination argument work
                       ({y : rtm} {dx : atom y A2} atom (R1 y) (arrow A3 A4))
                       -> hsubst_r_exists_sum M2 A2 R1 (arrow A3 A4)
                       -> hsubst_m M2 A2 M3 M3'
                       -> canon M3' A3
                       -> hsubst_r_exists_sum M2 A2 ([x] (app (R1 x) (M3 x))) A4
                       -> type.
%mode hsubst_m_exists_app +X-1 +X0 +X1 +X2 +X3 -X4.


%% canonical terms


- : hsubst_m_exists
     A2
     ([x] [dx] canon_asm (DaR x dx))
     DcM2
     DsR
     DcM'
     <- hsubst_r_exists A2 DaR DcM2 Dsum
     <- hsubst_m_exists_asm Dsum DsR DcM'.


- : hsubst_m_exists
     A2
     ([x] [dx] (canon_lam ([y] [dy] DcM x dx y dy)) : canon (lam (M x)) (arrow Af At))
     (DcM2 : canon M2 A2)
     (hsubst_m_lam DsM)
     (canon_lam DcM')
     <- ({y}
           {dy : atom y Af}
           hsubst_m_exists A2 ([x] [dx] (DcM x dx y dy)) DcM2 (DsM y) (DcM' y dy)).


- : hsubst_m_exists
     A2
     ([x] [dx] (canon_pair (DcMr x dx) (DcMl x dx)))
     DcM2
     (hsubst_m_pair DsMr DsMl)
     (canon_pair DcMr' DcMl')
     <- hsubst_m_exists A2 DcMl DcM2 DsMl DcMl'
     <- hsubst_m_exists A2 DcMr DcM2 DsMr DcMr'.


%% atomic terms


- : hsubst_r_exists
     A2
     ([x] [dx] D)
     _
     (hsubst_r_exists_sum_r D hsubst_r_closed).


- : hsubst_r_exists
     A2
     ([x] [dx] dx)
     DcM2
     (hsubst_r_exists_sum_rr DcM2 hsubst_rr_var).


- : hsubst_r_exists
     A2
     ([x] [dx] (atom_app (DcM x dx) (DaR x dx)))
     DcM2
     DsumApp
     <- hsubst_m_exists A2 DcM DcM2 DsM' DcM'
     <- hsubst_r_exists A2 DaR DcM2 DsumR'
     <- hsubst_m_exists_app A2 DaR DsumR' DsM' DcM' DsumApp.


- : hsubst_r_exists
     A2
     ([x] [dx] (atom_fst (DcR x dx)))
     DcM2
     DsumFst
     <- hsubst_r_exists A2 DcR DcM2 DsumR
     <- hsubst_r_exists_fst DsumR DsumFst.


- : hsubst_r_exists
     A2
     ([x] [dx] (atom_snd (DcR x dx)))
     DcM2
     DsumSnd
     <- hsubst_r_exists A2 DcR DcM2 DsumR
     <- hsubst_r_exists_snd DsumR DsumSnd.


%% app factoring lemma


- : hsubst_m_exists_app
     A2
     _
     (hsubst_r_exists_sum_r DaR1 DsR1)
     DsM3
     DcM3
     (hsubst_r_exists_sum_r (atom_app DcM3 DaR1) (hsubst_r_app DsM3 DsR1)).


- : hsubst_m_exists_app
     A2
     _
     (hsubst_r_exists_sum_rr (canon_lam DcM4') DsR1)
     DsM3
     DcM3
     (hsubst_r_exists_sum_rr DcM4'' (hsubst_rr_app DsM4' DsM3 DsR1))
     <- hsubst_rr_size A2 (arrow A3 A4) DsR1
     <- hsubst_m_exists A3 DcM4' DcM3 DsM4' DcM4''.


%worlds (atom_block)
(hsubst_m_exists_app _ _ _ _ _ _)
(hsubst_r_exists _ _ _ _)
(hsubst_m_exists _ _ _ _ _).


%total {(A2 A2' A2'') (D  D' D'')}
(hsubst_m_exists A2' D' _ _ _)
(hsubst_m_exists_app A2'' D'' _ _ _ _)
(hsubst_r_exists A2 D _ _).


id/mtm : mtm -> mtm -> type.
id/mtm_refl : id/mtm M M.


id/rtm : rtm -> rtm -> type.
id/rtm_refl : id/rtm R R.


id/tp : tp -> tp -> type.
id/tp_refl : id/tp A A.


id/rtm_sym : id/rtm R R'
        -> id/rtm R' R
        -> type.
%mode id/rtm_sym +X1 -X2.


- : id/rtm_sym id/rtm_refl id/rtm_refl.


%worlds (rtm_block) (id/rtm_sym _ _).
%total {} (id/rtm_sym _ _).


id/tp_arrow_inv : id/tp (arrow A1 A2) (arrow A1' A2')
       -> id/tp A1 A1'
       -> id/tp A2 A2'
       -> type.
%mode id/tp_arrow_inv +X1 -X2 -X3.


- : id/tp_arrow_inv _ id/tp_refl id/tp_refl.


%worlds (rtm_block) (id/tp_arrow_inv _ _ _).
%total {} (id/tp_arrow_inv _ _ _).


id/tp_prod_inv : id/tp (prod A1 A2) (prod A1' A2')
       -> id/tp A1 A1'
       -> id/tp A2 A2'
       -> type.
%mode id/tp_prod_inv +X1 -X2 -X3.


- : id/tp_prod_inv _ id/tp_refl id/tp_refl.


%worlds (rtm_block) (id/tp_prod_inv _ _ _).
%total {} (id/tp_prod_inv _ _ _).


id/rtm_app_cong : id/rtm R R'
       -> id/mtm M M'
       -> id/rtm (app R M) (app R' M')
       -> type.
%mode id/rtm_app_cong +X1 +X2 -X3.


- : id/rtm_app_cong _ _ id/rtm_refl.


%worlds (rtm_block) (id/rtm_app_cong _ _ _).
%total {} (id/rtm_app_cong _ _ _).


id/rtm_fst_cong : id/rtm R R'
       -> id/rtm (fst R) (fst R')
       -> type.
%mode id/rtm_fst_cong +X1  -X3.


- : id/rtm_fst_cong _ id/rtm_refl.


%worlds (rtm_block) (id/rtm_fst_cong _ _).
%total {} (id/rtm_fst_cong _ _).


id/rtm_snd_cong : id/rtm R R'
       -> id/rtm (snd R) (snd R')
       -> type.
%mode id/rtm_snd_cong +X1  -X3.


- : id/rtm_snd_cong _ id/rtm_refl.


%worlds (rtm_block) (id/rtm_snd_cong _ _).
%total {} (id/rtm_snd_cong _ _).


id/mtm_lam_cong :  ({x:rtm} id/mtm (M x) (M' x))
       -> id/mtm (lam M) (lam M')
       -> type.
%mode id/mtm_lam_cong +X1 -X3.


- : id/mtm_lam_cong _ id/mtm_refl.


%worlds (rtm_block) (id/mtm_lam_cong _ _).
%total {} (id/mtm_lam_cong _ _).


id/mtm_lam_inv :  id/mtm (lam M) (lam M')
      -> ({x:rtm} id/mtm (M x) (M' x))
      -> type.
%mode id/mtm_lam_inv +X1 -X3.


- : id/mtm_lam_inv _ ([_] id/mtm_refl).


%worlds (rtm_block) (id/mtm_lam_inv _ _).
%total {} (id/mtm_lam_inv _ _).


id/mtm_pair_cong : id/mtm M1 M1'
       -> id/mtm M2 M2'
       -> id/mtm (pair M1 M2) (pair M1' M2')
       -> type.
%mode id/mtm_pair_cong +X1 +X2 -X3.


- : id/mtm_pair_cong _ _ id/mtm_refl.


%worlds (rtm_block) (id/mtm_pair_cong _ _ _).
%total {} (id/mtm_pair_cong _ _ _).


id/mtm_pair_inv : id/mtm (pair M1 M2) (pair M1' M2')
       -> id/mtm M1 M1'
       -> id/mtm M2 M2'
       -> type.
%mode id/mtm_pair_inv +X1 -X2 -X3.


- : id/mtm_pair_inv _ id/mtm_refl id/mtm_refl.


%worlds (rtm_block) (id/mtm_pair_inv _ _ _).
%total {} (id/mtm_pair_inv _ _ _).


expand_respects_id : id/rtm R R'
          -> id/mtm M M'
          -> expand A R M
          -> expand A R' M'
          -> type.
%mode expand_respects_id +X1 +X2 +X3 -X4.


- : expand_respects_id _ _ D D.


%worlds (rtm_block) (expand_respects_id _ _ _ _).
%total {} (expand_respects_id _ _ _ _).
%reduces D1 = D2 (expand_respects_id _ _ D2 D1).


canon_respects_id :  id/mtm M M'
         -> id/tp A A'
         -> canon M A
         -> canon M' A'
         -> type.
%mode canon_respects_id +X1 +X2 +X3 -X4.


- : canon_respects_id _ _ D D.


%worlds (atom_block) (canon_respects_id _ _ _ _).
%total {} (canon_respects_id _ _ _ _).
%reduces D1 = D2 (canon_respects_id _ _ D2 D1).


hsubst_m_respects_id : id/mtm M2 M2'
      -> id/tp A2 A2'
      -> ({x} id/mtm (M x) (M' x))
      -> hsubst_m M2 A2 M Ms
      -> hsubst_m M2' A2' M' Ms
      -> type.
%mode hsubst_m_respects_id +X1 +X2 +X3 +X4 -X5.


- : hsubst_m_respects_id _ _ _ D D.


%worlds (rtm_block) (hsubst_m_respects_id _ _ _ _ _).
%total {} (hsubst_m_respects_id _ _ _ _ _).
%reduces D1 = D2 (hsubst_m_respects_id _ _ _ D2 D1).


id/mtm_asm_cong : id/rtm R R'
       -> id/mtm (asm R) (asm R')
       -> type.
%mode id/mtm_asm_cong +X1  -X3.


- : id/mtm_asm_cong _ id/mtm_refl.


%worlds (rtm_block) (id/mtm_asm_cong _ _).
%total {} (id/mtm_asm_cong _ _).


false : type.
%freeze false.


hsubst_rr_closed_contra : hsubst_rr M2 A2 ([_] R) M' A'
                           -> false
                           -> type.
%mode hsubst_rr_closed_contra +X1 -X2.


- : hsubst_rr_closed_contra
     (hsubst_rr_app _ _ Dr)
     X
     <- hsubst_rr_closed_contra Dr X.


- : hsubst_rr_closed_contra
     (hsubst_rr_fst D)
     X
     <- hsubst_rr_closed_contra D X.


- : hsubst_rr_closed_contra
     (hsubst_rr_snd D)
     X
     <- hsubst_rr_closed_contra D X.


%worlds (rtm_block) (hsubst_rr_closed_contra _ _).
%total D (hsubst_rr_closed_contra D _).


%% contradiction of root and non-root


hsubst_r_rr_contra : hsubst_r M2 A2 R R'
                      -> hsubst_rr M2 A2 R M' A'
                      -> false
                      -> type.
%mode hsubst_r_rr_contra +X1 +X2 -X3.


- : hsubst_r_rr_contra
     hsubst_r_closed
     Drr
     X
     <- hsubst_rr_closed_contra Drr X.


- : hsubst_r_rr_contra
     (hsubst_r_app _ DsrR)
     (hsubst_rr_app _ _ DsrrR)
     X
     <- hsubst_r_rr_contra DsrR DsrrR X.


- : hsubst_r_rr_contra
     (hsubst_r_fst DsrR)
     (hsubst_rr_fst DsrrR)
     X
     <- hsubst_r_rr_contra DsrR DsrrR X.


- : hsubst_r_rr_contra
     (hsubst_r_snd DsrR)
     (hsubst_rr_snd DsrrR)
     X
     <- hsubst_r_rr_contra DsrR DsrrR X.


%worlds (rtm_block) (hsubst_r_rr_contra _ _ _). %% bar in extra block for lemma below's future use
%total (D) (hsubst_r_rr_contra D _ _).


%% false implies id
false_implies_id/mtm : {M} {M'}
                        false
                        -> id/mtm M M'
                        -> type.
%mode false_implies_id/mtm +X1 +X2 +X3 -X4.
%worlds (rtm_block) (false_implies_id/mtm _ _ _ _). %% bar in extra block for lemma below's future use
%total {} (false_implies_id/mtm _ _ _ _).


hsubst_r_vacuous_id : hsubst_r M2 A2 ([_] R) R'
                     -> id/rtm R' R
                     -> type.
%mode hsubst_r_vacuous_id +X1 -X2.


hsubst_m_vacuous_id : hsubst_m M2 A2 ([_] M) M'
                     -> id/mtm M' M
                     -> type.
%mode hsubst_m_vacuous_id +X1 -X2.


%% R


- : hsubst_r_vacuous_id hsubst_r_closed id/rtm_refl.


- : hsubst_r_vacuous_id (hsubst_r_app Dm Dr) Did'
     <- hsubst_r_vacuous_id Dr DidR
     <- hsubst_m_vacuous_id Dm DidM
     <- id/rtm_app_cong DidR DidM Did'.


- : hsubst_r_vacuous_id (hsubst_r_fst D) Did'
     <- hsubst_r_vacuous_id D Did
     <- id/rtm_fst_cong Did Did'.


- : hsubst_r_vacuous_id (hsubst_r_snd D) Did'
     <- hsubst_r_vacuous_id D Did
     <- id/rtm_snd_cong Did Did'.


%% M


- : hsubst_m_vacuous_id
     (hsubst_m_r Dr)
     Did'
     <- hsubst_r_vacuous_id Dr Did
     <- id/mtm_asm_cong Did Did'.


- : hsubst_m_vacuous_id
     (hsubst_m_rr D)
     Did
     <- hsubst_rr_closed_contra D X
     <- false_implies_id/mtm _ _ X Did.


- : hsubst_m_vacuous_id
     (hsubst_m_lam D)
     Did'
     <- ({x}
           hsubst_m_vacuous_id (D x) (Did x))
     <- id/mtm_lam_cong Did Did'.


- : hsubst_m_vacuous_id
     (hsubst_m_pair D2 D1)
     Did'
     <- hsubst_m_vacuous_id D1 Did1
     <- hsubst_m_vacuous_id D2 Did2
     <- id/mtm_pair_cong Did1 Did2 Did'.


%worlds (rtm_block) (hsubst_r_vacuous_id _ _) (hsubst_m_vacuous_id _ _).
%total (D1 D2)
(hsubst_r_vacuous_id D1 _)
(hsubst_m_vacuous_id D2 _).


hsubst_m_unique : hsubst_m M2 A2 M M'
                   -> hsubst_m M2 A2 M M''
                   -> id/mtm M' M''
                   -> type.
%mode hsubst_m_unique +X1 +X2 -X3.


hsubst_r_unique : hsubst_r M2 A2 R R'
                   -> hsubst_r M2 A2 R R''
                   -> id/rtm R' R''
                   -> type.
%mode hsubst_r_unique +X1 +X2 -X3.


hsubst_rr_unique : hsubst_rr M2 A2 R M' A'
                    -> hsubst_rr M2 A2 R M'' A''
                    -> id/mtm M' M''
                    -> id/tp A' A''
                    -> type.
%mode hsubst_rr_unique +X1 +X2 -X3 -X4.


%% M


- : hsubst_m_unique
     (hsubst_m_r Dsr)
     (hsubst_m_r Dsr')
     DidAsm
     <- hsubst_r_unique Dsr Dsr' DidR
     <- id/mtm_asm_cong DidR DidAsm.


- : hsubst_m_unique
     (hsubst_m_rr Dsr)
     (hsubst_m_rr Dsr')
     Did
     <- hsubst_rr_unique Dsr Dsr' Did _.


%% contradict mismatch
- : hsubst_m_unique
     (hsubst_m_r Dsr)
     (hsubst_m_rr Dsrr)
     Did
     <- hsubst_r_rr_contra Dsr Dsrr X
     <- false_implies_id/mtm _ _ X Did.


%% contradict mismatch
- : hsubst_m_unique
     (hsubst_m_rr Dsrr)
     (hsubst_m_r Dsr)
     Did
     <- hsubst_r_rr_contra Dsr Dsrr X
     <- false_implies_id/mtm _ _ X Did.


- : hsubst_m_unique
     (hsubst_m_pair DsRight DsLeft)
     (hsubst_m_pair DsRight' DsLeft')
     DidPair
     <- hsubst_m_unique DsLeft DsLeft' DidLeft
     <- hsubst_m_unique DsRight DsRight' DidRight
     <- id/mtm_pair_cong DidLeft DidRight DidPair.


- : hsubst_m_unique
     (hsubst_m_lam Ds)
     (hsubst_m_lam Ds')
     DidLam
     <- ({y:rtm} hsubst_m_unique (Ds y) (Ds' y) (Did y))
     <- id/mtm_lam_cong Did DidLam.


%% R non-root


- : hsubst_r_unique D D id/rtm_refl.


- : hsubst_r_unique
     (hsubst_r_closed : hsubst_r M2 A2 ([_] R) R)
     (D : hsubst_r M2 A2 ([_] R) R')
     Did'
     <- hsubst_r_vacuous_id D Did
     <- id/rtm_sym Did Did'.


- : hsubst_r_unique
     (D : hsubst_r M2 A2 ([_] R) R')
     (hsubst_r_closed : hsubst_r M2 A2 ([_] R) R)
     Did
     <- hsubst_r_vacuous_id D Did.


- : hsubst_r_unique
     (hsubst_r_app DsM' DsR')
     (hsubst_r_app DsM'' DsR'')
     DidApp
     <- hsubst_r_unique DsR' DsR'' DidR
     <- hsubst_m_unique DsM' DsM'' DidM
     <- id/rtm_app_cong DidR DidM DidApp.


- : hsubst_r_unique
     (hsubst_r_fst DsR')
     (hsubst_r_fst DsR'')
     DidFst
     <- hsubst_r_unique DsR' DsR'' DidR
     <- id/rtm_fst_cong DidR DidFst.
- : hsubst_r_unique
     (hsubst_r_snd DsR')
     (hsubst_r_snd DsR'')
     DidSnd
     <- hsubst_r_unique DsR' DsR'' DidR
     <- id/rtm_snd_cong DidR DidSnd.


%% R root


- : hsubst_rr_unique
     hsubst_rr_var
     hsubst_rr_var
     id/mtm_refl
     id/tp_refl.


- : hsubst_rr_unique
     (hsubst_rr_app DsM4' DsM3 DsR1)
     (hsubst_rr_app DsM4'-2 DsM3-2 DsR1-2)
     DidM4''
     DidA4
     <- hsubst_rr_unique DsR1 DsR1-2 DidLam DidArrow
     <- hsubst_m_unique DsM3 DsM3-2 DidM3'
     <- id/tp_arrow_inv DidArrow DidA3 DidA4
     <- id/mtm_lam_inv DidLam DidM4'
     <- hsubst_m_respects_id DidM3' DidA3 DidM4' DsM4' DsM4'-1
     <- hsubst_m_unique DsM4'-1 DsM4'-2 DidM4''.


- : hsubst_rr_unique
     (hsubst_rr_fst DsR')
     (hsubst_rr_fst DsR'')
     DidMl
     DidAl
     <- hsubst_rr_unique DsR' DsR'' DidPair DidProd
     <- id/tp_prod_inv DidProd DidAl _
     <- id/mtm_pair_inv DidPair DidMl _.


- : hsubst_rr_unique
     (hsubst_rr_snd DsR')
     (hsubst_rr_snd DsR'')
     DidMr
     DidAr
     <- hsubst_rr_unique DsR' DsR'' DidPair DidProd
     <- id/tp_prod_inv DidProd _ DidAr
     <- id/mtm_pair_inv DidPair _ DidMr.


%worlds (rtm_block)
(hsubst_m_unique _ _ _)
(hsubst_r_unique _ _ _)
(hsubst_rr_unique _ _ _ _).


%total (D1 D2 D3)
(hsubst_r_unique D2 _ _)
(hsubst_rr_unique D3 _ _ _)
(hsubst_m_unique D1 _ _).


expand_exists : {A}
                 atom R A
                 -> expand A R M
                 -> canon M A
                 -> type.
%mode expand_exists +X0 +X1 -X2 -X3.


- : expand_exists
     b
     D
     expand_b
     (canon_asm D).


- : expand_exists
     (arrow A2 A)
     DaR
     (expand_arrow DeApp DeX)
     (canon_lam DcApp)
     <- ({x : rtm}
           {dx : atom x A2}
           expand_exists A2 dx (DeX x) (DcM x dx))
     <- ({x : rtm}
           {dx : atom x A2}
           expand_exists A (atom_app (DcM x dx) DaR) (DeApp x) (DcApp x dx)).


- : expand_exists
     (prod A1 A2)
     DaR
     (expand_prod DeS DeF)
     (canon_pair DcS DcF)
     <- expand_exists A1 (atom_fst DaR) DeF DcF
     <- expand_exists A2 (atom_snd DaR) DeS DcS.


%worlds (atom_block) (expand_exists _ _ _ _).
%total D (expand_exists D _ _ _).


expand_unique : expand A R M
                 -> expand A R M'
                 -> id/mtm M M'
                 -> type.
%mode expand_unique +X1 +X2 -X3.


- : expand_unique
     expand_b
     expand_b
     id/mtm_refl.


- : expand_unique
     (expand_arrow
        (DeApp : {x : rtm} expand A (app R (Mx x)) (MApp x))
        (DeX : {x : rtm} expand A2 x (Mx x)))
      (expand_arrow
         (DeApp' : {x : rtm} expand A (app R (Mx' x)) (MApp' x))
         (DeX' : {x : rtm} expand A2 x (Mx' x)))
     DidLam
     <- ({x : rtm}
           expand_unique (DeX x) (DeX' x) (DidX x))
     <- ({x : rtm}
           id/rtm_app_cong (id/rtm_refl : id/rtm R R) (DidX x) (DidApp x))
     <- ({x : rtm}
           expand_respects_id (DidApp x) id/mtm_refl (DeApp x) (DeApp-2 x))
     <- ({x : rtm}
           expand_unique (DeApp-2 x) (DeApp' x) (DidAppExp x))
     <- id/mtm_lam_cong DidAppExp DidLam.


- : expand_unique
     (expand_prod DeS DeF)
     (expand_prod DeS' DeF')
     DidPair
     <- expand_unique DeF DeF' DidF
     <- expand_unique DeS DeS' DidS
     <- id/mtm_pair_cong DidF DidS DidPair.


%worlds (rtm_block) (expand_unique _ _ _).
%total D (expand_unique _ D _).


 ## External language: syntax and judgements


### Syntax


The external language syntax is a copy of the internal language, where we additionally include canonincal terms `M` into atomic terms `R`.  To preserve the modes of the typing judgements, these canonical terms are annotated with the type that they should be checked against.


el_rtm : type.
el_mtm : type.


el_app : el_rtm -> el_mtm -> el_rtm.
el_c : el_rtm.
el_fst : el_rtm -> el_rtm.
el_snd : el_rtm -> el_rtm.
el_annot : el_mtm -> tp -> el_rtm.


el_asm : el_rtm -> el_mtm.
el_lam : (el_rtm -> el_mtm) -> el_mtm.
el_pair : el_mtm -> el_mtm -> el_mtm.


%block el_rtm_block : block {x : el_rtm}.


 Modulo the placement of type annotations, this grammar lets you write any term that you can write without the syntactic stratification.


### Typing judgements


The typing judgements for the external language extand the judgements for canonical forms with a rule `synth_annot` for synthesizing the type of an annotated term.  Additionally, the rules do not force terms to be η-long.


synth : el_rtm -> tp -> type.
%mode synth +X1 -X2.
check : el_mtm -> tp -> type.
%mode check +X1 +X2.


% synthesize


synth_c : synth el_c b.


synth_app : synth (el_app R1 M2) A
             <- synth R1 (arrow A2 A)
             <- check M2 A2.


synth_fst : synth (el_fst R) A1
             <- synth R (prod A1 A2).


synth_snd : synth (el_snd R) A2
             <- synth R (prod A1 A2).


%% admit non-canonical forms with an annotation
synth_annot : synth (el_annot M A) A
               <- check M A.


%% check


%% in the EL anything that synths also checks, no matter the type
check_asm : check (el_asm R) A
             <- synth R A.


check_lam : check (el_lam M) (arrow A2 A)
             <- ({x : el_rtm} (synth x A2) -> check (M x) A).


check_pair : check (el_pair M1 M2) (prod A1 A2)
              <- check M1 A1
              <- check M2 A2.


%block synth_block : some {A:tp} block {x : el_rtm} {dx : synth x A}.
%worlds (synth_block) (synth _ _) (check _ _).


 It is possible to show that any well-typed term in a standard presentation of the λ-calculus can be translated into a term in this syntax that is well-typed by these rules.  However, we have not formulated this step here, choosing instead to take these rules as the definition of the external language.


### Elaboration


We now define elaboration.  We define three mutually recursive elaboration judgements, one for checked terms, and two for synthesizing terms.  The two judgements for synthesizing terms differ in whether the elaboration of the synthesizing term is an atomic term or a canonical term.


elab_m : el_mtm -> mtm -> tp -> type.
%mode elab_m +X1 -X2 +X3.


elab_r_to_r : el_rtm -> rtm -> tp -> type.
%mode elab_r_to_r +X1 -X2 -X3.


elab_r_to_m : el_rtm -> mtm -> tp -> type.
%mode elab_r_to_m +X1 -X2 -X3.


% M


elab_m_asm_r2r : elab_m (el_asm ER) M A
                  <- elab_r_to_r ER R A
                  <- expand A R M.


elab_m_asm_r2m : elab_m (el_asm ER) M A
                  <- elab_r_to_m ER M A.


elab_m_lam : elab_m (el_lam EM) (lam M) (arrow A2 A)
              <- ({el_x : el_rtm} {x : rtm}
                    (elab_r_to_r el_x x A2)
                    -> elab_m (EM el_x) (M x) A).


elab_m_pair : elab_m (el_pair EM1 EM2) (pair M1 M2) (prod A1 A2)
               <- elab_m EM1 M1 A1
               <- elab_m EM2 M2 A2.


% R to R


elab_r_to_r_c : elab_r_to_r el_c c b.


elab_r_to_r_app : elab_r_to_r (el_app ER1 EM2) (app R1 M2) A
                   <- elab_r_to_r ER1 R1 (arrow A2 A)
                   <- elab_m EM2 M2 A2.


elab_r_to_r_fst : elab_r_to_r (el_fst ER) (fst R) A1
                   <- elab_r_to_r ER R (prod A1 A2).


elab_r_to_r_snd : elab_r_to_r (el_snd ER) (snd R) A2
                   <- elab_r_to_r ER R (prod A1 A2).


% R root


elab_r_to_m_annot : elab_r_to_m (el_annot EM A) M A
                     <- elab_m EM M A.


elab_r_to_m_app : elab_r_to_m (el_app ER1 EM2) M' A
                   <- elab_r_to_m ER1 (lam M) (arrow A2 A)
                   <- elab_m EM2 M2 A2
                   <- hsubst_m M2 A2 M M'.


elab_r_to_m_fst : elab_r_to_m (el_fst ER) M1 A1
                   <- elab_r_to_m ER (pair M1 M2) (prod A1 A2).


elab_r_to_m_snd : elab_r_to_m (el_snd ER) M2 A2
                   <- elab_r_to_m ER (pair M1 M2) (prod A1 A2).


%block elab_block : some {A:tp}
                     block
                     {el_x : el_rtm}
                     {x : rtm}
                     {dex : elab_r_to_r el_x x A}.


 The inductive structure of the elaboration judgements is similar to the structure of hereditary substitution.  Elaboration uses hereditary substitution in the key rule `elab_r_to_m_app` to compute the canonical result of a function application.  Elaboration also uses expansion to expand atomic terms into canonical ones.


## External Language: Metatheory


### Static Correctness of Elaboration


First, we prove that the elaboration of a well-typed term is well-typed.


elab_m_reg : elab_m EM M A
        -> check EM A
        -> canon M A
        -> type.
%mode elab_m_reg +X1 -X2 -X3.


elab_r2r_reg : elab_r_to_r ER R A
     -> synth ER A
     -> atom R A
     -> type.
%mode elab_r2r_reg +X1 -X2 -X3.


elab_r2m_reg : elab_r_to_m ER M A
    -> synth ER A
    -> canon M A
    -> type.
%mode elab_r2m_reg +X1 -X2 -X3.


%% M to M


- : elab_m_reg
     (elab_m_asm_r2r Dex Del)
     (check_asm DsynER)
     DcanM
     <- elab_r2r_reg Del DsynER DaR
     <- expand_exists _ DaR Dex-2 DcanM-2
     <- expand_unique Dex-2 Dex Did
     <- canon_respects_id Did id/tp_refl DcanM-2 DcanM.


- : elab_m_reg
     (elab_m_asm_r2m Del)
     (check_asm DsynER)
     DcanM
     <- elab_r2m_reg Del DsynER DcanM.


- : elab_m_reg
     (elab_m_lam Del)
     (check_lam Dcheck)
     (canon_lam Dcanon)
     <- ({el_x : el_rtm}
     {delx : synth el_x A}
     {x : rtm}
     {dx : atom x A}
     {delabx : elab_r_to_r el_x x A}
     {_ : elab_r2r_reg delabx delx dx}
     elab_m_reg (Del el_x x delabx) (Dcheck el_x delx) (Dcanon x dx)).


- : elab_m_reg
     (elab_m_pair De2 De1)
     (check_pair Dcheck2 Dcheck1)
     (canon_pair Dcanon2 Dcanon1)
     <- elab_m_reg De2 Dcheck2 Dcanon2
     <- elab_m_reg De1 Dcheck1 Dcanon1.


%% R to R


- : elab_r2r_reg
     elab_r_to_r_c
     synth_c
     atom_c.


- : elab_r2r_reg
     (elab_r_to_r_app De2 De1)
     (synth_app Dcheck2 Dsynth1)
     (atom_app Dcanon2 Datom1)
     <- elab_m_reg De2 Dcheck2 Dcanon2
     <- elab_r2r_reg De1 Dsynth1 Datom1.


- : elab_r2r_reg
     (elab_r_to_r_fst De1)
     (synth_fst Dsynth1)
     (atom_fst Datom1)
     <- elab_r2r_reg De1 Dsynth1 Datom1.


- : elab_r2r_reg
     (elab_r_to_r_snd De1)
     (synth_snd Dsynth1)
     (atom_snd Datom1)
     <- elab_r2r_reg De1 Dsynth1 Datom1.


%% R to M


- : elab_r2m_reg
     (elab_r_to_m_annot De)
     (synth_annot DcheckM)
     DcanonM
     <- elab_m_reg De DcheckM DcanonM.


- : elab_r2m_reg
     (elab_r_to_m_app DsubstM2 DeM2 DeR1)
     (synth_app DcheckM2 DsynthR1)
     DcanonM'
     <- elab_r2m_reg DeR1 DsynthR1 (canon_lam DcanonM)
     <- elab_m_reg DeM2 DcheckM2 DcanonM2
     <- hsubst_m_exists _ DcanonM DcanonM2 DsubstM2-2 DcanonM'-2
     <- hsubst_m_unique DsubstM2-2 DsubstM2 Did
     <- canon_respects_id Did id/tp_refl DcanonM'-2 DcanonM'.


- : elab_r2m_reg
     (elab_r_to_m_fst DeR)
     (synth_fst DsynthR)
     DcM1
     <- elab_r2m_reg DeR DsynthR (canon_pair DcM2 DcM1).


- : elab_r2m_reg
     (elab_r_to_m_snd DeR)
     (synth_snd DsynthR)
     DcM2
     <- elab_r2m_reg DeR DsynthR (canon_pair DcM2 DcM1).




%% because world subsumption doesn't do exchange,
%% you can't get this block to match both
%% atom_block/synth_block and elab_block.
%%
%% this order matches atom_block/synth_block but not elab_block.
%block elab_reg_block : some {A:tp}
                         block
                         {el_x : el_rtm}
                         {delx : synth el_x A}
                         {x : rtm}
                         {dx : atom x A}
                         {delabx : elab_r_to_r el_x x A}
                         {_ : elab_r2r_reg delabx delx dx}.




%worlds (elab_reg_block)
(elab_m_reg _ _ _)
(elab_r2r_reg _ _ _)
(elab_r2m_reg _ _ _).


%total (D1 D2 D3)
(elab_m_reg D1 _ _)
(elab_r2r_reg D2 _ _)
(elab_r2m_reg D3 _ _).


 The proof is a straightforward induction, using `hsubst_m_exists` and `expand_exists`.  Because these two lemmas _output_ a hereditary substitution or expansion, along with the typing derivation for the result of the operation, we use uniqueness here to show well-typedness of the outputs of the hereditary substitution and expansion derivations given by elaboration.  In retrospect, we should have factored this reasoning into separate lemmas that are like `hsubst_m_exists` and `expand_exists` but take the the hereditary substitution or expansion as an input.


### Existence of elaboration


We require one addtional [respects lemma](/wiki/respects-lemma/).


elab_r2m_respects_id :  id/mtm M M'
      -> id/tp A A'
      -> elab_r_to_m R M A
      -> elab_r_to_m R M' A'
      -> type.
%mode elab_r2m_respects_id +X1 +X2 +X3 -X4.


- : elab_r2m_respects_id _ _ D D.


%worlds (elab_block | elab_reg_block) (elab_r2m_respects_id _ _ _ _).  %% bar in other block
%total {} (elab_r2m_respects_id _ _ _ _).
%reduces D1 = D2 (elab_r2m_respects_id _ _ D2 D1).


 The worlds of this lemma require a little explanation.  `elab_reg_block` should equal `elab_block` for this type family.  However, [world subsumption](/wiki/world-subsumption/) does not notice this relationship because doing so would require permutation.  Consequently, we prove the theorem for both blocks directly.


Next, we prove that all well-typed terms elaborate.  Analogously to hereditary substitution, the theorem for synthesizing terms computes a sum of the two ways it could elaborate:


elab_r_exists_sum : el_rtm -> tp -> type.
elab_r_exists_sum_r2r : elab_r_exists_sum ER A
                         <- elab_r_to_r ER R A.
elab_r_exists_sum_r2m : elab_r_exists_sum ER A
                         <- elab_r_to_m ER M A.


 We begin with some [output factoring](/wiki/output-factoring/) and [canonical forms](/wiki/canonical-form/) lemmas:


elab_m_exists_asm : elab_r_exists_sum ER A
         -> elab_m (el_asm ER) M' A
         -> type.
%mode elab_m_exists_asm +X1 -X2.


- : elab_m_exists_asm
     (elab_r_exists_sum_r2m DeR)
     (elab_m_asm_r2m DeR).


- : elab_m_exists_asm
     (elab_r_exists_sum_r2r DeR)
     (elab_m_asm_r2r Dex DeR)
     <- elab_r2r_reg DeR _ DaR
     <- expand_exists _ DaR Dex _.


%worlds (elab_reg_block) (elab_m_exists_asm _ _).
%total {} (elab_m_exists_asm _ _).




canon_prod_is_pair : canon M (prod A1 A2)
          -> id/mtm M (pair M1 M2)
          -> type.
%mode canon_prod_is_pair +X1 -X2.


- : canon_prod_is_pair _ id/mtm_refl.


%worlds (elab_reg_block) (canon_prod_is_pair _ _).
%total {} (canon_prod_is_pair _ _).


elab_r_exists_fst : elab_r_exists_sum R (prod A1 A2)
         -> elab_r_exists_sum (el_fst R) A1
         -> type.
%mode elab_r_exists_fst +X1 -X2.


- : elab_r_exists_fst
     (elab_r_exists_sum_r2r DeR)
     (elab_r_exists_sum_r2r (elab_r_to_r_fst DeR)).


- : elab_r_exists_fst
     (elab_r_exists_sum_r2m DeR)
     (elab_r_exists_sum_r2m (elab_r_to_m_fst DeR-2))
     <- elab_r2m_reg DeR _ DcM
     <- canon_prod_is_pair DcM Did
     <- elab_r2m_respects_id Did id/tp_refl DeR DeR-2.


%worlds (elab_reg_block) (elab_r_exists_fst _ _).
%total {} (elab_r_exists_fst _ _).


elab_r_exists_snd : elab_r_exists_sum R (prod A1 A2)
         -> elab_r_exists_sum (el_snd R) A2
         -> type.
%mode elab_r_exists_snd +X1 -X2.


- : elab_r_exists_snd
     (elab_r_exists_sum_r2r DeR)
     (elab_r_exists_sum_r2r (elab_r_to_r_snd DeR)).


- : elab_r_exists_snd
     (elab_r_exists_sum_r2m DeR)
     (elab_r_exists_sum_r2m (elab_r_to_m_snd DeR-2))
     <- elab_r2m_reg DeR _ DcM
     <- canon_prod_is_pair DcM Did
     <- elab_r2m_respects_id Did id/tp_refl DeR DeR-2.


%worlds (elab_reg_block) (elab_r_exists_snd _ _).
%total {} (elab_r_exists_snd _ _).




canon_arrow_is_lam : canon M (arrow A2 A)
          -> id/mtm M (lam M')
          -> type.
%mode canon_arrow_is_lam +X1 -X2.


- : canon_arrow_is_lam _ id/mtm_refl.


%worlds (elab_reg_block) (canon_arrow_is_lam _ _).
%total {} (canon_arrow_is_lam _ _).


elab_r_exists_app : elab_r_exists_sum ER1 (arrow A2 A)
         -> elab_m EM2 M2 A2
         -> elab_r_exists_sum (el_app ER1 EM2) A
         -> type.
%mode elab_r_exists_app +X1 +X2 -X3.


- : elab_r_exists_app
     (elab_r_exists_sum_r2r DeR1)
     DeM2
     (elab_r_exists_sum_r2r (elab_r_to_r_app DeM2 DeR1)).


- : elab_r_exists_app
     (elab_r_exists_sum_r2m DeR1)
     DeM2
     (elab_r_exists_sum_r2m (elab_r_to_m_app Ds DeM2 DeR1-2))
     <- elab_r2m_reg DeR1 _ DcM1
     <- elab_m_reg DeM2 _ DcM2
     <- canon_arrow_is_lam DcM1 Did
     <- canon_respects_id Did id/tp_refl DcM1 (canon_lam DcBody)
     <- elab_r2m_respects_id Did id/tp_refl DeR1 DeR1-2
     <- hsubst_m_exists _ DcBody DcM2 Ds _.


%worlds (elab_reg_block) (elab_r_exists_app _ _ _).
%total {} (elab_r_exists_app _ _ _).


 Finally, we prove the main results:


elab_m_exists : check EM A
     -> elab_m EM M A
     -> type.
%mode elab_m_exists +X1 -X2.


elab_r_exists : synth ER A
      -> elab_r_exists_sum ER A
      -> type.
%mode elab_r_exists +X1 -X2.


%% M


- : elab_m_exists
     (check_asm Dsyn)
     DeRes
     <- elab_r_exists Dsyn Dsum
     <- elab_m_exists_asm Dsum DeRes.


- : elab_m_exists
     (check_lam DcM)
     (elab_m_lam DelabM)
     <- ({el_x : el_rtm}
     {delx : synth el_x A}
     {x : rtm}
     {dx : atom x A}
     {delabx : elab_r_to_r el_x x A}
     {_ : elab_r2r_reg delabx delx dx}
     {_ : elab_r_exists delx (elab_r_exists_sum_r2r delabx)}
     elab_m_exists (DcM el_x delx) (DelabM el_x x delabx)).


- : elab_m_exists
     (check_pair Dc2 Dc1)
     (elab_m_pair De2 De1)
     <- elab_m_exists Dc1 De1
     <- elab_m_exists Dc2 De2.


%% R


- : elab_r_exists
     synth_c
     (elab_r_exists_sum_r2r elab_r_to_r_c).


- : elab_r_exists
     (synth_app DchM DsynR)
     DsumApp
     <- elab_r_exists DsynR DsumR
     <- elab_m_exists DchM DeM
     <- elab_r_exists_app DsumR DeM DsumApp.




- : elab_r_exists
     (synth_fst Dsyn)
     Dsum'
     <- elab_r_exists Dsyn Dsum
     <- elab_r_exists_fst Dsum Dsum'.


- : elab_r_exists
     (synth_snd Dsyn)
     Dsum'
     <- elab_r_exists Dsyn Dsum
     <- elab_r_exists_snd Dsum Dsum'.


- : elab_r_exists
     (synth_annot DcM)
     (elab_r_exists_sum_r2m (elab_r_to_m_annot DeM))
     <- elab_m_exists DcM DeM.


% maintains all the invariants from elab_reg_block because the above lemmas use call regularity
%block elab_exists_block : some {A:tp}
                            block
                            {el_x : el_rtm}
                            {delx : synth el_x A}
                            {x : rtm}
                            {dx : atom x A}
                            {delabx : elab_r_to_r el_x x A}
                            {_ : elab_r2r_reg delabx delx dx}
                            {_ : elab_r_exists delx (elab_r_exists_sum_r2r delabx)}.
%worlds (elab_exists_block)
(elab_m_exists _ _)
(elab_r_exists _ _).


%total (D1 D2)
(elab_m_exists D1 _)
(elab_r_exists D2 _).

This page was copied from the MediaWiki version of the STELF Wiki. If anything looks wrong, you can refer to the wayback machine’s version here.