mutually inductive types workaround

Question

Consider a simple language which has natural numbers, vectors of natural numbers, variables, and some operations like +,- and nth. Naively, I would encode it in Coq like this:

Require Import Coq.Vectors.Vector.

Inductive NExpr: Type :=
| NVarValue: nat -> NExpr
| NConst: nat -> NExpr
| NPlus : NExpr -> NExpr -> NExpr
| NMinus: NExpr -> NExpr -> NExpr
| NNth  : forall n, VExpr n -> NExpr -> NExpr
with
VExpr (n:nat): Type :=
| VVarValue: nat -> VExpr n
| VConst: Vector.t nat n -> VExpr n.

Of course, this does not work due to the known limitation producing the error: "Error: Parameters should be syntactically the same for each inductive type."

What would be a correct way to encode such language in Coq? . Of course, I should be able to write an eval function, evaluating these expressions along the lines of https://softwarefoundations.cis.upenn.edu/lf-current/Imp.html

When evaluating, the dimensionality of vectors is used as follows:

match e with
  ...
  | @NNth v i => match Compare_dec.lt_dec (evalNexp st i) n with
                | left p => Vnth (evalNexp st v) p
                | right _ => 0
                end

N.B. In this example, VExpr does not depend on NExpr, but in future it could, with the addition of constructors some of which may use NExpr. Also, I may need to add more types, for example, ZExpr for integers.

Cn you give an example when VExpr would depend on NExpr? Do I understand your evaluation snippet correctly, then VExpr is used to represent values and NExpr represents abstract syntax? — nesreka
I do not understand the difference between NVarValue and VVarValue, which both seem to model natural number constants. — eponier
@eponier NVarValue and VVarValue are lookup functions which take a variable name (represented as a natural number) and return a natural number or a vector respectively. — krokodil
@nesreka They both are a syntactic representation of expressions which represent natural numbers and vectors respectively. Example of NExpr would be 1+2*3 and the example of VExpr would be [1,2,3] using more traditional syntax. An example of VExpr which depdens on NExpr would be if we add a new constructor to VExpr, say VZeroElement: VExpr n -> NExpr -> VExpr n which would represent a hypothetical function which takes a vector and replaces an element with given index with 0. — krokodil
@krokodil Thanks. Is it feasible to remove the n:nat parameter from the second inductive? You could add is as an argument to the constructors where needed and pattern match on them. You can also move the forall n:nat, ... into a constructor n : ... — nesreka

eponier eponier · Accepted Answer · 2018-04-11T11:47:03

You can change the second inductive so that it uses an index instead of a parameter.

Require Import Coq.Vectors.Vector.

Inductive NExpr: Type :=
| NVarValue: nat -> NExpr
| NConst: nat -> NExpr
| NPlus : NExpr -> NExpr -> NExpr
| NMinus: NExpr -> NExpr -> NExpr
| NNth  : forall n, VExpr n -> NExpr -> NExpr
with
VExpr : nat -> Type :=
| VVarValue: forall n, nat -> VExpr n
| VConst: forall n, Vector.t nat n -> VExpr n.

mutually inductive types workaround

1 Answers