mm0.mm0

import "peano_hex.mm0";

-- 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;
theorem binderSortBound (s: nat): $ binderSort (PBound s) = s $;
theorem binderSortReg (s vs: nat): $ binderSort (PReg s vs) = s $;

-- 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) $;

-- 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 $;

--| 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) $;

--| 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`
def Ctx (env ctx: nat): wff;
theorem Ctx0 (env: nat): $ Ctx env 0 $;
theorem CtxBound (env ctx s: nat) {sd: nat}: $ Ctx env (ctx |> PBound s) <->
  Ctx env ctx /\ E. sd (getSD env s sd /\ ~ sStrict sd) $;
theorem CtxReg (env ctx s vs: nat): $ Ctx env (ctx |> PReg s vs) <->
  Ctx env ctx /\ DepType env ctx (s <> vs) $;

--| 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`
def Expr (env ctx e s: nat): wff;
--| `ExprBi : Env -> Ctx -> SExpr -> Binder -> Bool`
def ExprBi (env ctx e bi: nat): wff;
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) $;
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) $;
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)) $;
theorem ExprBiReg (env ctx e s vs: nat):
  $ ExprBi env ctx e (PReg s vs) <-> Expr env ctx e s $;

--| 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 $;

--| 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`
def HasVar (ctx e v: nat): wff;
theorem HasVarBound (ctx u v s: nat):
  $ nth u ctx = suc (PBound s) -> (HasVar ctx (SVar u) v <-> u = v) $;
theorem HasVarReg (ctx u v s vs: nat):
  $ nth u ctx = suc (PReg s vs) -> (HasVar ctx (SVar u) v <-> v e. vs) $;
theorem HasVarApp (ctx f es v: nat) {e: nat}:
  $ HasVar ctx (SApp f es) v <-> E. e (e IN es /\ HasVar ctx e v) $;

--| 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)))) $;

--| 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`
def Free (env ctx e v: nat): wff;
theorem FreeVar (env ctx u v: nat):
  $ Free env ctx (SVar u) v <-> HasVar ctx (SVar u) v $;
theorem FreeApp (env ctx f es v: nat) {args r rs o n 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)))) $;


--| 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))) $;

--| Is this a valid declaration in the environment?
--|
--| `Decl : Env -> Decl -> Bool`
def Decl (env d: nat): wff;
theorem DeclSort (env id sd: nat): $ Decl env (DSort id sd) $;
theorem DeclTerm (env id args ret: nat):
  $ Decl env (DTerm id args ret) <-> TermOk env id args ret $;
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) $;
theorem DeclDef (env id args ret: nat) {ds e o v: 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) $;
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) $;

--| This defines a valid mm0 specification. These are well formed ASTs for which
--| we can assign a provability predicate.
--|
--| `Env : Env -> Bool`
def Env (e: nat): wff;
theorem Env0: $ Env 0 $;
theorem EnvS (e s: nat): $ Env (e |> s) <-> Env e /\ Decl e s $;

--| `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`
def EnvExtend (e1 e2: nat): wff;
theorem EnvExtend0 (e: nat): $ EnvExtend e 0 <-> e = 0 $;
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) $;
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) $;
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) $;
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 $;
theorem EnvExtendThm (e1 e2 id 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 $;

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

--| This performs simultaneous substitution of the variables in `e` with the
--| expressions in `subst`.
--|
--| `substExpr : list SExpr -> SExpr => SExpr`
def substExpr (subst e: nat): nat;
theorem substExprVar (subst v e: nat):
  $ substExpr subst (SVar v) = nth v subst - 1 $;
theorem substExprApp (subst f es: nat) {e: nat}:
  $ substExpr subst (SApp f es) = SApp f (map (\ e, substExpr subst e) es) $;

--| A CExpr is a convertibility proof:
--| `CRefl e : e = e`
--|
--| `CRefl : SExpr -> CExpr`
def CRefl (e: nat): nat = $ b0 (b0 e) $;
--| If `p : e = e'`, then `CSymm p : e' = e`
--|
--| `CSymm : CExpr -> CExpr`
def CSymm (p: nat): nat = $ b0 (b1 p) $;
--| 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
--| `p : e'[{x}, {y} -> {e}, {z}] = e'' |- CCong f {z} p : f {e} = e''`
--|
--| `CUnfold : TermID -> list VarID -> CExpr -> CExpr`
def CUnfold (f es zs c: nat): nat = $ b1 (b1 (f <> es <> zs <> c)) $;

-- 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) $;

--| Checking a conversion proof `c : (e1 : s) = (e2 : s)`.
--| `VerifyConv : Env -> Ctx -> CExpr -> SExpr -> SExpr -> SortID -> Bool`
def VerifyConv (env ctx c e1 e2 s: nat): wff;
--| `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 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 $;
theorem VerifyConvSymm (env ctx c e1 e2 s: nat):
  $ VerifyConv env ctx (CSymm c) e1 e2 s <-> VerifyConv env ctx c e2 e1 s $;
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) $;
theorem VerifyConvUnfold (env ctx f zs c e1 e2 s: nat)
  {args ret ys val es a y z e i: nat}:
  $ VerifyConv env ctx (CUnfold f es zs c) 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)}) /\
      VerifyConv env ctx c (substExpr (es ++ map (\ i, SVar i) zs) val) e2 s) $;

--| 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`
def VerifyProof (env ctx hs pf ret: nat): wff;
theorem VerifyProofHyp (env ctx hs n ret: nat):
  $ VerifyProof env ctx hs (VHyp n) ret <-> nth n hs = suc ret $;
theorem VerifyProofThm (env ctx hs args2 hs2 ret2 es ps ret: nat)
  {args 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) $;
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) $;

--| The main recursion for the proof judgment on an environment.
--| * `env`: The declarations that have already been processed.
--| * `e`: The declarations we are still stepping through.
--| * `p` is a proof object whose existence entails provability of the environment.
--|
--| `Proof : Env -> Proof -> Bool`
def Proof (env p: nat): wff;
theorem Proof0 (p: nat): $ Proof 0 p <-> p = 0 $;
theorem ProofSort (env id sd p: nat):
  $ Proof (env |> DSort id sd) p <-> Proof env p $;
theorem ProofTerm (env id a r p: nat):
  $ Proof (env |> DTerm id a r) p <-> Proof env p $;
theorem ProofAxiom (env a h r p: nat):
  $ Proof (env |> DAxiom a h r) p <-> Proof env p $;
theorem ProofDef (env id a r o p: nat):
  $ Proof (env |> DDef id a r o) p <-> Proof env p /\ o != 0 $;
theorem ProofThm (env e p a h r: nat) {p1 ds pf ctx: nat}:
  $ Proof (env |> DThm a h r) p <-> E. p1 E. ds E. pf E. ctx (
    p = p1 <> ds <> pf /\ Proof env p1 /\
    ctx = appendDummies a ds /\ Ctx env ctx /\
    VerifyProof env ctx h pf r) $;

-- 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 = $ E. e (EnvExtend env e /\ E. p Proof e p) $;


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

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

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

-- ASCII numbers
def _0: char = $ ch x3 x0 $;
def _1: char = $ ch x3 x1 $;
def _2: char = $ ch x3 x2 $;
def _3: char = $ ch x3 x3 $;
def _4: char = $ ch x3 x4 $;
def _5: char = $ ch x3 x5 $;
def _6: char = $ ch x3 x6 $;
def _7: char = $ ch x3 x7 $;
def _8: char = $ ch x3 x8 $;
def _9: char = $ ch x3 x9 $;

-- Don't really need capitals except as a range
def _A: char = $ ch x4 x1 $;
def _Z: char = $ ch x5 xa $;

-- Most of the lowercase alphabet, used in keywords
def _a: char = $ ch x6 x1 $;
def _b: char = $ ch x6 x2 $;
def _c: char = $ ch x6 x3 $;
def _d: char = $ ch x6 x4 $;
def _e: char = $ ch x6 x5 $;
def _f: char = $ ch x6 x6 $;
def _h: char = $ ch x6 x8 $;
def _i: char = $ ch x6 x9 $;
def _l: char = $ ch x6 xc $;
def _m: char = $ ch x6 xd $;
def _n: char = $ ch x6 xe $;
def _o: char = $ ch x6 xf $;
def _p: char = $ ch x7 x0 $;
def _r: char = $ ch x7 x2 $;
def _s: char = $ ch x7 x3 $;
def _t: char = $ ch x7 x4 $;
def _u: char = $ ch x7 x5 $;
def _v: char = $ ch x7 x6 $;
def _x: char = $ ch x7 x8 $;
def _z: char = $ ch x7 xa $;

-- Now we define the lexer:

def prefix (s t .x: nat): wff = $ E. x s ++ x = t $;

def maxPrefix (A: set) (s: nat): nat;
theorem maxPrefix0 {x: nat} (A: set) (s: nat):
  $ ~ (E. x (prefix x s /\ x e. A)) -> maxPrefix A s = 0 $;
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)) $;

def regexStar (R: set) (.s .t .L .x .y: nat): set =
$ S\ s, {t | E. L (L <> t e. all2 R /\ s = ljoin L)} $;
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;
def regexPlus (R: set) (.x: nat): set =
$ regexStar R i^i {x | snd x != 0} $;
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 $;

def regexLineComment (.x .y: nat): set =
$ (\ x, _hyphen : _hyphen : x ++ _nl : 0) '' {x | all {y | y != _nl} x} $;

def whitespace (.c: nat): set =
$ ((\ c, c : 0) '' white) u. regexLineComment $;

def regexMath (.x .y: nat): set =
$ (\ x, _dollar : x ++ _dollar : 0) '' {x | all {y | y != _dollar} x} $;

def IdentStart (.c: nat): set =
$ {c | (_a <= c /\ c <= _z) \/ (_A <= c /\ c <= _Z) \/ c = _under} $;

def digits (.c: nat): set = $ {c | _0 <= c /\ c <= _9} $;

def IdentRest (.c: nat): set = $ IdentStart u. digits $;

def regexIdent (.s .x .y .t: nat): set =
$ {s | E. x E. t (s = x : t /\ x e. IdentStart /\ all IdentRest t)} $;

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)} $;

def symbols: nat =
$ _ast ; _dot ; _colon ; _semi ; _lparen ; _rparen ;
  _gt ; _lbrace ; _rbrace ; sn _equal $;

def TK (s: nat): nat = $ b0 s $;
def MATH (s: nat): nat = $ b1 s $;

def Tokenize (s: nat): nat;
theorem Tokenize0: $ Tokenize 0 = suc 0 $;
theorem TokenizeWS (s x: nat):
  $ s e. whitespace -> Tokenize (s ++ x) = Tokenize x $;
theorem TokenizeIdent {t: nat} (s x r: nat):
  $ maxPrefix regexIdent s = suc (x <> r) ->
    Tokenize s = obind (Tokenize r) (\ t, suc (TK x : t)) $;
theorem TokenizeNumber {t: nat} (s x r: nat):
  $ maxPrefix isNumber s = suc (x <> r) ->
    Tokenize s = obind (Tokenize r) (\ t, suc (TK x : t)) $;
theorem TokenizeSymbol {t: nat} (c x: nat):
  $ c e. symbols -> Tokenize (c : x) =
    obind (Tokenize x) (\ t, suc (TK (c : 0) : t)) $;
theorem TokenizeMath {t: nat} (s x: nat):
  $ s e. regexMath -> Tokenize (s ++ x) =
    obind (Tokenize x) (\ t, suc (MATH s : t)) $;
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 $;


-- Now the parser:

def regexMap (F R: set): set = $ R o> cnv F $;
infixr regexMap: $<@>$ prec 100;

def regexAppL (R S: set) (.x: nat): set = $ (\ x, fst x) <@> (R <+> S) $;
infixl regexAppL: $<+$ prec 77;

def regexAppR (R S: set) (.x: nat): set = $ (\ x, snd x) <@> (R <+> S) $;
infixr regexAppR: $+>$ prec 76;

def parseTk (tk: string): set = $ sn (TK tk <> 0) $;
def parseOptTk (tk: string): set = $ regexOpt (parseTk tk) $;
def parseCh (c: char): set = $ parseTk (s1 c) $;

def _pure: string = $ _p ': _u ': _r ': _e ': s0 $;
def _strict: string = $ _s ': _t ': _r ': _i ': _c ': _t ': s0 $;
def _provable: string = $ _p ': _r ': _o ': _v ': _a ': _b ': _l ': _e ': s0 $;
def _free: string = $ _f ': _r ': _e ': _e ': s0 $;

def parseSortData: set =
$ (parseOptTk _pure <+> parseOptTk _strict) <+>
  (parseOptTk _provable <+> parseOptTk _free) $;

def parseIdent_ (.s: nat): set = $ (\ s, TK s <> s) '' regexIdent $;
def parseIdent (.x: nat): set = $ parseIdent_ i^i {x | snd x != s1 _under} $;

def ASTSort (x: nat): nat = $ b0 (b0 (b0 x)) $;
def ASTTerm (x: nat): nat = $ b0 (b0 (b1 x)) $;
def ASTAxiom (x: nat): nat = $ b0 (b1 (b0 x)) $;
def ASTDef (x: nat): nat = $ b0 (b1 (b1 x)) $;
def ASTThm (x: nat): nat = $ b1 (b0 (b0 x)) $;
def ASTIO (out x: nat): nat = $ b1 (b0 (b1 (out <> x))) $;
def ASTNota (x: nat): nat = $ b1 (b1 x) $;

def _sort: string = $ _s ': _o ': _r ': _t ': s0 $;
def parseSort (.x: nat): set = $ (\ x, ASTSort x) <@>
  (parseSortData <+> parseTk _sort +> parseIdent <+ parseCh _semi) $;

def parseType (.x: nat): set = $ (\ x, b0 x) <@>
  (parseIdent <+> regexStar parseIdent) $;
def parseFmla (.s: nat): set = $ Ran (\ s, MATH s <> b1 s) $;
def parseTypeFmla: set = $ parseType u. parseFmla $;

def parseDummyId (.x: nat): set =
$ (\ x, b0 x) <@> parseIdent_ u.
  (\ x, b1 x) <@> (parseCh _dot +> parseIdent) $;

-- This throws all binders into a common parsed representation.
-- {x: set}     goes to    (0, b0 "x", b0 ("set", []))
-- (x: set)     goes to    (1, b0 "x", b0 ("set", []))
-- (x: set y)   goes to    (1, b0 "x", b0 ("set", ["y"]))
-- (x: $foo$)   goes to    (1, b0 "x", b1 "foo")
-- (_: $foo$)   goes to    (1, b0 "_", b1 "foo")
-- (.x: set)    goes to    (1, b1 "x", b0 ("set", []))

def parseCurlyBinder (.x .z: nat): set =
$ (\ z, map (\ x, 0 <> x <> snd z) (fst z)) <@>
  (parseCh _lbrace +> regexStar parseDummyId <+>
    parseCh _colon +> parseTypeFmla <+ parseCh _rbrace) $;
def parseRegBinder (.x .z: nat): set =
$ (\ z, map (\ x, 1 <> x <> snd z) (fst z)) <@>
  (parseCh _lparen +> regexStar parseDummyId <+>
    parseCh _colon +> parseTypeFmla <+ parseCh _rparen) $;
def parseBinder (.x .y: nat): set = $ parseCurlyBinder u. parseRegBinder $;

def parseBinders (.x .z: nat): set =
$ (\ x, ljoin x) <@> regexStar parseBinder $;

def parseArrows: set =
$ regexStar (parseTypeFmla <+ parseCh _gt) <+> parseTypeFmla $;

def parseBindersAndArrows (.x .z: nat): set =
$ (\ x, (fst x ++ map (\ z, (1 <> b0 (s1 _under) <> z)) (pi21 x)) <> pi22 x) <@>
  (parseBinders <+> parseCh _colon +> parseArrows) $;

def parseSimple (tk: string): set =
$ parseTk tk +> parseIdent <+> parseBindersAndArrows <+ parseCh _semi $;

def _term: string = $ _t ': _e ': _r ': _m ': s0 $;
def parseTerm (.x: nat): set = $ (\ x, ASTTerm x) <@> parseSimple _term $;

def _axiom: string = $ _a ': _x ': _i ': _o ': _m ': s0 $;
def parseAxiom (.x: nat): set = $ (\ x, ASTAxiom x) <@> parseSimple _axiom $;

def _theorem: string = $ _t ': _h ': _e ': _o ': _r ': _e ': _m ': s0 $;
def parseThm (.x: nat): set = $ (\ x, ASTThm x) <@> parseSimple _theorem $;

def _def: string = $ _d ': _e ': _f ': s0 $;
def parseDef (.x: nat): set = $ (\ x, ASTDef x) <@>
  (parseTk _theorem +> parseIdent <+> parseBinders <+>
    parseCh _colon +> parseType <+>
    regexOpt (parseCh _equal +> parseFmla) <+ parseCh _semi) $;

def NotaDelim (x: nat): nat = $ b0 (b0 x) $;
def NotaInfix (x y: nat): nat = $ b0 (b1 (b0 (x <> y))) $;
def NotaPfx (x: nat): nat = $ b0 (b1 (b1 x)) $;
def NotaCoe (x: nat): nat = $ b1 (b0 x) $;
def NotaGen (x: nat): nat = $ b1 (b1 x) $;

def _delimiter: string =
$ _d ': _e ': _l ': _i ': _m ': _i ': _t ': _e ': _r ': s0 $;
def parseDelim (.x: nat): set = $ (\ x, NotaDelim x) <@>
  (parseTk _delimiter +>
    (((\ x, x <> x) <@> parseFmla) u.
     (parseFmla <+> parseFmla)) <+ parseCh _semi) $;

def stoi (x: nat): nat;
theorem stoi0: $ stoi 0 = 0 $;
theorem stoiS (s x: nat): $ stoi (s |> x) = stoi s * 10 + (x - _0) $;

def parseNumber (.s: nat): set = $ (\ s, TK s <> stoi s) '' isNumber $;

def _max: string = $ _m ': _a ': _x ': s0 $;
def parsePrec (.x: nat): set = $ parseTk _max u. (\ x, suc x) <@> parseNumber $;

def _prec: string = $ _p ': _r ': _e ': _c ': s0 $;
def parseSimpleNota (tk: string): set =
$ parseTk tk +> parseIdent <+> parseCh _colon +> parseFmla <+>
    parseTk _prec +> parsePrec <+ parseCh _semi $;

def _infixl: string = $ _i ': _n ': _f ': _i ': _x ': _l ': s0 $;
def _infixr: string = $ _i ': _n ': _f ': _i ': _x ': _r ': s0 $;
def _prefix: string = $ _p ': _r ': _e ': _f ': _i ': _x ': s0 $;
def parseInfixl (.x: nat): set = $ (\ x, NotaInfix 0 x) <@> parseSimpleNota _infixl $;
def parseInfixr (.x: nat): set = $ (\ x, NotaInfix 1 x) <@> parseSimpleNota _infixr $;
def parsePfx (.x: nat): set = $ (\ x, NotaPfx x) <@> parseSimpleNota _prefix $;

def _coercion: string = $ _c ': _o ': _e ': _r ': _c ': _i ': _o ': _n ': s0 $;
def parseCoe (.x: nat): set = $ (\ x, NotaCoe x) <@>
  (parseTk _coercion +> parseIdent <+>
   parseCh _colon +> parseIdent <+>
   parseCh _gt +> parseIdent <+> parseCh _semi) $;

def parseLiteral (.x: nat): set =
$ ((\ x, b0 x) <@> (parseCh _lparen +> parseFmla <+>
    parseCh _colon +> parsePrec <+ parseCh _rparen)) u.
  ((\ x, b1 x) <@> parseIdent) $;

def _notation: string = $ _n ': _o ': _t ': _a ': _t ': _i ': _o ': _n ': s0 $;
def parseGenNota (.x: nat): set = $ (\ x, NotaCoe 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) $;

def _input: string = $ _i ': _n ': _p ': _u ': _t ': s0 $;
def _output: string = $ _o ': _u ': _t ': _p ': _u ': _t ': s0 $;

def inputKinds: nat = $0$;
def outputKinds: nat = $0$;

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 $;

def parseIO (.x: nat): set =
$ ((\ x, ASTIO 0 x) <@> parseIO1 _input inputKinds) u.
  ((\ x, ASTIO 1 x) <@> parseIO1 _output outputKinds) $;

def parseAST: set =
$ regexStar (parseSort u. parseTerm u. parseAxiom u.
    parseThm u. parseDef u. parseNota u. parseIO) $;

def parse (s ast .tks: nat): wff =
$ E. tks (Tokenize s = suc tks /\ tks <> ast e. parseAST) $;

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

def lookupVar (ctx x: nat): nat;
theorem lookupVar0 (x: nat): $ lookupVar 0 x = 0 $;
theorem lookupVarEq (bis c x t: nat):
  $ lookupVar (bis |> (c <> x <> t)) x = suc (len bis) $;
theorem lookupVarNe (bis c x y t: nat): $ y != x ->
  lookupVar (bis |> (c <> x <> t)) y = lookupVar bis y $;

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

def nonemptyNonwhite (.s .c: nat): set =
$ {s | s != 0 /\ all {c | ~c e. white} s} $;

def simpleTokenize (s: nat): nat;
theorem simpleTokenize0: $ simpleTokenize 0 = 0 $;
theorem simpleTokenizeWS (c s: nat):
  $ c e. white -> simpleTokenize (c : s) = simpleTokenize s $;
theorem simpleTokenizeTk (s x r: nat):
  $ maxPrefix nonemptyNonwhite s = suc (x <> r) ->
    simpleTokenize s = x : simpleTokenize r $;

def getDelimiters (ast: nat): nat;
theorem getDelimiters0: $ getDelimiters 0 = 0 <> 0 $;
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)) $;
theorem getDelimitersOther {l r: nat} (ast t: nat):
  $ ~(E. l E. r t = ASTNota (NotaDelim (b1 l <> b1 r))) ->
    getDelimiters (ast |> t) = getDelimiters ast $;

def delimitersOk (A: set) (.x .y: nat): wff =
$ A. x (x e. A -> len x = 1) $;

def tokenizeFmla (ast f: nat): nat;
theorem tokenizeFmla0 (ast: nat): $ tokenizeFmla ast 0 = 0 $;
theorem tokenizeFmlaWhite (ast x xs: nat): $ x e. white ->
  tokenizeFmla ast (x : xs) = tokenizeFmla ast xs $;
theorem tokenizeFmla1 (ast x: nat): $ ~x e. white ->
  tokenizeFmla ast (x : 0) = (x : 0) : 0 $;
theorem tokenizeFmlaSLDelim (ast x xs: nat):
  $ x : 0 e. fst (getDelimiters ast) ->
    tokenizeFmla ast (x : xs) = (x : 0) : tokenizeFmla ast xs $;
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) $;
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 $;

-- the below non-free recursive definition is harder to work with so
-- we will stick to the obvious one unless we need these theorems

-- theorem tokenizeFmlaWS (ast s c t: nat): $ c e. white ->
--   tokenizeFmla ast (s ++ c : t) = tokenizeFmla ast s ++ tokenizeFmla ast t $;
-- theorem tokenizeFmlaLDelim (ast x s t: nat):
--   $ x e. fst (getDelimiters ast) ->
--     tokenizeFmla ast (s ++ x ++ t) =
--     tokenizeFmla ast (s ++ x) ++ tokenizeFmla ast t $;
-- theorem tokenizeFmlaRDelim (ast x s t: nat):
--   $ x e. snd (getDelimiters ast) ->
--     tokenizeFmla ast (s ++ x ++ t) =
--     tokenizeFmla ast s ++ tokenizeFmla ast (x ++ t) $;
-- theorem tokenizeFmlaJoin (ast x s t: nat):
--   $ s e. nonemptyNonwhite -> ljoin (tokenizeFmla ast s) = s $;
-- 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) $;

def getPfx (ast: nat): nat;
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) $;

def getInfix (ast r: nat): nat;
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) $;

def getNota (ast: nat): nat;
theorem getNotaEl (ast x y: nat):
  $ x <> y e. getNota ast <-> ASTNota (NotaGen (x <> y)) IN ast $;

def getCoe (ast: nat): nat;
theorem getCoeEl (ast x y: nat):
  $ x <> y e. getCoe ast <-> ASTNota (NotaCoe (x <> y)) IN ast $;

def precle (m n: nat): wff; infixl precle: $<=p$ prec 50;
theorem precle02 (n: nat): $ n <=p 0 $;
theorem precle01 (m: nat): $ ~ 0 <=p suc m $;
theorem precleS (m n: nat): $ suc m <=p suc n <-> m <= n $;

def precSuc (n: nat): nat;
theorem precSuc0: $ precSuc 0 = 0 $;
theorem precSucS (n: nat): $ precSuc (suc n) = suc (suc n) $;

def litsPrec (lits q: nat): nat;
theorem litsPrec0 (q: nat): $ litsPrec 0 q = q $;
theorem litsPrecC (c p lits q: nat):
  $ litsPrec (b0 (c <> p) : lits) q = precSuc p $;
theorem litsPrecV (v lits q: nat):
  $ litsPrec (b1 v : lits) q = 0 $;

-- This is a more precise version of SExpr that allows reconstructing an
-- exact token string from a parse proof
def PTVar (v: nat): nat = $ b0 (b0 (b0 v)) $;
def PTParens (x: nat): nat = $ b0 (b0 (b1 x)) $;
def PTFunc (f x: nat): nat = $ b0 (b1 (f <> x)) $;
def PTPfx (f c x: nat): nat = $ b1 (b0 (b0 (f <> c <> x))) $;
def PTNota (f x: nat): nat = $ b1 (b0 (b1 (f <> x))) $;
def PTInfix (r f c x y: nat): nat = $ b1 (b1 (b0 (r <> f <> c <> x <> y))) $;
def PTCoe (f x: nat): nat = $ b1 (b1 (b1 (f <> x))) $;

def ptToStr (pt: nat): nat;
theorem ptToStrVar (v: nat): $ ptToStr (PTVar v) = v : 0 $;
theorem ptToStrParens {s: nat} (e: nat):
  $ ptToStr (PTParens e) = s1 _lparen : ptToStr e ++ s1 _rparen : 0 $;
theorem ptToStrFunc {s: nat} (f x: nat): $ ptToStr (PTFunc f x) =
  f : ljoin (map (\ s, ptToStr s) x) $;
theorem ptToStrPfx {s: nat} (f c x: nat): $ ptToStr (PTPfx f c x) =
  c : ljoin (map (\ s, ptToStr s) x) $;
theorem ptToStrNota {y: nat} (f x: nat):
  $ ptToStr (PTNota f x) =
    ljoin (map (case (\ y, y : 0) (\ y, ptToStr y)) x) $;
theorem ptToStrInfix (r f c x y: nat):
  $ ptToStr (PTInfix r f c x y) = ptToStr x ++ c : ptToStr y $;
theorem ptToStrCoe {y: nat} (f x: nat):
  $ ptToStr (PTCoe f x) = ptToStr x $;

def ptCheck (eac p pt e: nat): wff;
def ptCheckNotaLs (eac bis lits xs es p: nat): wff;

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) $;
theorem ptCheckParens (eac p pt e: nat):
  $ ptCheck eac p (PTParens pt) e <->
    ptCheck eac (suc 0) pt e $;
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 /\ len xs = len args /\
      xs <> e2 e. all2 (S\ x, {y | ptCheck (env <> ast <> ctx) 0 x y}) /\
      e = SApp f e2) $;
theorem ptCheckPfx (eac p f c xs e: nat) {l z f2 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)) $;
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) $;
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)) $;
theorem ptCheckCoe {y e2: nat} (eac p f x e: nat):
  $ p <= eac ->
    (ptCheck eac p (PTCoe f x) e <->
    E. y E. e2 (
      f <> y e. getCoe (pi21 eac) /\ ptCheck eac p x e2 /\
      e = SApp f e2)) $;

theorem ptCheckNotaLs0 (eac bis xs es q: nat):
  $ ptCheckNotaLs eac bis 0 xs es q <-> xs = 0 $;
theorem ptCheckNotaLsC {x 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) $;
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)) $;

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)} $;

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.

def splitDummies (bis: nat): nat;
theorem splitDummies0: $ splitDummies 0 = 0 $;
theorem splitDummiesL (bis bis1 bis2 c x t: nat): $
  splitDummies bis = bis1 <> bis2 ->
  splitDummies (bis |> (c <> b0 x <> t)) =
    (bis1 |> (c <> x <> t)) <> bis2 $;
theorem splitDummiesR (bis bis1 bis2 c x t: nat): $
  splitDummies bis = bis1 <> bis2 ->
  splitDummies (bis |> (c <> b1 x <> t)) = bis1 <> (bis2 |> (x <> t)) $;

def checkDummies (ds bis: nat): wff;
theorem checkDummies0 (bis: nat): $ checkDummies 0 bis <-> bis = 0 $;
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 = (0 <> x <> t) : bis2) $;

def lookupVars (ctx .s .t: nat): set = $ S\ s, {t | lookupVar ctx s = suc t} $;

def elabType (ast 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) $;

def elabTermBinder (ast ctx bi s: nat): wff;
theorem elabTermBinderFmla (ast ctx c x f s: nat):
  $ ~ elabTermBinder ast ctx (c <> x <> b1 f) s $;
theorem elabTermBinderBound {t2: nat} (ast ctx bi x t s: nat):
  $ elabTermBinder ast ctx (0 <> x <> b0 t) s <->
    E. t2 (elabType ast ctx t (t2 <> 0) /\ s = PBound t2) $;
theorem elabTermBinderReg {t2 vs2: nat} (ast ctx bi x t s: nat):
  $ elabTermBinder ast ctx (1 <> x <> b0 t) s <->
    E. t2 E. vs2 (elabType ast ctx t (t2 <> vs2) /\ s = PReg t2 vs2) $;

def elabTermBinders (ast ctx ctx2: nat): wff;
theorem elabTermBinders0 (ast ctx2: nat):
  $ elabTermBinders ast 0 ctx2 <-> ctx2 = 0 $;
theorem elabTermBindersS {ctx2 bi2: nat} (ast ctx bi ctx3: nat):
  $ elabTermBinders ast (ctx |> bi) ctx3 <->
    E. ctx2 E. bi2 (elabTermBinders ast ctx ctx2 /\
      elabTermBinder ast ctx bi bi2 /\ ctx3 = ctx2 |> bi2) $;

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) $;

def elabFmlaProv (env ast ctx args f e .f2: nat): wff =
$ E. f2 (f = b1 f2 /\ parseExprProv (env <> ast <> ctx) args f2 == sn e) $;

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 = 1 <> b0 x <> f /\
    elabFmlaProv env ast ctx args f hyp2)}) $;

def elabDefO (env ast ctx s ds o o2: nat): wff;
theorem elabDefO0 (env ast ctx s ds o2: nat):
  $ elabDefO env ast ctx s ds 0 o2 <-> ds = 0 /\ o2 = 0 $;
theorem elabDefOS {args2 e: nat} (env ast ctx s ds f o2: nat):
  $ elabDefO env ast ctx s ds (suc f) o2 <-> E. args2 E. e (
      elabTermBinders ast (ctx ++ ds) args2 /\
      elabFmla env ast (ctx ++ ds) args2 f e s /\
      o2 = suc (ds <> e)) $;

def Elaborate (ast: nat): set;
theorem Elaborate0: $ Elaborate 0 == sn 0 $;
theorem ElaborateSort {e: nat} (ast sd x: nat):
  $ Elaborate (ast |> ASTSort (sd <> x)) ==
    (\ e, e |> DSort x sd) '' Elaborate ast $;
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 ast ctx args /\
      elabType ast ctx ret ret2 /\
      e2 = e |> DTerm x args ret2) $;
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 ast ctx args /\
      elabHyps e ast ctx args hyps hyps2 /\
      elabFmlaProv e ast ctx args ret ret2 /\
      e2 = e |> DAxiom args hyps2 ret2) $;
theorem ElaborateDef {e ctx ds ret2 ctx2 args o2: 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 ast ctx ret ret2 /\
      checkDummies ds ctx2 /\
      elabTermBinders ast ctx args /\
      elabDefO e ast ctx (fst ret2) ctx2 o o2 /\
      e2 = e |> DDef x args ret2 o2) $;
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 ast ctx args /\
      elabHyps e ast ctx args hyps hyps2 /\
      elabFmlaProv e ast ctx args ret ret2 /\
      e2 = e |> DThm args hyps2 ret2) $;
theorem ElaborateIO (ast out n: nat):
  $ Elaborate (ast |> ASTIO out n) == 0 $;
theorem ElaborateNota (ast n: nat):
  $ Elaborate (ast |> ASTNota n) == Elaborate ast $;

def Valid (s .ast .e: nat): wff =
$ E. ast E. e (parse s ast /\ e e. Elaborate ast /\ ValidEnv e) $;