Coq中归纳数据类型的广义折叠

Question

我发现自己要一遍又一遍地重复一个模式，我想对它进行抽象。我相当有信心coq具有足够的表现力来捕捉模式，但是我在弄清楚如何做到这一点上有些麻烦。我正在定义一种编程语言，它具有表示语法术语的相互递归的归纳数据类型：

Inductive Expr : Set :=
  | eLambda  (x:TermVar) (e:Expr)
  | eVar     (x:TermVar)
  | eAscribe (e:Expr)  (t:IFType)
  | ePlus    (e1:Expr) (e2:Expr)

  | ... many other forms ...

with DType : Set :=
  | tArrow (x:TermVar) (t:DType) (c:Constraint) (t':DType)
  | tInt

  | ... many other forms ...

with Constraint : Set :=
  | cEq (e1:Expr) (e2:Expr)
  | ...

现在，我需要在这些类型上定义许多功能。例如，我想要一个函数来查找所有自由变量，一个函数来执行替换，以及一个函数来拉出所有约束的集合。这些函数都具有以下形式：

Fixpoint doExpr (e:Expr) := match e with
  (* one or two Interesting cases *)
  | ...

  (* lots and lots of boring cases,
  ** all of which just recurse on the subterms
  ** and then combine the results in the same way
  *)
  | ....

with doIFType (t:IFType) := match t with
  (* same structure as above *)

with doConstraint (c:Constraint) := match c with
  (* ditto *)

例如，要查找自由变量，我需要在变量情况和绑定的情况下做一些有趣的事情，但对于其他所有情况，我只是递归地找到子表达式的所有自由变量，然后将这些列表合并在一起。对于产生所有约束列表的函数，情况类似。替换的情况有些棘手，因为这三个函数的结果类型不同，并且用于组合子表达式的构造函数也不同：

Variable x:TermVar, v:Expr.
Fixpoint substInExpr (e:Expr) : **Expr** := match e with
  (* interesting cases *)
  | eLambda y e' =>
      if x = y then eLambda y e' else eLambda y (substInExpr e')
  | eVar y =>
      if x = y then v else y

  (* boring cases *)
  | eAscribe e' t  => **eAscribe** (substInExpr e') (substInType t)
  | ePlus    e1 e2 => **ePlus**    (substInExpr e1) (substInExpr e2)
  | ...

with substInType       (t:Type)       : **Type** := match t with ...
with substInConstraint (c:Constraint) : **Constraint** := ...
.

编写这些函数既乏味又容易出错，因为我必须为每个函数写出所有无关紧要的情况，并且需要确保对所有子项都递归。我想写的是如下内容：

Fixpoint freeVars X:syntax := match X with
  | syntaxExpr eVar    x         => [x]
  | syntaxExpr eLambda x e       => remove x  (freeVars e)
  | syntaxType tArrow  x t1 c t2 => remove x  (freeVars t1)++(freeVars c)++(freeVars t2)
  | _          _       args      => fold (++) (map freeVars args)
end.

Variable x:TermVar, v:Expr.
Fixpoint subst X:syntax := match X with
  | syntaxExpr eVar y      => if y = x then v else eVar y
  | syntaxExpr eLambda y e => eLambda y (if y = x then e else (subst e))
  | syntaxType tArrow ...

  | _ cons args => cons (map subst args)
end.

这个想法的关键是通常能够将构造函数应用于一些参数，并具有某种“映射”来保留参数的类型和数量的能力。

显然，此伪代码不起作用，因为_情况不正确。所以我的问题是，是否有可能编写以这种方式组织的代码，或者我注定要手动列出所有无聊的情况？

Answer 1

这是一种方法，但它没有提供非常可读的代码：使用策略。

假设我有一种具有许多不同数量的构造函数的语言，并且我只想将特定目标仅应用于构造函数 aaa 给出的情况，并且我想遍历所有其他构造函数，以了解可能出现在下面的 aaa他们。我可以执行以下操作：

假设你想定义一个函数 A -> B （A 是语言的类型），你需要跟踪你所处的情况，所以你应该在 A 上定义一个幻像类型，减少到 B。

Definition phant (x : A) : Type := B.

我假设 union 函数的类型为 B -> B -> B 并且 B 中有一个默认值，称为empty_B

Ltac generic_process f acc :=
  match goal with
    |- context [phan (aaa _)] => (* assume aaa has arith 1 *)
       intros val_of_aaa_component; exact process_this_value val_of_aaa_component
  | |- _ =>
  (* This should be used when the next argument of the current
     constructor is in type A, you want to process recursively
     down this argument, using the function f, and keep this result
     in the accumulator. *)
     let v := fresh "val_in_A" in
     intros v; generic_process f (union acc (f v))
     (* This clause will fail if val_in_A is not in type A *)
  | |- _ => let v := fresh "val_not_in_A" in
    (* This should be used when the next argument of the current
       constructor is not in type A, you want to ignore it *)
       intros v; generic_process f acc
  | |- phant _ =>
    (* this rule should be used at the end, when all
       the arguments of the constructor have been used. *)
    exact acc
  end.

现在，您通过证明来定义该函数。假设该函数名为 process_aaa。

Definition process_aaa (x : A) : phant x.
fix process_aaa 1.
  (* This adds process_add : forall x:A, phant x. in the context. *)
intros x; case x; generic_process process_aaa empty_B.
Defined.

请注意，generic_process 的定义只提到了一个名为 aaa 的构造函数，所有其他构造函数都以系统的方式处理。我们使用类型信息来检测要在其中执行递归下降的那些子组件。如果您有多个相互归纳的类型，则可以向 generic_process 函数添加参数，以指示每种类型将使用哪个函数，并拥有更多子句，每个子句对应每种类型的每个参数。

下面是对这个想法的测试，该语言有 4 个构造函数，要处理的值是出现在构造函数中的值var，并且类型 nat 也用于另一个构造函数 ( c2) 中。当遇到变量时，我们使用自然数列表的类型作为 type B，将nil空列表和单例列表作为结果。该函数收集所有出现的var.

Require Import List.

Inductive expr : Type :=
  var : nat -> expr
| c1 : expr -> expr -> expr -> expr
| c2 : expr -> nat -> expr
| c3 : expr -> expr -> expr
| c4 : expr -> expr -> expr
.

Definition phant (x : expr) : Type := list nat.

Definition union := (@List.app nat).

Ltac generic_process f acc := 
  match goal with
  |- context[phant (var _)] => exact (fun y => y::nil)
  | |- _ => let v := fresh "val_in_expr" in
        intros v; generic_process f (union acc (f v))
  | |- _ => let v := fresh "val_not_in_expr" in
        intros v; generic_process f acc
  | |-  phant _ => exact acc
  end.

Definition collect_vars : forall x : expr, phant x.
fix collect_vars 1.
intros x; case x; generic_process collect_vars (@nil nat).
Defined.

Compute collect_vars (c1 (var 0) (c2 (var 4) 1)
         (c3 (var 2) (var 3))).

最后一次计算返回一个列表，其中包含预期的值 0 4 2 和 3，但不是 1，这不会出现在var构造函数内。