Well-Typed Vectors of PrimOp Arguments

Annotated.lean

/-
Grammar

Typing throughout is handled in the same way as
[The Well-Typed Interpreter](https://lean-lang.org/lean4/doc/examples/interp.lean.html), 
i.e., all terms are typed directly.

The interesting bit here is primop application and the handling of args.  The
primops and the arguments are all well-typed with arity tracked and represented
by sized vectors.  This works except for one particular case.
-/

mutual
  /-- Types: Bools, Nats, and Functions.  Functions are from a Domain of
    arguments (a vector of types) to a result type. -/
  inductive Ty: Type where
    | bool: Ty
    | nat: Ty
    | fn {α: Nat} (δ: Domain α) (ρ: Ty): Ty

  /-- The domain of a function as a vector of types -/
  inductive Domain: Nat → Type where
    | nil (τ: Ty): Domain 1
    | cons {α: Nat} (τ: Ty) (rest: Domain α): Domain α.succ
end

/--
Two domains can be appended.

Note: it's `β + α` instead of `α + β` fails because Lean can automatically
reduce `x + 1` but stumbles on `1 + x`.  Don't know if this is strictly relevant
to the issue below, but I also don't know of a way to remind Lean that
`Nat.add_comm` in this particular context.

This doesn't affect the order of the types in the appended domains, though, as
both `α` and `β` are just the arities (i.e., `Nat`s)
-/
@[reducible]
instance: {α β: Nat} → HAppend (Domain α) (Domain β) (Domain (β + α)) where
  hAppend lhs rhs :=
    append lhs rhs
    where
      @[reducible]
      append {α β: Nat}: Domain α → Domain β → Domain (β + α)
        | .nil τ,     δ₂ => .cons τ δ₂
        | .cons τ δ₁, δ₂ => .cons τ (append δ₁ δ₂)

/-- An individual type can be appended to a domain -/
@[reducible]
instance: {α: Nat} → HAppend (Domain α) Ty (Domain (α + 1)) where
  hAppend lhs rhs :=
    append lhs rhs
    where
      @[reducible]
      append {α: Nat}: Domain α → Ty → Domain (α + 1)
        | .nil τ₁,    τ₂ => .cons τ₁ (.nil τ₂)
        | .cons τ₁ δ, τ₂ => .cons τ₁ (append δ τ₂)

/-- A set of primitive operations -/
inductive PrimOp: {α: Nat} → Domain α → Ty → Type where
  | and: PrimOp (.cons .bool (.nil .bool)) .bool
  | or:  PrimOp (.cons .bool (.nil .bool)) .bool
  | not: PrimOp (.nil  .bool)              .bool

  | add: PrimOp (.cons .nat (.nil .nat)) .nat
  | mul: PrimOp (.cons .nat (.nil .nat)) .nat

  | eq  {τ: Ty}: PrimOp (.cons τ (.nil τ)) .bool
  | neq {τ: Ty}: PrimOp (.cons τ (.nil τ)) .bool

  | lt:  PrimOp (.cons .nat (.nil .nat)) .bool
  | lte: PrimOp (.cons .nat (.nil .nat)) .bool
  | gt:  PrimOp (.cons .nat (.nil .nat)) .bool
  | gte: PrimOp (.cons .nat (.nil .nat)) .bool

mutual
  /-- The values of the language -/
  inductive Value: Ty → Type where
    | bool (b: Bool): Value .bool
    | nat (n: Nat): Value .nat

  /-- A vector of values from a domain  -/
  inductive Values: {α: Nat} → Domain α → Type where
    | nil {τ: Ty} (v: Value τ): Values (.nil τ)
    | cons {τ: Ty} {α: Nat} {δ: Domain α} (v: Value τ) (rest: Values δ): Values (.cons τ δ)

  /--
  Terms: Values, primitive operation applications, and conditionals.  PrimOps
  apply the operation to a vector of arguments.
  -/
  inductive Term: Ty → Type where
    | value {τ: Ty} (v: Value τ): Term τ
    | primOp {α: Nat} {δ: Domain α} {ρ: Ty} (op: PrimOp δ ρ) (operands: Args δ): Term ρ
    | cond {τ: Ty} (c: Term .bool) (t f: Term τ): Term τ

  /-- A vector of terms from a domain -/
  inductive Terms: {α: Nat} → Domain α → Type where
    | nil {τ: Ty} (t: Term τ): Terms (.nil τ)
    | cons {τ: Ty} {α: Nat} {δ: Domain α} (t: Term τ) (rest: Terms δ): Terms (.cons τ δ)

  /--
  A vector of function application arguments.  These are intended to be
  evaluated left-to-right, turning a vector of unevaluated terms into a vector
  of fully-evaluated values. The three cases are:

  * `terms`: A vector of unevaluated terms matching the domain.  This is the
    "initial" value of an arguments vector.
  * `mix`: A vector of values and a vector of unevalutated terms that when
    appended match the domain.  This is a partially-evaluated intermediary state
    of the arguments vector.
  * `values`: A vector of values matching the domain.  This is the "final" value
    of an arguments vector.
  -/
  inductive Args: {α: Nat} → Domain α → Type where
    | terms {α: Nat} {δ: Domain α} (ts: Terms δ): Args δ
    | mix {α β: Nat} {δ₁: Domain α} {δ₂: Domain β} (vs: Values δ₁) (ts: Terms δ₂): Args (δ₁ ++ δ₂)
    | values {α: Nat} {δ: Domain α} (vs: Values δ): Args δ
end

/-- Vectors of values can be appended -/
@[reducible]
instance: {α β: Nat} → {δ₁: Domain α} → {δ₂: Domain β} → HAppend (Values δ₁) (Values δ₂) (Values (δ₁ ++ δ₂)) where
  hAppend lhs rhs :=
    append lhs rhs
    where
      @[reducible]
      append {α β: Nat} {δ₁: Domain α} {δ₂: Domain β}: Values δ₁ → Values δ₂ → Values (δ₁ ++ δ₂)
        | .nil v,       vs => .cons v vs
        | .cons v rest, vs => .cons v (append rest vs)

/-- Individual values can be appended to a vector of values -/
@[reducible]
instance: {α: Nat} → {δ: Domain α} → {τ: Ty} → HAppend (Values δ) (Value τ) (Values (δ ++ τ)) where
  hAppend lhs rhs :=
    append lhs rhs
    where
      @[reducible]
      append {α: Nat} {δ: Domain α} {τ: Ty}: Values δ → Value τ → Values (δ ++ τ)
        | .nil v,       vs => .cons v (.nil vs)
        | .cons v rest, vs => .cons v (append rest vs)

/-
Semantics
-/

namespace PrimOp
  /--
  All primitive operations take a vector of values and produce a term (which
  will always be a value) in a single step.
  -/
  inductive Eval₁: {α: Nat} → {δ: Domain α} → {τ: Ty} → PrimOp δ τ → Values δ → Term τ → Prop where
    | and {lhs rhs: Bool} (vs: Values (.cons .bool (.nil .bool))): Eval₁ .and (.cons (.bool lhs) (.nil (.bool rhs))) (.value (.bool (lhs && rhs)))
    | or  {lhs rhs: Bool} (vs: Values (.cons .bool (.nil .bool))): Eval₁ .or  (.cons (.bool lhs) (.nil (.bool rhs))) (.value (.bool (lhs || rhs)))
    | not {operand: Bool} (vs: Values (.nil .bool)): Eval₁ .not (.nil (.bool operand)) (.value (.bool (!operand)))

    | add {lhs rhs: Nat} (vs: Values (.cons .nat (.nil .nat))): Eval₁ .add (.cons (.nat lhs) (.nil (.nat rhs))) (.value (.nat (lhs + rhs)))
    | mul {lhs rhs: Nat} (vs: Values (.cons .nat (.nil .nat))): Eval₁ .mul (.cons (.nat lhs) (.nil (.nat rhs))) (.value (.nat (lhs * rhs)))

    | eqBool  {lhs rhs: Bool} (vs: Values (.cons .bool (.nil .bool))): Eval₁ .eq  (.cons (.bool lhs) (.nil (.bool rhs))) (.value (.bool (lhs == rhs)))
    | eqNat   {lhs rhs: Nat}  (vs: Values (.cons .nat  (.nil .nat))):  Eval₁ .eq  (.cons (.nat  lhs) (.nil (.nat  rhs))) (.value (.bool (lhs == rhs)))
    | neqBool {lhs rhs: Bool} (vs: Values (.cons .bool (.nil .bool))): Eval₁ .neq (.cons (.bool lhs) (.nil (.bool rhs))) (.value (.bool (lhs != rhs)))
    | neqNat  {lhs rhs: Nat}  (vs: Values (.cons .nat  (.nil .nat))):  Eval₁ .neq (.cons (.nat  lhs) (.nil (.nat  rhs))) (.value (.bool (lhs != rhs)))

    | lt  {lhs rhs: Nat} (vs: Values (.cons .nat (.nil .nat))): Eval₁ .lt  (.cons (.nat lhs) (.nil (.nat rhs))) (.value (.bool (lhs < rhs)))
    | lte {lhs rhs: Nat} (vs: Values (.cons .nat (.nil .nat))): Eval₁ .lte (.cons (.nat lhs) (.nil (.nat rhs))) (.value (.bool (lhs ≤ rhs)))
    | gt  {lhs rhs: Nat} (vs: Values (.cons .nat (.nil .nat))): Eval₁ .gt  (.cons (.nat lhs) (.nil (.nat rhs))) (.value (.bool (lhs > rhs)))
    | gte {lhs rhs: Nat} (vs: Values (.cons .nat (.nil .nat))): Eval₁ .gte (.cons (.nat lhs) (.nil (.nat rhs))) (.value (.bool (lhs ≥ rhs)))
end PrimOp

mutual
  /--
  Single-step evaluation of terms:

  * PrimOp applications evaluate their args to values, then apply the primop to
    the values.
  * Conditionals evaluate their condition to a value, then return the
    appropriate branch
  -/
  inductive Term.Eval₁: {τ: Ty} → Term τ → Term τ → Prop where
    | primOpArgs {α: Nat} {δ: Domain α} {ρ: Ty} {op: PrimOp δ ρ} {args₁ args₂: Args δ} (h: Args.Eval₁ args₁ args₂): Term.Eval₁ (.primOp op args₁) (.primOp op args₂)
    | primOp {α: Nat} {δ: Domain α} {ρ: Ty} {op: PrimOp δ ρ} {vs: Values δ} {res: Term ρ} (h: PrimOp.Eval₁ op vs res): Term.Eval₁ (.primOp op (.values vs)) res
    | condTrue {τ: Ty} {t f: Term τ}: Term.Eval₁ (.cond (.value (.bool true)) t f) t
    | condFalse {τ: Ty} {t f: Term τ}: Term.Eval₁ (.cond (.value (.bool false)) t f) f
    | cond {τ: Ty} {c₁ c₂: Term .bool} {t f: Term τ} (h: Term.Eval₁ c₁ c₂): Term.Eval₁ (.cond c₁ t f) (.cond c₂ t f)

  /--
  Single-step evaluation of args:

  * Arguments are evaluated left-to-right
  * The head of the term vector is evaluated to a value, then "shifted" to the
    end of the values array.

  I've aligned everything on the right so it should hopefully be easier to see
  which step does what without all the implicits noise.

  QUESTIONS (likely inter-related):

  1. `mixConstValue`: This is the case where a term has been evaluated to a
     value and is "shifted" to the values vector, specifically when there are
     remaining terms to evaluate.  The domains of the value vectors in the two
     `.mix` constructors are equal once reduced, but aren't identical as stated.
     They're `δ₁ ++ (τ ++ δ₂)` and `(δ₁ ++ τ) ++ δ₂`. Lean can't seem to deduce
     that those are equal, so it throws an error.  Similarly, if you hack around
     the `Values` typing issue, the mirror-image issue comes up with the `Terms`
     vector.
  2. `mixNilValue`: There's an `HAppend` instance to append a `Value` onto a
     `Values` vector, but this case doesn't like `(vs ++ v)`, only
     `(vs ++ (Values.nil v))`.  I don't know why it's not able to use the more
     specific instance.
  -/
  inductive Args.Eval₁: {α: Nat} → {δ: Domain α} → Args δ → Args δ → Prop where
    | termsNil {τ: Ty} {t₁ t₂: Term τ}                                                                        (h: Term.Eval₁ t₁ t₂): Args.Eval₁ (.terms (.nil t₁))              (.terms (.nil t₂))
    | termsNilValue {τ: Ty} {v: Value τ}:                                                                                            Args.Eval₁ (.terms (.nil (.value v)))      (.values (.nil v))
    | termsCons {α: Nat} {δ: Domain α} {τ: Ty} {t₁ t₂: Term τ} {ts: Terms δ}                                  (h: Term.Eval₁ t₁ t₂): Args.Eval₁ (.terms (.cons t₁ ts))          (.terms (.cons t₂ ts))
    | termsConsValue {α: Nat} {δ: Domain α} {τ: Ty} {v: Value τ} {ts: Terms δ}:                                                      Args.Eval₁ (.terms (.cons (.value v) ts))  (.mix (.nil v) ts)
    | mixNil {α: Nat} {δ: Domain α} {vs: Values δ} {τ: Ty} {t₁ t₂: Term τ}                                    (h: Term.Eval₁ t₁ t₂): Args.Eval₁ (.mix vs (.nil t₁))             (.mix vs (.nil t₂))
    | mixNilValue {α: Nat} {δ: Domain α} {vs: Values δ} {τ: Ty} {v: Value τ}:                                                        Args.Eval₁ (.mix vs (.nil (.value v)))     (.values (vs ++ (Values.nil v)))
    | mixCons {α β: Nat} {δ₁: Domain α} {δ₂: Domain β} {vs: Values δ₁} {τ: Ty} {t₁ t₂: Term τ} {ts: Terms δ₂} (h: Term.Eval₁ t₁ t₂): Args.Eval₁ (.mix vs (.cons t₁ ts))         (.mix vs (.cons t₂ ts))
    | mixConsValue {α β: Nat} {δ₁: Domain α} {δ₂: Domain β} {τ: Ty} {vs: Values δ₁} {v: Value τ} {ts: Terms δ₂}:                     Args.Eval₁ (.mix vs (.cons (.value v) ts)) (.mix (vs ++ v) ts)
end