mm0.mm1

import "peano_hex.mm1";

-- The sort modifiers 'pure', 'strict', 'provable', 'free'

--| `sPure : SortData -> Bool`
@_ def sPure     (n: nat): wff = $ true (pi11 n) $;
--| `sStrict : SortData -> Bool`
@_ def sStrict   (n: nat): wff = $ true (pi12 n) $;
--| `sProvable : SortData -> Bool`
@_ def sProvable (n: nat): wff = $ true (pi21 n) $;
--| `sFree : SortData -> Bool`
@_ def sFree     (n: nat): wff = $ true (pi22 n) $;

-- A binder is either a bound variable with sort s, or a regular variable
-- with sort s and dependencies vs.

--| `PBound : SortID -> Binder`
@_ def PBound (s: nat): nat = $ b0 s $;
--| `PReg : SortID -> set VarID -> Binder`
@_ def PReg (s vs: nat): nat = $ b1 (s, vs) $;

--| Get the sort of a binder.
--|
--| `binderSort : Binder -> SortID`
@_ def binderSort (x: nat): nat =
$ case (\ n, n) (\ n, fst n) @ x $;
pub theorem binderSortBound (s: nat): $ binderSort (PBound s) = s $ =
(named '(eqtr casel @ applame id));
pub theorem binderSortReg (s vs: nat): $ binderSort (PReg s vs) = s $ =
(named '(eqtr caser @ applame @ syl6eq fstpr fsteq));

theorem binderSort_leid: $ binderSort bi <= bi $ =
'(eori
  (mpbiri b0leid (leeqd (syl6eq binderSortBound binderSorteq) id))
  (mpbiri (leb1tr fstleid)
    (leeqd (syl6eq binderSortReg @ binderSorteqd @ syl6eqr (b1eq fstsnd) id) id)) b0orb1);

-- An s-expression, representing the terms and formulas. It can be either a
-- variable (v is a VarID) or an application of the term with TermID `f`
-- to arguments `x` (a list of s-expressions).

--| `SVar : VarID -> SExpr`
@_ def SVar (v: nat): nat = $ b0 v $;
--| `SApp : TermID -> list SExpr -> SExpr`
@_ def SApp (f x: nat): nat = $ b1 (f, x) $;

theorem SApp_ltid: $ e IN es -> e < SApp f es $ =
'(rsyl lmemlt @ mpi (ltb1tr leprid2) lttr);

@_ local def SExprRec (V F: set): set =
$ \ e, srec (\ ih, case V (\\ f, \ x, F @ (f, x, map ih x)) @ size (Dom ih)) e $;

theorem SExprRec_val: $ SExprRec V F @ e =
  case V (\\ f, \ x, F @ (f, x, map (SExprRec V F |` upto e) x)) @ e $ =
(named '(eqtr (applame sreceq2) @
  ! eqtr _ $ _ @ lower (SExprRec V F |` _) $ _ srecval @
  applame @ appeqd
    (caseeq2d @ slameqd @ lameqd @ appeq2d @ preq2d @
      preq2d @ mapeq1d @ bi2 @ eqlower2 @ finlam finns)
    sreclem));

theorem SExprRec_Var: $ SExprRec V F @ SVar v = V @ v $ =
(named '(eqtr SExprRec_val casel));
theorem SExprRec_App:
  $ SExprRec V F @ SApp f es = F @ (f, es, map (SExprRec V F) es) $ =
(named '(eqtr SExprRec_val @ eqtr caser @
  appslame @ applamed @ appeq2d @ preqd anl @ preqd anr @ syl6eq
    (mapeqg @ mpbir allal @ !! ax_gen e @ syl resapp @ sylibr elupto SApp_ltid)
    (mapeq2d anr)));

theorem indd_aux (G p: wff x) (e: $ x = b -> (p <-> q) $)
  (h: $ G /\ a = b -> q $): $ G /\ a = b -> [a / x] p $ =
'(mpbird (syl6bb (sbe e) @ anwr sbeq1) h);

theorem SExpr_indd {x f es} (n) (px: wff x) (pv: wff v) (pe: wff f es)
  (hn: $ x = n -> (px <-> pn) $)
  (hv: $ x = SVar v -> (px <-> pv) $)
  (he: $ x = SApp f es -> (px <-> pe) $)
  (h1: $ G -> pv $) (h2: $ G /\ all {x | px} es -> pe $): $ G -> pn $ =
(focus
  '(sylib (sbe hn) @ !! indstr z w sbeq1 sbeq1 _)
  (split-sop '{
    ($SVar v$ => (indd_aux hv @ anwll h1)) +
    ($SApp f es$ => (indd_aux he @ sylan h2 anll @
      sylibr (alleq1 cbvabs) @ sylibr allal @ sylc _ anr anlr))
  })
  '(alimd @ imim1d @ syl5 SApp_ltid @ bi2d lteq2));

-- The environment is composed of declarations, which come in a few types:

--| A `sort` declaration has an associated `SortData` with the sort modifiers.
--| Sorts are indexed by SortID and picked out by `getSD`.
--|
--| `DSort : SortID -> SortData -> Decl`
@_ def DSort (id sd: nat): nat = $ b0 (b0 (b0 (id, sd))) $;
--| A `term` declaration has a list of binders, and a target type (a DepType,
--| which is a `(SortID, set VarID)` pair).
--| Terms are indexed by TermID and picked out by `getTerm`.
--|
--| `DTerm : TermID -> Ctx -> DepType -> Decl`
@_ def DTerm (id args ret: nat): nat = $ b0 (b0 (b1 (id, args, ret))) $;
--| An `axiom` declaration has a list of binders, a list of hypotheses,
--| and a consequent.
--|
--| Axioms are not indexed, they are simply found by statement.
--|
--| `DAxiom : Ctx -> list SExpr -> SExpr -> Decl`
@_ def DAxiom (args hs ret: nat): nat = $ b0 (b1 (args, hs, ret)) $;
--| A `def` declaration is the same as a `term` except it also has an optional
--| definition component which lists the sorts of the dummy variables and the
--| definition's expression.
--|
--| Defs are indexed by TermID and picked out by `getTerm`.
--|
--| `DDef : TermID -> Ctx -> DepType -> option (list SortID, SExpr) -> Decl`
@_ def DDef (id args ret def: nat): nat =
  $ b1 (b0 (id, args, ret, def)) $;
--| A `theorem` declaration is exactly the same structure as an `axiom`, but
--| the interpretation is different - theorems require proofs, while axioms are
--| added in the spec.
--|
--| Theorems are not indexed, they are simply found by statement.
--|
--| `DThm : Ctx -> list SExpr -> SExpr -> Decl`
@_ def DThm (vs hs ret: nat): nat = $ b1 (b1 (vs, hs, ret)) $;

--| This function extracts the `SortData` for a sort given by `SortID`.
--|
--| `getSD : Env -> SortID -> SortData -> Bool`
@_ def getSD (env id sd: nat): wff = $ DSort id sd IN env $;

--| This function gets the term and definition data for a term.
--|
--| `getTerm : Env -> TermID -> Ctx -> DepType -> option (list SortID, SExpr) -> Bool`
@_ def getTerm (env id a r v: nat): wff =
$ v = 0 /\ DTerm id a r IN env \/ DDef id a r v IN env $;

theorem getTerm_ltid: $ getTerm env x a r v -> x < env /\ a < env /\ r < env /\ v < env $ =
(focus
  '(eor _ _)
  (focus
    '(imp @ syl5 (rsyl lmemlt @ lelttr @ leb0tr @ leb0tr b1leid) @
      mpbiri _ (imeq2d @ aneq2d lteq1))
    '(iand (iand (iand _ _) _) (lelttr le01))
    '(lelttr leprid1)
    '(lelttr @ lepr2tr leprid1)
    '(lelttr @ lepr2tr leprid2))
  (focus
    '(rsyl lmemlt @ rsyl (lelttr @ leb1tr b0leid) _)
    '(iand (iand (iand _ _) _) _)
    '(lelttr leprid1)
    '(lelttr @ lepr2tr leprid1)
    '(lelttr @ lepr2tr @ lepr2tr leprid1)
    '(lelttr @ lepr2tr @ lepr2tr leprid2)));

theorem getTerm_retltid: $ getTerm env x a r v -> r < env $ = '(rsyl getTerm_ltid anlr);
theorem getTerm_valltid: $ getTerm env x a r v -> v < env $ = '(rsyl getTerm_ltid anr);

--| This function gets the data for an axiom or theorem.
--|
--| `getThm : Env -> Ctx -> list SExpr -> SExpr -> Bool`
@_ def getThm (env a h r: nat): wff =
$ DAxiom a h r IN env \/ DThm a h r IN env $;

--| Is this ID a valid sort?
--|
--| `isSort : Env -> SortID -> Bool`
@_ def isSort (env s .sd: nat): wff = $ E. sd getSD env s sd $;

--| Looks this variable up in the context, and reports whether it represents a
--| bound variable.
--|
--| `isBound : Ctx -> VarID -> Bool`
@_ def isBound (ctx x .s: nat): wff = $ E. s nth x ctx = suc (PBound s) $;

--| Checks if this a well formed dependent type in the context. A DepType is a
--| pair (SortID, set VarID) giving the sort and the variable dependencies.
--|
--| `DepType : Env -> Ctx -> DepType -> Bool`
@_ def DepType (env ctx ty .x: nat): wff =
$ isSort env (fst ty) /\ A. x (x e. snd ty -> isBound ctx x) $;

@_ local def Ctx_aux (env ctx: nat): nat =
$ rlrec 1 (\\ ctx2, \\ bi, \ ih, ih * nat (bi e. Sum
    {s | E. sd (getSD env s sd /\ ~ sStrict sd)}
    {svs | DepType env ctx2 svs})) ctx $;
theorem Ctx_aux0 (env: nat): $ Ctx_aux env 0 = 1 $ = (named 'rlrec0);
theorem Ctx_auxS (env: nat): $ Ctx_aux env (ctx |> bi) = Ctx_aux env ctx *
  nat (bi e. Sum
    {s | E. sd (getSD env s sd /\ ~ sStrict sd)}
    {svs | DepType env ctx svs}) $ =
(named '(! eqtr _ $ _ @ (_, _, Ctx_aux env ctx) $ _ rlrecS @
  appslame @ appslamed @ applamed @ muleqd anr @
  nateqd @ eleqd anlr @ Sumeq2d @ abeqd @ DepTypeeq2d anll));

--| Checks if this a well formed context. A context can be extended with a bound
--| variable binder if the sort of the binder is not `strict`.
--| Note `Ctx = list Binder`.
--|
--| `Ctx : Env -> Ctx -> Bool`
@_ abstract def Ctx (env ctx: nat): wff = $ true (Ctx_aux env ctx) $;
pub theorem Ctx0 (env: nat): $ Ctx env 0 $ = '(mpbir (trueeq Ctx_aux0) true1);
pub theorem CtxBound (env ctx s: nat) {sd: nat}: $ Ctx env (ctx |> PBound s) <->
  Ctx env ctx /\ E. sd (getSD env s sd /\ ~ sStrict sd) $ =
(named '(bitr (trueeq Ctx_auxS) @ bitr truemul @ aneq2i @
  bitr truenat @ bitr Suml @ elabe @ exeqd @ aneq1d getSDeq2));
pub theorem CtxReg (env ctx s vs: nat): $ Ctx env (ctx |> PReg s vs) <->
  Ctx env ctx /\ DepType env ctx (s, vs) $ =
(named '(bitr (trueeq Ctx_auxS) @ bitr truemul @ aneq2i @
  bitr truenat @ bitr Sumr @ elabe DepTypeeq3));

@_ local def ExprBi_aux (ctx e ih: nat): set = $ Sum
  {s | E. v (e = SVar v /\ nth v ctx = suc (PBound s))}
  {svs | fst svs e. ih} $;

@_ local def Expr_aux (env ctx: nat): set =
$ SExprRec
  (\ v, lower {s | E. bi (nth v ctx = suc bi /\ binderSort bi = s)})
  (\\ f, \\ xs, \ ih, lower {s | E. args E. ret E. o
    (getTerm env f args ret o /\
     zip xs ih, args e. all2 (S\ x, ExprBi_aux ctx (fst x) (snd x)) /\
     s = fst ret)}) $;

theorem Expr_aux_Var: $ Expr_aux env ctx @ SVar v =
  lower {s | E. bi (nth v ctx = suc bi /\ binderSort bi = s)} $ =
(named '(eqtr SExprRec_Var @ applame @
  lowereqd @ abeqd @ exeqd @ aneq1d @ eqeq1d @ ntheq1));

theorem Expr_aux_App: $ Expr_aux env ctx @ SApp f es =
  lower {s | E. args E. ret E. o
    (getTerm env f args ret o /\
     zip es (map (Expr_aux env ctx) es), args e. all2 (S\ x, ExprBi_aux ctx (fst x) (snd x)) /\
     s = fst ret)} $ =
(named '(eqtr SExprRec_App @
  ! appslame _ $_, map (Expr_aux _ _) _$ _ _ _ @ appslamed @ applamed @
  lowereqd @ abeqd @ exeqd @ exeqd @ exeqd @ aneq1d @ aneqd
    (getTermeq2d anll)
    (eleq1d @ preq1d @ zipeqd anlr anr)));

--| These mutually recursive functions check if an expression `e` is well-typed
--| with sort `s`, and that `e` is well-typed and valid for entry into a binder
--| `bi`. The main difference is that for an expression to be valid for a
--| BV binder, the expression must itself be a bound variable.
--|
--| `Expr : Env -> Ctx -> SExpr -> SortID -> Bool`
@_ abstract def Expr (env ctx e s: nat): wff = $ s e. Expr_aux env ctx @ e $;
--| `ExprBi : Env -> Ctx -> SExpr -> Binder -> Bool`
@_ abstract def ExprBi (env ctx e bi: nat): wff =
$ bi e. ExprBi_aux ctx e (Expr_aux env ctx @ e) $;

theorem ExprBi_aux_map:
  $ zip es (map (Expr_aux env ctx) es), args e. all2 (S\ p, ExprBi_aux ctx (fst p) (snd p)) <->
    es, args e. all2 (S\ x, {a | ExprBi env ctx x a}) $ =
(named @ focus
  (def h '(bieqd (eleq1d preq2) (eleq1d preq2)))
  '(eale ,h ,(induct '(listind) 'es _ _))
  '(ax_gen @ bitr (eleq1 @ preq1 zip01) @ bitr4 all201 all201)
  '(sylbi (cbval ,h) @ iald @
    bitr4g (bitr (eleq1 @ preq1 @ eqtr (zipeq2 mapS) zipS) all2S1) all2S1 @
    exeqd @ syl exeq @ alimi @ syl aneq2a @ exp @ aneqd (a1i _) anl)
  '(bitr4 (elsabe @ sylbir (eqeq1 fstsnd) @ sylbi prth ,eqtac) @
    elsabe @ eleq2d @ syl5eqs abid2 ,eqtac));

pub theorem ExprVar (env ctx v s: nat) {bi: nat}: $ Expr env ctx (SVar v) s <->
  E. bi (nth v ctx = suc bi /\ binderSort bi = s) $ =
(named @ focus
  '(bitr (elneq2 Expr_aux_Var) @ bitr (ellower @ subsnfin @ subsnss _ subsnsn) @
     elabe @ exeqd @ aneq2d eqeq2)
  '(mpbi ssab1 @ ax_gen @ eex @ sylibr elsn @ eqtr2d _ anr)
  '(binderSorteqd @ syl6eq sucsub1 @ subeq1d anl));

pub theorem ExprApp (env ctx f xs s: nat) {args ret o x a: nat}:
  $ Expr env ctx (SApp f xs) s <-> E. args E. ret E. o
    (getTerm env f args ret o /\
     xs, args e. all2 (S\ x, {a | ExprBi env ctx x a}) /\
     s = fst ret) $ =
(named @ focus
  '(bitr (elneq2 Expr_aux_App) @ bitr (ellower @ finss _ ltfin) @
    elabe @ exeqd @ exeqd @ exeqd @ aneqd (a1i @ aneq2i ExprBi_aux_map) eqeq1)
  '(mpbi ssab @ ax_gen @ eex @ eex @ eex @ mpbird (lteq1d anr) @ anwll @
    syl (lelttr fstleid) getTerm_retltid));

pub theorem ExprBiBound (env ctx e s: nat) {v: nat}:
  $ ExprBi env ctx e (PBound s) <->
    E. v (e = SVar v /\ nth v ctx = suc (PBound s)) $ =
(named '(bitr Suml @ elabe @ exeqd @ aneq2d @ eqeq2d @ suceqd @ PBoundeq));
pub theorem ExprBiReg (env ctx e s vs: nat):
  $ ExprBi env ctx e (PReg s vs) <-> Expr env ctx e s $ =
(named '(bitr Sumr @ elabe @ eleq1d @ syl6eq fstpr fsteq));

--| Is this a type correct expression of provable type? This is used to
--| typecheck expressions appearing in hypotheses and conclusions of
--| axiom/theorem.
--|
--| `ExprProv : Env -> Ctx -> SExpr -> Bool`
@_ def ExprProv (env ctx e .s .sd: nat): wff =
$ E. s E. sd (Expr env ctx e s /\ getSD env s sd /\ sProvable sd) $;

--| A helper function to add dummy variables to the context.
--|
--| `appendDummies : Ctx -> list SortID -> Ctx`
@_ def appendDummies (ctx ds .d: nat): nat = $ ctx ++ map (\ d, PBound d) ds $;

@_ local def HasVar_aux (ctx: nat): set =
$ SExprRec
  (\ u, lower {v | E. s nth u ctx = suc (PBound s) /\ u = v \/
     E. s E. vs (nth u ctx = suc (PReg s vs) /\ v e. vs)})
  (\\ f, \\ xs, \ ih, lower {v | E. s (s IN ih /\ v e. s)}) $;

--| Does this expression contain any occurrence of the variable `v`? This check
--| ignores bound variables, "metamath style". We use this stricter check for
--| verifying theorem applications.
--|
--| `HasVar : Ctx -> SExpr -> VarID -> Bool`
@_ abstract def HasVar (ctx e v: nat): wff = $ v e. HasVar_aux ctx @ e $;

theorem HasVar_Var: $ HasVar ctx (SVar u) v <->
  E. s nth u ctx = suc (PBound s) /\ u = v \/
    E. s E. vs (nth u ctx = suc (PReg s vs) /\ v e. vs) $ =
(named @ focus
  '(bitr (elneq2 @ eqtr SExprRec_Var @ applame @ lowereqd @ abeqd @
      oreqd (aneqd (exeqd @ eqeq1d ntheq1) eqeq1) (exeqd @ exeqd @ aneq1d @ eqeq1d ntheq1)) @
    bitr (ellower @ finss (mpbi ssab @ ax_gen _) ltfin) @
    elabe @ oreqd (aneq2d eqeq2) (exeqd @ exeqd @ aneq2d eleq1))
  '(eor
    (mpbid (lteq1d anr) @ anwl @ eex @ syl (mpi lenleid ltletr) @
      sylib nthne0 sucne0)
    (eex @ eex @ lttrd (anwr ellt) @
      anwl @ syl (lelttr @ leb1tr leprid2) @ syl lmemlt nthlmem)));

pub theorem HasVarBound (ctx u v s: nat):
  $ nth u ctx = suc (PBound s) -> (HasVar ctx (SVar u) v <-> u = v) $ =
(named '(syl5bb HasVar_Var @ bitrd
  (syl bior2 @ nexd @ nexd @ mpi b0neb1 @
    con3d @ exp @ sylib peano2 @ eqtr3d anl anrl)
  (syl bian1 @ iexe @ eqeq2d @ suceqd PBoundeq)));

pub theorem HasVarReg (ctx u v s vs: nat):
  $ nth u ctx = suc (PReg s vs) -> (HasVar ctx (SVar u) v <-> v e. vs) $ =
(named '(syl5bb HasVar_Var @ bitrd
  (syl bior1 @ syl (con3 anl) @ nexd @ mpi b0neb1 @ con3d @ exp @
    sylib peano2 @ eqtr3d anr anl)
  (syl6bb (exeqe biidd) @ exeqd @ syl6bb (exeqe @ aneq2d elneq2) @ exeqd @
    syl6bb anlass @ syl6bb anass @ aneq1d @
    syl6bb (bitr peano2 @ bitr b1can @ bitr eqcomb prth) eqeq1)));

pub theorem HasVarApp (ctx f es v: nat) {e: nat}:
  $ HasVar ctx (SApp f es) v <-> E. e (e IN es /\ HasVar ctx e v) $ =
(named @ focus
  '(bitr (elneq2 @ eqtr {SExprRec_App : $ _ = _ @ (_, _, map (HasVar_aux ctx) _) $} @
      appslame @ appslamed @ applamed @ lowereqd @ abeqd @
        exeqd @ aneq1d @ lmemeq2d anr) @
    bitr (ellower @ finss (mpbi ssab @ ax_gen _) ltfin) @
    bitr (elabe @ exeqd @ syl6bbr exan2 @ aneqd (a1i lmemmap) eleq1) @
    bitr excomb @ exeqi @ bitr (exeqi @ bitr (aneq1i ancomb) anass) @
    exeqe @ aneq2d elneq2)
  '(eex @ lttrd (anwr ellt) (anwl lmemlt)));

--| A helper function for `Free`. This constructs the set `_V \ deps(a)` if `a`
--| is a regular argument and `(/)` if `a` is a bound argument.
--|
--| `MaybeFreeArgs : list SExpr -> Binder -> VarID -> Bool`
@_ def MaybeFreeArgs (es a v .s .vs .u: nat): wff =
$ E. s E. vs (a = PReg s vs /\ ~(E. u (u e. vs /\ nth u es = suc (SVar v)))) $;

@_ local def Free_aux (env ctx v: nat): set =
$ SExprRec
  (\ u, nat (HasVar ctx (SVar u) v))
  (\\ f, \\ es, \ ih, nat (E. args E. r E. rs E. o
    (getTerm env f args (r, rs) o /\
      (ih, args e. ex2 (S\ ih1, {a | true ih1 /\ MaybeFreeArgs es a v}) \/
        E. u (u e. rs /\ nth u es = suc (SVar v)))))) $;

--| Does this expression contain any _free_ occurrence of the variable `v`?
--| This is the more complex binder-respecting check. Intuitively, if
--| `term foo {x y: set} (ph: set x): set y;`, then `foo` binds occurrences of
--| `x` in `ph`, and adds a dependency on `y` regardless. We might write this
--| as `FV(foo x y ph) = (FV(ph) \ {x}) u {y}`, but the definition below is
--| for arbitrary binding structures.
--|
--| `Free : Env -> Ctx -> SExpr -> VarID -> Bool`
@_ abstract def Free (env ctx e v: nat): wff = $ true (Free_aux env ctx v @ e) $;
pub theorem FreeVar (env ctx u v: nat):
  $ Free env ctx (SVar u) v <-> HasVar ctx (SVar u) v $ =
(named '(bitr
  (trueeq @ eqtr SExprRec_Var @ applame @ nateqd @ HasVareq2d SVareq)
  truenat));

pub theorem FreeApp (env ctx f es v: nat) {args r rs o e a u: nat}:
  $ Free env ctx (SApp f es) v <-> E. args E. r E. rs E. o
    (getTerm env f args (r, rs) o /\
      (es, args e. ex2 (S\ e, {a | Free env ctx e v /\ MaybeFreeArgs es a v}) \/
        E. u (u e. rs /\ nth u es = suc (SVar v)))) $ =
(named @ focus
  '(bitr (trueeq _) truenat)
  '(eqtr {SExprRec_App : $ _ = _ @ (_, _, map (Free_aux env ctx v) _) $} _)
  '(appslame @ appslamed @ applamed @
    nateqd @ exeqd @ exeqd @ exeqd @ exeqd @ aneqd (getTermeq2d anll) @
    oreqd _ @ exeqd @ aneq2d @ eqeq1d @ ntheq2d anlr)
  '(syl6bb _ (eleqd (preq1d anr) (ex2eqd @ sabeqd @ abeqd @ aneq2d @ MaybeFreeArgseq1d anlr)))
  '(bitr4 elex2 @ bitr4 elex2 @ aneq (eqeq1 maplen) @ exeqi @
    bitr excomb @ bitr (exeqi _) excomb)
  '(bitr (exeqi @ bitr4 (aneq1i @ bitr4 (aneq1i mapnthb) exan2) exan2) @
    bitr excomb @ exeqi @
    bitr (exeqi @ bitr (aneq1i @ bitr (aneq1i ancomb) anass) anass) @
    exeqe @ aneq2d @ bitr4g _ _ @ aneq1d trueeq)
  '(elsabe @ elabed ,eqtac) '(elsabe @ elabed ,eqtac));

--| Is this a valid term in the given environment? A term is valid if
--| the argument list is valid, the return type is valid, and the return sort
--| is not `pure` (because `pure` sorts are not allowed to have term
--| constructors).
--|
--| `TermOk : Env -> TermID -> Ctx -> DepType -> Bool`
@_ def TermOk (env id args ret .a .r .v .sd: nat): wff =
$ ~E. a E. r E. v getTerm env id a r v /\
  Ctx env args /\ DepType env args ret /\
  E. sd (getSD env (fst ret) sd /\ ~ sPure sd) $;

--| Is this a valid definition in the given environment? A definition is valid
--| if it is a valid term, and the definition typechecks, and all free variables
--| are declared in the return type. (Note in particular that dummies cannot
--| appear in the return type dependencies, so this ensures that all dummies are
--| bound by the definition.)
--|
--| `DefOk : Env -> TermID -> Ctx -> DepType -> Bool`
@_ def DefOk (env id args ret ds e .ctx .v .s .sd: nat): wff =
$ TermOk env id args ret /\ [ appendDummies args ds / ctx ]
  (Ctx env ctx /\ Expr env ctx e (fst ret) /\
    A. v (Free env ctx e v -> v e. snd ret \/
      E. sd E. s (nth v ctx = suc (PBound s) /\
        getSD env s sd /\ sFree sd))) $;

@_ local def DeclThm_aux (env: nat): set =
$ S\ args, S\ hs, {ret | Ctx env args /\ all {x | ExprProv env args x} (ret : hs)} $;

theorem DeclThm_aux_val (env args hs ret: nat) {x: nat}:
  $ args, hs, ret e. DeclThm_aux env <->
    Ctx env args /\ all {x | ExprProv env args x} (ret : hs) $ =
(named '(elsabe @ elsabed @ elabed @ aneqd (Ctxeq2d anll) @
  alleqd (abeqd @ ExprProveq2d anll) (conseqd anr anlr)));

--| Is this a valid declaration in the environment?
--|
--| `Decl : Env -> Decl -> Bool`
@_ abstract def Decl (env d: nat): wff =
$ d e. Sum
  (Sum
    (Sum
      (S\ id, {sd | ~E. sd2 getSD env id sd2})
      (S\ id, S\ args, {ret | TermOk env id args ret}))
    (DeclThm_aux env))
  (Sum
    (S\ id, S\ args, S\ ret, {o | TermOk env id args ret /\
      A. ds A. e (o = suc (ds, e) -> DefOk env id args ret ds e)})
    (DeclThm_aux env)) $;

pub theorem DeclSort (env id sd: nat) {sd2: nat}:
  $ Decl env (DSort id sd) <-> ~E. sd2 getSD env id sd2 $ =
(named '(bitr Suml @ bitr Suml @ bitr Suml @ elsabe @ elabed ,eqtac));
pub theorem DeclTerm (env id args ret: nat):
  $ Decl env (DTerm id args ret) <-> TermOk env id args ret $ =
(named '(bitr Suml @ bitr Suml @ bitr Sumr @ elsabe @ elsabed @ elabed ,eqtac));
pub theorem DeclAxiom (env args hs ret: nat) {x: nat}:
  $ Decl env (DAxiom args hs ret) <->
    Ctx env args /\ all {x | ExprProv env args x} (ret : hs) $ =
(named '(bitr Suml @ bitr Sumr DeclThm_aux_val));
pub theorem DeclDef (env id args ret: nat) {ds e o: nat}:
  $ Decl env (DDef id args ret o) <-> TermOk env id args ret /\
    A. ds A. e (o = suc (ds, e) -> DefOk env id args ret ds e) $ =
(named '(bitr Sumr @ bitr Suml @ elsabe @ elsabed @ elsabed @ elabed @
  aneqd (TermOkeqd eqidd an3l anllr anlr) @ aleqd @ aleqd @
  imeqd (eqeq1d anr) @ DefOkeqd eqidd an3l anllr anlr eqidd eqidd));
pub theorem DeclThm (env args hs ret: nat) {x: nat}:
  $ Decl env (DThm args hs ret) <->
    Ctx env args /\ all {x | ExprProv env args x} (ret : hs) $ =
(named '(bitr Sumr @ bitr Sumr DeclThm_aux_val));

@_ local def Env_aux (e: nat): nat =
$ rlrec 1 (\\ e1, \\ s, \ ih, ih * nat (Decl e1 s)) e $;

--| This defines a valid mm0 specification. These are well formed ASTs for which
--| we can assign a provability predicate.
--|
--| `Env : Env -> Bool`
@_ abstract def Env (e: nat): wff = $ true (Env_aux e) $;
pub theorem Env0: $ Env 0 $ = (named '(mpbir (trueeq rlrec0) true1));
pub theorem EnvS (e s: nat): $ Env (e |> s) <-> Env e /\ Decl e s $ =
(named '(bitr
  (trueeq @ eqtr {rlrecS : $_ = _ @ (_, _, Env_aux _)$} @
    appslame @ appslamed @ applamed @ muleqd anr @ nateqd @ Decleqd anll anlr)
  (bitr truemul @ aneq2i truenat)));

@_ local def EnvExtend_aux (e2_: nat): nat =
$ rlrec (sn 0)
    (\\ e2, \\ d, \ ih, case
      (case
        (case
          (\\ id, \ sd, lower {e1 | E. e (e1 = e |> DSort id sd /\ e e. ih)})
          (\\ id, \\ a, \ r, lower {e1 | E. e (e1 = e |> DTerm id a r /\ e e. ih)}))
        (\\ a, \\ h, \ r, lower {e1 | E. e (e1 = e |> DAxiom a h r /\ e e. ih)}))
      (case
        (\\ id, \\ a, \\ r, \ o, lower {e1 |
          E. e E. o2 ((o2 != 0 -> o2 = o) /\
            e1 = e |> DDef id a r o2 /\ e e. ih) \/
          e1 e. ih})
        (\\ a, \\ h, \ r, lower {e1 |
          E. e (e1 = e |> DThm a h r /\ e e. ih) \/
          e1 e. ih}))
      @ d)
    e2_ $;

--| `EnvExtend e1 e2` means that environment `e2` is an extension of `e1`,
--| meaning that all sorts, terms, and axioms are preserved, but abstract defs
--| may be provided definitions, and new defs and theorems can be added.
--|
--| `EnvExtend : Env -> Env -> Bool`
@_ abstract def EnvExtend (e1 e2: nat): wff = $ e1 e. EnvExtend_aux e2 $;
pub theorem EnvExtend0 (e: nat): $ EnvExtend e 0 <-> e = 0 $ =
(named '(bitr (elneq2 rlrec0) elsn));

theorem EnvExtend_lem {ih} (p: wff e1 e o2) (q: wff e o2) (A: nat o2)
  (h1: $ ih = EnvExtend_aux E2 -> case
    (case
      (case
        (\\ id, \ sd, lower {e1 | E. e (e1 = e |> DSort id sd /\ e e. ih)})
        (\\ id, \\ a, \ r, lower {e1 | E. e (e1 = e |> DTerm id a r /\ e e. ih)}))
      (\\ a, \\ h, \ r, lower {e1 | E. e (e1 = e |> DAxiom a h r /\ e e. ih)}))
    (case
      (\\ id, \\ a, \\ r, \ o, lower {e1 |
        E. e E. o2 ((o2 != 0 -> o2 = o) /\
          e1 = e |> DDef id a r o2 /\ e e. ih) \/
        e1 e. ih})
      (\\ a, \\ h, \ r, lower {e1 |
        E. e (e1 = e |> DThm a h r /\ e e. ih) \/
        e1 e. ih}))
    @ d
    = lower {e1 | p} $)
  (h2: $ e1 = E1 -> (p <-> q) $)
  (h3: $ p -> E. e E. x (x e. A /\ e1 = e |> x /\ EnvExtend e E2) \/ EnvExtend e1 E2 $):
  $ EnvExtend E1 (E2 |> d) <-> q $ =
(named @ focus
  '(bitr (elneq2 @ eqtr {rlrecS : $_ = _ @ (_, _, EnvExtend_aux _)$} @
      appslame @ appslamed @ applamed @ eqtrd (appeq2d anlr) (anwr h1)) @
    bitr (ellower _) (elabe h2))
  '(finss (mpbi ssab @ ax_gen _) @
    ! ltfin $ lower ((\ u, fst u |> snd u) |` Xp (EnvExtend_aux E2) A) + EnvExtend_aux E2 $)
  '(rsyl h3 @ eor
    (ltletrd (eex @ eex @ mpbird (lteq1d anlr) _) (a1i leaddid1))
    (ltletrd ellt (a1i leaddid2)))
  '(lelttrd (a1i leprid2) @ syl ellt @
    sylibr (ellower @ finlam @ xpfin finns finns) @
    sylibr prelres @ iand (a1i _) @ sylibr prelxp @ iand anr anll)
  '(mpbir ellam @ iexe (eqeq2d @ preqd id _) eqid)
  '(snoceqd (syl6eq fstpr fsteq) (syl6eq sndpr sndeq)));

theorem EnvExtend_lem2 (p: wff e x)
  (h: $ p -> E. e (e1 = e |> A /\ EnvExtend e E2) \/ EnvExtend e1 E2 $):
  $ p -> E. e E. x (x e. sn A /\ e1 = e |> x /\ EnvExtend e E2) \/ EnvExtend e1 E2 $ =
'(rsyl h @ orim1 @ eximi @ iexe @ aneq1d @
  bitrd (aneqd (a1i elsn) @ eqeq2d snoceq2) bian1);

pub theorem EnvExtendSort (e1 e2 id sd: nat) {e: nat}:
  $ EnvExtend e1 (e2 |> DSort id sd) <->
    E. e (e1 = e |> DSort id sd /\ EnvExtend e e2) $ =
(named '(EnvExtend_lem
  (syl5eq casel @ syl5eq casel @ syl5eq casel @ appslamed @ applamed @
    lowereqd @ abeqd @ exeqd @
    aneqd (eqeq2d @ snoceq2d @ DSorteqd anlr anr) (elneq2d anll))
  (exeqd @ aneq1d eqeq1)
  (EnvExtend_lem2 orl)));

pub theorem EnvExtendTerm (e1 e2 id a r: nat) {e: nat}:
  $ EnvExtend e1 (e2 |> DTerm id a r) <->
    E. e (e1 = e |> DTerm id a r /\ EnvExtend e e2) $ =
(named '(EnvExtend_lem
  (syl5eq casel @ syl5eq casel @ syl5eq caser @ appslamed @ appslamed @ applamed @
    lowereqd @ abeqd @ exeqd @
    aneqd (eqeq2d @ snoceq2d @ DTermeqd anllr anlr anr) (elneq2d an3l))
  (exeqd @ aneq1d eqeq1)
  (EnvExtend_lem2 orl)));

pub theorem EnvExtendAxiom (e1 e2 a h r: nat) {e: nat}:
  $ EnvExtend e1 (e2 |> DAxiom a h r) <->
    E. e (e1 = e |> DAxiom a h r /\ EnvExtend e e2) $ =
(named '(EnvExtend_lem
  (syl5eq casel @ syl5eq caser @ appslamed @ appslamed @ applamed @
    lowereqd @ abeqd @ exeqd @
    aneqd (eqeq2d @ snoceq2d @ DAxiomeqd anllr anlr anr) (elneq2d an3l))
  (exeqd @ aneq1d eqeq1)
  (EnvExtend_lem2 orl)));

pub theorem EnvExtendDef (e1 e2 id a r o: nat) {e o2: nat}:
  $ EnvExtend e1 (e2 |> DDef id a r o) <->
    E. e E. o2 ((o2 != 0 -> o2 = o) /\
      e1 = e |> DDef id a r o2 /\ EnvExtend e e2) \/
    EnvExtend e1 e2 $ =
(named @ focus
  '(EnvExtend_lem
    (syl5eq caser @ syl5eq casel @ appslamed @ appslamed @ appslamed @ applamed @
      lowereqd @ abeqd @ oreqd
        (exeqd @ exeqd @ aneqd
          (aneqd (anwr @ imeq2d eqeq2) @
            eqeq2d @ snoceq2d @ DDefeqd an3lr anllr anlr eqidd)
          (elneq2d an4l))
        (elneq2d an4l))
    (oreqd (exeqd @ exeqd @ aneq1d @ aneq2d eqeq1) eleq1)
    _)
  '(orim1 @ eximi @ eex @ iexde @ imp @ com12 @ anim1d @
    animd (syl5 _ (bi2d eleq1)) (bi2d @ eqeq2d snoceq2))
  '(sylibr elupto @ sylib leltsuc _)
  '(sylib b1le @ sylib b0le @ sylib lepr2 @ sylib lepr2 @ sylib lepr2 _)
  '(eor (mpbiri le01 leeq1) eqle));

pub theorem EnvExtendThm (e1 e2 a h r: nat) {e: nat}:
  $ EnvExtend e1 (e2 |> DThm a h r) <->
    E. e (e1 = e |> DThm a h r /\ EnvExtend e e2) \/
    EnvExtend e1 e2 $ =
(named '(EnvExtend_lem
  (syl5eq caser @ syl5eq caser @ appslamed @ appslamed @ applamed @
    lowereqd @ abeqd @ oreqd
      (exeqd @ aneqd (eqeq2d @ snoceq2d @ DThmeqd anllr anlr anr) (elneq2d an3l))
      (elneq2d an3l))
    (oreqd (exeqd @ aneq1d eqeq1) eleq1)
  (EnvExtend_lem2 id)));

------------------
-- Verification --
------------------

@_ local def substExpr_aux (subst: nat): set =
$ SExprRec (\ v, nth v subst - 1) (\\ f, \\ xs, \ ih, SApp f ih) $;

--| This performs simultaneous substitution of the variables in `e` with the
--| expressions in `subst`.
--|
--| `substExpr : list SExpr -> SExpr => SExpr`
@_ abstract def substExpr (subst e: nat): nat = $ substExpr_aux subst @ e $;

theorem substExpr_aux_lam: $ substExpr_aux subst == \ e, substExpr subst e $ =
(named '(eqscom (lameqi applam)));

pub theorem substExprVar (subst v: nat):
  $ substExpr subst (SVar v) = nth v subst - 1 $ =
(named '(eqtr SExprRec_Var @ applame @ subeq1d ntheq1));
pub theorem substExprApp (subst f es: nat) {e: nat}:
  $ substExpr subst (SApp f es) = SApp f (map (\ e, substExpr subst e) es) $ =
(named '(eqtr SExprRec_App @
  ! appslame _ $_, map (substExpr_aux _) _$ _ _ _ @ appslamed @ applamed @
  SAppeqd anll @ syl6eq (mapeq1 substExpr_aux_lam) anr));

--| A CExpr is a convertibility proof:
--| `CRefl e : e = e`
--|
--| `CRefl : SExpr -> CExpr`
@_ def CRefl (e: nat): nat = $ b0 (b0 (b0 e)) $;
--| If `p : e = e'`, then `CSymm p : e' = e`
--|
--| `CSymm : CExpr -> CExpr`
@_ def CSymm (p: nat): nat = $ b0 (b0 (b1 p)) $;
--| If `p : e1 = e2` and `q : e2 = e3`, then `CTrans p q : e1 = e3`
--|
--| `CTrans : CExpr -> CExpr -> CExpr`
@_ def CTrans (p q: nat): nat = $ b0 (b1 (p, q)) $;
--| If `{p : e = e'}` then `CCong f {p} : f {e} = f {e'}`
--| where the braces denote iteration
--|
--| `CCong : TermID -> list CExpr -> CExpr`
@_ def CCong (f cs: nat): nat = $ b1 (b0 (f, cs)) $;
--| If `f {x} := {y}. e'`, then
--| `CCong f {z} p : f {e} = e'[{x}, {y} -> {e}, {z}]`
--|
--| `CUnfold : TermID -> list Expr -> list VarID -> CExpr`
@_ def CUnfold (f es zs: nat): nat = $ b1 (b1 (f, es, zs)) $;

theorem CSymm_ltid: $ c < CSymm c $ = '(ltb0tr @ ltb0tr b1ltid);

theorem CTrans_ltid1: $ c1 < CTrans c1 c2 $ = '(ltb0tr @ ltb1tr leprid1);
theorem CTrans_ltid2: $ c2 < CTrans c1 c2 $ = '(ltb0tr @ ltb1tr leprid2);

theorem CCong_ltid: $ c IN cs -> c < CCong f cs $ =
'(rsyl lmemlt @ mpi (ltb1tr @ leb0tr leprid2) lttr);

@_ local def CExprRec (R S T C U: set): set =
$ \ e, srec (\ ih, case
  (case
    (case R (\ c, S @ (c, ih @ c)))
    (\\ c1, \ c2, T @ (c1, c2, ih @ c1, ih @ c2)))
  (case
    (\\ f, \ cs, C @ (f, cs, map ih cs))
    U) @ size (Dom ih)) e $;

theorem CExprRec_val: $ CExprRec R S T C U @ e = case
  (case
    (case R (\ c, S @ (c, (CExprRec R S T C U |` upto e) @ c)))
    (\\ c1, \ c2, T @ (c1, c2,
      (CExprRec R S T C U |` upto e) @ c1,
      (CExprRec R S T C U |` upto e) @ c2)))
  (case
    (\\ f, \ cs, C @ (f, cs, map (CExprRec R S T C U |` upto e) cs))
    U) @ e $ =
(named '(eqtr (applame sreceq2) @
  ! eqtr _ $ _ @ lower (CExprRec R S T C U |` _) $ _ srecval @
  !! applame ih @ appeqd (rsyl (bi2 @ eqlower2 @ finlam finns) ,eqtac) sreclem));

theorem CExprRec_CRefl: $ CExprRec R S T C U @ CRefl e = R @ e $ =
(named '(eqtr CExprRec_val @ eqtr casel @ eqtr casel casel));
theorem CExprRec_CSymm:
  $ CExprRec R S T C U @ CSymm c = S @ (c, CExprRec R S T C U @ c) $ =
(named '(eqtr CExprRec_val @ eqtr casel @ eqtr casel @ eqtr caser @
  applame @ appeq2d @ preqd id @ syl6eq (resapp @ mpbir elupto CSymm_ltid) appeq2));
theorem CExprRec_CTrans:
  $ CExprRec R S T C U @ CTrans c1 c2 =
    T @ (c1, c2, CExprRec R S T C U @ c1, CExprRec R S T C U @ c2) $ =
(named '(eqtr CExprRec_val @ eqtr casel @ eqtr caser @
  appslame @ applamed @ appeq2d @ syl6eq (preq2 @ preq2 @
    preq (resapp @ mpbir elupto CTrans_ltid1) (resapp @ mpbir elupto CTrans_ltid2))
  ,eqtac));
theorem CExprRec_CCong:
  $ CExprRec R S T C U @ CCong f cs = C @ (f, cs, map (CExprRec R S T C U) cs) $ =
(named '(eqtr CExprRec_val @ eqtr caser @ eqtr casel @
  appslame @ applamed @ appeq2d @ preqd anl @ preqd anr @ syl6eq
    (mapeqg @ mpbir allal @ !! ax_gen e @ syl resapp @ sylibr elupto CCong_ltid)
    (mapeq2d anr)));
theorem CExprRec_CUnfold:
  $ CExprRec R S T C U @ CUnfold f es zs = U @ (f, es, zs) $ =
(named '(eqtr CExprRec_val @ eqtr caser caser));

theorem indd_aux2 (G p: wff x) (e: $ x = c -> (p <-> q) $)
  (h: $ c < b $): $ G /\ A. z (z < a -> [z / x] p) /\ a = b -> q $ =
'(sylc (eale (imeqd lteq1 (syl6bb (sbe e) sbeq1))) anlr @ mpbiri h @ lteq2d anr);

theorem CExpr_indd {x f e c es zs cs} (n)
  (px: wff x) (pi: wff c) (pi2: wff c2) (pr: wff e) (ps: wff c) (pt: wff c c2)
  (pc: wff f cs) (pu: wff f es zs)
  (hn: $ x = n -> (px <-> pn) $)
  (hr: $ x = CRefl e -> (px <-> pr) $)
  (hs: $ x = CSymm c -> (px <-> ps) $)
  (ht: $ x = CTrans c c2 -> (px <-> pt) $)
  (hc: $ x = CCong f cs -> (px <-> pc) $)
  (hu: $ x = CUnfold f es zs -> (px <-> pu) $)
  (hi: $ x = c -> (px <-> pi) $)
  (hi2: $ x = c2 -> (px <-> pi2) $)
  (ir: $ G -> pr $)
  (is: $ G /\ pi -> ps $)
  (it: $ G /\ pi /\ pi2 -> pt $)
  (ic: $ G /\ all {x | px} cs -> pc $)
  (iu: $ G -> pu $): $ G -> pn $ =
'(sylib (sbe hn) @ !! indstr z w sbeq1 sbeq1 ,(split-sop '{
 {{($CRefl e$ => (indd_aux hr @ anwll ir)) +
   ($CSymm c$ => (indd_aux hs @ mpd (indd_aux2 hi CSymm_ltid) (anwll @ exp is)))} +
   ($CTrans c c2$ => (indd_aux ht @
    mpd (indd_aux2 hi2 CTrans_ltid2) @ mpd (indd_aux2 hi CTrans_ltid1) @
    anwll @ exp @ exp it))} +
  {($CCong f cs$ => (indd_aux hc @ sylan ic anll @
    sylibr (alleq1 cbvabs) @ sylibr allal @
    sylc (alimd @ imim1d @ syl5 CCong_ltid @ bi2d lteq2) anr anlr)) +
   ($CUnfold f es zs$ => (indd_aux hu @ anwll iu))}
}));

-- A `VExpr` is a proof term.

--| A `VHyp` is a hypothesis step - a term is asserted from the local context.
--| Indexing is relative to the list of hypotheses to the theorem.
--|
--| `VHyp : HypID -> VExpr`
@_ def VHyp (n: nat): nat = $ b0 (b0 n) $;
--| A `VThm` is a theorem application - a step follows from previous steps by
--| application of a theorem. The arguments give the theorem to apply, the list
--| of substitutions of expressions for the variables, and the list of subproofs
--| for the hypotheses to the theorem.
--|
--| `VThm : ThmID -> list SExpr -> list VExpr -> VExpr`
@_ def VThm (a h r es ps: nat): nat = $ b0 (b1 (a, h, r, es, ps)) $;
--| `c : A = B, p : A |- VConv c p : B`
--|
--| `VConv : CExpr -> VExpr -> VExpr`
@_ def VConv (c p: nat): nat = $ b1 (c, p) $;

theorem VThm_ltid: $ p IN ps -> p < VThm a h r es ps $ =
'(rsyl lmemlt @ mpi (ltb0tr @ ltb1tr @ lepr2tr @ lepr2tr @ lepr2tr leprid2) lttr);

theorem VConv_ltid: $ p < VConv c p $ =
'(ltb1tr leprid2);

@_ local def VExprRec (H T C: set): set =
$ \ e, srec (\ ih, case
  (case H
    (\\ a, \\ h, \\ r, \\ es, \ ps, T @ (a, h, r, es, ps, map ih ps)))
  (\\ c, \ p, C @ (c, p, ih @ p)) @ size (Dom ih)) e $;

theorem VExprRec_val: $ VExprRec H T C @ e = case
  (case H
    (\\ a, \\ h, \\ r, \\ es, \ ps, T @ (a, h, r, es, ps, map (VExprRec H T C |` upto e) ps)))
  (\\ c, \ p, C @ (c, p, (VExprRec H T C |` upto e) @ p)) @ e $ =
(named '(eqtr (applame sreceq2) @
  ! eqtr _ $ _ @ lower (VExprRec H T C |` _) $ _ srecval @
  applame @ appeqd
    (rsyl (bi2 @ eqlower2 @ finlam finns) @
      caseeqd (caseeq2d @ slameqd @ slameqd @ slameqd @ slameqd @ lameqd @
        appeq2d @ preq2d @ preq2d @ preq2d @ preq2d @ preq2d mapeq1) @
      slameqd @ lameqd @ appeq2d @ preq2d @ preq2d appeq1)
    sreclem));

theorem VExprRec_VHyp: $ VExprRec H T C @ VHyp n = H @ n $ =
(named '(eqtr VExprRec_val @ eqtr casel casel));
theorem VExprRec_VThm:
  $ VExprRec H T C @ VThm a h r es ps = T @ (a, h, r, es, ps, map (VExprRec H T C) ps) $ =
(named '(eqtr VExprRec_val @ eqtr casel @ eqtr caser @
  appslame @ appslamed @ appslamed @ appslamed @ applamed @
  appeq2d @ preqd an4l @ preqd an3lr @ preqd anllr @ preqd anlr @ preqd anr @ syl6eq
    (mapeqg @ mpbir allal @ !! ax_gen p @ syl resapp @ sylibr elupto VThm_ltid)
    (mapeq2d anr)));
theorem VExprRec_VConv:
  $ VExprRec H T C @ VConv c p = C @ (c, p, VExprRec H T C @ p) $ =
(named '(eqtr VExprRec_val @ eqtr caser @
  appslame @ applamed @ appeq2d @
  preqd anl @ preqd anr @ syl6eq
    (resapp @ mpbir elupto VConv_ltid)
    (appeq2d anr)));

theorem VExpr_indd {x n a h r es ps c p} (q)
  (px: wff x) (pi: wff p) (ph: wff n) (pt: wff a h r es ps) (pc: wff c p)
  (hn: $ x = q -> (px <-> pq) $)
  (hr: $ x = VHyp n -> (px <-> ph) $)
  (hs: $ x = VThm a h r es ps -> (px <-> pt) $)
  (hc: $ x = VConv c p -> (px <-> pc) $)
  (hi: $ x = p -> (px <-> pi) $)
  (h1: $ G -> ph $)
  (h2: $ G /\ all {x | px} ps -> pt $)
  (h3: $ G /\ pi -> pc $): $ G -> pq $ =
'(sylib (sbe hn) @ !! indstr z w sbeq1 sbeq1 ,(split-sop '{
  {($VHyp n$ => (indd_aux hr @ anwll h1)) +
   ($VThm a h r es ps$ => (indd_aux hs @ sylan h2 anll @
    sylibr (alleq1 cbvabs) @ sylibr allal @
    sylc (alimd @ imim1d @ syl5 VThm_ltid @ bi2d lteq2) anr anlr))} +
   ($VConv c p$ => (indd_aux hc @ mpd (indd_aux2 hi VConv_ltid) (anwll @ exp h3)))}));

@_ local def VerifyConv_aux (env ctx: nat): set =
$ CExprRec
    (\ e, lower (S\ e1, S\ e2, {s | Expr env ctx e s /\ e = e1 /\ e = e2}))
    (\\ c, \ ih, lower (S\ e1, S\ e2, {s | e2, e1, s e. ih}))
    (\\ c1, \\ c2, \\ ih1, \ ih2, lower (S\ e1, S\ e2, {s |
      E. e (e1, e, s e. ih1 /\ e, e2, s e. ih2)}))
    (\\ f, \\ cs, \ ih, lower (S\ e1, S\ e2, {s |
      E. args E. ret E. o E. es1 E. es2 (
        e1 = SApp f es1 /\ e2 = SApp f es2 /\
        getTerm env f args ret o /\
        E. n (len cs = n /\ len es1 = n /\ len es2 = n /\ len args = n /\
          A. i A. c A. e1 A. e2 A. bi (nth i ih = suc c ->
            nth i es1 = suc e1 -> nth i es2 = suc e2 -> nth i args = suc bi ->
            ExprBi env ctx e1 bi /\ ExprBi env ctx e2 bi /\
            e1, e2, binderSort bi e. c)) /\
        s = fst ret)}))
    (\\ f, \\ es, \ zs, lower (S\ e1, S\ e2, {s |
      E. args E. ret E. ys E. val (
        getTerm env f args ret (suc (ys, val)) /\
        e1 = SApp f es /\ s = fst ret /\
        es, args e. all2 (S\ e, {a | ExprBi env ctx e a}) /\
        ys, zs e. all2 (S\ y, {z | nth z ctx = suc (PBound y) /\
          A. e (e IN es -> ~HasVar ctx e z)}) /\
        e2 = substExpr (es ++ map (\ i, SVar i) zs) val)})) $;

--| Checking a conversion proof `c : (e1 : s) = (e2 : s)`.
--| `VerifyConv : Env -> Ctx -> CExpr -> SExpr -> SExpr -> SortID -> Bool`
@_ abstract def VerifyConv (env ctx c e1 e2 s: nat): wff =
$ e1, e2, s e. VerifyConv_aux env ctx @ c $;

--| `VerifyConvs : Env -> Ctx -> list CExpr -> list SExpr ->
--|    list SExpr -> list Binder -> Bool`
@_ def VerifyConvs (env ctx cs es1 es2 bis .n .i .c .e1 .e2 .bi: nat): wff =
$ E. n (len cs = n /\ len es1 = n /\ len es2 = n /\ len bis = n /\
  A. i A. c A. e1 A. e2 A. bi (nth i cs = suc c ->
    nth i es1 = suc e1 -> nth i es2 = suc e2 -> nth i bis = suc bi ->
    ExprBi env ctx e1 bi /\ ExprBi env ctx e2 bi /\
    VerifyConv env ctx c e1 e2 (binderSort bi))) $;

theorem VerifyConvs_fin: $ E. n A. es1 A. es2 A. bis
  (VerifyConvs env ctx cs es1 es2 bis -> es1 < n /\ es2 < n) $ =
(focus
  (have 'h1
    $ len cs = m /\ len es1 = m /\ len es2 = m /\ len bis = m -> i < m ->
      E. c nth i cs = suc c /\ E. e1 nth i es1 = suc e1 /\
      E. e2 nth i es2 = suc e2 /\ E. bi nth i bis = suc bi $
    (def h '(syl6ib (bitr3 nthne0 exsuc) (com12 @ bi2d lteq2)))
    '(com12 @ animd (animd (animd ,h ,h) ,h) ,h))
  '(! iexe _ $ lower (Array (upto (map (VerifyConv_aux env ctx) cs)) (len cs)) $ _ _
    (aleqd @ aleqd @ aleqd @ imeq2d @ aneqd lteq2 lteq2) @
    ax_gen @ ax_gen @ ax_gen @ eex @ iand _ _)
  (def (lem hlen hlen2 hpr f) @ focus
    '(syl ellt @ sylibr (ellower @ Arrayfin finns) @
      sylibr elArray @ iand _ @ eqtr4d ,hlen an4l)
    '(sylibr elList @ sylibr allnth @ imp @ alimd @
      syl6ib (bitr3 alim1 @ aleqi @ bitr3 impexp @ imeq1i @ bian1a @ sylib nthne0 sucne0) @
      com23 @ syl6 _ @ mpbird (imeq1d @ lteq2d ,hlen2) h1)
    '(com12 @ impd @ impd @ impd @ sylibr eexb @ alimi @
      sylbi (bitr (!! aleqi e1 @ bitr (!! aleqi e2 alim1) alim1) alim1) @
      a2i @ syl5bi (aleqi @ bitr (aleqi alim1) @ bitr alim1 @ imeq2i @ aleqi alim1) _)
    (f '(alimd @ imim2d @ imp @ com23 @ syl6ibr eexb @ alimd @ imim2d @
      exp @ sylibr elupto @ syl (lelttr ,hpr) @
      lttrd (syl ellt anrr) @
      syl lmemlt @ syl lmemmapi @ anwl nthlmem)))
  (lem 'an3lr 'anllr 'leprid1 (fn (x)
    '(syl6 ax_1 @ com23 @ exp @ com23 @ exp @ alimd @ imim2d @
      anrasss @ imp @ com23 @ syl6ibr eexb ,x)))
  (lem 'anllr 'anlr '(lepr2tr leprid1) (fn (x)
    '(syl6ibr eexb @ alimd @ imim2d @ syl6 ax_1 @ com23 @ exp ,x))));

theorem VerifyConv_aux_Refl:
  $ VerifyConv_aux env ctx @ CRefl e = lower (S\ e1, S\ e2, {s |
    Expr env ctx e s /\ e = e1 /\ e = e2}) $ =
(named '(eqtr CExprRec_CRefl @ applame @ lowereqd @ sabeqd @ sabeqd @ abeqd @
  aneqd (aneqd Expreq3 eqeq1) eqeq1));

pub theorem VerifyConvRefl (env ctx e e1 e2 s: nat):
  $ VerifyConv env ctx (CRefl e) e1 e2 s <->
    Expr env ctx e s /\ e = e1 /\ e = e2 $ =
(named @ focus
  '(bitr (elneq2 VerifyConv_aux_Refl) @ bitr (ellower @ trud _) @
    elsabe @ elsabed @ elabed @
    aneqd (aneqd (Expreq4d anr) (eqeq2d anll)) (eqeq2d anlr))
  '(sabfin (eexsabd @ eelabd @ a1i @ sylibr elsn @ eqcomd anlr) (a1i finns) @
    sabfin (eelabd @ a1i @ sylibr elsn @ eqcomd anr) (a1i finns) @
    a1i @ finss (mpbi ssab1 @ ax_gen anll) finns));

theorem VerifyConv_aux_Symm:
  $ VerifyConv_aux env ctx @ CSymm c = lower (S\ e1, S\ e2, {s |
    VerifyConv env ctx c e2 e1 s}) $ =
(named '(eqtr {CExprRec_CSymm : $_ = _ @ (_, VerifyConv_aux _ _ @ c)$} @
  appslame @ applamed @ lowereqd ,eqtac));

pub theorem VerifyConvSymm (env ctx c e1 e2 s: nat):
  $ VerifyConv env ctx (CSymm c) e1 e2 s <-> VerifyConv env ctx c e2 e1 s $ =
(named @ focus
  '(bitr (elneq2 VerifyConv_aux_Symm) @ bitr (ellower @ trud _) @
    elsabe @ elsabed @ elabed @ VerifyConveqd eqidd eqidd eqidd anlr anll anr)
  '(sabfin (eexsabd @ eelabd @ a1i @ syl preldm prelrn) (a1i @ dmfin @ rnfin finns) @
    sabfin (eelabd @ a1i preldm) (a1i @ dmfin finns) @
    a1i @ finss (mpbi ssab1 @ ax_gen @ syl prelrn prelrn) (rnfin @ rnfin finns)));

theorem VerifyConv_aux_Trans:
  $ VerifyConv_aux env ctx @ CTrans c1 c2 = lower (S\ e1, S\ e2, {s |
    E. e (VerifyConv env ctx c1 e1 e s /\ VerifyConv env ctx c2 e e2 s)}) $ =
(named '(eqtr {CExprRec_CTrans : $ _ = _ @
    (_, _, VerifyConv_aux _ _ @ c1, VerifyConv_aux _ _ @ c2) $} @
  appslame @ appslamed @ appslamed @ applamed ,eqtac));

pub theorem VerifyConvTrans (env ctx c1 c2 e1 e2 s: nat) {e: nat}:
  $ VerifyConv env ctx (CTrans c1 c2) e1 e2 s <->
    E. e (VerifyConv env ctx c1 e1 e s /\ VerifyConv env ctx c2 e e2 s) $ =
(named @ focus
  '(bitr (elneq2 VerifyConv_aux_Trans) @ bitr (ellower @ trud _) @
    elsabe @ elsabed @ elabed ,eqtac)
  '(sabfin (eexsabd @ eelabd @ a1i @ eex @ anwl preldm) (a1i @ dmfin finns) @
    sabfin (eelabd @ a1i @ eex @ anwr @ syl preldm prelrn) (a1i @ dmfin @ rnfin finns) @
    a1i @ finss (mpbi ssab1 @ ax_gen @ eex @ anwr @ syl prelrn prelrn) (rnfin @ rnfin finns)));

theorem VerifyConv_aux_Cong:
  $ VerifyConv_aux env ctx @ CCong f cs = lower (S\ e1, S\ e2, {s |
    E. args E. ret E. o E. es1 E. es2 (
      e1 = SApp f es1 /\ e2 = SApp f es2 /\
      getTerm env f args ret o /\
      VerifyConvs env ctx cs es1 es2 args /\
      s = fst ret)}) $ =
(named @ focus
  '(eqtr {CExprRec_CCong : $_ = _ @ (_, _, map (VerifyConv_aux _ _) _)$} @
    appslame @ appslamed @ applamed @ lowereqd @ sabeqd @ sabeqd @ abeqd @
    exeqd @ exeqd @ exeqd @ exeqd @ exeqd @ aneq1d @
    aneqd (aneqd
      (aneqd (eqeq2d @ SAppeq1d anll) (eqeq2d @ SAppeq1d anll))
      (getTermeq2d anll)) _)
  '(exeqd @ aneqd (aneq1d @ aneq1d @ aneq1d @ eqeq1d @ leneqd anlr) @
    !! aleqd n @
    bitr4g alcomb alcomb @ !! aleqd e1 @
    bitr4g alcomb alcomb @ !! aleqd e2 @
    bitr4g alcomb alcomb @ !! aleqd bi @
    syl6bb _ @ aleqd @ imeq1d @ eqeq1d @ ntheq2d anr)
  '(bitr (aleqi @ bitr (imeq1i @ mapnthb) eexb) @
    bitr alcomb @ aleqi @
    bitr (!! aleqi _ @ bitr (imeq1i ancomb) impexp) @ aleqe @
    imeq2d @ imeq2d @ imeq2d @ imeq2d @ aneq2d elneq2));

pub theorem VerifyConvCong (env ctx f cs e1 e2 s: nat) {args ret o es1 es2: nat}:
  $ VerifyConv env ctx (CCong f cs) e1 e2 s <->
    E. args E. ret E. o E. es1 E. es2 (
      e1 = SApp f es1 /\ e2 = SApp f es2 /\
      getTerm env f args ret o /\
      VerifyConvs env ctx cs es1 es2 args /\
      s = fst ret) $ =
(named @ focus
  '(bitr (elneq2 VerifyConv_aux_Cong) @ bitr (ellower _) @
    elsabe @ elsabed @ elabed @ exeqd @ exeqd @ exeqd @ exeqd @ exeqd @
    aneqd (aneq1d @ aneq1d @ aneqd (eqeq1d anll) (eqeq1d anlr)) (eqeq1d anr))
  (suffices 'h $ _ -> _ -> e1_ < SApp env n /\ e2_ < SApp env n /\ s_ < env $ '_)
  (focus
    '(ax_mp (eex _) VerifyConvs_fin)
    '(sabfin (eexsabd @ eelabd @ syl6ibr elupto @ syl6 anll h) (a1i finns) @ anwl @
      sabfin (eelabd @ syl6ibr elupto @ syl6 anlr h) (a1i finns) @ anwl @
      syl (mpi ltfin finss) @ ssabd @ syl6 anr h))
  '(eexd @ eexd @ eexd @ sylibr eexb @ alimi @ sylibr eexb @ alimi @
    sylbir eexb @ com12 @ syld (rsyl anlr @ com12 @ imim1i @ iexe VerifyConvseq6) @
    syld _ (bi2d @ aneqd (aneqd (lteq1d an4l) (lteq1d an3lr)) (lteq1d anr)))
  '(rsyl anllr @ rsyl getTerm_ltid @ exp @ iand (iand _ _) _)
  (focus '(sylib b1lt @ lttrd (sylib ltpr1 an4l) (sylib ltpr2 anrl)))
  (focus '(sylib b1lt @ lttrd (sylib ltpr1 an4l) (sylib ltpr2 anrr)))
  (focus '(syl (lelttr fstleid) anllr)));

theorem VerifyConv_aux_Unfold:
  $ VerifyConv_aux env ctx @ CUnfold f es zs = lower (S\ e1, S\ e2, {s |
    E. args E. ret E. ys E. val (
      getTerm env f args ret (suc (ys, val)) /\
      e1 = SApp f es /\ s = fst ret /\
      es, args e. all2 (S\ e, {a | ExprBi env ctx e a}) /\
      ys, zs e. all2 (S\ y, {z | nth z ctx = suc (PBound y) /\
        A. e (e IN es -> ~HasVar ctx e z)}) /\
      e2 = substExpr (es ++ map (\ i, SVar i) zs) val)}) $ =
(named '(eqtr CExprRec_CUnfold @ appslame @ appslamed @ applamed ,eqtac));

pub theorem VerifyConvUnfold (env ctx f zs e1 e2 s: nat)
  {args ret ys val es a y z e i: nat}:
  $ VerifyConv env ctx (CUnfold f es zs) e1 e2 s <->
    E. args E. ret E. ys E. val (
      getTerm env f args ret (suc (ys, val)) /\
      e1 = SApp f es /\ s = fst ret /\
      es, args e. all2 (S\ e, {a | ExprBi env ctx e a}) /\
      ys, zs e. all2 (S\ y, {z | nth z ctx = suc (PBound y) /\
        A. e (e IN es -> ~HasVar ctx e z)}) /\
      e2 = substExpr (es ++ map (\ i, SVar i) zs) val) $ =
(named @ focus
  '(bitr (elneq2 VerifyConv_aux_Unfold) @ bitr (ellower @ trud _) @
    elsabe @ elsabed @ elabed @ exeqd @ exeqd @ exeqd @ exeqd ,eqtac)
  '(sabfin (eexsabd @ eelabd @ syl6ibr elsn @ a1i @
      eex @ eex @ eex @ eex an4lr) (a1i finns) @
    sabfin
      (eelabd @ a1i @ eex @ eex @ eex @ eex @
        mpbird (eleq1d anr) @ appelima (a1i lamisf) (a1i @ mpbir (eleq2 dmlam) elv) @
        sylibr elupto @ syl (lttr @ mpbi leltsuc leprid2) @ syl getTerm_valltid an5l)
      (a1i @ finlamima finns) @
    a1i @ finss (mpbi ssab @ ax_gen @ eex @ eex @ eex @ eex @
      mpbird (lteq1d an3lr) @ syl (lelttr fstleid) @
      syl getTerm_retltid an5l) ltfin));

@_ local def VerifyProof_aux (env ctx hs: nat): set =
$ VExprRec
    (\ n, lower {ret | nth n hs = suc ret})
    (\\ args2, \\ hs2, \\ ret2, \\ es, \\ ps, \ ih, lower {ret |
      getThm env args2 hs2 ret2 /\
      es, args2 e. all2 (S\ e, {a | ExprBi env ctx e a}) /\
      A. u A. v (E. s nth u ctx = suc (PBound s) ->
        v < len ctx -> ~HasVar ctx (SVar v) u ->
        A. y A. e2 (nth u es = suc (SVar y) -> nth v es = suc e2 ->
          ~HasVar ctx e2 y)) /\
      ih, hs2 e. all2 (S\ p, {h | substExpr es h e. p}) /\
      substExpr es ret2 = ret})
    (\\ c, \\ p, \ ih, lower {ret |
      E. e1 E. s (VerifyConv env ctx c e1 ret s /\ e1 e. ih)}) $;

--| The main proof checking function.
--|
--| This typechecks a `VExpr` and determines the `SExpr` that it represents.
--| * At a hypothesis step, this is just looking up the
--|   nth element in the list.
--| * At a theorem step, we get the theorem data,
--|   check that all the substituting expressions match the binders they are going
--|   in for, check that all the disjoint variable conditions of the theorem
--|   are honored by the substitution, and then check recursively that the
--|   subproofs are okay and the return is what it should be.
--|
--| `VerifyProof : Env -> Ctx -> list SExpr -> VExpr -> SExpr -> Bool`
@_ abstract def VerifyProof (env ctx hs pf ret: nat): wff =
$ ret e. VerifyProof_aux env ctx hs @ pf $;

theorem VerifyProof_aux_Hyp:
  $ VerifyProof_aux env ctx hs @ VHyp n = lower {ret | nth n hs = suc ret} $ =
(named '(eqtr VExprRec_VHyp @ applame @ lowereqd @ abeqd @ eqeq1d ntheq1));

pub theorem VerifyProofHyp (env ctx hs n ret: nat):
  $ VerifyProof env ctx hs (VHyp n) ret <-> nth n hs = suc ret $ =
(named @ focus
  '(bitr (elneq2 VerifyProof_aux_Hyp) @ bitr (ellower _) @ elabe @ eqeq2d suceq)
  '(finss (mpbi ssab1 @ ax_gen nthlmem) finns));

theorem VerifyProof_aux_Thm:
  $ VerifyProof_aux env ctx hs @ VThm args2 hs2 ret2 es ps = lower {ret |
      getThm env args2 hs2 ret2 /\
      es, args2 e. all2 (S\ e, {a | ExprBi env ctx e a}) /\
      A. u A. v (E. s nth u ctx = suc (PBound s) ->
        v < len ctx -> ~HasVar ctx (SVar v) u ->
        A. y A. e2 (nth u es = suc (SVar y) -> nth v es = suc e2 ->
          ~HasVar ctx e2 y)) /\
      ps, hs2 e. all2 (S\ p, {h | VerifyProof env ctx hs p (substExpr es h)}) /\
      substExpr es ret2 = ret} $ =
(named @ focus
  '(eqtr {VExprRec_VThm : $_ = _ @ (_, _, _, _, _, map (VerifyProof_aux _ _ _) _)$} @
    appslame @ appslamed @ appslamed @ appslamed @ appslamed @ applamed @ lowereqd @ abeqd @
    aneqd (aneqd (aneqd (aneqd
      (getThmeqd eqidd an5l an4lr an3lr)
      (eleq1d @ preqd anllr an5l))
      (aleqd @ aleqd @ imeq2d @ imeq2d @ imeq2d @ aleqd @ aleqd @
        imeqd (eqeq1d @ ntheq2d anllr) @ imeq1d (eqeq1d @ ntheq2d anllr)))
      (syl6bb _ @ eleqd (preqd anr an4lr) (all2eqd @ sabeqd @ abeqd @ eleq1d @ substExpreq1d anllr)))
      (eqeq1d @ substExpreqd anllr an3lr))
  '(bitr4 elall2 @ bitr4 elall2 @ aneq (eqeq1 maplen) @ aleqi @
    bitr (aleqi @ bitr alim1 @ bitr (imeq1i mapnthb) @ eexb) @
    bitr alcomb @ aleqi @ bitr (aleqi @ bitr (imeq1i ancomb) impexp) @ aleqe @
    syl6bbr alim1 @ imeq2d @ aleqd @ imeq2d @ bitr4g _ _ elneq2)
  '(elsabe @ elabed ,eqtac) '(elsabe @ elabed ,eqtac));

pub theorem VerifyProofThm (env ctx hs args2 hs2 ret2 es ps ret: nat)
  {e a u v s y e2 p h: nat}:
  $ VerifyProof env ctx hs (VThm args2 hs2 ret2 es ps) ret <->
      getThm env args2 hs2 ret2 /\
      es, args2 e. all2 (S\ e, {a | ExprBi env ctx e a}) /\
      A. u A. v (E. s nth u ctx = suc (PBound s) ->
        v < len ctx -> ~HasVar ctx (SVar v) u ->
        A. y A. e2 (nth u es = suc (SVar y) -> nth v es = suc e2 ->
          ~HasVar ctx e2 y)) /\
      ps, hs2 e. all2 (S\ p, {h | VerifyProof env ctx hs p (substExpr es h)}) /\
      substExpr es ret2 = ret $ =
(named @ focus
  '(bitr (elneq2 VerifyProof_aux_Thm) @ bitr (ellower _) @ elabe @ aneq2d eqeq2)
  '(finss (mpbi ssab1 @ ax_gen @ sylibr elsn @ eqcomd anr) finns));

theorem VerifyProof_aux_Conv:
  $ VerifyProof_aux env ctx hs @ VConv c p = lower {ret |
      E. e1 E. s (VerifyConv env ctx c e1 ret s /\ VerifyProof env ctx hs p e1)} $ =
(named '(eqtr {VExprRec_VConv : $_ = _ @ (_, _, VerifyProof_aux _ _ _ @ p)$} @
  appslame @ appslamed @ applamed @ lowereqd @ abeqd @
  exeqd @ exeqd @ aneqd (VerifyConveq3d anll) (elneq2d anr)));

pub theorem VerifyProofConv (env ctx hs c p ret: nat) {e1 s: nat}:
  $ VerifyProof env ctx hs (VConv c p) ret <->
    E. e1 E. s (
      VerifyConv env ctx c e1 ret s /\
      VerifyProof env ctx hs p e1) $ =
(named @ focus
  '(bitr (elneq2 VerifyProof_aux_Conv) @ bitr (ellower _) @
    elabe @ exeqd @ exeqd @ aneq1d VerifyConveq5)
  '(finss (mpbi ssab1 @ ax_gen @ eex @ eex @ syl preldm @ syl prelrn anl) (dmfin @ rnfin finns)));

@_ local def EnvFull_aux (env: nat): nat =
$ rlrec 1 (\\ e, \\ d, \ ih, case (\ x, ih)
  (case
    (\\ id, \\ a, \\ r, \ o, nat (true ih /\ o != 0))
    (\\ a, \\ h, \ r, nat (true ih /\ E. ds E. pf E. ctx (
        ctx = appendDummies a ds /\ Ctx e ctx /\
        VerifyProof e ctx h pf r)))) @ d) env $;

theorem EnvFull_aux_0: $ EnvFull_aux 0 = 1 $ = (named 'rlrec0);
theorem EnvFull_aux_S: $ EnvFull_aux (env |> d) = case (\ x, EnvFull_aux env)
  (case
    (\\ id, \\ a, \\ r, \ o, nat (true (EnvFull_aux env) /\ o != 0))
    (\\ a, \\ h, \ r, nat (true (EnvFull_aux env) /\ E. ds E. pf E. ctx (
        ctx = appendDummies a ds /\ Ctx env ctx /\
        VerifyProof env ctx h pf r)))) @ d $ =
'(eqtr {rlrecS : $ _ = _ @ (_, _, EnvFull_aux env) $} @
  appslame @ appslamed @ applamed ,eqtac);

theorem EnvFull_aux_b0: $ EnvFull_aux (env |> b0 x) = EnvFull_aux env $ =
(named '(eqtr EnvFull_aux_S @ eqtr casel @ applame eqidd));

--| An environment is "full" if it has no missing definitions, and all the theorems
--| are provable.
--|
--| `EnvFull : Env -> Bool`
@_ abstract def EnvFull (env: nat): wff = $ true (EnvFull_aux env) $;
pub theorem EnvFull0: $ EnvFull 0 $ = '(mpbir (trueeq EnvFull_aux_0) true1);
pub theorem EnvFullSort (env id sd: nat):
  $ EnvFull (env |> DSort id sd) <-> EnvFull env $ = '(trueeq EnvFull_aux_b0);
pub theorem EnvFullTerm (env id a r: nat):
  $ EnvFull (env |> DTerm id a r) <-> EnvFull env $ = '(trueeq EnvFull_aux_b0);
pub theorem EnvFullAxiom (env a h r: nat):
  $ EnvFull (env |> DAxiom a h r) <-> EnvFull env $ = '(trueeq EnvFull_aux_b0);
pub theorem EnvFullDef (env id a r o: nat):
  $ EnvFull (env |> DDef id a r o) <-> EnvFull env /\ o != 0 $ =
(named '(bitr (trueeq @ eqtr EnvFull_aux_S @ eqtr caser @ eqtr casel @
    appslame @ appslamed @ appslamed @ applamed ,eqtac) truenat));
pub theorem EnvFullThm (env a h r: nat) {ds pf ctx: nat}:
  $ EnvFull (env |> DThm a h r) <-> EnvFull env /\
    E. ds E. pf E. ctx (
      ctx = appendDummies a ds /\ Ctx env ctx /\
      VerifyProof env ctx h pf r) $ =
(named '(bitr (trueeq @ eqtr EnvFull_aux_S @ eqtr caser @ eqtr caser @
    appslame @ appslamed @ applamed ,eqtac) truenat));

--| A specification is provable if some extension of the specification has a proof.
--| The extension provides definitions for the providing all the omitted definitions
--| and proving all the theorems in the file.
--|
--| `ValidEnv : Env -> Bool`
@_ def ValidEnv (env .e .p: nat): wff =
$ Env env /\ E. e (Env e /\ EnvExtend env e /\ EnvFull e) $;


-------------
-- Parsing --
-------------

-- Definition of ASCII, or at least the part of it we need

--| `\n`: newline character
@_ def _nl:     char = "\n";
--| ` `: space
@_ def __:      char = " ";
--| `$`: dollar sign
@_ def _dollar: char = "$";
--| `(`: left parenthesis
@_ def _lparen: char = "(";
--| `)`: right parenthesis
@_ def _rparen: char = ")";
--| `*`: asterisk / multiplication symbol
@_ def _ast:    char = "*";
--| `-`: hyphen / minus sign
@_ def _hyphen: char = "-";
--| `.`: dot / period / full stop
@_ def _dot:    char = ".";
--| `:`: colon
@_ def _colon:  char = ":";
--| `;`: semicolon
@_ def _semi:   char = ";";
--| `=`: equal sign
@_ def _equal:  char = "=";
--| `>`: greater than, right arrow
@_ def _gt:     char = ">";
--| `_`: underscore (note: __ is space)
@_ def _under:  char = "_";
--| `{`: left brace / curly bracket
@_ def _lbrace: char = "{";
--| `}`: right brace / curly bracket
@_ def _rbrace: char = "}";

-- ASCII numbers
@_ def _0: char = "0";
@_ def _1: char = "1";
@_ def _2: char = "2";
@_ def _3: char = "3";
@_ def _4: char = "4";
@_ def _5: char = "5";
@_ def _6: char = "6";
@_ def _7: char = "7";
@_ def _8: char = "8";
@_ def _9: char = "9";

-- Don't really need capitals except as a range
@_ def _A: char = "A";
@_ def _Z: char = "Z";

-- Most of the lowercase alphabet, used in keywords
@_ def _a: char = "a";
@_ def _b: char = "b";
@_ def _c: char = "c";
@_ def _d: char = "d";
@_ def _e: char = "e";
@_ def _f: char = "f";
@_ def _h: char = "h";
@_ def _i: char = "i";
@_ def _l: char = "l";
@_ def _m: char = "m";
@_ def _n: char = "n";
@_ def _o: char = "o";
@_ def _p: char = "p";
@_ def _r: char = "r";
@_ def _s: char = "s";
@_ def _t: char = "t";
@_ def _u: char = "u";
@_ def _v: char = "v";
@_ def _x: char = "x";
@_ def _z: char = "z";

do (begin
  (def (mkth-pr m a b f)
    (def t '(,m (c2n (,a)) (c2n (,b))))
    (add-thm! (atom-app a "_" m b) () () t () @ fn ()
      (def g (ref! (goal t)))
      (set-goals g) (refine (f)) '(() ,g)))
  (def (mkth m a b)
    (mkth-pr m a b @ fn () '{,norm_num : (,m (c2n (ch _ _)) (c2n (ch _ _)))}))
  (let ([a (ref!)]) @
    scan '(_nl _dot _0 _9 _colon _gt _A _Z _under _a _z _lbrace _rbrace) @ fn (b)
      (if (def? a) (mkth 'lt a b))
      (set! a b))
  (mkth 'le '_0 '_1)
  (mkth 'lt '_dollar '_hyphen)
  (mkth 'lt '_dollar '_0)
  (scan '((_nl __ _dollar _lparen _rparen _ast _hyphen _dot)
          (_colon _semi _equal _gt)) @ fn (s)
    @ match s @ (a . l) @ match (split-last s) @ (r . m)
    (scan l @ fn (b) (mkth 'le a b))
    (scan l @ fn (a) (mkth 'le a r)))
  (scan
    '((_dollar _0 _9) (_9 _colon _gt) (_9 _gt _A) (_0 _9 _A) (_dollar _9 _A)
      (_Z _under _a) (_Z _a _z) (_A _Z _under) (_A _Z _a)
      (_under _a _z) (_9 _A _Z) (_9 _Z _z) (_dollar _9 _z))
    @ match-fn @ (a b c)
    @ mkth-pr 'lt a c @ fn () '(lttr ,(atom-app a "_lt" b) ,(atom-app b "_lt" c))));

-- Now we define the lexer:

--| `prefix s t` means that `s` is a prefix of `t`, for example `prefix "he" "hello"`.
@_ def prefix (s t .x: nat): wff = $ E. x s ++ x = t $;

theorem takeprefix: $ prefix (take l n) l $ = '(!! iexe l2 (eqeq1d appendeq2) takedrop);

theorem prefix_eq_take: $ prefix l1 l2 <-> l1 = take l2 (len l1) $ =
(focus
  '(ibii (!! eex r @ syl5eqr _ takeeq1) (mpbiri takeprefix prefixeq1))
  '(eqtrd takeappend1 takeall leid));

theorem prefix_len: $ prefix l1 l2 -> len l1 <= len l2 $ =
'(sylbi prefix_eq_take @ mpbiri minle1 @ leeq1d @ syl6eq takelen @ leneq);

theorem prefix_asymm: $ len l2 <= len l1 -> prefix l1 l2 -> l1 = l2 $ =
'(syl5bi prefix_eq_take @ bi1d @ eqeq2d takeall);

theorem prefix_0: $ prefix 0 l $ = '(!! iexe r (eqeq1d appendeq2) append0);
theorem prefix_id: $ prefix l l $ = '(!! iexe r (eqeq1d appendeq2) append02);
theorem prefix_tr: $ prefix l1 l2 -> prefix l2 l3 -> prefix l1 l3 $ =
'(!! eex r1 @ !! eexda r2 @ !! iexde r3 @ eqtrd (appendeq2d anr) @
  syl5eqr appendass @ eqtrd (appendeq1d anll) anlr);

theorem prefix_02: $ prefix l 0 <-> l = 0 $ =
(named '(bitr (exeqi @ bitr appendeq0 ancomb) @ exeqe biidd));

theorem prefix_S1: $ prefix (x : l1) l2 <-> E. l3 (prefix l1 l3 /\ l2 = x : l3) $ =
(named '(bitr4 (exeqi @
    bitr3 (exeqe @ syl6bb eqcomb @ eqeq2d @ syl6eqr appendS conseq2) @
    exeqi @ aneq1i eqcomb) @
  bitr3 (exeqi exan2) excomb));

theorem prefix_append1: $ prefix (l ++ l1) (l ++ l2) <-> prefix l1 l2 $ =
'(!! exeqi x @ bitr (eqeq1 appendass) appendcan1);

theorem prefix_S: $ prefix (x : l1) (y : l2) <-> x = y /\ prefix l1 l2 $ =
(named '(bitr4 prefix_S1 @ bitr3 (exeqe @ syl5bb ancomb @ aneq2d prefixeq2) @
  exeqi @ bitr anlass @ aneq2i @ bitr4 ancomb @ bitr eqcomb consinj));

theorem prefix_nth: $ prefix l1 l2 -> nth n l1 = suc x -> nth n l2 = suc x $ =
'(sylbi prefix_eq_take @ exp @
  eqtr3d (syl takenth @ anwr @ sylib nthne0 sucne0) @ eqtr3d (ntheq2d anl) anr);

--| `maxPrefix A s` splits `s` at the longest prefix of `s` which satisfies `A`, if any.
--| `maxPrefix: Set X -> List X -> Option (List X, List X)`
@_ def maxPrefix (A: set) (s: nat): nat =
$ the {z | E. x E. t (x ++ t = s /\ x e. A /\
    A. y (prefix y s /\ y e. A -> prefix y x) /\
    z = suc (x, t))} $;

pub theorem maxPrefix0 {x: nat} (A: set) (s: nat):
  $ ~ (E. x (prefix x s /\ x e. A)) -> maxPrefix A s = 0 $ =
(named '(eqthe0abd @ syl absurd @ con3 @ eximi @ eex @
  anwl @ anwl @ anim1 @ iexe @ eqeq1d appendeq2));

theorem maxPrefix_subsn: $ subsn {z |
  E. x E. t (x ++ t = s /\ x e. A /\
    A. y (prefix y s /\ y e. A -> prefix y x) /\
    z = suc (x, t))} $ =
(named @ focus
  (def h '(elabe @ exeqd @ exeqd @ aneq2d eqeq1))
  '(ax_gen @ ax_gen @ sylbi ,h @ syl5bi (bitr ,h _) @ eex @ eex @ eexd @ eexd @ exp _)
  (focus '(cbvex @ cbvexd @
    aneqd (aneqd (aneqd (eqeq1d @ imp appendeq) @ eleq1d anl) @
    aleqd @ imeq2d @ prefixeq2d anl) @
    eqeq2d @ suceqd @ imp preq))
  (suffices 'h2 $ _ -> x = w $ _)
  '(eqtr4d anlr @ eqtr4d anrr @ suceqd @ preqd h2 @
    sylib appendcan1 @ eqtr4d an4l @ eqtrd (appendeq1d h2) (anwr an3l))
  (def (lem hl hr)
    '(sylc (eale @ imeqd (aneqd prefixeq1 eleq1) prefixeq1) (syl anlr ,hl) @
      iand (syl (anw3l @ iexe @ eqeq1d appendeq2) ,hr) (syl anllr ,hr)))
  '(sylc prefix_asymm (syl prefix_len _) _)
  (lem 'anl 'anr)
  (lem 'anr 'anl));

pub theorem maxPrefixS {x y t: nat} (A: set) (s: nat):
  $ E. x (prefix x s /\ x e. A) ->
    E. x E. t (x ++ t = s /\ x e. A /\
      A. y (prefix y s /\ y e. A -> prefix y x) /\
      maxPrefix A s = suc (x, t)) $ =
(named @ focus
  '(! rsyl _ $ E. n (n <= len s /\ take s n e. A /\ A. y (prefix y s -> y e. A -> len y <= n)) $)
  (focus
    (def h2 '(elabe @ aleqd @ imeq2d leeq2))
    (def N $ least {i | A. m (take s m e. A -> min (len s) m <= i)} $)
    '(syl (! iexe _ ,N _ _ @
        aneqd (aneqd leeq1 @ eleq1d takeeq2) (aleqd @ imeq2d @ imeq2d leeq2)) _)
    (have 'h3 $ len s e. {i | A. m (take s m e. A -> min (len s) m <= i)} $
      '(mpbir ,h2 @ ax_gen @ a1i minle1))
    (have 'h4 $ _ -> y = take s (len y) $ '(sylib prefix_eq_take anlr))
    (def hal '(imeqd (eleq1d takeeq2) (leeq1d mineq2)))
    (have 'h5 $ A. m2 (take s m2 e. A -> min (len s) m2 <= ,N) $
      '(mpbi ,h2 @ mpbi (eleq2 @ cbvab @ syl5bb (cbval ,hal) @ aleqd @ imeq2d leeq2) @ leastel h3))
    (def h5 '(eale ,hal h5))
    '(eex @ iand (iand (a1i @ leastle h3) _) @ iald @ exp @ exp @
      mpbid (leeq1d @ syl5eqr takelen @ leneqd @ eqcomd h4) @
      syl ,h5 @ mpbid (eleq1d h4) anr)
    (have 'h6 $ _ -> x = take s (len x) $ '(sylib prefix_eq_take anll))
    (have 'h7 $ _ -> take s (len x) e. A $ '(mpbid (eleq1d h6) anlr))
    '(casesd
      (exp @ mpbird (eleq1d @ takeeq2d @ eqtr4d anr @ eqtrd (leneqd h6) @ syl5eq takelen @
        sylib le02 @ mpbid (leeq2d anr) @ syl ,h5 h7) h7)
      (syl5bi exsuc @ !! eexda j @ mpbird (eleq1d @ takeeq2d anr) @ mpi ltirr @ con1d @
        exp @ mpbid (leeq1d anlr) @ syl leastle @
        sylibr ,h2 @ sylibr (cbval ,hal) @ iald @ exp @ sylibr leltsuc @ sylibr ltlene @
        iand (mpbid (leeq2d anllr) @ anwr @ eal h5) @
        mpd anlr @ con3d @ syl5ibrcom (eleq1d @ syl6eq takemin @ takeeq2d eqcom) anr)))
  (def h '(elabe @ exeqd @ exeqd @ aneq2d eqeq1))
  '(eex @ sylib ,h @ syl (mpbird (eleq1d (subsnthe maxPrefix_subsn)) id) @ sylibr ,h @ iexde @ iexde @
    iand (iand (iand (syl6eq takedrop @ appendeqd anlr anr) @ mpbird (eleq1d anlr) an3lr) @
      sylc _ (iand an4l anlr) anllr) (eqcomd @ suceqd @ preqd anlr anr))
  '(alimd @ syl5bir impexp @ a2d @ exp @ exp @ sylibr prefix_eq_take @
    eqtrd (sylib prefix_eq_take @ anld anlr) @ syl5eqr (takeeq1 takedrop) @
    eqtr4d (syl takeappend1 @ mpbird (leeq2d @ syl5eq takelen @ syl eqmin2 an3l) anr) @
    takeeq1d anllr));

theorem maxPrefixSilem: $ maxPrefix A s = suc (x, t) ->
  x ++ t = s /\ x e. A /\ A. y (prefix y s /\ y e. A -> prefix y x) $ =
(named '(mpd (syl maxPrefixS @ rsyl sucne0 @ con1 maxPrefix0) @
  eexd @ eexd @ impd @ com23 @ exp @ rsyl (sylib prth @ sylib peano2 @ eqtr3d anl anr) @
  bi2d @ aneqd (aneqd (eqeq1d @ imp appendeq) (eleq1d anl)) @
  anwl @ aleqd @ imeq2d prefixeq2));

theorem maxPrefixSi1: $ maxPrefix A s = suc (x, t) -> x ++ t = s $ = (named '(anld @ anld maxPrefixSilem));
theorem maxPrefixSi2: $ maxPrefix A s = suc (x, t) -> x e. A $ = (named '(anrd @ anld maxPrefixSilem));
theorem maxPrefixSi3 (h1: $ G -> maxPrefix A s = suc (x, t) $)
  (h2: $ G -> prefix y s $) (h3: $ G -> y e. A $): $ G -> prefix y x $ =
(named '(sylc (eale @ imeqd (aneqd prefixeq1 eleq1) prefixeq1)
  (anrd @ syl maxPrefixSilem h1) @ iand h2 h3));

theorem maxPrefix_eqS (h1: $ G -> prefix a s $) (h2: $ G -> a e. A $):
  $ G -> E. x E. t maxPrefix A s = suc (x, t) $ =
(named '(syl (eximi @ eximi anr) @ syl maxPrefixS @
  syl (iexe @ aneqd prefixeq1 eleq1) (iand h1 h2)));

theorem maxPrefix_prefix: $ maxPrefix A s = suc (x, t) -> prefix x s $ =
(named '(syl (iexe @ eqeq1d appendeq2) maxPrefixSi1));

theorem maxPrefix_asymm {y} (h: $ x e. A /\ y e. A /\ prefix x y -> x = y $):
  $ maxPrefix A s = suc (x, t) <-> x ++ t = s /\ x e. A $ =
(named @ focus
  '(ibii (iand maxPrefixSi1 maxPrefixSi2) @
    mpd (maxPrefix_eqS (iexde @ eqtrd (appendeq2d anr) anll) anr) @
    eexd @ eexd @ exp @ eqtr4d anr @ suceqd _)
  (suffices 'h2)
  '(preqd h2 @ sylib appendcan1 @ eqtr3d (appendeq1d h2) @ eqtr4d anll (anwr maxPrefixSi1))
  '(syl h @ iand (iand anlr @ anwr maxPrefixSi2) @
    maxPrefixSi3 anr (anwll @ iexe @ eqeq1d appendeq2) anlr));

-- The parsers here are relations `R: Parser S A` where
-- `Parser S A := List S -> A -> Bool`, with the meaning that
-- if `s, a e. R` then parsing `s: List S` results in an output value `a: A`.
-- They are all nondeterministic; determinism is ensured by applying additional
-- constraints to the matches until at most one thing can match.

--| `regexStar R` is the `many` combinator on regexes. It matches `s` if there exists
--| some way to split `s` into pieces `s_i` satisfying `s_i, a_i e. R`;
--| the list of resulting `a_i` values is returned.
--|
--| `regexStar: Parser S A -> Parser S (List A)`
@_ def regexStar (R: set) (.s .t .L .x .y: nat): set =
$ S\ s, {t | E. L (L, t e. all2 R /\ s = ljoin L)} $;

--| `regexApp R S` is the sequential composition of regexes.
--| It matches `s ++ t` and returns `a, b` if `s R a` and `t S b`.
--|
--| `regexApp: Parser S A -> Parser S B -> Parser S (A, B)`
@_ def regexApp (R S: set) (.z .a .b .x .y: nat): set =
$ {z | E. x E. y E. a E. b (x, a e. R /\ y, b e. S /\ z = x ++ y, a, b)} $;
infixr regexApp: $<+>$ prec 75;

--| `regexPlus R` is the `many1` combinator: it is like `regexStar`
--| except it must match at least once.
--|
--| `regexPlus: Parser S A -> Parser S (List A)`
@_ def regexPlus (R: set) (.x: nat): set =
$ regexStar R i^i {x | snd x != 0} $;

--| `regexOpt R` is the `optional` combinator: it matches the empty string
--| and returns `0`, as well as matching `s` if `s R a`, and returns `suc a`.
--|
--| `regexOpt: Parser S A -> Parser S (Option A)`
@_ def regexOpt (R: set) (.s .t .y: nat): set =
$ sn 0 u. S\ s, {t | E. y (s, y e. R /\ t = suc y)} $;

--| The set of whitespace characters
--|
--| `white : set char`
@_ def white: nat = $ __ ; sn _nl $;

theorem el_white: $ c e. white <-> c = __ \/ c = _nl $ = '(bitr elins @ oreq2i elsn);

theorem white_lt_dollar: $ c e. white -> c < _dollar $ =
(focus (def h '(mpbiri {_ : $ch < ch$} lteq1))
  '(sylbi el_white @ eor ,h ,h) norm_num norm_num);

theorem white_lt_hyphen: $ c e. white -> c < _hyphen $ =
'(rsyl white_lt_dollar @ mpi (ltle _dollar_lt_hyphen) ltletr);

--| A predicate that matches a line comment: two hyphens,
--| then zero or more non-newline characters and a newline.
--|
--| `regexLineComment: Set String`
@_ def regexLineComment (.x .y: nat): set =
$ (\ x, _hyphen : _hyphen : x ++ _nl : 0) '' {x | all {y | y != _nl} x} $;

theorem el_regexLineComment: $ s e. regexLineComment <->
  E. x (all {y | y != _nl} x /\ s = _hyphen : _hyphen : (x ++ _nl : 0)) $ =
'(bitr ellamimaab @ exeqi @ aneq2i @ eqeq2 @ eqtr appendS @ conseq2 appendS);

theorem regexLineComment_n0: $ s e. regexLineComment -> s != 0 $ =
(named '(sylbi el_regexLineComment @ eex @ anwr sucne0));

theorem regexLineComment_hd: $ x : t e. regexLineComment -> x = _hyphen /\ t != 0 $ =
(named '(sylbi el_regexLineComment @ eex @ anwr @ sylbi consinj @ anim2 sucne0));

theorem regex_asymm_lem
  (hA: $ A == (\ x, l ++ x ++ c : 0) '' {x | all {y | y != c} x} $)
  (hs: $ G -> s e. A $) (ht: $ G -> t e. A $) (h: $ G -> prefix s t $): $ G -> s = t $ =
(focus
  (def (f x) '(sylib ellamimaab @ sylib (eleq2 hA) ,x))
  '(mpd h @ syl prefix_asymm @ mpd ,(f 'hs) @ eexda @
    mpd (sylibr _ ,(f '(anwl ht))) @ eexda _)
  '(!! cbvex z _ (aneqd alleq2 @ eqeq2d @ appendeq2d appendeq1))
  (def (f x) '(syl6eq (addeq2 appendlen) @ syl6eq appendlen @ leneqd ,x))
  '(mpbird (leeqd ,(f 'anrr) ,(f '(anrd anlr))) @ sylib leadd2 @ sylib leadd1 @
    sylibr lenlt @ mpi eqid @ con2d @
    exp @ sylib (elabe neeq1) @ sylc elall (anld anlr) @
    syl nthlmem @ eqtr3d (syl appendnth1 anr) @
    syl (mpi (eqtr (appendnth2 leid) @ eqtr (ntheq1 subid) nthZ) prefix_nth) @ anwl _)
  '(sylib prefix_append1 @ mpbid (prefixeqd (anrd anlr) anrr) (anwll h)));

theorem regexLineComment_asymm (hs: $ G -> s e. regexLineComment $) (ht: $ G -> t e. regexLineComment $)
  (h: $ G -> prefix s t $): $ G -> s = t $ =
(named @ focus
  '(regex_asymm_lem _ hs ht h)
  '(imaeq1 @ lameqi @ eqtr3 (appendeq1 @ eqtr appendS @ conseq2 append1) appendass));

--| A predicate that matches a semantic whitespace: either a whitespace character or a line comment.
--|
--| `whitespace: Set String`
@_ def whitespace (.c: nat): set =
$ ((\ c, c : 0) '' white) u. regexLineComment $;

theorem el_whitespace: $ s e. whitespace <->
  E. c (c e. white /\ s = c : 0) \/ s e. regexLineComment $ = '(bitr elun @ oreq1i ellamima);

theorem whitespace_n0: $ s e. whitespace -> s != 0 $ =
'(sylbi el_whitespace @ eor (!! eex x @ anwr sucne0) regexLineComment_n0);

theorem whitespace_hd: $ x : t e. whitespace -> x e. white \/ x = _hyphen $ =
(named '(sylbi el_whitespace @ orim
  (eex @ impcom @ bi2d @ sylbi consinj @ anwl eleq1)
  (anld regexLineComment_hd)));

theorem whitespace_lt_0: $ x : t e. whitespace -> x < _0 $ =
(focus
  '(rsyl whitespace_hd @ eor (sylbi el_white @ eor _ _) _)
  (def (p) @ focus '(mpbiri {_ : $ch < ch$} lteq1) norm_num)
  (p) (p) (p));

theorem whitespace_hd_RLC: $ x : t e. whitespace -> x = _hyphen -> x : t e. regexLineComment $ =
(named '(syl5 (con2 @ eex @ syl ltne @ syl white_lt_hyphen @
    impcom @ bi2d @ eleq1d @ sylbi consinj anl) @
  bi1 el_whitespace));

theorem whitespace_hd_white: $ x : t e. whitespace -> x != _hyphen -> x e. white /\ t = 0 $ =
'(sylbi el_whitespace @ eor
  (a1d @ !! eex y @ imp @ syl5bi consinj @ anim1d @ com12 @ bi2d eleq1)
  (syl absurdr @ anld regexLineComment_hd));

theorem whitespace_asymm (hs: $ G -> s e. whitespace $) (ht: $ G -> t e. whitespace $)
  (h: $ G -> prefix s t $): $ G -> s = t $ =
(named @ focus
  '(mpd (sylib excons @ syl whitespace_n0 hs) @ eexd @ eexda @ casesda _ _)
  (focus
    '(regexLineComment_asymm
      (mpbird (eleq1d anlr) @ sylc whitespace_hd_RLC (mpbid (eleq1d anlr) @ anwll hs) anr)
      (mpd (sylib prefix_S1 @ mpbid (prefixeq1d anlr) (anwll h)) @ eexda @ mpbird (eleq1d anrr) @
        sylc whitespace_hd_RLC (mpbid (eleq1d anrr) (anw3l ht)) anlr)
      (anwll h)))
  (focus
    '(eqtr4d (eqtrd anlr @ conseq2d @ anrd @
        sylc whitespace_hd_white (mpbid (eleq1d anlr) (anwll hs)) anr) @
      mpd (sylib prefix_S1 @ mpbid (prefixeq1d anlr) @ anwll h) @
      eexda @ eqtrd anrr @ conseq2d @ anrd @
      sylc whitespace_hd_white (mpbid (eleq1d anrr) (anw3l ht)) anlr)));

theorem whitespace_maxPrefix: $ s e. whitespace <-> maxPrefix whitespace (s ++ t) = suc (s, t) $ =
(named '(bitr4 (bicom @ bian1 eqid) (maxPrefix_asymm @ whitespace_asymm anll anlr anr)));

--| A predicate that matches a math string: zero or more non-`$` characters surrounded by `$`.
--|
--| `regexMath: Set String`
@_ def regexMath (.x .y: nat): set =
$ (\ x, _dollar : x ++ _dollar : 0) '' {x | all {y | y != _dollar} x} $;

theorem el_regexMath: $ s e. regexMath <->
  E. x (all {y | y != _dollar} x /\ s = _dollar : x ++ _dollar : 0) $ = 'ellamimaab;

theorem regexMath_n0: $ s e. regexMath -> s != 0 $ =
(named '(sylbi el_regexMath @ eex @ anwr @ sylbi (eqeq2 appendS) sucne0));

theorem regexMath_asymm (hs: $ G -> s e. regexMath $) (ht: $ G -> t e. regexMath $)
  (h: $ G -> prefix s t $): $ G -> s = t $ =
(named @ focus '(regex_asymm_lem _ hs ht h)
  '(imaeq1 @ lameqi @ eqtr3 (appendeq1 append1) appendass));

theorem regexMath_hd: $ x : t e. regexMath -> x = _dollar $ =
(named '(sylbi el_regexMath @ eex @ anwr @ sylbi (eqeq2 appendS) @ sylbi consinj anl));

theorem regexMath_maxPrefix: $ s e. regexMath <-> maxPrefix regexMath (s ++ t) = suc (s, t) $ =
(named '(bitr4 (bicom @ bian1 eqid) (maxPrefix_asymm @ regexMath_asymm anll anlr anr)));

--| The set of characters that can start an identifier: `[_A-Za-z]`
--|
--| `IdentStart: Set char`
@_ def IdentStart (.c: nat): set =
$ {c | (_a <= c /\ c <= _z) \/ (_A <= c /\ c <= _Z) \/ c = _under} $;

theorem el_IdentStart: $ c e. IdentStart <-> (_a <= c /\ c <= _z) \/ (_A <= c /\ c <= _Z) \/ c = _under $ =
(named '(elabe @ oreqd (oreqd (aneqd leeq2 leeq1) (aneqd leeq2 leeq1)) eqeq1));

theorem IdentStart_bound: $ c e. IdentStart -> _A <= c /\ c <= _z $ =
'(sylbi el_IdentStart @ eor
  (eor (anim1 @ letr @ ltle _A_lt_a) (anim2 @ mpi (ltle _Z_lt_z) letr))
  (mpbiri (ian (ltle _A_lt_under) (ltle _under_lt_z)) (aneqd leeq2 leeq1)));

--| The set of ASCII digits: `[0-9]`
--|
--| `digits: Set char`
@_ def digits (.c: nat): set = $ {c | _0 <= c /\ c <= _9} $;

theorem eldigits: $ c e. digits <-> _0 <= c /\ c <= _9 $ = (named '(elabe @ aneqd leeq2 leeq1));

theorem digits0: $ _0 e. digits $ = '(mpbir eldigits @ ian leid @ ltle _0_lt_9);
theorem digits9: $ _9 e. digits $ = '(mpbir eldigits @ ian (ltle _0_lt_9) leid);

--| The set of characters that are legal in an identifier: `[_A-Za-z0-9]`
--|
--| `IdentRest: Set char`
@_ def IdentRest (.c: nat): set = $ IdentStart u. digits $;

theorem IdentRest_bound: $ c e. IdentRest -> _0 <= c /\ c <= _z $ =
'(sylbi elun @ eor
  (rsyl IdentStart_bound @ anim1 @ letr @ ltle _0_lt_A)
  (sylbi eldigits @ anim2 @ mpi (ltle _9_lt_z) letr));

--| A regex that matches an identifier. Note: this is not deterministic, it allows end-extension
--|
--| `regexIdent: Set String`
@_ def regexIdent (.s .x .y .t: nat): set =
$ {s | E. x E. t (s = x : t /\ x e. IdentStart /\ all IdentRest t)} $;

theorem el_regexIdent: $ s e. regexIdent <->
  E. x E. t (s = x : t /\ x e. IdentStart /\ all IdentRest t) $ =
(named '(elabe @ exeqd @ exeqd @ aneq1d @ aneq1d eqeq1));

theorem regexIdent_n0: $ s e. regexIdent -> s != 0 $ =
(named '(sylbi el_regexIdent @ eex @ eex @ rsyl anll sucne0));

theorem regexIdent_cons: $ x : t e. regexIdent <-> x e. IdentStart /\ all IdentRest t $ =
(named '(bitr el_regexIdent @ bitr (exeqi @ bitr (exeqi @
    bitr anass @ bitr (aneq1i @ bitr eqcomb consinj) anass) exan1) @
  exeqe @ syl6bb (exeqe @ aneq2d alleq2) (exeqd @ aneq2d @ aneq1d eleq1)));

theorem regexIdent_bound: $ x : t e. regexIdent -> _A <= x /\ x <= _z $ =
'(sylbi regexIdent_cons @ anwl IdentStart_bound);

--| `s e. isNumber` is true if `s` denotes a natural number.
--| Leading `0` is not allowed, but `0` itself is okay.
--|
--| `isNumber: Set String`
@_ def isNumber (.s .x .y .t: nat): set =
$ sn (_0 : 0) u. {s | E. x E. t (s = x : t /\
  _1 <= x /\ x <= _9 /\ all digits t)} $;

theorem el_isNumber: $ s e. isNumber <-> s = _0 : 0 \/
  E. x E. t (s = x : t /\ _1 <= x /\ x <= _9 /\ all digits t) $ =
(named '(bitr elun @ oreq elsn @ elabe @ exeqd @ exeqd @ aneq1d @ aneq1d @ aneq1d eqeq1));

theorem isNumber_n0: $ s e. isNumber -> s != 0 $ =
(named '(sylbi el_isNumber @ eor sucne0 @ eex @ eex @ rsyl an3l sucne0));

theorem isNumber_allDigits: $ l e. isNumber -> all digits l $ =
(named '(sylbi el_isNumber @ eor (mpbiri (mpbir all1 digits0) alleq2) @
  eex @ eex @ mpbird (alleq2d an3l) @ sylibr allS @
  anim1 @ sylibr eldigits @ anim1 @ anwr @ letr _0_le_1));

theorem isNumber_hd: $ x : t e. isNumber -> _0 <= x /\ x <= _9 $ =
'(rsyl isNumber_allDigits @ sylbi allS @ sylib eldigits anl);

--| The set of MM0 punctuation characters in the "outer syntax": `* . : ; ( ) > { } =`
--|
--| `symbols: Set char`
@_ def symbols: nat =
$ _ast ; _dot ; _colon ; _semi ; _lparen ; _rparen ;
  _gt ; _lbrace ; _rbrace ; sn _equal $;

theorem symbols_bound: $ c e. symbols -> _dollar < c /\ c < _0 \/ _9 < c /\ c < _A \/ _z < c $ =
(focus
  (def (nn) (refine '{,norm_num : $ch _ _ < ch _ _$}))
  (def (d1 r) (r '(orld @ orld @ mpbiri (ian _ _) (aneqd lteq2 lteq1))) (nn) (nn))
  (def (d2 r) (r '(orld @ orrd @ mpbiri (ian _ _) (aneqd lteq2 lteq1))) (nn) (nn))
  (def (d3 r) (r '(orrd @ mpbiri _ lteq2)) (nn))
  (scan (list d1 d1 d2 d2 d1 d1 d2 d3 d3) @ fn (f)
    (f @ fn (x) @ refine '(sylbi elins @ eor ,x _)))
  (d2 @ fn (x) (refine '(sylbi elsn ,x))));

theorem symbols_bound2: $ c e. symbols -> _dollar < c /\ (c < _0 \/ _9 < c) /\ (c < _A \/ _z < c) $ =
'(rsyl symbols_bound @ iand (iand
  (eor (eor anl @ anwl @ lttr _dollar_lt_9) (lttr _dollar_lt_z))
  (eor (orim anr anl) (orrd @ lttr _9_lt_z)))
  (orim1 @ eor (anwr @ mpi _0_lt_A lttr) anr));

theorem symbols_ne_hyphen: $ c e. symbols -> c != _hyphen $ =
(focus
  (def (f) @ focus '(mpbiri {_ : $ch != ch$} neeq1) norm_num)
  (for 0 9 @ fn (_) (refine '(sylbi elins @ eor _ _)) (f))
  '(sylbi elsn _) (f));

--| A token: either punctuation or an identifier. `TK: String -> Token`
@_ def TK (s: nat): nat = $ b0 s $;
--| The (unparsed) contents of a math string: `MATH: String -> Token`
@_ def MATH (s: nat): nat = $ b1 s $;

@_ local def Tokenize_aux (G s A F n): nat =
$ if (maxPrefix A s = 0) n
    (obind (G @ snd (maxPrefix A s - 1)) (\ t,
      suc (F @ (fst (maxPrefix A s - 1), t)))) $;

theorem Tokenize_aux_0: $ maxPrefix A s = 0 -> Tokenize_aux G s A F n = n $ = (named 'ifpos);

theorem Tokenize_aux_n0 (a: nat x) {y} (h: $ y e. A -> y != 0 $):
  $ f = \. x e. upto s, a ->
    Tokenize_aux f s A F n = Tokenize_aux (\ x, a) s A F n $ =
(named @ focus
  '(casesda (anwr @ eqtr4d Tokenize_aux_0 Tokenize_aux_0) @
    eqtr4d (syl ifneg anr) @ eqtr4d (syl ifneg anr) @
    obindeq1d @ eqtrd (appeq1d @ sylibr (eqlower2 @ finlam finns) anl) _)
  (have 'h2 $ _ -> maxPrefix A s = suc _ $ '(eqcomd @ anwr consfstsnd))
  '(syl resapp @ sylibr elupto @ mpbid (lteq2d @ syl maxPrefixSi1 h2) @
    sylib ltappendid2 @ syl (sbeth h @ imeqd eleq1 neeq1) @ syl maxPrefixSi2 h2));

--| The MM0 lexer. This parses a full MM0 file into a list of tokens.
--|
--| `Tokenize: String -> Option (List Token)`
@_ abstract def Tokenize {.s1} (s: nat): nat =
$ srec (\ f, N[size (Dom f) / s1]
    if (s1 = 0) 1 (
    Tokenize_aux f s1 whitespace (\\ x, \ t, t) (
    Tokenize_aux f s1 regexIdent (\\ x, \ t, TK x : t) (
    Tokenize_aux f s1 isNumber (\\ x, \ t, TK x : t) (
    Tokenize_aux f s1 ((\ c, c : 0) '' symbols) (\\ x, \ t, TK x : t) (
    Tokenize_aux f s1 regexMath (\\ x, \ t, MATH x : t) (
    0))))))) s $;

theorem symbols_cons: $ x : b e. (\ c, c : 0) '' A <-> x e. A /\ b = 0 $ =
'(bitr ellamima @ bitr (exeqi @ bitr (aneq2i @
    bitr consinj @ aneq1i eqcomb) anlass) @ exeqe @ aneq1d eleq1);

theorem symbols_n0: $ x e. (\ c, c : 0) '' A -> x != 0 $ = '(sylbi ellamima @ eex @ anwr sucne0);

theorem symbols_asymm:
  $ x e. (\ c, c : 0) '' A /\ y e. (\ c, c : 0) '' A /\ prefix x y -> x = y $ =
(named '(imp @ imp @ sylbi ellamima @
  syl5bi (bitr ellamima @ cbvex @ aneqd eleq1 @ eqeq2d conseq1) @
  eex @ eexda @ mpbiri (sylbi prefix_S @ conseq1d anl) @
  imeqd (prefixeqd anlr anrr) (eqeqd anlr anrr)));

theorem symbols_maxPrefix: $ x e. A <-> maxPrefix ((\ c, c : 0) '' A) (x : t) = suc (x : 0, t) $ =
(named '(bitr2 (maxPrefix_asymm symbols_asymm) @
  bitr (bian1 append1) @ bitr symbols_cons @ bian2 eqid));

theorem Tokenize_val: $ Tokenize s = if (s = 0) 1 (
    Tokenize_aux (\ r, Tokenize r) s whitespace (\\ x, \ t, t) (
    Tokenize_aux (\ r, Tokenize r) s regexIdent (\\ x, \ t, TK x : t) (
    Tokenize_aux (\ r, Tokenize r) s isNumber (\\ x, \ t, TK x : t) (
    Tokenize_aux (\ r, Tokenize r) s ((\ c, c : 0) '' symbols) (\\ x, \ t, TK x : t) (
    Tokenize_aux (\ r, Tokenize r) s regexMath (\\ x, \ t, MATH x : t) (
    0)))))) $ =
(named @ focus
  '(eqtr {srecval : $ _ = _ @ rlam r _ (Tokenize r) $} @ applame @ sbned _)
  (have 'h '(eqtrd anr (anwl sreclem)))
  '(ifeqd (eqeq1d h) eqidd ,(foldr
    '(whitespace_n0 regexIdent_n0 isNumber_n0 symbols_n0 regexMath_n0)
    'eqidd
    (fn (x acc) '(eqtrd (Tokenize_auxeq2d h) @
      eqtrd (anwl @ !! Tokenize_aux_n0 _ y ,x) @ Tokenize_auxeq5d ,acc)))));

theorem Tokenize_aux_S (v1 n: nat x1 t1 r1) (v: nat t) (h: $ x1 = x /\ t1 = t -> v1 = v $):
  $ maxPrefix A s = suc (x, r) ->
    Tokenize_aux (\ r1, Tokenize r1) s A (\\ x1, \ t1, v1) n = obind (Tokenize r) (\ t, suc v) $ =
'(eqtrd (syl ifneg sucne0) @ obindeqd
  (applamed @ Tokenizeeqd @ eqtrd anr @ syl6eq sndpr @ sndeqd @ syl6eq sucsub1 @ subeq1d anl)
  (lameqd @ suceqd @ syl6eq (appslame @ applamed h) @
   appeq2d @ preq1d @ syl6eq fstpr @ fsteqd @ syl6eq sucsub1 subeq1));

pub theorem Tokenize0: $ Tokenize 0 = suc 0 $ = (named '(eqtr Tokenize_val @ ifpos eqid));

theorem Tokenize_n0_lem (h: $ x e. A -> x != 0 $): $ maxPrefix A s = suc (x, r) -> s != 0 $ =
'(mtd (rsyl maxPrefixSi2 h) @ mpbii anl @ imeq1d @ syl5bbr appendeq0 @ eqeq1d maxPrefixSi1);

pub theorem TokenizeWS (s x: nat):
  $ s e. whitespace -> Tokenize (s ++ x) = Tokenize x $ =
(named '(sylbi whitespace_maxPrefix @ syl5eq Tokenize_val @
  eqtrd (syl ifneg @ Tokenize_n0_lem whitespace_n0) @
  syl6eq obindS2 @ Tokenize_aux_S anr));

theorem Tokenize_ne_lem {a b c y} (p: wff a b c)
  (hA: $ x e. A -> x != 0 $) (hB: $ y e. B -> y != 0 $)
  (h1: $ a : b e. A -> p $) (h2: $ a : c e. B -> ~p $):
  $ maxPrefix A s = suc (x, r) -> maxPrefix B s = 0 $ =
(named @ focus
  '(mpd (sylib excons @ syl hA maxPrefixSi2) @ eexd @ eexda @ syl contra @
    syl5bi excons @ eexd @ eexda @
    mpd (anwr @ sylib excons @ syl hB maxPrefixSi2) @ eexd @ eexda @ sylc absurd
    (syl h2 @ mpbid (eleq1d _) @ syl maxPrefixSi2 anlr)
    (syl h1 @ mpbid (eleq1d anllr) @ syl maxPrefixSi2 an3l))
  '(eqtr4d anr @ conseq1d @ anld @ sylib consinj @
    syl5eqr appendS @ eqtr3d (appendeq1d anllr) @ eqtr4d (anw3l maxPrefixSi1) @
    syl5eqr appendS @ eqtr3d (appendeq1d anr) @ rsyl anlr maxPrefixSi1));

pub theorem TokenizeIdent {t: nat} (s x r: nat):
  $ maxPrefix regexIdent s = suc (x, r) ->
    Tokenize s = obind (Tokenize r) (\ t, suc (TK x : t)) $ =
(named '(syl5eq Tokenize_val @
  eqtrd (syl ifneg @ Tokenize_n0_lem regexIdent_n0) @
  eqtrd (syl Tokenize_aux_0 @ Tokenize_ne_lem regexIdent_n0 whitespace_n0
    (anld regexIdent_bound) (sylib ltnle @ syl (mpi _0_lt_A lttr) whitespace_lt_0)) @
  Tokenize_aux_S @ conseqd (TKeqd anl) anr));

pub theorem TokenizeNumber {t: nat} (s x r: nat):
  $ maxPrefix isNumber s = suc (x, r) ->
    Tokenize s = obind (Tokenize r) (\ t, suc (TK x : t)) $ =
(named '(syl5eq Tokenize_val @
  eqtrd (syl ifneg @ Tokenize_n0_lem isNumber_n0) @
  eqtrd (syl Tokenize_aux_0 @ Tokenize_ne_lem isNumber_n0 whitespace_n0
    (anld isNumber_hd) (sylib ltnle @ rsyl whitespace_hd @ eor
      (rsyl white_lt_dollar @ mpi _dollar_lt_0 lttr)
      (mpbiri (lelttr _hyphen_le_dot _dot_lt_0) lteq1))) @
  eqtrd (syl Tokenize_aux_0 @ Tokenize_ne_lem isNumber_n0 regexIdent_n0
    (anrd isNumber_hd) (sylib ltnle @ syl (ltletr _9_lt_A) @ anld regexIdent_bound)) @
  Tokenize_aux_S @ conseqd (TKeqd anl) anr));

pub theorem TokenizeSymbol {t: nat} (c x: nat):
  $ c e. symbols -> Tokenize (c : x) =
    obind (Tokenize x) (\ t, suc (TK (c : 0) : t)) $ =
(named @ focus
  (have 'n0 '(a1i consne0))
  (have 'bd '(sylbi symbols_cons anl))
  (have 'bd2 '(syl symbols_bound2 bd))
  '(syl5eq Tokenize_val @ syl5eq (ifneg consne0) @ sylbi symbols_maxPrefix @
    eqtrd (syl Tokenize_aux_0 @ Tokenize_ne_lem n0 whitespace_n0 bd @
      rsyl whitespace_hd @ eor
        (syl (con3 @ anld @ anld symbols_bound2) @ syl ltnlt @ white_lt_dollar)
        (con2 symbols_ne_hyphen)) @
    eqtrd (syl Tokenize_aux_0 @ Tokenize_ne_lem n0 regexIdent_n0 (anrd bd2) @
      sylibr notor @ sylib (aneq lenlt lenlt) regexIdent_bound) @
    eqtrd (syl Tokenize_aux_0 @ Tokenize_ne_lem n0 isNumber_n0 (anrd @ anld bd2) @
      sylibr notor @ sylib (aneq lenlt lenlt) isNumber_hd) @
    Tokenize_aux_S @ conseqd (TKeqd anl) anr));

pub theorem TokenizeMath {t: nat} (s x: nat):
  $ s e. regexMath -> Tokenize (s ++ x) =
    obind (Tokenize x) (\ t, suc (MATH s : t)) $ =
(named '(sylbi regexMath_maxPrefix @ syl5eq Tokenize_val @
  eqtrd (syl ifneg @ Tokenize_n0_lem regexMath_n0) @
  eqtrd (syl Tokenize_aux_0 @ Tokenize_ne_lem regexMath_n0 whitespace_n0 regexMath_hd @
    rsyl whitespace_hd @ eor (syl ltne white_lt_dollar) (mpbiri (ltner _dollar_lt_hyphen) neeq1)) @
  eqtrd (syl Tokenize_aux_0 @ Tokenize_ne_lem regexMath_n0 regexIdent_n0 regexMath_hd @
    rsyl regexIdent_bound @ anwl @ syl ltner @ ltletr _dollar_lt_A) @
  eqtrd (syl Tokenize_aux_0 @ Tokenize_ne_lem regexMath_n0 isNumber_n0 regexMath_hd @
    rsyl isNumber_hd @ anwl @ syl ltner @ ltletr _dollar_lt_0) @
  eqtrd (syl Tokenize_aux_0 @ Tokenize_ne_lem regexMath_n0 symbols_n0 regexMath_hd @
    sylbi symbols_cons @ anwl @ rsyl symbols_bound2 @ anwll ltner) @
  Tokenize_aux_S @ conseqd (MATHeqd anl) anr));

pub theorem TokenizeElse {x: nat} (s: nat):
  $ s != 0 ->
    ~(E. x (x e. whitespace /\ prefix x s)) ->
    maxPrefix regexIdent s = 0 ->
    maxPrefix isNumber s = 0 ->
    ~(E. x (x e. symbols /\ prefix (x : 0) s)) ->
    ~(E. x (x e. regexMath /\ prefix x s)) ->
    Tokenize s = 0 $ =
(named @ focus
  '(exp @ exp @ exp @ exp @ exp _)
  '(syl5eq Tokenize_val @ eqtrd (syl ifneg an5l) @
    eqtrd (syl Tokenize_aux_0 @ syl (sylbi (noteq @ exeqi ancomb) maxPrefix0) an4lr) @
    eqtrd (syl Tokenize_aux_0 an3lr) @
    eqtrd (syl Tokenize_aux_0 anllr) @
    eqtrd (syl Tokenize_aux_0 @ syl (syl maxPrefix0 @
      con3 @ eex @ imp @ syl5bi ellamima @ eximd @ anim2d @ com12 @ bi1d prefixeq1) anlr) @
    syl Tokenize_aux_0 @ syl (sylbi (noteq @ exeqi ancomb) maxPrefix0) anr));

-- Now the parser:

--| The `map` combinator on regexes. If `R` returns `a` on `s` then `regexMap F R` returns `F @ a`.
--|
--| `regexMap: (A -> B) -> Parser S A -> Parser S B`
@_ def regexMap (F R: set): set = $ R o> cnv F $;
infixr regexMap: $<@>$ prec 100;

--| The `seqLeft` combinator on regexes. Reads two regexes in sequence and keeps the first value.
--|
--| `regexAppL: Parser S A -> Parser S B -> Parser S A`
@_ def regexAppL (R S: set) (.x: nat): set = $ (\ x, fst x) <@> (R <+> S) $;
infixl regexAppL: $<+$ prec 77;

--| The `seqRight` combinator on regexes. Reads two regexes in sequence and keeps the second value.
--|
--| `regexAppR: Parser S A -> Parser S B -> Parser S B`
@_ def regexAppR (R S: set) (.x: nat): set = $ (\ x, snd x) <@> (R <+> S) $;
infixr regexAppR: $+>$ prec 76;

-- We will be interested in the special case `TParser A := Parser Token A` here.

--| A regex to parse token `tk` and returns `0`. `parseTk: String -> TParser ()`
def parseTk (tk: string): set = $ sn (TK tk, 0) $;
--| A regex to (nondeterministically) optionally parse token `tk`.
--| Returns `1` if it consumed `tk` and `0` otherwise. `parseOptTk: String -> TParser Bool`
def parseOptTk (tk: string): set = $ regexOpt (parseTk tk) $;
--| A regex to parse a single character `c`. `parseOptTk: String -> TParser ()`
def parseCh (c: char): set = $ parseTk (s1 c) $;

--| The string literal `"pure"`.
@_ def _pure: string = $ _p ': _u ': _r ': _e ': s0 $;
--| The string literal `"strict"`.
@_ def _strict: string = $ _s ': _t ': _r ': _i ': _c ': _t ': s0 $;
--| The string literal `"provable"`.
@_ def _provable: string = $ _p ': _r ': _o ': _v ': _a ': _b ': _l ': _e ': s0 $;
--| The string literal `"free"`.
@_ def _free: string = $ _f ': _r ': _e ': _e ': s0 $;

--| Parse the sort modifiers before a sort. `parseSortData: TParser SortData`
@_ def parseSortData: set =
$ (parseOptTk _pure <+> parseOptTk _strict) <+>
  (parseOptTk _provable <+> parseOptTk _free) $;

--| Parse an identifier or `_`. `parseIdent_: TParser Ident_`
@_ def parseIdent_ (.s: nat): set = $ (\ s, TK s, s) '' regexIdent $;
--| Parse an identifier. `parseIdent: TParser Ident`
@_ def parseIdent (.x: nat): set = $ parseIdent_ i^i {x | snd x != s1 _under} $;

--| `ASTSort (mods, s)` is the parsed result of `[mods] sort s;`.
--| `ASTSort: (SortData, String) -> AST`
@_ def ASTSort (x: nat): nat = $ b0 (b0 (b0 x)) $;
--| `ASTTerm (x, bis, b0 ret)` is the parsed result of `term x (bis): ret;`.
--| `ASTTerm: (Ident, List ASTBinder, ASTDepType) -> AST`
@_ def ASTTerm (x: nat): nat = $ b0 (b0 (b1 x)) $;
--| `ASTAxiom (x, bis, b1 concl)` is the parsed result of `axiom x (bis): concl;`.
--| `ASTAxiom: (Ident, List ASTBinder, Formula) -> AST`
@_ def ASTAxiom (x: nat): nat = $ b0 (b1 (b0 x)) $;
--| `ASTDef (x, bis, b0 ret, 0)` is the parsed result of `def x (bis): ret;`.
--| `ASTDef (x, bis, b0 ret, suc (b1 val))` is the result of `def x (bis): ret = $ val $;`.
--| `ASTDef: (Ident, List ASTBinder, ASTDepType, Option Formula) -> AST`
@_ def ASTDef (x: nat): nat = $ b0 (b1 (b1 x)) $;
--| `ASTThm (x, bis, b1 concl)` is the parsed result of `theorem x (bis): concl;`.
--| `ASTThm: (Ident, List ASTBinder, Formula) -> AST`
@_ def ASTThm (x: nat): nat = $ b1 (b0 (b0 x)) $;
--| An `input` or `output` declaration.
--| `ASTIO: Bool -> (Ident, List Token) -> AST`
@_ def ASTIO (out x: nat): nat = $ b1 (b0 (b1 (out, x))) $;
--| `ASTNota n` is a notation declatation. `ASTNota: Nota -> AST`
@_ def ASTNota (x: nat): nat = $ b1 (b1 x) $;

--| The string literal `"sort"`.
@_ def _sort: string = $ _s ': _o ': _r ': _t ': s0 $;
--| Parse a sort declaration. `parseSort: TParser AST`
@_ def parseSort (.x: nat): set = $ (\ x, ASTSort x) <@>
  (parseSortData <+> parseTk _sort +> parseIdent <+ parseCh _semi) $;

-- This throws all binders into a common parsed representation:
--
-- `BinderType := (Ident, List Ident) + String`,
-- with `ASTDepType` being the left variant and `Formula` being the right variant
--
-- `ASTBinder := (Fin 3, Ident_, BinderType)`
--
-- {x: set}     goes to    (1, "x", b0 ("set", []))
-- (x: set)     goes to    (0, "x", b0 ("set", []))
-- (x: set y)   goes to    (0, "x", b0 ("set", ["y"]))
-- (x: $foo$)   goes to    (0, "x", b1 "foo")
-- (_: $foo$)   goes to    (0, "_", b1 "foo")
-- (.x: set)    goes to    (2, "x", b0 ("set", []))

--| Parse a type binder. `parseType: TParser ASTDepType`
@_ def parseType (.x: nat): set = $ (\ x, b0 x) <@>
  (parseIdent <+> regexStar parseIdent) $;
--| Parse a formula binder. `parseFmla: TParser Formula`
@_ def parseFmla (.s: nat): set = $ Ran (\ s, MATH s, b1 s) $;
--| Parse a type or formula binder. `parseTypeFmla: TParser BinderType`
@_ def parseTypeFmla: set = $ parseType u. parseFmla $;

--| Parse a binder variable or dummy variable. `parseDummyId: TParser (Ident_ + Ident)`
@_ def parseDummyId (.x: nat): set =
$ (\ x, b0 x) <@> parseIdent_ u.
  (\ x, b1 x) <@> (parseCh _dot +> parseIdent) $;

--| Parse a binder surrounded in `{}` braces. `parseCurlyBinder: TParser (List ASTBinder)`
@_ def parseCurlyBinder (.x .z: nat): set =
$ (\ z, map (case (\ x, 1, x, snd z) (\ x, 2, x, snd z)) (fst z)) <@>
  (parseCh _lbrace +> regexStar parseDummyId <+>
    parseCh _colon +> parseTypeFmla <+ parseCh _rbrace) $;
--| Parse a binder surrounded in `()` parentheses. `parseRegBinder: TParser (List ASTBinder)`
@_ def parseRegBinder (.x .z: nat): set =
$ (\ z, map (case (\ x, 0, x, snd z) (\ x, 2, x, snd z)) (fst z)) <@>
  (parseCh _lparen +> regexStar parseDummyId <+>
    parseCh _colon +> parseTypeFmla <+ parseCh _rparen) $;
--| Parse a binder. `parseBinder: TParser (List ASTBinder)`
@_ def parseBinder (.x .y: nat): set = $ parseCurlyBinder u. parseRegBinder $;

--| Parse a list of binders. `parseRegBinder: TParser (List ASTBinder)`
@_ def parseBinders (.x .z: nat): set =
$ (\ x, ljoin x) <@> regexStar parseBinder $;

--| Parse a sequence of formulas separated by `>`.
--|
--| `parseArrows: TParser (List BinderType, BinderType)`
@_ def parseArrows: set =
$ regexStar (parseTypeFmla <+ parseCh _gt) <+> parseTypeFmla $;

--| Parse a sequence of binders, then a colon, then an arrow-list.
--| The arrow-list hypotheses are converted to anonymous binders.
--|
--| `parseBindersAndArrows: TParser (List ASTBinder, BinderType)`
@_ def parseBindersAndArrows (.x .z: nat): set =
$ (\ x, fst x ++ map (\ z, (0, s1 _under, z)) (pi21 x), pi22 x) <@>
  (parseBinders <+> parseCh _colon +> parseArrows) $;

--| Parse a simple declaration of the form `tk ident (binders): concl;`.
--|
--| `parseSimple: String -> TParser (Ident, List ASTBinder, BinderType)`
def parseSimple (tk: string): set =
$ parseTk tk +> parseIdent <+> parseBindersAndArrows <+ parseCh _semi $;

--| The string literal `"term"`.
@_ def _term: string = $ _t ': _e ': _r ': _m ': s0 $;
--| Parse a term constructor declaration. `parseTerm: TParser AST`
@_ def parseTerm (.x: nat): set = $ (\ x, ASTTerm x) <@> parseSimple _term $;

--| The string literal `"axiom"`.
@_ def _axiom: string = $ _a ': _x ': _i ': _o ': _m ': s0 $;
--| Parse an axiom declaration. `parseAxiom: TParser AST`
@_ def parseAxiom (.x: nat): set = $ (\ x, ASTAxiom x) <@> parseSimple _axiom $;

--| The string literal `"theorem"`.
@_ def _theorem: string = $ _t ': _h ': _e ': _o ': _r ': _e ': _m ': s0 $;
--| Parse a theorem declaration. `parseThm: TParser AST`
@_ def parseThm (.x: nat): set = $ (\ x, ASTThm x) <@> parseSimple _theorem $;

--| The string literal `"def"`.
@_ def _def: string = $ _d ': _e ': _f ': s0 $;
--| Parse a `def` declaration. `parseDef: TParser AST`
@_ def parseDef (.x: nat): set = $ (\ x, ASTDef x) <@>
  (parseTk _theorem +> parseIdent <+> parseBinders <+>
    parseCh _colon +> parseType <+>
    regexOpt (parseCh _equal +> parseFmla) <+ parseCh _semi) $;

--| A delimiter declaration. `NotaDelim: (Formula, Formula) -> Nota`
@_ def NotaDelim (x: nat): nat = $ b0 (b0 x) $;
--| An infix declaration. `NotaInfix: Bool -> (Ident, Formula, Prec) -> Nota`
@_ def NotaInfix (x y: nat): nat = $ b0 (b1 (b0 (x, y))) $;
--| A prefix declaration. `NotaPfx: (Ident, Formula, Prec) -> Nota`
@_ def NotaPfx (x: nat): nat = $ b0 (b1 (b1 x)) $;
--| A coercion declaration. `NotaCoe: (Ident, Ident, Ident) -> Nota`
@_ def NotaCoe (x: nat): nat = $ b1 (b0 x) $;
--| A general notation declaration.
--| `NotaGen: (Ident, List Binder, ASTDepType, List Literal) -> Nota`
@_ def NotaGen (x: nat): nat = $ b1 (b1 x) $;

--| The string literal `"delimiter"`.
@_ def _delimiter: string =
$ _d ': _e ': _l ': _i ': _m ': _i ': _t ': _e ': _r ': s0 $;
--| Parse a `delimiter` declaration. `parseDelim: TParser (Formula, Formula)`
@_ def parseDelim (.x: nat): set = $ (\ x, NotaDelim x) <@>
  (parseTk _delimiter +>
    (((\ x, x, x) <@> parseFmla) u.
     (parseFmla <+> parseFmla)) <+ parseCh _semi) $;

--| Convert a string representing a number to a natural number. `stoi: String -> nat`
@_ abstract def stoi (x: nat): nat = $ rlrec 0 (\\ s, \\ i, \ ih, ih * 10 + (i - _0)) x $;
pub theorem stoi0: $ stoi 0 = 0 $ = (named 'rlrec0);
pub theorem stoiS (s x: nat): $ stoi (s |> x) = stoi s * 10 + (x - _0) $ =
(named '(eqtr {rlrecS : $ _ = _ @ (_, _, stoi _) $} @
  appslame @ appslamed @ applamed @ addeqd (muleq1d anr) (subeq1d anlr)));

--| Parse a numerical expression. `parseNumber: TParser nat`
@_ def parseNumber (.s: nat): set = $ (\ s, TK s, stoi s) '' isNumber $;

--| The string literal `"max"`.
@_ def _max: string = $ _m ': _a ': _x ': s0 $;
--| Parse a precendence, `parsePrec: TParser Prec` where `Prec := Option nat`
@_ def parsePrec (.x: nat): set = $ parseTk _max u. (\ x, suc x) <@> parseNumber $;

--| The string literal `"prec"`.
@_ def _prec: string = $ _p ': _r ': _e ': _c ': s0 $;
--| Parse a simple notation declaration of the form `tk name: $constant$ prec num;`.
--| `parseSimpleNota: String -> TParser (Ident, Formula, Prec)`
def parseSimpleNota (tk: string): set =
$ parseTk tk +> parseIdent <+> parseCh _colon +> parseFmla <+>
    parseTk _prec +> parsePrec <+ parseCh _semi $;

--| The string literal `"infixl"`.
@_ def _infixl: string = $ _i ': _n ': _f ': _i ': _x ': _l ': s0 $;
--| The string literal `"infixr"`.
@_ def _infixr: string = $ _i ': _n ': _f ': _i ': _x ': _r ': s0 $;
--| The string literal `"prefix"`.
@_ def _prefix: string = $ _p ': _r ': _e ': _f ': _i ': _x ': s0 $;
--| Parse a left-associative infix notation. `parseInfixl: TParser Nota`
@_ def parseInfixl (.x: nat): set = $ (\ x, NotaInfix 0 x) <@> parseSimpleNota _infixl $;
--| Parse a right-associative infix notation. `parseInfixl: TParser Nota`
@_ def parseInfixr (.x: nat): set = $ (\ x, NotaInfix 1 x) <@> parseSimpleNota _infixr $;
--| Parse a prefix notation. `parsePrefix: TParser Nota`
@_ def parsePfx (.x: nat): set = $ (\ x, NotaPfx x) <@> parseSimpleNota _prefix $;

--| The string literal `"coercion"`.
@_ def _coercion: string = $ _c ': _o ': _e ': _r ': _c ': _i ': _o ': _n ': s0 $;
--| Parse a coercion notation. `parseCoe: TParser Nota`
@_ def parseCoe (.x: nat): set = $ (\ x, NotaCoe x) <@>
  (parseTk _coercion +> parseIdent <+>
   parseCh _colon +> parseIdent <+>
   parseCh _gt +> parseIdent <+ parseCh _semi) $;

--| Parse a literal in a general notation. `parseLiteral: TParser Literal`,
--| where `Literal := (Formula, Prec) + Ident`
@_ def parseLiteral (.x: nat): set =
$ ((\ x, b0 x) <@> (parseCh _lparen +> parseFmla <+>
    parseCh _colon +> parsePrec <+ parseCh _rparen)) u.
  ((\ x, b1 x) <@> parseIdent) $;

--| The string literal `"notation"`.
@_ def _notation: string = $ _n ': _o ': _t ': _a ': _t ': _i ': _o ': _n ': s0 $;
--| Parse a general notation. `parseGenNota: TParser Nota`
@_ def parseGenNota (.x: nat): set = $ (\ x, NotaGen x) <@>
  (parseTk _notation +> parseIdent <+>
   parseBinders <+> parseCh _colon +> parseType <+>
   parseCh _equal +> regexPlus parseLiteral <+ parseCh _semi) $;

@_ def parseNota (.x: nat): set = $ (\ x, ASTNota x) <@>
  (parseDelim u. parseInfixl u. parseInfixr u. parsePfx u.
    parseCoe u. parseGenNota) $;

--| The string literal `"input"`.
@_ def _input: string = $ _i ': _n ': _p ': _u ': _t ': s0 $;
--| The string literal `"output"`.
@_ def _output: string = $ _o ': _u ': _t ': _p ': _u ': _t ': s0 $;

--| The supported set of input kinds, currently empty. `inputKinds: Set String`
@_ def inputKinds: nat = $0$;
--| The supported set of output kinds, currently empty. `outputKinds: Set String`
@_ def outputKinds: nat = $0$;

--| Parse an input or output declaration.
--| `parseIO1: String -> Set String -> TParser (Ident, List Token)`
def parseIO1 (tk: string) (k .x .s: nat): set =
$ parseTk tk +> (parseIdent i^i {x | snd x e. k}) <+>
  parseCh _colon +>
    regexStar (((\ s, TK s) <@> parseIdent) u. Ran (\ s, MATH s, MATH s))
    <+ parseCh _semi $;

--| Parse an input or output declaration. `parseIO: TParser AST`
@_ def parseIO (.x: nat): set =
$ ((\ x, ASTIO 0 x) <@> parseIO1 _input inputKinds) u.
  ((\ x, ASTIO 1 x) <@> parseIO1 _output outputKinds) $;

--| Parse a full file AST. `parseAST: TParser (List AST)`
@_ def parseAST: set =
$ regexStar (parseSort u. parseTerm u. parseAxiom u.
    parseThm u. parseDef u. parseNota u. parseIO) $;

--| Parse the string contents of a file. `parse: String -> List AST -> Bool`
@_ def parse (s ast .tks: nat): wff =
$ E. tks (Tokenize s = suc tks /\ tks, ast e. parseAST) $;

--------------------
-- AST Navigation --
--------------------

--| Look up a variable in the context to get its index.
--| `lookupVar: List ASTBinder -> Ident -> Option Nat`
@_ abstract def lookupVar (ctx x: nat): nat =
$ rlrec 0 (\\ bis, \\ p, \ ih, N[fst (snd p) / y] if (x = y) (suc (len bis)) ih) ctx $;

pub theorem lookupVar0 (x: nat): $ lookupVar 0 x = 0 $ = (named 'rlrec0);

theorem lookupVarS:
  $ lookupVar (bis |> (c, x, t)) y =
    if (y = x) (suc (len bis)) (lookupVar bis y) $ =
(named '(eqtr {rlrecS : $ _ = _ @ (_, _, lookupVar _ _) $} @
  appslame @ appslamed @ applamed @ sbned @
  ifeqd (eqeq2d @ eqtrd anr @ syl6eq fstpr @ fsteqd @ syl6eq sndpr @ sndeqd anllr)
    (suceqd @ leneqd an3l) anlr));

pub theorem lookupVarEq (bis c x t: nat):
  $ lookupVar (bis |> (c, x, t)) x = suc (len bis) $ = '(eqtr lookupVarS @ ifpos eqid);
pub theorem lookupVarNe (bis c x y t: nat): $ y != x ->
  lookupVar (bis |> (c, x, t)) y = lookupVar bis y $ = '(syl5eq lookupVarS ifneg);

------------------
-- Math Parsing --
------------------

--| `s e. nonemptyNonwhite` means that `s` is a nonempty list of non-whitespace characters.
--| `nonemptyNonwhite: Set String`
@_ def nonemptyNonwhite (.s .c: nat): set =
$ {s | s != 0 /\ all {c | ~c e. white} s} $;

theorem el_nonemptyNonwhite: $ s e. nonemptyNonwhite <-> s != 0 /\ all {c | ~c e. white} s $ =
(named '(elabe @ aneqd neeq1 alleq2));

--| `simpleTokenize s` splits `s` into chunks of non-whitespace characters separated by whitespace.
--| `simpleTokenize: String -> List String`
@_ abstract def simpleTokenize {.s1} (s: nat): nat =
$ srec (\ f,
    lrec 0 (\\ c, \\ s1, \ _ih,
      if (c e. white) (f @ s1) (
        N[maxPrefix nonemptyNonwhite (c : s1) - 1 / p]
        (fst p : f @ snd p)))
    (size (Dom f))) s $;

theorem simpleTokenize_val: $ simpleTokenize s =
  lrec 0 (\\ c, \\ t, \ _ih,
      if (c e. white) ((\. r e. upto s, simpleTokenize r) @ t) (
        N[maxPrefix nonemptyNonwhite (c : t) - 1 / p]
        (fst p : (\. r e. upto s, simpleTokenize r) @ snd p))) s $ =
(named @ focus
  '(eqtr {srecval : $ _ = _ @ rlam r _ (simpleTokenize r) $} @
    applame @ lreceqd eqidd (slameqd @ slameqd @ lameqd _) sreclem)
  '(ifeqd biidd appneq1 @ sbneq2d @ conseq2d appneq1));

pub theorem simpleTokenize0: $ simpleTokenize 0 = 0 $ = (named '(eqtr simpleTokenize_val lrec0));

theorem simpleTokenize_S: $ s = c : t -> simpleTokenize s =
  if (c e. white) (simpleTokenize t) (
    N[maxPrefix nonemptyNonwhite s - 1 / p]
    (fst p : (\. r e. upto s, simpleTokenize r) @ snd p)) $ =
(named @ focus
  '(syl5eq simpleTokenize_val @ eqtrd lreceq3 @ syl5eq lrecS @
    sbeth _ @ imeq2d @ eqeq1d @ appeq2d @ preq2d preq2)
  '(appslamed @ appslamed @ applamed @ anwl @
    ifeqd (eleq1d anlr)
      (apprlamed (simpleTokenizeeqd @ eqtrd anr anlr) @
        sylibr elupto @ mpbiri ltconsid2 (lteqd anr anll))
      (sbneq1d @ subeq1d @ maxPrefixeq2d @ eqtr4d (conseqd anlr anr) anll)));

pub theorem simpleTokenizeWS (c s: nat):
  $ c e. white -> simpleTokenize (c : s) = simpleTokenize s $ =
(named '(syl5eq (simpleTokenize_S eqid) ifpos));

pub theorem simpleTokenizeTk (s x r: nat):
  $ maxPrefix nonemptyNonwhite s = suc (x, r) ->
    simpleTokenize s = x : simpleTokenize r $ =
(named @ focus
  (have 'h '(sylib el_nonemptyNonwhite maxPrefixSi2))
  (have 'h2 '(anwl maxPrefixSi1))
  '(mpd (sylib excons @ anld h) @ eexd @ eexda @
    eqtrd (syl simpleTokenize_S @ eqtr3d h2 @ syl6eq appendS @ appendeq1d anr) @
    eqtrd (syl ifneg @ sylib (elabe @ noteqd eleq1) @
      syl (mpi lmemconsid elall) @ mpbid (alleq2d anr) (anrd @ anwl h)) @
    eqtrd (sbneq1d @ syl6eq sucsub1 @ subeq1d anl) @
    sbned @ conseqd (syl6eq fstpr @ fsteqd anr) @
    eqtrd (appeq2d @ syl6eq sndpr @ sndeqd anr) @ anwl @
    syl (apprlame simpleTokenizeeq) @
    sylibr elupto @ mpbid (lteq2d h2) @ sylib ltappendid2 @ anwl @ anld h));

theorem simpleTokenize_infix: $ all {x | x e. nonemptyNonwhite /\ E. a E. b s = a ++ x ++ b} (simpleTokenize s) $ =
(named @ focus
  (def h '(alleqd (abeqd @ aneq2d @ exeqd @ exeqd eqeq1) simpleTokenizeeq))
  '(trud @ !! indstr y z ,h ,h @ anwr @ cases _ _)
  '(a1d @ mpbiri all0 @ alleq2d @ syl6eq simpleTokenize0 simpleTokenizeeq)
  '(sylbi excons @ eex @ eex @ casesda _ _)
  '(ealde @ eimd (mpbiri ltconsid2 @ lteqd anr anll) @
    syld (syl ssall @ ssabd @ anim2d @
      syl5bi (cbvex @ exeqd @ eqeq2d appendeq1) @
      eexd @ iexdde @ eximd @ exp @ eqtr4d an4l @
      eqtr4d (syl6eq appendS @ appendeq1d anlr) @
      conseq2d @ eqtr3d anllr anr) @
    bi2d @ alleq2d @ mpbird (eqeqd (simpleTokenizeeqd anll) (simpleTokenizeeqd anr)) @
    syl simpleTokenizeWS anlr)
  (have 'h1 '(mpbiri (mpbir prefix_S @ ian eqid prefix_0) (prefixeq2d anl)))
  (have 'h2
    '(sylibr el_nonemptyNonwhite @ iand (a1i consne0) @
      sylibr all1 @ sylibr (elabe @ noteqd eleq1) anr))
  '(rsyl (maxPrefix_eqS h1 h2) @
    eex @ exp @ rsyl exanal @ eex @ imp @
    eimd (mpbid (lteq2d maxPrefixSi1) @
      sylib ltappendid2 @ anld @ sylib el_nonemptyNonwhite maxPrefixSi2) @
    syld (syl ssall @ ssabd @ anim2d @
      syl5bi (cbvex @ exeqd @ eqeq2d appendeq1) @
      eexd @ iexdde @ eximd @ exp @ eqtr3d (anwll maxPrefixSi1) @
      eqtr4d (appendeq2d anr) @ syl6eq appendass @ appendeq1d anlr) @
    bi2d @ bitrd (alleq2d simpleTokenizeTk) @ syl5bb allS @ syl bian1 @
    sylibr (elabe @ aneqd eleq1 @ exeqd @ exeqd @ eqeq2d @ appendeq2d appendeq1) @
    iand maxPrefixSi2 @ iexde @ iexde @
    eqtr2d (syl5eqr appendass @ appendeqd (syl6eq append0 @ appendeq1d anlr) anr) @
    anwll maxPrefixSi1));

theorem simpleTokenize_nonemptyNonwhite: $ all nonemptyNonwhite (simpleTokenize s) $ =
(named '(ssall (mpbi ssab1 @ ax_gen anl) simpleTokenize_infix));

theorem simpleTokenize_le: $ c IN simpleTokenize s -> c <= s $ =
(named '(rsyl (elall simpleTokenize_infix) @
  sylbi (elabe @ aneqd eleq1 @ exeqd @ exeqd @ eqeq2d @ appendeq2d appendeq1) @
  anwr @ eex @ eex @ mpbiri (letr leappendid1 leappendid2) leeq2));

--| Compute the list of valid delimiters from the given AST.
--| `getDelimiters: List AST -> (Set char, Set char)`
@_ abstract def getDelimiters (ast: nat): nat =
$ rlrec 0 (\\ a, \\ t, \ ih,
  if (E. l E. r t = ASTNota (NotaDelim (b1 l, b1 r))) (
    N[t // 2 // 2 // 2 // 2 / p] (
      lower (fst ih u. lmems (simpleTokenize (fst p // 2))),
      lower (snd ih u. lmems (simpleTokenize (snd p // 2)))))
    ih) ast $;

pub theorem getDelimiters0: $ getDelimiters 0 = 0, 0 $ = (named '(eqtr4 rlrec0 pr0));

theorem getDelimitersS (h1: $ t // 2 // 2 // 2 // 2 = p $)
  (h2: $ fst p // 2 = x $) (h3: $ snd p // 2 = y $):
  $ getDelimiters ast = a, b -> getDelimiters (ast |> t) =
    if (E. l E. r t = ASTNota (NotaDelim (b1 l, b1 r))) (
      lower (a u. lmems (simpleTokenize x)),
      lower (b u. lmems (simpleTokenize y)))
    (getDelimiters ast) $ =
(named @ focus
  '(syl5eq {rlrecS : $ _ = _ @ (_, _, getDelimiters _) $} @
    appslamed @ appslamed @ applamed @ ifeqd (exeqd @ exeqd @ eqeq1d anlr) _ anr)
  (def (f x y z) '(lowereqd @ uneqd (nseqd @ syl6eq ,x @ ,y @ eqtrd anlr an4l) @
    nseqd @ lmemseqd @ simpleTokenizeeqd @ syl6eq ,z @ diveq1d @ ,y anr))
  '(eqtrd (sbneq1d @ syl6eq h1 @ diveq1d @ diveq1d @ diveq1d @ diveq1d anlr) @
    sbned @ preqd ,(f 'fstpr 'fsteqd 'h2) ,(f 'sndpr 'sndeqd 'h3)));

pub theorem getDelimitersDelim (ast a b l r: nat):
  $ getDelimiters ast = a, b ->
    getDelimiters (ast |> ASTNota (NotaDelim (b1 l, b1 r))) =
      lower (a u. lmems (simpleTokenize l)),
      lower (b u. lmems (simpleTokenize r)) $ =
(named @ let ([(f x th) '(eqtr (diveq1 ,th) ,x)])
  '(syl6eq (ifpos @ iexde (iexde @
      eqcomd @ ASTNotaeqd @ NotaDelimeqd @ preqd (b1eqd anlr) (b1eqd anr)) eqid) @
    getDelimitersS
      ,(foldr '(b0div2 b0div2 b1div2) 'b1div2 f)
      ,(f 'b1div2 'fstpr) ,(f 'b1div2 'sndpr)));

pub theorem getDelimitersOther {l r: nat} (ast t: nat):
  $ ~(E. l E. r t = ASTNota (NotaDelim (b1 l, b1 r))) ->
    getDelimiters (ast |> t) = getDelimiters ast $ =
'(syl5eq (getDelimitersS eqid eqid eqid @ eqcom fstsnd) ifneg);

theorem getDelimiters_nonemptyNonwhite:
  $ x e. fst (getDelimiters ast) \/ x e. snd (getDelimiters ast) ->
    x e. nonemptyNonwhite $ =
(named @ induct '(rlistind) 'ast
  '(sylbi (oreq
        (elneq2 @ eqtr (fsteq getDelimiters0) fstpr)
        (elneq2 @ eqtr (sndeq getDelimiters0) sndpr))
      (sylbi oridm @ absurd nel0))
  (def h '(bitr (ellower @ unfin finns finns) elun))
  (def h2 '(elall simpleTokenize_nonemptyNonwhite))
  '(casesd
    (eexd @ eexd @ syl5ibrcom
      (imeq1d @
        rsyl (syl6eq (getDelimitersDelim @ eqcom fstsnd) @ getDelimiterseqd snoceq2) @
        oreqd (elneq2d @ syl6eq fstpr fsteq) (elneq2d @ syl6eq sndpr sndeq)) @
      syl5bi (oreq ,h ,h) @ syl5bi or4 @ eord id @ a1i @ eor ,h2 ,h2)
    (com12 @ bi2d @ imeq1d @ rsyl getDelimitersOther @
      oreqd (elneq2d fsteq) (elneq2d sndeq))));

--| Validation of a delimiter set. Delimiters must be one character in this implementation.
--| `delimitersOk: Set char -> Bool`
@_ def delimitersOk (A: set) (.x .y: nat): wff =
$ A. x (x e. A -> len x = 1) $;

@_ local def delimiterFree (ast: nat): set =
$ {s | ~(E. l E. x E. r (x e. getDelimiters ast /\ s = l ++ x ++ r))} $;

--| Tokenize a formula using the delimiters from the given AST context.
--| `tokenizeFmla: List AST -> String -> List String`
@_ abstract def tokenizeFmla (ast f: nat): nat =
$ lrec 0 (\\ x, \\ xs, \ ih,
    if (x e. white) ih (
      if (x : 0 e. fst (getDelimiters ast) \/
          A. y A. r (xs = y : r -> y e. white \/ y : 0 e. snd (getDelimiters ast)))
        ((x : 0) : ih)
        ((x : fst (ih - 1)) : snd (ih - 1))))
  f $;

pub theorem tokenizeFmla0 (ast: nat): $ tokenizeFmla ast 0 = 0 $ = (named 'lrec0);

theorem tokenizeFmlaS: $ tokenizeFmla ast xs = ih ->
  tokenizeFmla ast (x : xs) = if (x e. white) ih (
    if (x : 0 e. fst (getDelimiters ast) \/
        A. y A. r (xs = y : r -> y e. white \/ y : 0 e. snd (getDelimiters ast)))
      ((x : 0) : ih)
      ((x : fst (ih - 1)) : snd (ih - 1))) $ =
(named @ focus
  '(syl5eq lrecS @ syl6eq _ @ appeq2d @ preq2d preq2)
  '(appslame @ appslamed @ applamed @ ifeqd (eleq1d anll) anr @
    ifeqd (oreqd (eleq1d @ conseq1d anll) (aleqd @ aleqd @ imeq1d @ eqeq1d anlr))
      (conseqd (conseq1d anll) anr)
      (conseqd (conseqd anll @ fsteqd @ subeq1d anr) (sndeqd @ subeq1d anr))));

theorem tokenizeFmlaS_n0: $ ~x e. white -> tokenizeFmla ast (x : xs) != 0 $ =
(named @ focus
  (def (f x) '(mpbiri consne0 @ neeq1d ,x))
  '(mpbiri (cases ,(f 'ifpos) ,(f 'ifneg)) @ neeq1d @ syl5eq (tokenizeFmlaS eqid) ifneg));

pub theorem tokenizeFmlaWhite: $ x e. white -> tokenizeFmla ast (x : xs) = tokenizeFmla ast xs $ =
(named '(syl5eq (tokenizeFmlaS eqid) ifpos));

pub theorem tokenizeFmla1: $ ~x e. white -> tokenizeFmla ast (x : 0) = (x : 0) : 0 $ =
(named '(syl5eq (tokenizeFmlaS tokenizeFmla0) @
  syl6eq (ifpos @ orr @ ax_gen @ ax_gen @ absurd @ necom consne0) ifneg));

theorem tokenizeFmlaSS: $ tokenizeFmla ast (y : xs) = ih -> ~x e. white ->
  tokenizeFmla ast (x : y : xs) =
  if (x : 0 e. fst (getDelimiters ast) \/ y e. white \/ y : 0 e. snd (getDelimiters ast))
    ((x : 0) : ih)
    ((x : fst (ih - 1)) : snd (ih - 1)) $ =
(named @ focus
  '(exp @ eqtrd (anwl tokenizeFmlaS) @ syl6eqr _ @ anwr ifneg)
  '(ifeq1 @ bitr4 orass @ oreq2 @ bitr3 _ @ aleqe @ oreqd eleq1 (eleq1d conseq1))
  '(aleqi @ bitr3 (aleqe biidd) @ aleqi @ bitr3 impexp @ imeq1i @ bitr ancomb @ bitr3 consinj eqcomb));

theorem tokenizeFmla_nonemptyNonwhite_lem: $ all nonemptyNonwhite l /\ ~x e. white ->
   all nonemptyNonwhite ((x : 0) : 0) /\ all nonemptyNonwhite ((x : fst (l - 1)) : snd (l - 1)) $ =
(named @ focus
  (def h '(elabe @ noteqd eleq1))
  (def (f x y z) '(sylibr allS @ iand (sylibr el_nonemptyNonwhite @
    iand (a1i consne0) @ sylibr allS @ iand (sylibr ,h ,x) ,y) ,z))
  '(mpd ,(f 'anr '(a1i all0) '(a1i all0)) @ exp @ iand anr @
    casesd (exp @ mpbird (alleq2d @ conseqd
      (conseq2d @ syl6eq fst0 @ fsteqd @ syl6eq sub01 @ subeq1d anr) @
      syl6eq snd0 @ sndeqd @ syl6eq sub01 @ subeq1d anr) anlr) @
    syl5bi excons @ eexd @ eexda _)
  (have 'h2 '(sylib allS @ mpbid (alleq2d anr) an3l))
    ,(f 'anllr
      '(mpbird (alleq2d @ syl6eq fstpr @ fsteqd @ syl6eq sucsub1 @ subeq1d anr) @ anrd @
        sylib el_nonemptyNonwhite @ anld h2)
      '(mpbird (alleq2d @ syl6eq sndpr @ sndeqd @ syl6eq sucsub1 @ subeq1d anr) @ anrd h2)));

theorem tokenizeFmla_nonemptyNonwhite: $ all nonemptyNonwhite (tokenizeFmla ast xs) $ =
(named @ focus
  (induct '(listind) 'xs '(mpbir (alleq2 tokenizeFmla0) all0) _)
  (def h '(mpbir (elabe neeq1) consne0))
  (def h2 '(bitr el_nonemptyNonwhite @
    bitr (bian1 consne0) @ bitr all1 @ elabe @ noteqd eleq1))
  '(casesd (com12 @ bi2d @ alleq2d @ syl5eq (tokenizeFmlaS eqid) ifpos) @ exp _)
  (have 'h '(tokenizeFmla_nonemptyNonwhite_lem))
  '(casesd
    (exp @ mpbird (alleq2d @ eqtrd (tokenizeFmlaeq2d @ conseq2d anr) (syl tokenizeFmla1 anlr)) @
      anwl @ anld h)
    (syl5bi excons @ eexd @ eexda @
      mpbird (alleq2d @ eqtrd (tokenizeFmlaeq2d @ conseq2d anr) (rsyl anlr @ tokenizeFmlaSS eqid)) @
      casesda
        (mpbird (alleq2d @ anwr ifpos) @ anwl @ sylibr allS @ iand (sylib all1 @ anwl @ anld h) @
          mpbid (alleq2d @ tokenizeFmlaeq2d anr) anll)
        (mpbird (alleq2d @ anwr ifneg) @ syl (anrd tokenizeFmla_nonemptyNonwhite_lem) @
          iand (mpbid (alleq2d @ tokenizeFmlaeq2d anlr) an3l) anllr))));

theorem tokenizeFmla_hd:
  $ tokenizeFmla ast (x : xs) = l : r2 -> (~x e. white <-> E. r l = x : r) $ =
(named @ focus
  (have 'h '(sylib el_nonemptyNonwhite @ syl (elall tokenizeFmla_nonemptyNonwhite) @
    mpbiri lmemconsid @ lmemeq2))
  '(ibid _ _)
  (focus
    '(exp @ mpd (sylib excons @ anld @ anwl h) @ eexd @ eximd @ exp @ eqtrd anr @ conseq1d @
      syl _ @ eqtr3d (syl5eq (tokenizeFmlaS eqid) (rsyl anlr ifneg)) @
        eqtrd anll @ conseq1d anr)
    (def (h x) '(anld @ sylib consinj @ anld @ sylib consinj @ eqtr3d anl @ anwr ,x))
    '(casesda ,(h 'ifpos) ,(h 'ifneg)))
  (focus
    '(eexda @ sylib (elabe @ noteqd eleq1) @ syl (mpi lmemconsid elall) @
      mpbid (alleq2d anr) @ anrd @ anwl h)));

theorem tokenizeFmla_hd2:
  $ ~x e. white -> E. l E. r2 tokenizeFmla ast (x : xs) = (x : l) : r2 $ =
(named '(mpd (sylib excons tokenizeFmlaS_n0) @ syl6 excom @ eexd @ eximd @ exp @
  mpd (mpbid (anwr tokenizeFmla_hd) anl) @ eximd @ exp @ eqtrd anlr @ conseq1d anr));

pub theorem tokenizeFmlaSLDelim (ast x xs: nat):
  $ x : 0 e. fst (getDelimiters ast) ->
    tokenizeFmla ast (x : xs) = (x : 0) : tokenizeFmla ast xs $ =
(named '(syl5eq (tokenizeFmlaS eqid) @
  eqtrd (syl ifneg @ rsyl orl @ rsyl getDelimiters_nonemptyNonwhite @
    sylbi el_nonemptyNonwhite @ anwr @ sylib (elabe @ noteqd eleq1) @ mpi lmemconsid elall) @
  syl ifpos orl));

theorem tokenizeFmlaS_RDelim_lem
  (h1: $ G -> ~x e. white $) (h2: $ G -> y e. white \/ y : 0 e. snd (getDelimiters ast) $):
  $ G -> tokenizeFmla ast (x : y : xs) = (x : 0) : tokenizeFmla ast (y : xs) $ =
(named '(syl5eq (tokenizeFmlaS eqid) @ eqtrd (syl ifneg h1) @ syl ifpos @ orrd @
  iald @ iald @ syl5bi consinj @ exp @
  mpbid (rsyl anrl @ oreqd eleq1 (eleq1d conseq1)) @ anwl h2));

pub theorem tokenizeFmlaSRDelim (ast x y xs: nat):
  $ ~x e. white /\ y : 0 e. snd (getDelimiters ast) ->
    tokenizeFmla ast (x : y : xs) = (x : 0) : tokenizeFmla ast (y : xs) $ =
'(tokenizeFmlaS_RDelim_lem anl @ orrd anr);

theorem tokenizeFmlaS_Else
  (h1: $ G -> ~x e. white $)
  (h2: $ G -> tokenizeFmla ast (y : xs) = (y : r) : r2 $)
  (h3: $ G -> ~x : 0 e. fst (getDelimiters ast) $)
  (h4: $ G -> ~y : 0 e. snd (getDelimiters ast) $):
  $ G -> tokenizeFmla ast (x : y : xs) = (x : y : r) : r2 $ =
(named '(eqtrd (sylc tokenizeFmlaSS h2 h1) @
  syl6eq (conseq (conseq2 @ eqtr (fsteq sucsub1) fstpr) (eqtr (sndeq sucsub1) sndpr)) @
  syl ifneg @ sylibr notor @ iand (sylibr notor @ iand h3 @
    mpbiri (iexe (eqeq2d conseq2) eqid) (syl tokenizeFmla_hd h2)) h4));

pub theorem tokenizeFmlaSElse (ast x y xs r r2: nat):
  $ ~x e. white /\
    tokenizeFmla ast (y : xs) = (y : r) : r2 /\
    ~x : 0 e. fst (getDelimiters ast) /\
    ~y : 0 e. snd (getDelimiters ast) ->
    tokenizeFmla ast (x : y : xs) = (x : y : r) : r2 $ =
'(tokenizeFmlaS_Else an3l anllr anlr anr);

theorem tokenizeFmlaWS (ast s c t: nat): $ c e. white ->
  tokenizeFmla ast (s ++ c : t) = tokenizeFmla ast s ++ tokenizeFmla ast t $ =
(named @ focus
  (induct '(listindd) 's
    '(sylibr (eqeq (tokenizeFmlaeq2 append0)
      (eqtr (appendeq1 tokenizeFmla0) append0)) tokenizeFmlaWhite) _)
  '(syl5eq (tokenizeFmlaeq2 appendS) @
    casesda (eqtr4d (anwr tokenizeFmlaWhite) @
      eqtr4d (anwr @ appendeq1d tokenizeFmlaWhite) anlr) @
    casesda (eqtr4d (anwr tokenizeFmlaSLDelim) @
      eqtr4d (anwr @ appendeq1d tokenizeFmlaSLDelim) @ syl6eqr appendS @ conseq2d anllr) @
    casesda (eqtr4d (tokenizeFmlaeq2d @ conseq2d @ syl6eq append0 @ appendeq1d anr) @
      eqtr4d (appendeq1d @ eqtrd (tokenizeFmlaeq2d @ conseq2d anr) @ syl tokenizeFmla1 anllr) @
      syl6eqr append1 @ eqtrd (tokenizeFmlaS_RDelim_lem anllr @ orld an4l) @
      conseq2d @ syl tokenizeFmlaWhite an4l) _)
  '(imp @ syl5bi excons @ eexd @ eexda @
    eqtr4d (tokenizeFmlaeq2d @ conseq2d @ syl6eq appendS @ appendeq1d anr) @
    eqtr4d (appendeq1d @ tokenizeFmlaeq2d @ conseq2d anr) @
    casesda (eqtr4d (tokenizeFmlaS_RDelim_lem an3lr anr) @
      eqtr4d (appendeq1d @ tokenizeFmlaS_RDelim_lem an3lr anr) @
      syl6eqr appendS @ conseq2d @
      eqtr3d (tokenizeFmlaeq2d @ syl6eq appendS @ appendeq1d anlr) @
      eqtrd an4lr @ appendeq1d @ tokenizeFmlaeq2d anlr) @
    mpd (syl tokenizeFmla_hd2 an3lr) @ eexd @ eexda @
    mpd (syl tokenizeFmla_hd2 @ rsyl anlr @ con3 orl) @ eexd @ eexda @
    eqtr4d (tokenizeFmlaS_Else an5lr _ an4lr @ rsyl anllr @ con3 orr) @
    syl6eq appendS @ appendeq1d @ tokenizeFmlaS_Else an5lr anr an4lr @ rsyl anllr @ con3 orr)
  '(eqtr3d (tokenizeFmlaeq2d @ syl6eq appendS @ appendeq1d an3lr) @
    eqtrd an6lr @ syl6eq appendS @ appendeq1d @
    eqtrd (tokenizeFmlaeq2d an3lr) anr));

-- pub theorem tokenizeFmlaLDelim (ast x s t: nat):
--   $ x e. fst (getDelimiters ast) ->
--     tokenizeFmla ast (s ++ x ++ t) =
--     tokenizeFmla ast (s ++ x) ++ tokenizeFmla ast t $;
-- pub theorem tokenizeFmlaRDelim (ast x s t: nat):
--   $ x e. snd (getDelimiters ast) ->
--     tokenizeFmla ast (s ++ x ++ t) =
--     tokenizeFmla ast s ++ tokenizeFmla ast (x ++ t) $;

-- pub theorem tokenizeFmlaJoin (ast x s t: nat):
--   $ s e. nonemptyNonwhite -> ljoin (tokenizeFmla ast s) = s $;

-- pub theorem tokenizeFmlaMinimal {l r: nat} (ast s a x y b: nat):
--   $ tokenizeFmla ast s = a ++ x : y : b ->
--     E. l E. r (r e. fst (getDelimiters ast) /\ x = l ++ r) \/
--     E. l E. r (l e. snd (getDelimiters ast) /\ y = l ++ r) $;

--| `x, c, p e. getPfx ast` says that the AST contains a
--| prefix declaration `c` for `x` at precedence `p`.
--|
--| `getPfx: List AST -> Set (Ident, String, Prec)`
@_ abstract def getPfx (ast: nat): nat =
$ lower (S\ x, S\ c, {p | E. fmla (
    ASTNota (NotaPfx (x, b1 fmla, p)) IN ast /\
    simpleTokenize fmla = c : 0)}) $;
pub theorem getPfxEl {fmla: nat} (ast x c p: nat):
  $ x, c, p e. getPfx ast <-> E. fmla (
    ASTNota (NotaPfx (x, b1 fmla, p)) IN ast /\
    simpleTokenize fmla = c : 0) $ =
(named @ focus
  '(bitr (ellower @ trud _) @ elsabe @ elsabed @ elabed @
    exeqd @ aneqd
      (lmemeq1d @ ASTNotaeqd @ NotaPfxeqd @ preqd anll @ preq2d anr)
      (eqeq2d @ conseq1d anlr))
  (have 'h $ ASTNota (NotaPfx _) IN ast /\ _ -> _ $
    '(rsyl (syl lmemlt anl) @ lelttr @ leb1tr @ leb1tr @ leb0tr @ leb1tr b1leid))
  '(sabfin (eexsabd @ eelabd @ a1i @ eex @ sylibr elupto @ rsyl h @ lelttr leprid1) (a1i finns) @
    sabfin (eelabd @ a1i @ sylibr ellamima @ eximi @ iand
      (sylibr elupto @ rsyl h @ lelttr @ lepr2tr @ lepr1tr b1leid)
      (eqcomd @ syl6eq fstpr @ fsteqd @ syl6eq sucsub1 @ subeq1d anr)) (a1i @ finlamima finns) @
    a1i @ finss (mpbi ssab1 @ ax_gen @ eex @ sylibr elupto @ rsyl h @ lelttr @ lepr2tr leprid2) @
    finns));

--| `x, c, p e. getInfix ast r` says that the AST contains a
--| infix(r) declaration `c` for `x` at precedence `p`.
--|
--| `getInfix: List AST -> Bool -> Set (Ident, String, Prec)`
@_ abstract def getInfix (ast r: nat): nat =
$ lower (S\ x, S\ c, {p | E. fmla (
    ASTNota (NotaInfix r (x, b1 fmla, p)) IN ast /\
    simpleTokenize fmla = c : 0)}) $;
pub theorem getInfixEl {fmla: nat} (ast r x c p: nat):
  $ x, c, p e. getInfix ast r <-> E. fmla
    (ASTNota (NotaInfix r (x, b1 fmla, p)) IN ast /\
     simpleTokenize fmla = c : 0) $ =
(named @ focus
  '(bitr (ellower @ trud _) @ elsabe @ elsabed @ elabed @
    exeqd @ aneqd
      (lmemeq1d @ ASTNotaeqd @ NotaInfixeq2d @ preqd anll @ preq2d anr)
      (eqeq2d @ conseq1d anlr))
  (have 'h $ ASTNota (NotaInfix _) IN ast /\ _ -> _ $
    '(rsyl (syl lmemlt anl) @ lelttr @ leb1tr @ leb1tr @ leb0tr @ leb1tr b0leid))
  '(sabfin (eexsabd @ eelabd @ a1i @ eex @ sylibr elupto @ rsyl h @ lelttr @ lepr2tr leprid1) (a1i finns) @
    sabfin (eelabd @ a1i @ sylibr ellamima @ eximi @ iand
      (sylibr elupto @ rsyl h @ lelttr @ lepr2tr @ lepr2tr @ lepr1tr b1leid)
      (eqcomd @ syl6eq fstpr @ fsteqd @ syl6eq sucsub1 @ subeq1d anr)) (a1i @ finlamima finns) @
    a1i @ finss (mpbi ssab1 @ ax_gen @ eex @ sylibr elupto @ rsyl h @ lelttr @ lepr2tr @ lepr2tr leprid2) @
    finns));

--| `n e. getNota ast` says that the AST contains a notation declaration `n`.
--|
--| `getNota: List AST -> Set (Ident, List ASTBinder, ASTDepType, List Literal)`
@_ abstract def getNota (ast: nat): nat = $ lower {z | ASTNota (NotaGen z) IN ast} $;
pub theorem getNotaEl (ast x: nat):
  $ x e. getNota ast <-> ASTNota (NotaGen x) IN ast $ =
(named @ focus
  '(bitr (ellower @ finss _ finns) @ elabe @ lmemeq1d @ ASTNotaeqd NotaGeneq)
  '(mpbi ssab1 @ ax_gen @ sylibr elupto @ rsyl lmemlt @ lelttr @
    leb1tr @ leb1tr @ leb1tr b1leid));

--| `c e. getNota ast` says that the AST contains a coercion declaration `c`.
--|
--| `getCoe: List AST -> Set (Ident, Ident, Ident)`
@_ abstract def getCoe (ast: nat): nat = $ lower {z | ASTNota (NotaCoe z) IN ast} $;
pub theorem getCoeEl (ast x: nat):
  $ x e. getCoe ast <-> ASTNota (NotaCoe x) IN ast $ =
(named @ focus
  '(bitr (ellower @ finss _ finns) @ elabe @ lmemeq1d @ ASTNotaeqd NotaCoeeq)
  '(mpbi ssab1 @ ax_gen @ sylibr elupto @ rsyl lmemlt @ lelttr @
    leb1tr @ leb1tr @ leb1tr b0leid));

--| `m <=p n` is the `<=` relation for precedences. `0` represents `max`,
--| so it is ordered after everything else and the other numbers are in the usual order.
--| `precle: Prec -> Prec -> Bool`
@_ abstract def precle (m n: nat): wff = $ n = 0 \/ m != 0 /\ m - 1 <= n - 1 $;
infixl precle: $<=p$ prec 50;
pub theorem precle02 (n: nat): $ n <=p 0 $ = '(orl eqid);
pub theorem precle01 (m: nat): $ ~ 0 <=p suc m $ =
'(mpbir notor @ ian peano1 @ con2 anl eqid);
pub theorem precleS (m n: nat): $ suc m <=p suc n <-> m <= n $ =
'(bitr (bior1 peano1) @ bitr (bian1 peano1) @ leeq sucsub1 sucsub1);

--| The successor operation on precedences. `precSuc: Prec -> Prec`
@_ abstract def precSuc (n: nat): nat = $ if (n = 0) 0 (suc n) $;
pub theorem precSuc0: $ precSuc 0 = 0 $ = '(ifpos eqid);
pub theorem precSucS (n: nat): $ precSuc (suc n) = suc (suc n) $ = '(ifneg peano1);

--| Extracts the precedence of a variable given the list of literals that follow.
--| `litsPrec: List Literal -> Prec -> Prec`
@_ abstract def litsPrec (lits q: nat): nat =
$ if (lits = 0) q (case (\\ c, \ p, precSuc p) (\ v, 0) @ fst (lits - 1)) $;
pub theorem litsPrec0 (q: nat): $ litsPrec 0 q = q $ = (named '(ifpos eqid));
theorem litsPrecS:
  $ litsPrec (z : lits) q = case (\\ c, \ p, precSuc p) (\ v, 0) @ z $ =
'(eqtr (ifneg peano1) @ appeq2 @ eqtr (fsteq sucsub1) fstpr);
pub theorem litsPrecC (c p lits q: nat):
  $ litsPrec (b0 (c, p) : lits) q = precSuc p $ =
(named '(eqtr litsPrecS @ eqtr casel @ appslame @ applamed @ precSuceqd anr));
pub theorem litsPrecV (v lits q: nat):
  $ litsPrec (b1 v : lits) q = 0 $ =
(named '(eqtr litsPrecS @ eqtr caser @ applame eqidd));

-- This is a more precise version of SExpr that allows reconstructing an
-- exact token string from a parse proof

--| A variable reference `v`. `PTVar: Ident -> ParseTree`
@_ def PTVar (v: nat): nat = $ b0 (b0 (b0 v)) $;
--| A parenthesized expression `(x)`. `PTParens: ParseTree -> ParseTree`
@_ def PTParens (x: nat): nat = $ b0 (b0 (b1 x)) $;
--| A function call expression `f xs`. `PTFunc: Ident -> List ParseTree -> ParseTree`
@_ def PTFunc (f xs: nat): nat = $ b0 (b1 (f, xs)) $;
--| A prefix notation expression `c xs` which resolves to `f`.
--| `PTPfx: Ident -> String -> List ParseTree -> ParseTree`
@_ def PTPfx (f c xs: nat): nat = $ b1 (b0 (b0 (f, c, xs))) $;
--| A notation expression, consisting of literals `lits` which are either `String` constants
--| or expression subtrees, which resolves to `f`.
--| `PTNota: Ident -> List (String + ParseTree) -> ParseTree`
@_ def PTNota (f lits: nat): nat = $ b1 (b0 (b1 (f, lits))) $;
--| An infix(r) expression, with parse trees `x` and `y` separated by `c`, which resolves to `f`.
--| `PTInfix: Bool -> Ident -> String -> ParseTree -> ParseTree -> ParseTree`
@_ def PTInfix (r f c x y: nat): nat = $ b1 (b1 (b0 (r, f, c, x, y))) $;
--| A coercion expression, which applies `f` to the parse tree `x`.
--| `PTCoe: Ident -> ParseTree -> ParseTree`
@_ def PTCoe (f x: nat): nat = $ b1 (b1 (b1 (f, x))) $;

theorem PTParens_ltid: $ e < PTParens e $ = '(ltb0tr @ ltb0tr b1ltid);
theorem PTFunc_ltid: $ e IN es -> e < PTFunc f es $ =
'(rsyl lmemlt @ mpi (ltb0tr @ ltb1tr leprid2) lttr);
theorem PTPfx_ltid: $ e IN es -> e < PTPfx f c es $ =
'(rsyl lmemlt @ mpi (ltb1tr @ leb0tr @ leb0tr @ lepr2tr leprid2) lttr);
theorem PTNota_ltid: $ b1 e IN ls -> e < PTNota f ls $ =
'(rsyl lmemlt @ rsyl (lttr b1ltid) @ mpi (ltb1tr @ leb0tr @ leb1tr leprid2) lttr);
theorem PTInfix_ltid1: $ x < PTInfix r f c x y $ =
'(ltb1tr @ leb1tr @ leb0tr @ lepr2tr @ lepr2tr @ lepr2tr leprid1);
theorem PTInfix_ltid2: $ y < PTInfix r f c x y $ =
'(ltb1tr @ leb1tr @ leb0tr @ lepr2tr @ lepr2tr @ lepr2tr leprid2);
theorem PTCoe_ltid: $ x < PTCoe f x $ = '(ltb1tr @ leb1tr @ leb1tr leprid2);

--| Convert a parse tree object to a string of tokens. `ptToStr: ParseTree -> List String`
@_ abstract def ptToStr (pt: nat): nat =
$ srec (\ ih, case
    (case
      (case
        (\ v, v : 0)
        (\ e, s1 _lparen : ih @ e ++ s1 _rparen : 0))
      (\\ f, \ x, f : ljoin (map ih x)))
    (case
      (case
        (\\ f, \\ c, \ x, c : ljoin (map ih x))
        (\\ f, \ x, ljoin (map (case (\ y, y : 0) ih) x)))
      (case
        (\\ r, \\ f, \\ c, \\ x, \ y, ih @ x ++ c : ih @ y)
        (\\ f, \ x, ih @ x)))
  @ size (Dom ih)) pt $;

theorem ptToStr_val:
  $ ptToStr ei = case
    (case
      (case
        (\ v, v : 0)
        (\ e, s1 _lparen : (\. e2 e. upto ei, ptToStr e2) @ e ++ s1 _rparen : 0))
      (\\ f, \ x, f : ljoin (map (\. e2 e. upto ei, ptToStr e2) x)))
    (case
      (case
        (\\ f, \\ c, \ x, c : ljoin (map (\. e2 e. upto ei, ptToStr e2) x))
        (\\ f, \ x, ljoin (map (case (\ y, y : 0) (\. e2 e. upto ei, ptToStr e2)) x)))
      (case
        (\\ r, \\ f, \\ c, \\ x, \ y,
          (\. e2 e. upto ei, ptToStr e2) @ x ++ c : (\. e2 e. upto ei, ptToStr e2) @ y)
        (\\ f, \ x, (\. e2 e. upto ei, ptToStr e2) @ x)))
  @ ei $ =
'(eqtr {srecval : $ _ = _ @ rlam _ _ (ptToStr _) $} @ !! applame a @ appeqd ,eqtac sreclem);

pub theorem ptToStrVar (v: nat): $ ptToStr (PTVar v) = v : 0 $ =
(named '(eqtr ptToStr_val @ eqtr casel @ eqtr casel @ eqtr casel @ applame conseq1));

pub theorem ptToStrParens (e: nat):
  $ ptToStr (PTParens e) = s1 _lparen : ptToStr e ++ s1 _rparen : 0 $ =
(named '(eqtr ptToStr_val @ eqtr casel @ eqtr casel @ eqtr caser @
  !! applame x @ appendeq1d @ conseq2d @ !! apprlamed y (ptToStreqd @ eqtrd anr anl) @
  mpbiri (mpbir elupto PTParens_ltid) eleq1));

pub theorem ptToStrFunc {s: nat} (f x: nat): $ ptToStr (PTFunc f x) =
  f : ljoin (map (\ s, ptToStr s) x) $ =
(named '(eqtr ptToStr_val @ eqtr casel @ eqtr caser @
  !! appslame f1 @ !! applamed c1 @ eqtrd ,eqtac @
  conseq2d @ ljoineqd @ syl mapeqg @ sylibr allal @ iald @ exp @
  eqtr4d (!! apprlamed z ,eqtac @ anwr @ sylibr elupto PTFunc_ltid) (applamed ,eqtac)));

pub theorem ptToStrPfx {s: nat} (f c x: nat): $ ptToStr (PTPfx f c x) =
  c : ljoin (map (\ s, ptToStr s) x) $ =
(named '(eqtr ptToStr_val @ eqtr caser @ eqtr casel @ eqtr casel @
  appslame @ appslamed @ applamed @ eqtrd ,eqtac @
  conseq2d @ ljoineqd @ syl mapeqg @ sylibr allal @ iald @ exp @
  eqtr4d (!! apprlamed z ,eqtac @ anwr @ sylibr elupto PTPfx_ltid) (applamed ,eqtac)));

pub theorem ptToStrNota {y: nat} (f x: nat):
  $ ptToStr (PTNota f x) = ljoin (map (case (\ y, y : 0) (\ y, ptToStr y)) x) $ =
(named '(eqtr ptToStr_val @ eqtr caser @ eqtr casel @ eqtr caser @
  appslame @ applamed @ eqtrd ,eqtac @
  ljoineqd @ syl mapeqg @ sylibr allal @ !! iald e @ exp
  ,(split-sop '{
    (1 => {(mpbiri (eqtr4 casel casel) ,eqtac) : $ _ /\ e = _ -> _$}) +
    (1 => (mpbird ,eqtac @ eqtr4g caser caser @
      eqtr4d (!! apprlamed z ,eqtac @ sylibr elupto @ syl PTNota_ltid @ mpbid (lmemeq1d anr) anlr)
        (applamed ,eqtac)))})));

pub theorem ptToStrInfix (r f c x y: nat):
  $ ptToStr (PTInfix r f c x y) = ptToStr x ++ c : ptToStr y $ =
(named '(eqtr ptToStr_val @ eqtr caser @ eqtr caser @ eqtr casel @
  appslame @ appslamed @ appslamed @ appslamed @ applamed @ eqtrd ,eqtac @
  appendeqd (apprlamed ,eqtac @ a1i @ mpbir elupto PTInfix_ltid1) @
  conseq2d (apprlamed ,eqtac @ a1i @ mpbir elupto PTInfix_ltid2)));

pub theorem ptToStrCoe (f x: nat): $ ptToStr (PTCoe f x) = ptToStr x $ =
(named '(eqtr ptToStr_val @ eqtr caser @ eqtr caser @ eqtr caser @
  appslame @ applamed @ apprlamed (ptToStreqd @ eqtrd anr anlr) @
  mpbiri (mpbir elupto PTCoe_ltid) (eleq1d anr)));

@_ local def ptCheckNotaLs_aux (bis lits: nat) (IH: set) (xs es p: nat): wff =
$ nztails lits, xs e. all2 (S\ lits1, {x | lits1 e. S\ lit, {lr | lit e. Sum
    {c | x = b0 (fst c)}
    {v | E. y E. n E. e (x = b1 y /\
      lookupVar bis v = suc n /\ nth n es = suc e /\
      e e. IH @ y @ litsPrec lr p)}
  }}) $;

theorem ptCheckNotaLs_aux_0:
  $ ptCheckNotaLs_aux bis 0 IH xs es p <-> xs = 0 $ =
(named '(bitr (eleq1 @ preq1 nztails0) all201));
theorem ptCheckNotaLs_aux_S:
  $ ptCheckNotaLs_aux bis (lit : lits) IH xs es p <-> E. x E. xs2 (
    xs = x : xs2 /\ (lit e. Sum
      {c | x = b0 (fst c)}
      {v | E. y E. n E. e (x = b1 y /\
        lookupVar bis v = suc n /\ nth n es = suc e /\
        e e. IH @ y @ litsPrec lits p)} /\
    ptCheckNotaLs_aux bis lits IH xs2 es p)) $ =
'(bitr (eleq1 @ preq1 nztailsS) @ bitr all2S1 @ exeqi @ exeqi @
  aneq2i @ aneq1i @ elsabe @ elabed @ bitrd (eleq1d anl) @ elsabed @ elabed ,eqtac);

theorem ptCheckNotaLs_aux_fin_lem:
  $ ptCheckNotaLs_aux bis lits (ns ih) xs es p ->
    b1 v IN lits -> lookupVar bis v = suc n ->
    nth n es = suc e -> e < ih $ =
(named @ focus
  '(ax_mp (eale ,(eqtac-gen 'xs))
    ,(induct '(listind) 'lits '(ax_gen @ a1i @ absurd lmem0) _))
  '(sylbi (cbval ,eqtac) @ iald @
    syl5bi ptCheckNotaLs_aux_S @ eexd @ sylibr eexb @ alimi @
    exp @ syl5bi lmemS @ eorda _ @ imp @ imp @ imim1i anrr)
  '(rsyl (mpbird (eleq1d anr) @ rsyl anlr anrl) @
    sylbi Sumr @ sylbi (elabe ,eqtac) @
    eex @ eex @ eex @ exp @ exp @
    syl (rsyl ellt @ mpi (letr appleid1 appleid1) ltletr) @
    mpbird (eleq1d @ sylib peano2 @ eqtr3d anr _) anllr)
  '(eqtrd (ntheq1d @ sylib peano2 @ eqtr3d anlr an4lr) an3lr));

@_ local def ptCheck_aux1 (eac: nat) (ih: set) (p pt e: nat): wff =
$ pt e. Sum
    (Sum
      (Sum
        {v | E. n (lookupVar (pi22 eac) v = suc n /\ e = SVar n)}
        {x | e e. ih @ x @ suc 0})
      (S\ f, {xs |
        suc (2 ^ 10) <=p p /\ E. args E. ret E. v E. e2
        (getTerm (fst eac) f args ret v /\ lookupVar (pi22 eac) f = 0 /\ len xs = len args /\
          xs, e2 e. all2 (S\ x, ih @ x @ 0) /\
          e = SApp f e2)}))
    (Sum
      (Sum
        (S\ f, S\ c, {xs |
          E. l E. z E. q E. es2 E. e2 (xs = l |> z /\
            f, c, q e. getPfx (pi21 eac) /\ q <=p p /\
            l, es2 e. all2 (S\ x, ih @ x @ 0) /\ e2 e. ih @ z @ q /\
            e = SApp f (es2 |> e2))})
        (S\ f, {xs |
          E. bis E. ty E. c E. q E. lits E. es (
            f, bis, ty, b0 (c, q) : lits e. getNota (pi21 eac) /\
            len bis = len es /\
            A. n (n < len es -> E. v (b1 v IN lits /\ lookupVar bis v = suc n)) /\
            ptCheckNotaLs_aux bis lits ih xs es q /\
            e = SApp f es)}))
      (Sum
        (S\ r, S\ f, S\ c, S\ x, {y |
          E. q E. e1 E. e2 (
            f, c, q e. getInfix (pi21 eac) r /\ q <=p p /\
            e1 e. ih @ x @ if (true r) (precSuc q) q /\
            e2 e. ih @ y @ if (true r) q (precSuc q) /\
            e = SApp f (e1 : e2 : 0))})
        (S\ f, {x |
          E. y E. e2 (p <= eac /\
            f, y e. getCoe (pi21 eac) /\ e2 e. ih @ x @ p /\
            e = SApp f e2)}))) $;

theorem ptCheck_aux_Var: $ ptCheck_aux1 eac ih p (PTVar v) e <->
  E. n (lookupVar (pi22 eac) v = suc n /\ e = SVar n) $ =
(named '(bitr Suml @ bitr Suml @ bitr Suml @ elabe ,eqtac));
theorem ptCheck_aux_Parens: $ ptCheck_aux1 eac ih p (PTParens pt) e <->
  e e. ih @ pt @ suc 0 $ =
(named '(bitr Suml @ bitr Suml @ bitr Sumr @ elabe ,eqtac));
theorem ptCheck_aux_Func: $ ptCheck_aux1 eac ih p (PTFunc f xs) e <->
  suc (2 ^ 10) <=p p /\ E. args E. ret E. v E. e2
  (getTerm (fst eac) f args ret v /\ lookupVar (pi22 eac) f = 0 /\ len xs = len args /\
    xs, e2 e. all2 (S\ x, ih @ x @ 0) /\
    e = SApp f e2) $ =
(named '(bitr Suml @ bitr Sumr @ elsabe @ elabed ,eqtac));
theorem ptCheck_aux_Pfx: $ ptCheck_aux1 eac ih p (PTPfx f c xs) e <->
  E. l E. z E. q E. es2 E. e2 (xs = l |> z /\
    f, c, q e. getPfx (pi21 eac) /\ q <=p p /\
    l, es2 e. all2 (S\ x, ih @ x @ 0) /\ e2 e. ih @ z @ q /\
    e = SApp f (es2 |> e2)) $ =
(named '(bitr Sumr @ bitr Suml @ bitr Suml @
  elsabe @ elsabed @ elabed ,eqtac));
theorem ptCheck_aux_Nota: $ ptCheck_aux1 eac ih p (PTNota f xs) e <->
  E. bis E. ty E. c E. q E. lits E. es (
    f, bis, ty, b0 (c, q) : lits e. getNota (pi21 eac) /\
    len bis = len es /\
    A. n (n < len es -> E. v (b1 v IN lits /\ lookupVar bis v = suc n)) /\
    ptCheckNotaLs_aux bis lits ih xs es q /\
    e = SApp f es) $ =
(named '(bitr Sumr @ bitr Suml @ bitr Sumr @ elsabe @ elabed ,eqtac));
theorem ptCheck_aux_Infix: $ ptCheck_aux1 eac ih p (PTInfix r f c x y) e <->
  E. q E. e1 E. e2 (
    f, c, q e. getInfix (pi21 eac) r /\ q <=p p /\
    e1 e. ih @ x @ if (true r) (precSuc q) q /\
    e2 e. ih @ y @ if (true r) q (precSuc q) /\
    e = SApp f (e1 : e2 : 0)) $ =
(named '(bitr Sumr @ bitr Sumr @ bitr Suml @
  elsabe @ elsabed @ elsabed @
  elsabed @ elabed ,eqtac));
theorem ptCheck_aux_Coe: $ ptCheck_aux1 eac ih p (PTCoe f x) e <->
  E. y E. e2 (p <= eac /\
    f, y e. getCoe (pi21 eac) /\ e2 e. ih @ x @ p /\
    e = SApp f e2) $ =
(named '(bitr Sumr @ bitr Sumr @ bitr Sumr @ elsabe @ elabed ,eqtac));

theorem getPfx_precle: $ f, c, p e. getPfx (pi21 eac) -> p <= suc eac $ =
'(sylbi getPfxEl @ !! eex x @ anwl @
  letrd (a1i @ leb1tr @ leb1tr @ leb0tr @ leb1tr @ leb1tr @ lepr2tr leprid2) @
  letrd (syl ltle lmemlt) @ a1i @ letr fstleid @ letr sndleid lesucid);
theorem getNota_precle:
  $ f, bis, ty, lits e. getNota (pi21 eac) -> bis, ty, lits <= eac $ =
'(sylbi getNotaEl @
  letrd (a1i @ leb1tr @ leb1tr @ leb1tr @ leb1tr leprid2) @
  letrd (syl ltle lmemlt) @ a1i @ letr fstleid sndleid);
theorem getInfix_precle:
  $ f, c, p e. getInfix (pi21 eac) r -> p <= eac $ =
'(sylbi getInfixEl @ !! eex x @ anwl @
  letrd (a1i @ leb1tr @ leb1tr @ leb0tr @ leb1tr @ leb0tr @ lepr2tr @ lepr2tr leprid2) @
  letrd (syl ltle lmemlt) @ a1i @ letr fstleid sndleid);

theorem ptCheck_aux1_fin: $ finite {e | ptCheck_aux1 eac (ns ih) p pt e} $ =
(named @ focus
  (def (g0 x) '(finss (mpbi ssab @ ax_gen ,x) ltfin))
  (def (g1 n x) @ iterate n (fn (x) '(eex ,x))
    '(mpbird (lteq1d anr) @ sylib b1lt @ sylib ltpr2 @ anwl ,x))
  (def (g2 x) '(syl ellt @ sylibr (ellower @ Arrayfin finns) ,x))
  (def (g3 x) @ g2 '(sylibr elArray ,x))
  (def h1 '(rsyl ellt @ mpi (letr appleid1 appleid1) ltletr))
  '(trud ,(split-sop 'pt
    (fn (x y) '(syl5ibrcom (fineqd @ abeqd @ syl6bb ,x ptCheck_aux1eq4) @ a1i ,y))
    '{{{($PTVar v$ => ptCheck_aux_Var (mpbi (fineq _) finns))
      + ($PTParens x$ => ptCheck_aux_Parens (mpbir (fineq abid2) finns))}
      + ($PTFunc f xs$ => ptCheck_aux_Func ,(g0 '(anwr ,(g1 4 @ g3 _))))}
      + {{($PTPfx f c xs$ => ptCheck_aux_Pfx ,(g0 @ g1 5 @ g3 _))
      + ($PTNota f xs$ => ptCheck_aux_Nota ,(g0 @ g1 6 _))}
      + {($PTInfix r f c x y$ => ptCheck_aux_Infix ,(g0 @ g1 3 @ g2 _))
      + ($PTCoe f x$ => ptCheck_aux_Coe ,(g0 @ g1 2 '(anwr ,h1)))}}}))
  (def h2 '(sylibr elupto ,h1))
  (focus -- PTVar v
    '(eqab2i @ bitr elobind @ exeqi @ aneq2i @
      bitr (elneq2 @ applame @ sneqd SVareq) elsn))
  (focus -- PTFunc f xs
    '(iand (anwr _) @ eqcomd @ anwr all2len)
    '(sylibr elList @ syl all2all2 @ ssel @ all2ss @ sabssi @ ax_gen ,h2))
  (focus -- PTPfx f c xs
    '(iand (sylibr snocT @ iand (rsyl anlr _) (anwr ,h2)) @
      eqtr2d (leneqd an4l) @ eqtr4g snoclen snoclen @ suceqd @ rsyl anlr all2len)
    '(sylibr elList @ syl all2all2 @ ssel @ all2ss @ sabssi @ ax_gen ,h2))
  (focus -- PTNota f xs
    '(syl (lelttr leprid2) @ syl ellt @
      sylibr (ellower @ xabfin id (a1i @ Arrayfin finns) finns) @
      sylibr (elxabe @ eleq2d Arrayeq2) @ iand _ @
      sylibr elArray @ iand _ @ eqcomd anllr)
    '(sylibr elupto @ syl (lelttr lenleid) @ rsyl an3l @
      rsyl getNota_precle @ sylib leltsuc @ letr leprid1)
    '(sylibr elList @ sylibr allnth @ sylib alcomb @ iald @
      sylbi anrass @ imp @ alimd @ com23 @ exp @
      eimd (anwr @ sylib nthne0 sucne0) @ eexda _)
    '(mpd (rsyl anllr ptCheckNotaLs_aux_fin_lem) @
      syl5bir impexp @ eimd anr @ eimd anlr @ a1i @ bi2i elupto))
  (focus -- PTInfix r f c x y
    '(sylibr elArrayS @ iand (rsyl anlr ,h2) (sylibr elArray1 @ anwr ,h2))));

@_ local def ptCheck_aux (eac pt: nat): nat =
$ srec (\ ih, \. p e. upto (eac + 2), lower {e | ptCheck_aux1 eac ih p (size (Dom ih)) e}) pt $;

--| ```
--| ptCheck (eac: (Env, List AST, Ctx')) (p: Prec) (pt: ParseTree) (e: SExpr): Bool
--| ```
--| checks that `pt` is a valid parse tree elaborating to the expression `e`.
--|
--| This function has the technical restriction that `p <= eac`.
--| This is easy to satisfy since `eac` is a *huge* number (the encoding of the environment)
--| and we will never attempt to parse an expression at precedence `p` unless `p`
--| or its predecessor is mentioned somewhere in the environment.
@_ abstract def ptCheck (eac p pt e: nat): wff =
$ ptCheck_aux1 eac (\. pt1 e. upto pt, ptCheck_aux eac pt1) p pt e $;

--| ```
--| ptCheckNotaLs (eac: (Env, List AST, Ctx'))
--|   (bis: List ASTBinder) (lits: List Literal)
--|   (xs: List (String + ParseTree)) (es: List SExpr) (p: Prec): Bool
--| ```
--| checks that `xs` consists of a list of constants and subtrees
--| according to the given literal list.
@_ abstract def ptCheckNotaLs (eac bis lits xs es p .pt1: nat): wff =
$ ptCheckNotaLs_aux bis lits (\ pt1, ptCheck_aux eac pt1) xs es p $;

theorem ptCheck_aux_val:
  $ ptCheck_aux eac pt = \. p e. upto (eac + 2), lower {e | ptCheck eac p pt e} $ =
'(eqtr {srecval : $ _ = _ @ (\. pt1 e. upto pt, ptCheck_aux eac pt1) $} @
  !! applame ih @ rlameq2d @ lowereqd @ abeqd @ bitrd (ptCheck_aux1eq4d sreclem) ,eqtac);

theorem ptCheck_fin: $ finite {e | ptCheck eac p pt e} $ = (named 'ptCheck_aux1_fin);
theorem ptCheck_val: $ p <= suc eac -> (e e. ptCheck_aux eac pt @ p <-> ptCheck eac p pt e) $ =
(named '(syl6bb (bitr (ellower ptCheck_fin) @ elabe ptCheckeq4) @
  elneq2d @ syl5eq (appneq1 ptCheck_aux_val) @
  !! apprlamed p1 ,eqtac @ bi2i @ bitr elupto @ bitr4 (lteq2 add22) leltsuc));

theorem ptCheck_lem: $ p <= suc eac -> pt < pt1 ->
  (e e. (\. z e. upto pt1, ptCheck_aux eac z) @ pt @ p <-> ptCheck eac p pt e) $ =
'(exp @ bitrd
  (elneq2d @ appneq1d @ apprlamed (ptCheck_auxeq2d anr) @ sylibr elupto anr)
  (anwl ptCheck_val));

theorem ptCheckNotaLs_lem: $ all (Sum Univ t) xs ->
  (ptCheckNotaLs_aux bis lits (\. pt e. t, ptCheck_aux eac pt) xs es q <->
  ptCheckNotaLs eac bis lits xs es q) $ =
(named @ focus
  '(ax_mp (eale ,(eqtac-gen 'xs)) ,(induct '(listind) 'lits _ _))
  '(ax_gen @ a1i @ bitr4 ptCheckNotaLs_aux_0 ptCheckNotaLs_aux_0)
  '(sylbi (cbval ,eqtac) @ iald @
    syl6ibr (bieq ptCheckNotaLs_aux_S ptCheckNotaLs_aux_S) @
    expcom @ exeqd @ syl exeq @ imp @ alimd @ expcom @
    syl aneq2a @ imp @ com23 @
    syl5ibrcom (imeq1d @ syl6bb allS alleq2) @
    syl6 (imp aneq) @ anim @ eleq2d @ Sumeq2d @ abeqd @
    exeqd @ exeqd @ exeqd @ syl aneq2a @ syl5 anll @
    com12 @ syl6 _ @ bi1d eleq1)
  '(sylbi Sumr @ elneq2d @ appneq1d @ eqtr4d apprlams @ a1i applams));

pub theorem ptCheckVar {n: nat} (eac p v e: nat): $ ptCheck eac p (PTVar v) e <->
  E. n (lookupVar (pi22 eac) v = suc n /\ e = SVar n) $ = (named 'ptCheck_aux_Var);
pub theorem ptCheckParens (eac p pt e: nat):
  $ ptCheck eac p (PTParens pt) e <-> ptCheck eac (suc 0) pt e $ =
(named '(bitr ptCheck_aux_Parens @ ptCheck_lem (mpbi lesuc le01) PTParens_ltid));
pub theorem ptCheckFunc (env ast ctx p f xs e: nat) {args r v e2 x y: nat}:
  $ ptCheck (env, ast, ctx) p (PTFunc f xs) e <->
    suc (2 ^ 10) <=p p /\ E. args E. r E. v E. e2
    (getTerm env f args r v /\ lookupVar ctx f = 0 /\ len xs = len args /\
      xs, e2 e. all2 (S\ x, {y | ptCheck (env, ast, ctx) 0 x y}) /\
      e = SApp f e2) $ =
(named @ focus
  '(bitr ptCheck_aux_Func @ aneq2i @ exeqi @ exeqi @ exeqi @ exeqi @
    aneq1i @ aneq (aneq1i @ aneq (getTermeq1 fstpr) @ eqeq1 @ lookupVareq1 pi22pr) @
    all2eqg @ ax_gen @ ax_gen @ anwl @ bitr4g _ _ @ syl (ptCheck_lem le01) PTFunc_ltid)
  '(elsabe ,eqtac) '(elsabe @ elabed ,eqtac));
pub theorem ptCheckPfx (eac p f c xs e: nat) {l z q es2 e2 x y: nat} :
  $ ptCheck eac p (PTPfx f c xs) e <->
    E. l E. z E. q E. es2 E. e2 (xs = l |> z /\
      f, c, q e. getPfx (pi21 eac) /\ q <=p p /\
      l, es2 e. all2 (S\ x, {y | ptCheck eac 0 x y}) /\ ptCheck eac q z e2 /\
      e = SApp f (es2 |> e2)) $ =
(named '(bitr ptCheck_aux_Pfx @ exeqi @ exeqi @ exeqi @ exeqi @ exeqi @
  rbid an4l an4l @ aneq1d @ aneqd
  (aneq2d @ syl all2eqg @ iald @ iald @ exp @
    bitr4g (elsabe ,eqtac) (elsabe @ elabed ,eqtac) @
    syl (ptCheck_lem le01) @ syl PTPfx_ltid @ mpbird (lmemeq2d anll) @
    sylibr lmemsnoc @ orld anrl)
  (sylc ptCheck_lem (anwr getPfx_precle) @
    syl PTPfx_ltid @ mpbiri lmemsnocid @ lmemeq2d anl)));
pub theorem ptCheckNota {bis ty c q lits es n v: nat} (eac p f xs e: nat):
  $ ptCheck eac p (PTNota f xs) e <->
    E. bis E. ty E. c E. q E. lits E. es (
      f, bis, ty, b0 (c, q) : lits e. getNota (pi21 eac) /\
      len bis = len es /\
      A. n (n < len es -> E. v (b1 v IN lits /\ lookupVar bis v = suc n)) /\
      ptCheckNotaLs eac bis lits xs es q /\
      e = SApp f es) $ =
(named @ focus
  '(bitr ptCheck_aux_Nota @ exeqi @ exeqi @ exeqi @ exeqi @ exeqi @ exeqi @
    aneq1i @ aneq2a @ a1i @ ptCheckNotaLs_lem @
    mpbir allal2 @ !! ax_gen a @ trud _)
  (split-sop 'a (fn (x y) '(a1i @ mpbiri (sylibr ,x ,y) ,eqtac))
    '{(1 => Suml (a1i elv)) + (1 => Sumr (sylibr elupto PTNota_ltid))}));
pub theorem ptCheckInfix {q e1 e2: nat} (eac p r f c x y e: nat):
  $ ptCheck eac p (PTInfix r f c x y) e <->
    E. q E. e1 E. e2 (
      f, c, q e. getInfix (pi21 eac) r /\ q <=p p /\
      ptCheck eac (if (true r) (precSuc q) q) x e1 /\
      ptCheck eac (if (true r) q (precSuc q)) y e2 /\
      e = SApp f (e1 : e2 : 0)) $ =
(named @ focus
  '(bitr ptCheck_aux_Infix @ exeqi @ exeqi @ exeqi @ aneq1i _)
  (have 'h1 '(mpi lesucid letr))
  (have 'h2 '(ifbothd leeq1 leeq1 (a1i le01) @ sylib lesuc anl))
  (def (f x y z) '(syl (mpi ,z ptCheck_lem) (ifbothd leeq1 leeq1 (anwl ,x) (anwl ,y))))
  '(rbid an3l an3l @ rsyl getInfix_precle @
    aneqd (aneq2d ,(f 'h2 'h1 'PTInfix_ltid1)) ,(f 'h1 'h2 'PTInfix_ltid2)));
pub theorem ptCheckCoe {y e2: nat} (eac p f x e: nat):
  $ ptCheck eac p (PTCoe f x) e <->
    p <= eac /\ E. y E. e2 (
      f, y e. getCoe (pi21 eac) /\ ptCheck eac p x e2 /\
      e = SApp f e2) $ =
(named @ focus
  '(bitr ptCheck_aux_Coe @ bian1exi @ bian1exi @ bian11i @ bitr anass @ aneq2a @ aneq2d @
    syl (mpi PTCoe_ltid ptCheck_lem) @ mpi lesucid letr));

pub theorem ptCheckNotaLs0 (eac bis xs es q: nat):
  $ ptCheckNotaLs eac bis 0 xs es q <-> xs = 0 $ =
(named 'ptCheckNotaLs_aux_0);
pub theorem ptCheckNotaLsC {xs2: nat} (eac bis c p lits xs es q: nat):
  $ ptCheckNotaLs eac bis (b0 (c, p) : lits) xs es q <->
    E. xs2 (xs = b0 c : xs2 /\ ptCheckNotaLs eac bis lits xs2 es q) $ =
(named @ focus
  '(bitr ptCheckNotaLs_aux_S @ bitr _ @ exeqe @ exeqd @ aneq1d @ eqeq2d conseq1)
  '(exeqi @ bian1rexi @ aneq1i @ bitr Suml @
    elabe @ eqeq2d @ b0eqd @ syl6eq fstpr fsteq));

pub theorem ptCheckNotaLsV {n x e xs2: nat} (eac bis v lits xs es q: nat):
  $ litsPrec lits q <= suc eac ->
    (ptCheckNotaLs eac bis (b1 v : lits) xs es q <->
    E. n E. x E. xs2 E. e (xs = b1 x : xs2 /\
      lookupVar bis v = suc n /\ nth n es = suc e /\
      ptCheck eac (litsPrec lits q) x e /\
      ptCheckNotaLs eac bis lits xs2 es q)) $ =
(named @ focus
  '(syl5bb ptCheckNotaLs_aux_S @ syl6bb excomb @
    syl6bb (exeqi @ exeqe @ exeqd @ exeqd @ syl5bbr exan1 @ exeqd @
      syl5bbr anass @ aneq1d @ syl5bbr anass @ aneq1d @ syl5bbr anass @ aneq1d @
      aneq1d @ eqeq2d conseq1) @
    syl6bb excomb @ exeqd @ syl6bbr (exeqi @ bitr4 (aneq2i excomb) exan1) @
    syl6bb excomb @ exeqd @ syl6bbr (exeqi @ bitr4 (aneq2i exan1) anlass) @
    syl6bbr exan1 @ aneq2d @ syl5bb (aneq1i @ bitr Sumr @ elabe ,eqtac) @
    syl5bbr exan2 @ exeqd @ syl6bb exan1 @
    syl5bbr exan2 @ exeqd @ syl5bbr exan2 @ syl6bb exan1 @ exeqd @
    syl6bb anass @ aneq1d @ syl6bb anass @ aneqd (a1i anass) @
    syl5bb (elneq2 @ appneq1 @ applame ptCheck_auxeq2) @
    ptCheck_val));

--| ```
--| parseExpr (eac: (Env, List AST, Ctx'))
--|   (args: List Binder) (f: List String) (s: SortID): Set SExpr
--| ```
--| `e e. parseExpr eac args f s` means that parsing `f` at sort `s` yields `e`.
--| Although it returns a set of values, there is at most one possible result.
@_ def parseExpr (eac args f s .e .pt: nat): set =
$ {e | E. pt (ptToStr pt = f /\
  ptCheck eac 0 pt e /\ Expr (fst eac) args e s)} $;

--| ```
--| parseExprProv (eac: (Env, List AST, Ctx'))
--|   (args: List Binder) (f: List String) (s: SortID): Set SExpr
--| ```
--| `e e. parseExpr eac args f` means that parsing `f` at provable sort yields `e`.
--| Although it returns a set of values, there is at most one possible result.
@_ def parseExprProv (eac args f .e .pt: nat): set =
$ {e | E. pt (ptToStr pt = f /\
  ptCheck eac 0 pt e /\ ExprProv (fst eac) args e)} $;

-----------------
-- Elaboration --
-----------------

-- Here we have to convert a parsed AST into an Env, and also
-- parse the math strings.

-- `ASTBinder' := (Bool, Ident_, BinderType)`
-- `Ctx' := List ASTBinder'`
-- is the special case of `ASTBinder` with no dummy binders.

--| ```
--| splitDummies: List ASTBinder -> (Ctx', List (Ident, BinderType))
--| ```
--| Removes the dummy binders from the input list,
--| returning all the regular binders, plus the dummies.
@_ abstract def splitDummies (bis: nat): nat =
$ rlrec 0 (\\ l, \\ a, \\ bis1, \ bis2,
  (\\ c, \\ x, \ t, if (bool c) (bis1 |> (c, x, t), bis2) (bis1, bis2 |> (x, t)))
  @ a) bis $;

pub theorem splitDummies0: $ splitDummies 0 = 0 $ = (named 'rlrec0);
pub theorem splitDummiesL (bis bis1 bis2 c x t: nat): $
  splitDummies bis = bis1, bis2 /\ bool c ->
  splitDummies (bis |> (c, x, t)) = bis1 |> (c, x, t), bis2 $ =
'(syl5eq rlrecS @ eqtrd (appeq2d @ preq2d @ preq2d anl) @ anwr @
  syl5eq (appslame @ appslamed @ appslamed @ applamed ,eqtac) @
  syl5eq (appslame @ appslamed @ applamed ,eqtac) ifpos);
pub theorem splitDummiesR (bis bis1 bis2 x t: nat): $
  splitDummies bis = bis1, bis2 ->
  splitDummies (bis |> (2, x, t)) = bis1, bis2 |> (x, t) $ =
'(syl5eq rlrecS @ eqtrd (appeq2d @ preq2d preq2) @ a1i @
  eqtr (appslame @ appslamed @ appslamed @ applamed ,eqtac) @
  eqtr (appslame @ appslamed @ applamed ,eqtac) @ ifneg ltirr);

--| ```
--| checkDummies: List (Ident, BinderType) -> Ctx' -> Bool`
--| ```
--| Checks that all dummy declarations are well formed
--| and converts them into `Ctx'` representation.
@_ abstract def checkDummies (ds bis: nat): wff =
$ ds, bis e. all2 (S\ d, {bi | d e. S\ x, {t |
    E. t2 (t = b0 (t2, 0) /\ bi = 1, x, t)
  }}) $;
pub theorem checkDummies0 (bis: nat): $ checkDummies 0 bis <-> bis = 0 $ = (named 'all201);
pub theorem checkDummiesS {t2 bis2: nat} (bis x t ds: nat):
  $ checkDummies ((x, t) : ds) bis <-> E. t2 E. bis2 (
      t = b0 (t2, 0) /\ checkDummies ds bis2 /\
      bis = (1, x, t) : bis2) $ =
(named @ focus
  '(bitr4 all2S1 @
    bitr3 (exeqe @ exeqd @ exeqd @ syl6bb ancomb @ aneq1d @ eqeq2d conseq1) @ exeqi @
    bitr4 (birexan2i @ birexexi biid) @ rexeqi @
    bitr4 (aneq1i @ elsabe @ elabed @ bitrd (eleq1d anl) @ elsabed @ elabed ,eqtac) @
    bitr (bian22i exan2) @ aneq1i @ bitr4 ancomb exan2));

--| `lookupVars: Ctx' -> (Ident => Nat)` is the same as `lookupVar`
--| but expressed as a finite (partial) function.
@_ def lookupVars (ctx .s .t: nat): set = $ S\ s, {t | lookupVar ctx s = suc t} $;

--| ```
--| elabType (ctx: Ctx') (s: ASTDepType) (out: DepType): Bool
--| ```
--| elaborates `s` into a type in context `ctx`.
@_ def elabType (ctx s out .t .vs .vs2: nat): wff =
$ E. t E. vs E. vs2 (s = b0 (t, vs) /\ out = t, vs2 /\
    vs2 == lookupVars ctx '' vs) $;

@_ local def elabTermBinders_aux (n: nat): nat =
$ rlrec (suc 0) (\\ bis, \\ bi, \ ih,
  (\\ c, \\ x, case
    (\\ t2, \ vs2, ocase
      (ocase 0 (\ ctx, suc (ctx |> if (true c) (PBound t2) (PReg t2 vs2))) @ ih) 0
      @ lookupVar bis x)
    0) @ bi) n $;

--| ```
--| elabTermBinders (bis: Ctx') (ctx: Ctx): Bool
--| ```
--| elaborates a binder list `bis` into an abstract context `ctx`.
@_ abstract def elabTermBinders (ctx ctx2: nat): wff =
$ elabTermBinders_aux ctx = suc ctx2 $;
pub theorem elabTermBinders0 (ctx: nat):
  $ elabTermBinders 0 ctx <-> ctx = 0 $ =
(named '(bitr (eqeq1 rlrec0) @ bitr eqcomb peano2));
pub theorem elabTermBindersS {ctx c x t t2 vs2: nat} (bis ctx2: nat):
  $ elabTermBinders (bis |> (c, x, t)) ctx2 <->
    E. ctx E. t2 E. vs2 (
      elabTermBinders bis ctx /\
      lookupVar bis x = 0 /\ t = b0 (t2, vs2) /\
      ctx2 = ctx |> if (true c) (PBound t2) (PReg t2 vs2)) $ =
(named @ focus
  '(bitr (eqeq1 @ eqtr {rlrecS : $ _ = _ @ (_, _, elabTermBinders_aux _) $} @
    appslame @ appslamed @ applamed @ eqtrd (appeq2d anlr) @ appslamed @ appslamed ,eqtac) @
    bitr3 (bian1a @
      rsyl (rsyl sucne0 @ con3 @ syl6eq app01 @ syl6eq caser @ appeq2d @ bi1 eqb1) @
        sylbi eqb0 @ mpi expr @ eximd @ eximd @ com12 @ bi1d @ eqeq2d b0eq) @
    bitr3 (bian2exi exan2) @ biexexi @ biexexi @ bitr4 (aneq2a _) @ bian1exi @ bian11i ancomb)
  '(syl6bb _ @ eqeq1d @ eqtrd (syl6eq casel appeq2) @ appslamed @ applamed ,eqtac)
  '(bitr2 (bian2exi anrass) @ bitr3 (aneq1a @ syl6bb _ @ eqeq1d @ syl6eq ocase0 appeq2) @
    bian2a @ rsyl sucne0 @ con1 @ sylbi exsuc @ eex @ syl6eq app01 @ syl6eq ocaseS appeq2)
  '(bitr2 _ @ bian1a @ sylib exsuc @ rsyl sucne0 @ con3 @ syl6eq ocase0 appeq2)
  '(bian2exi @ aneq2a @ syl5bb eqcomb @ bicomd @
    syl6bb peano2 @ eqeq1d @ eqtrd (syl6eq ocaseS appeq2) @ applamed ,eqtac));

--| ```
--| elabFmla (env: Env) (ast: List AST) (ctx: Ctx')
--|   (args: List Binder) (f: Formula) (e: SExpr) (s: SortID): Bool
--| ```
--| Elaborate formula `f` to expression `e` when expecting sort `s`.
@_ def elabFmla (env ast ctx args f e s .f2: nat): wff =
$ E. f2 (f = b1 f2 /\ parseExpr (env, ast, ctx) args f2 s == sn e) $;

--| ```
--| elabFmlaProv (env: Env) (ast: List AST) (ctx: Ctx')
--|   (args: List Binder) (f: Formula) (e: SExpr): Bool
--| ```
--| Elaborate formula `f` to expression `e` when expecting a provable sort.
@_ def elabFmlaProv (env ast ctx args f e .f2: nat): wff =
$ E. f2 (f = b1 f2 /\ parseExprProv (env, ast, ctx) args f2 == sn e) $;

--| ```
--| elabHyps (env: Env) (ast: List AST) (ctx: Ctx') (args: List Binder)
--|   (hyps: List ASTBinder') (hyps2: List SExpr): Bool
--| ```
--| Elaborate a list of hypotheses `hyps` to a list of expressions `hyps2`.
@_ def elabHyps (env ast ctx args hyps hyps2 .hyp .hyp2 .x .f: nat): wff =
$ hyps, hyps2 e. all2 (S\ hyp, {hyp2 | E. x E. f (hyp = 0, x, f /\
    elabFmlaProv env ast ctx args f hyp2)}) $;

--| ```
--| elabDefO (env: Env) (ast: List AST) (ctx: Ctx')
--|   (s: SortID) (ds: Ctx') (ds2: List SortID) (o: Option Formula)
--|   (o2: Option (List SortID, SExpr)): Bool
--| ```
--| Elaborate a definition's optional value to an optional list of dummies and an expression.
@_ abstract def elabDefO (env ast ctx s ds ds2 o o2: nat): wff =
$ o e. ocasep (ds = 0 /\ o2 = 0) {f | E. args2 E. e (
      elabTermBinders (ctx ++ ds) args2 /\
      elabFmla env ast (ctx ++ ds) args2 f e s /\
      o2 = suc (ds2, e))} $;
pub theorem elabDefO0 (env ast ctx s ds ds2 o2: nat):
  $ elabDefO env ast ctx s ds ds2 0 o2 <-> ds = 0 /\ o2 = 0 $ = (named 'ocasep0);
pub theorem elabDefOS {args2 e: nat} (env ast ctx s ds ds2 f o2: nat):
  $ elabDefO env ast ctx s ds ds2 (suc f) o2 <-> E. args2 E. e (
      elabTermBinders (ctx ++ ds) args2 /\
      elabFmla env ast (ctx ++ ds) args2 f e s /\
      o2 = suc (ds2, e)) $ =
'(bitr ocasepS @ elabe ,eqtac);

@_ local def Elaborate_aux (aste: nat): wff =
$ srecp (S\ aste1, {ih | aste1 e. S\ e2, {ast2 | ifp (ast2 = 0) (e2 = 0) (
    E. ast E. d (ast2 = ast |> d /\ d e. Sum
      (Sum
        (Sum
          (S\ sd, {x | E. e (e, ast e. ih /\ e2 = e |> DSort x sd)})
          (S\ x, S\ bis, {ret |
            E. e E. ctx E. args E. ret2 (e, ast e. ih /\
              splitDummies bis = ctx, 0 /\
              elabTermBinders ctx args /\
              elabType ctx ret ret2 /\
              e2 = e |> DTerm x args ret2)}))
        (Sum
          (S\ x, S\ bis, {ret |
            E. e E. ctx E. hyps E. hyps2 E. args E. ret2 (e, ast e. ih /\
              splitDummies bis = ctx ++ hyps, 0 /\
              elabTermBinders ctx args /\
              elabHyps e ast ctx args hyps hyps2 /\
              elabFmlaProv e ast ctx args ret ret2 /\
              e2 = e |> DAxiom args hyps2 ret2)})
          (S\ x, S\ bis, S\ ret, {o |
            E. e E. ctx E. ds E. ret2 E. ctx2 E. args E. o2 (
              e, ast e. ih /\
              splitDummies bis = ctx, ds /\
              elabType ctx ret ret2 /\
              checkDummies ds ctx2 /\
              elabTermBinders ctx args /\
              elabDefO e ast ctx (fst ret2) ctx2 (map (\ t, snd t) ds) o o2 /\
              e2 = e |> DDef x args ret2 o2)})))
      (Sum
        (Sum
          (S\ x, S\ bis, {ret |
            E. e E. ctx E. hyps E. hyps2 E. args E. ret2 (e, ast e. ih /\
              splitDummies bis = ctx ++ hyps, 0 /\
              elabTermBinders ctx args /\
              elabHyps e ast ctx args hyps hyps2 /\
              elabFmlaProv e ast ctx args ret ret2 /\
              e2 = e |> DThm args hyps2 ret2)})
          0)
        {n | e2, ast e. ih}))
  )}}) aste $;

theorem Elaborate_aux_val {ih}
  (p: wff args bis ctx ctx2 ds e hyps hyps2 i n o o2 ret ret2 sd t x)
  (h: $ ih = sep (upto (e2, ast2)) {i | Elaborate_aux i} ->
    (,(foldr '(2 2 2 2 2 1 6) (get-decl 'Elaborate_aux) nth) <-> p) $):
  $ Elaborate_aux (e2, ast2) <-> p $ =
'(bitr {srecpval : $ _ <-> _, sep _ {i | Elaborate_aux i} e. _ $} @
  elsabe @ bitrd ,eqtac @ a1i @ elabe @ syl5bb (elsabe @ elabed ,eqtac) h);

theorem Elaborate_auxS {ih}
  (p: wff args bis ctx ctx2 ds e hyps hyps2 i n o o2 ret ret2 sd t x)
  (h: $ ih = sep (upto (e2, ast |> d)) {i | Elaborate_aux i} ->
    (,(foldr '(2 2 2 3 1 2 1 0 3) (get-decl 'Elaborate_aux_val) nth) <-> p) $):
  $ Elaborate_aux (e2, ast |> d) <-> p $ =
(named '(Elaborate_aux_val @ syl5bb (ifpneg snocne0) @
  syl5bb (bitr (exeqi @
      bitr (exeqi @ bitr (aneq1i @ bitr eqcomb snocinj) anass) @
      bitr exan1 @ aneq2i @ exeqe eleq1) @
    exeqe ,eqtac) h));

--| ```
--| Elaborate (ast: List AST): Set Env
--| ```
--| Elaborate an AST to an environment.
--| Even though this returns a set, the environment is uniquely determined by the AST.
@_ abstract def Elaborate (ast: nat): set = $ {e | Elaborate_aux (e, ast)} $;

theorem elElaborate: $ e e. Elaborate ast <-> Elaborate_aux (e, ast) $ =
'(elabe ,eqtac);

theorem Elaborate_aux_lem: $ e2 = e |> s \/ e = e2 ->
  (e, ast e. sep (upto (e2, ast |> d)) {i | Elaborate_aux i} <->
   e e. Elaborate ast) $ =
'(rsyl (eor (mpbiri (ltle snoclt) leeq2) eqle) @
  syl5bb elsep @ syl6bbr elElaborate @ syl6bb (elabe Elaborate_auxeq) @
  syl bian1 @ sylibr elupto @ lelttrd (bi1i lepr1) @ a1i @ mpbi ltpr2 snoclt);

pub theorem Elaborate0: $ Elaborate 0 == sn 0 $ =
(named '(eqab1i @ Elaborate_aux_val @ a1i @ bitr4 (ifppos eqid) elsn));

pub theorem ElaborateSort {e: nat} (ast sd x: nat):
  $ Elaborate (ast |> ASTSort (sd, x)) ==
    (\ e, e |> DSort x sd) '' Elaborate ast $ =
(named @ focus
  '(eqab1i @ Elaborate_auxS @ syl5bb Suml @ syl5bb Suml @ syl5bb Suml {_ : $ih = _ -> _$})
  '(elsabed @ elabed @ syl6bbr ellamima @ syl6bb _ ,eqtac)
  '(exeqi @ aneq1a @ syl Elaborate_aux_lem orl));

pub theorem ElaborateTerm {e ctx args ret2: nat} (ast x bis ret e2: nat):
  $ e2 e. Elaborate (ast |> ASTTerm (x, bis, ret)) <->
    E. e E. ctx E. args E. ret2 (e e. Elaborate ast /\
      splitDummies bis = ctx, 0 /\
      elabTermBinders ctx args /\
      elabType ctx ret ret2 /\
      e2 = e |> DTerm x args ret2) $ =
(named @ focus
  '(bitr elElaborate @ Elaborate_auxS @ syl5bb Suml @ syl5bb Suml @ syl5bb Sumr {_ : $ih = _ -> _$})
  '(elsabed @ elsabed @ elabed @ syl6bb _ ,eqtac)
  '(exeqi @ exeqi @ exeqi @ exeqi @
    aneq1a @ aneq1d @ aneq1d @ aneq1d @ syl Elaborate_aux_lem orl));

pub theorem ElaborateAxiom
  {e ctx hyps hyps2 args ret2: nat} (ast x bis ret e2: nat):
  $ e2 e. Elaborate (ast |> ASTAxiom (x, bis, ret)) <->
    E. e E. ctx E. hyps E. hyps2 E. args E. ret2 (e e. Elaborate ast /\
      splitDummies bis = ctx ++ hyps, 0 /\
      elabTermBinders ctx args /\
      elabHyps e ast ctx args hyps hyps2 /\
      elabFmlaProv e ast ctx args ret ret2 /\
      e2 = e |> DAxiom args hyps2 ret2) $ =
(named @ focus
  '(bitr elElaborate @ Elaborate_auxS @ syl5bb Suml @ syl5bb Sumr @ syl5bb Suml {_ : $ih = _ -> _$})
  '(elsabed @ elsabed @ elabed @ syl6bb _ ,eqtac)
  '(exeqi @ exeqi @ exeqi @ exeqi @ exeqi @ exeqi @
    aneq1a @ aneq1d @ aneq1d @ aneq1d @ aneq1d @ syl Elaborate_aux_lem orl));

pub theorem ElaborateDef {e ctx ds ret2 ctx2 args o2 t: nat} (ast x bis ret o e2: nat):
  $ e2 e. Elaborate (ast |> ASTDef (x, bis, ret, o)) <->
    E. e E. ctx E. ds E. ret2 E. ctx2 E. args E. o2 (
      e e. Elaborate ast /\
      splitDummies bis = ctx, ds /\
      elabType ctx ret ret2 /\
      checkDummies ds ctx2 /\
      elabTermBinders ctx args /\
      elabDefO e ast ctx (fst ret2) ctx2 (map (\ t, snd t) ds) o o2 /\
      e2 = e |> DDef x args ret2 o2) $ =
(named @ focus
  '(bitr elElaborate @ Elaborate_auxS @ syl5bb Suml @ syl5bb Sumr @ syl5bb Sumr {_ : $ih = _ -> _$})
  '(elsabed @ elsabed @ elsabed @ elabed @ syl6bb _ ,eqtac)
  '(exeqi @ exeqi @ exeqi @ exeqi @ exeqi @ exeqi @ exeqi @
    aneq1a @ aneq1d @ aneq1d @ aneq1d @ aneq1d @ aneq1d @ syl Elaborate_aux_lem orl));

pub theorem ElaborateThm
  {e ctx hyps hyps2 args ret2: nat} (ast x bis ret e2: nat):
  $ e2 e. Elaborate (ast |> ASTThm (x, bis, ret)) <->
    E. e E. ctx E. hyps E. hyps2 E. args E. ret2 (e e. Elaborate ast /\
      splitDummies bis = ctx ++ hyps, 0 /\
      elabTermBinders ctx args /\
      elabHyps e ast ctx args hyps hyps2 /\
      elabFmlaProv e ast ctx args ret ret2 /\
      e2 = e |> DThm args hyps2 ret2) $ =
(named @ focus
  '(bitr elElaborate @ Elaborate_auxS @ syl5bb Sumr @ syl5bb Suml @ syl5bb Suml {_ : $ih = _ -> _$})
  '(elsabed @ elsabed @ elabed @ syl6bb _ ,eqtac)
  '(exeqi @ exeqi @ exeqi @ exeqi @ exeqi @ exeqi @
    aneq1a @ aneq1d @ aneq1d @ aneq1d @ aneq1d @ syl Elaborate_aux_lem orl));

pub theorem ElaborateIO (ast out n: nat):
  $ Elaborate (ast |> ASTIO out n) == 0 $ =
(named '(eqab1i @ Elaborate_auxS @ a1i @ bitr Sumr @ bitr Suml @ bitr Sumr @ binth nel0 nel0));

pub theorem ElaborateNota (ast n: nat):
  $ Elaborate (ast |> ASTNota n) == Elaborate ast $ =
(named @ focus
  '(eqab1i @ Elaborate_auxS @ syl5bb Sumr @ syl5bb Sumr {_ : $ih = _ -> _$})
  '(elabed @ syl6bb _ ,eqtac)
  '(Elaborate_aux_lem @ orr eqid));

--| ```
--| Valid (s: String): Bool
--| ```
--| The top level validity statement.
--| A string denoting an MM0 file is valid if it parses to some `ast`
--| which elaborates to an environment `e` which is valid,
--| which is to say that it extends to an environment `e2`
--| which is well formed and has a proof `p`.
@_ def Valid (s .ast .e: nat): wff =
$ E. ast E. e (parse s ast /\ e e. Elaborate ast /\ ValidEnv e) $;