让我们从你的第三个问题开始。Vector.eqb
对其第一个参数执行嵌套递归调用。为了让 Coq 相信这些正在减少,我们需要定义coerceVec
透明,通过替换Qed
with Defined
:
Require Coq.Arith.EqNat.
Require Coq.Structures.Equalities.
Require Coq.Arith.Peano_dec.
Require Fin.
Require Vector.
Set Implicit Arguments.
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.
Inductive arityCode : nat -> Type :=
| Num : arityCode 0
| Hole : arityCode 0
| 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.
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
.
Lemma coerceArity (n1 n2 : nat) (pf : n1 = n2) (c1 : arityCode n1) : arityCode n2.
exact (eq_rect n1 arityCode c1 n2 pf).
Defined.
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).
Defined.
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.
至于你的第二个问题:一般来说,你确实需要使用相等证明来实现强制转换操作,就像你所做的那样coerceVec
。然而,在这种特殊情况下,更容易避免使用具有不同索引的元素的强制转换和编写比较函数:
Require Coq.Arith.EqNat.
Require Coq.Structures.Equalities.
Require Coq.Arith.Peano_dec.
Require Fin.
Require Vector.
Set Implicit Arguments.
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.
Inductive arityCode : nat -> Type :=
| Num : arityCode 0
| Hole : arityCode 0
| Arrow : arityCode 2
| Sum : arityCode 2
.
Definition codeEq (n1 n2 : nat) (l : arityCode n1) (r : arityCode n2) : bool :=
match l, r with
| Num, Num => true
| Hole, Hole => true
| Arrow, Arrow => true
| Sum, Sum => true
| _, _ => false
end.
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
.
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 =>
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 =>
codeEq c1 c2 && Vector.eqb _ eq v1 v2 && Fin.eqb l1 l2 && eq f1 f2
end
| _, _ => false
end.
End Typ.
你的问题中最难、最开放的就是第一个问题。我认为对类型进行建模的最简单方法是将其分为两部分:一种原始语法树类型和一种由树索引的路径类型。例如:
Require Fin.
Require Vector.
Set Implicit Arguments.
Module Typ.
Inductive arityCode : nat -> Type :=
| Num : arityCode 0
| Hole : arityCode 0
| Arrow : arityCode 2
| Sum : arityCode 2
.
Inductive t : Type :=
| Node : forall n, arityCode n -> Vector.t t n -> t.
Inductive path : t -> Type :=
| Here : forall n (c : arityCode n) (v : Vector.t t n), path (Node c v)
| There : forall n (c : arityCode n) (v : Vector.t t n) (i : Fin.t n),
path (Vector.nth v i) -> path (Node c v).
End Typ.
Here, path tree
表示树中索引的类型tree
.
Coq 社区对于如何以及何时使用依赖类型经常存在分歧。在这种特殊情况下,我认为有一个类型会更容易t
原始语法树和非依赖类型path
成树的路径。您可以定义表示相对于树的路径的格式良好的谓词,并在事后证明您关心的函数尊重格式良好的概念。我发现在这种情况下这更灵活,因为您不必担心在函数中操作类型索引并推理它们(要理解这意味着什么,请尝试陈述原始的正确性定理Typ.eq
功能)。