【发布时间】：2017-12-12 02:14:51
【问题描述】：
我正在编写一种玩具语言，其中 AST 中的节点可以有任意数量的子节点（Num 有 0，Arrow 有 2，等等）。您可以调用这些运算符。此外，AST 中的一个节点可能是“聚焦”的。如果有焦点，我们用Z 索引数据类型，如果没有，我们用H 索引。
我需要关于代码的几个部分的建议。希望可以一次询问所有这些问题，因为它们是相关的。
您将如何定义具有一个焦点的内部节点类型
InternalZ？现在我说“我们有S n孩子——其中n没有焦点，而一个（在某个给定索引处）有焦点。一个稍微更直观的选项（看起来像拉链）是InternalZ : forall n m, arityCode (n + 1 + m) -> Vector.t (t H) n -> t Z -> Vector.t (t H) m -> t Z。我不过我知道我不想处理这个添加。精炼类型：在
eq的两个有趣案例中，我比较了两个ns（孩子的数量）。如果它们相同，我应该能够“强制”arityCodes 和Vector.ts 具有相同的类型。现在我用两个引理破解了这个。我应该如何正确地做到这一点？似乎 Adam Chlipala 的 "convoy pattern" 可能会有所帮助，但我不知道如何解决。如果我取消注释任何一个
Vector.eqb调用，Coq 会抱怨“无法猜测修复的递减参数。”。我理解这个错误，但我不确定如何规避它。首先想到的是我可能必须按子级的深度来索引t。
我的代码：
Module Typ.
Import Coq.Arith.EqNat.
Import Coq.Structures.Equalities.
Import Coq.Arith.Peano_dec.
Import Fin.
Import Vector.
(* h: unfocused, z: focused *)
Inductive hz : Set := H | Z.
(* how many children can these node types have *)
Inductive arityCode : nat -> Type :=
| Num : arityCode 0
| Hole : arityCode 0
(* | Cursor : arityCode 1 *)
| Arrow : arityCode 2
| Sum : arityCode 2
.
Definition codeEq (n : nat) (l r : arityCode n) : bool :=
match l, r with
| Num, Num => true
| Hole, Hole => true
| Arrow, Arrow => true
| Sum, Sum => true
| _, _ => false
end.
(* our AST *)
Inductive t : hz -> Type :=
| Leaf : arityCode 0 -> t H
| Cursor : t H -> t Z
| InternalH : forall n, arityCode n -> Vector.t (t H) n -> t H
| InternalZ : forall n, arityCode (S n) -> Vector.t (t H) n -> Fin.t n * t Z -> t Z
(* alternative formulation: *)
(* | InternalZ : forall n m, arityCode (n + 1 + m) -> Vector.t (t H) n -> t Z -> Vector.t (t H) m -> t Z *)
.
Lemma coerceArity (n1 n2 : nat) (pf : n1 = n2) (c1 : arityCode n1) : arityCode n2.
exact (eq_rect n1 arityCode c1 n2 pf).
Qed.
Lemma coerceVec {A : Type} {n1 n2 : nat} (pf : n1 = n2) (c1 : Vector.t A n1) : Vector.t A n2.
exact (eq_rect n1 (Vector.t A) c1 n2 pf).
Qed.
(* this is the tricky bit *)
Fixpoint eq {h_or_z : hz} (ty1 ty2 : t h_or_z) : bool :=
match ty1, ty2 with
| Leaf c1, Leaf c2 => codeEq c1 c2
| Cursor ty1, Cursor ty2 => eq ty1 ty2
| InternalH n1 c1 ty1, InternalH n2 c2 ty2 =>
match eq_nat_dec n1 n2 with
| right _neqPrf => false
| left eqPrf =>
let c1' := coerceArity eqPrf c1 in
let ty1' := coerceVec eqPrf ty1 in
codeEq c1' c2 (* && Vector.eqb _ eq ty1' ty2 *)
end
| InternalZ n1 c1 v1 (l1, f1), InternalZ n2 c2 v2 (l2, f2) =>
match eq_nat_dec n1 n2 with
| right _neqPrf => false
| left eqPrf =>
let eqPrf' := f_equal S eqPrf in
let c1' := coerceArity eqPrf' c1 in
let v1' := coerceVec eqPrf v1 in
codeEq c1' c2 (* && Vector.eqb _ eq v1' v2 *) && Fin.eqb l1 l2 && eq f1 f2
end
| _, _ => false
end.
End Typ.
【问题讨论】：
-
标准库中有
Vector.cast，与coerceVec基本相同。
标签： coq