De Bruijn indices with "fake" name?

Use De Bruijn indices to represent expr variables, but keep a "fake" name for better readability. "Fake" name is not used in evaluation or type checking.

Easier to write assertion operations and prove correctness.

A name checker in Coq can be implemented to ensure that the fake names are valid.

Notation:

Check (ƛ "x", '0 "x").
(*  : expr ?Γ (?t2 -> ?t2)  *)

Well-scoped expressions

Definition Ctx n := list (type n).

Inductive Var {n} : Ctx n -> type n -> Type :=
  | VZ {Γ t} : Var (t :: Γ) t
  | VS {Γ t u} (v: Var Γ t) : Var (u :: Γ) t.

Inductive expr : forall {n: nat}, Ctx n -> type n -> Type :=
  | EConst {m n Γ} (i: string) (t: type m) (ts: vec (type n) m) : expr Γ (type_map t ts)
  | EVar {n Γ} {t: type n} (i: Var Γ t) (j: string) : expr Γ t
  | EApp {n Γ} {t1 t2: type n} (f: expr Γ (t1 -> t2)) (x: expr Γ t1) : expr Γ t2
  | ELam {n Γ} {t1 t2: type n} (i: string) (e: expr (t1 :: Γ) t2) : expr Γ (t1 -> t2).

Benefits:

• Statically ensure that variables are only used in scope
• Enables defining lambda expression (variable binding) within expr
  • Function extensionality is needed to prove expr_subst_sound on lambda expr?

Problems:

• Longer expressions

Problem of PHOAS (Parametric Higher-Order Abstract Syntax), Deeper Shallow Embedding

A Verified Foreign Function Interface between Coq and C JOOMY KORKUT, Princeton University, USA and Bloomberg L.P., USA KATHRIN STARK, Heriot-Watt University, Scotland ANDREW W. APPEL

Use host language variable binding to represent object language variable binding.

Cannot match the variable in the term with a variable in the context. (Not sure if possible with UIP axiom)

No decidable equality for embedding of types or expressions.

Note: Migrate to Coq 8.20

<: record field coercion changed to ::intuition will be deprecated standard library changes