如何理解Coq中归纳类型term的类型构造器var (t: T)？

Great question! Let's unpack what this constructor is doing in the linear logic mechanization you're diving into:

• First, context is key: This repository implements First-Order Linear Logic (FOLL), so T here refers to the universe of types (or propositions) in this system. In linear logic (and via the Curry-Howard correspondence), propositions correspond to types, so this var constructor is defining a typed variable for the logic's syntax.

• Why not just a name/index?: In simpler lambda calculi or logics, variables are often defined with a name (like var (name: string)) or De Bruijn index (like var (idx: nat)). But here, the design ties the variable directly to its type via the t: T parameter. This makes sense for linear logic because:

  • Linear logic enforces strict usage rules (each variable must be used exactly once), so having the type baked into the variable's syntax simplifies later proofs about type preservation and linearity.
  • It eliminates the need to carry around a separate type environment when reasoning about terms—you can immediately see a variable's type just by looking at its constructor.

• Consistency with other constructors: Look at the other term constructors:

  • cte (e:A) carries a constant from domain A
  • fc1 (n:nat) (t: term) uses a natural number to index a family of unary functions
    All of these constructors include metadata that classifies the term. The var constructor follows this pattern by including the variable's type as part of its definition, keeping the syntax uniform and easier to reason about in Coq.

• What to check next: To get a full picture, look for the definition of T in the same file (SyntaxLL.v) or its dependencies. It should be an inductive type that defines all the type expressions of this linear logic—think atomic types, linear connectives like ⊗ (tensor), ⅋ (par), ! (bang), and quantifiers if it's first-order.

For example, if T includes a constructor for atomic types like atom : T, then var atom would be a variable of atomic type, ready to be used in linear logic sequents or proofs.

内容的提问来源于stack exchange，提问作者TomR