Theory HIT_Syntax

theory HIT_Syntax
  imports Main
begin

section ‹A structural HIT calculus›

text ‹
  This stand-alone Isabelle/HOL session fixes a small type theory whose
  ∗‹only› type formers are function spaces and higher inductive types drawn
  from a signature environment.  The calculus is finitary, one-dimensional
  and nondependent: signatures contain finite lists of point and path
  constructors, constructor arguments have fixed higher-inductive types, and
  eliminators have a constant motive.  The development studies syntax,
  reduction, typing, signature well-formedness, free dimension support,
  boundary coherence, substitution, subject reduction, progress, multi-step
  type safety, strong normalization, confluence, and canonical forms.

  Two design decisions make the treatment uniform.

    ▪ Higher inductive types are not built in one at a time.  A signature
      lists point constructors and path constructors, each with a list of
      argument specifications, and each path constructor with two endpoints
      expressed over its own arguments.  Ordinary inductive types are the
      signatures with no path constructors, so the natural numbers, the unit
      type and the empty type are instances of the same schema.

    ▪ Path constructors are ∗‹cubical-style›: a path constructor applied
      to its arguments takes a further dimension argument, and the eliminator
      computes on it judgmentally.  The endpoints are not separate rules but
      the result of substituting the two constant dimensions, so the boundary
      of a path constructor is part of dimension substitution rather than of
      reduction.  This is a small syntax with dimension variables, not a
      formalization of cubical type theory or its Kan operations.

  Dimension variables are natural numbers.  Index ‹0› is reserved: it is the
  dimension bound by the path methods of an eliminator.  Ambient dimension
  contexts therefore consist of strictly positive indices, and no shifting is
  ever required.
›

subsection ‹Types, dimensions, endpoints, and terms›

datatype ty =
    Fun ty ty
  | Hit nat

text ‹
  An argument of a constructor is either a parameter, whose type is one of
  the higher inductive types of the signature environment, or a recursive
  occurrence of the type being described.  Restricting parameters to higher
  inductive types is no loss for the usual examples: ordinary inductive types
  are themselves instances of the schema.  What it excludes is infinitary
  constructors, whose arguments are functions into the type being defined.
›

datatype argspec =
    Par nat
  | Rec

text ‹
  An endpoint of a path constructor is a point-constructor term over the
  arguments of that path constructor.
›

datatype endpt =
    EArg nat
  | ECon nat "endpt list"

datatype dim =
    D0
  | D1
  | DVar nat

record hsig =
  pcons :: "argspec list list"
  lcons :: "argspec list list"
  lends :: "(endpt × endpt) list"

datatype tm =
    Var nat
  | Lam ty tm
  | App tm tm
  | PCon nat nat "tm list"
  | LCon nat nat "tm list" dim
  | HElim nat ty "tm list" "tm list" tm

type_synonym sigenv = "nat ⇒ hsig"

subsection ‹Instantiating an endpoint›

primrec instE :: "nat ⇒ tm list ⇒ endpt ⇒ tm" where
  "instE h as (EArg j) = as ! j"
| "instE h as (ECon k es) = PCon h k (map (instE h as) es)"

definition lhsOf :: "sigenv ⇒ nat ⇒ nat ⇒ tm list ⇒ tm" where
  "lhsOf S h k as = instE h as (fst (lends (S h) ! k))"

definition rhsOf :: "sigenv ⇒ nat ⇒ nat ⇒ tm list ⇒ tm" where
  "rhsOf S h k as = instE h as (snd (lends (S h) ! k))"

text ‹
  The smart constructor for path constructors.  Applying a path constructor
  at a constant dimension ∗‹is› the corresponding endpoint; there is no
  separate boundary rule.
›

definition mkL :: "sigenv ⇒ nat ⇒ nat ⇒ tm list ⇒ dim ⇒ tm" where
  "mkL S h k as d =
    (case d of
       D0 ⇒ lhsOf S h k as
     | D1 ⇒ rhsOf S h k as
     | DVar j ⇒ LCon h k as (DVar j))"

lemma mkL_simps [simp]:
  "mkL S h k as D0 = lhsOf S h k as"
  "mkL S h k as D1 = rhsOf S h k as"
  "mkL S h k as (DVar j) = LCon h k as (DVar j)"
  by (simp_all add: mkL_def)

subsection ‹Substitution for term variables›

primrec lift :: "nat ⇒ tm ⇒ tm" where
  "lift n (Var i) = (if i < n then Var i else Var (Suc i))"
| "lift n (Lam A t) = Lam A (lift (Suc n) t)"
| "lift n (App t u) = App (lift n t) (lift n u)"
| "lift n (PCon h k as) = PCon h k (map (lift n) as)"
| "lift n (LCon h k as d) = LCon h k (map (lift n) as) d"
| "lift n (HElim h C pms lms t) =
    HElim h C (map (lift n) pms) (map (lift n) lms) (lift n t)"

primrec subst :: "nat ⇒ tm ⇒ tm ⇒ tm" where
  "subst n s (Var i) =
    (if i < n then Var i else if i = n then s else Var (i - 1))"
| "subst n s (Lam A t) = Lam A (subst (Suc n) (lift 0 s) t)"
| "subst n s (App t u) = App (subst n s t) (subst n s u)"
| "subst n s (PCon h k as) = PCon h k (map (subst n s) as)"
| "subst n s (LCon h k as d) = LCon h k (map (subst n s) as) d"
| "subst n s (HElim h C pms lms t) =
    HElim h C (map (subst n s) pms) (map (subst n s) lms) (subst n s t)"

subsection ‹Substitution for dimension variables›

primrec dsubstD :: "nat ⇒ dim ⇒ dim ⇒ dim" where
  "dsubstD n d D0 = D0"
| "dsubstD n d D1 = D1"
| "dsubstD n d (DVar j) = (if j = n then d else DVar j)"

primrec dsubst :: "sigenv ⇒ nat ⇒ dim ⇒ tm ⇒ tm" where
  "dsubst S n d (Var i) = Var i"
| "dsubst S n d (Lam A t) = Lam A (dsubst S n d t)"
| "dsubst S n d (App t u) = App (dsubst S n d t) (dsubst S n d u)"
| "dsubst S n d (PCon h k as) = PCon h k (map (dsubst S n d) as)"
| "dsubst S n d (LCon h k as e) =
    mkL S h k (map (dsubst S n d) as) (dsubstD n d e)"
| "dsubst S n d (HElim h C pms lms t) =
    HElim h C (map (dsubst S n d) pms)
      (if n = 0 then lms else map (dsubst S n d) lms)
      (dsubst S n d t)"

subsection ‹Iterated application and eliminator arguments›

definition apps :: "tm ⇒ tm list ⇒ tm" where
  "apps t xs = foldl App t xs"

lemma apps_Nil [simp]: "apps t [] = t"
  by (simp add: apps_def)

lemma apps_Cons [simp]: "apps t (x # xs) = apps (App t x) xs"
  by (simp add: apps_def)

lemma apps_append: "apps t (xs @ ys) = apps (apps t xs) ys"
  by (simp add: apps_def)

text ‹
  When an eliminator meets a constructor, every argument is handed to the
  method, and every ∗‹recursive› argument is handed over a second time
  together with the value of the eliminator on it.
›

primrec elimArgs ::
  "nat ⇒ ty ⇒ tm list ⇒ tm list ⇒ argspec list ⇒ tm list ⇒ tm list"
where
  "elimArgs h C pms lms [] as = []"
| "elimArgs h C pms lms (s # ss) as =
    (case as of
       [] ⇒ []
     | a # as' ⇒
         (case s of
            Par h' ⇒ [a]
          | Rec ⇒ [a, HElim h C pms lms a])
         @ elimArgs h C pms lms ss as')"

lemma elimArgs_Nil_args [simp]: "elimArgs h C pms lms ss [] = []"
  by (induct ss) simp_all

end