Coq 等式实现

Question

我正在编写一种玩具语言，其中 AST 中的节点可以有任意数量的子节点(Num 有 0，Arrow 有 2，等等)。您可以调用这些运算符。此外，AST 中可能只有一个节点是“聚焦的”。我们用 Z 索引数据类型如果它有焦点，或者 H如果没有。

我需要关于代码的几个部分的建议。希望一次问所有这些没问题，因为它们是相关的。

您将如何定义一个焦点的内部节点类型，InternalZ ?现在我说“我们有 S n 个 child -- n 其中一个是未聚焦的，一个(在某个给定的索引处)是聚焦的。一个稍微更直观的选项(看起来像 zipper )是 InternalZ : forall n m, arityCode (n + 1 + m) -> Vector.t (t H) n -> t Z -> Vector.t (t H) m -> t Z 。我我知道我不想处理这个添加，不过。

精炼类型:在 eq 中的两个有趣案例中我比较两者 n s( child 的数量)。如果它们相同，我应该能够“强制”arityCode s 和 Vector.t s 具有相同的类型。现在我用两个引理来破解它。我应该如何正确地做到这一点？好像是 Adam Chlipala 的 "convoy pattern"可能有帮助，但我不知道怎么做。

如果我取消注释 Vector.eqb调用，Coq 提示“无法猜测修复的减少参数。”。我理解这个错误，但我不知道如何规避它。我首先想到的是我可能必须索引 t由其深度的 child 。

我的代码:

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.

Answer 1

让我们从你的第三个问题开始。 Vector.eqb对其第一个参数执行嵌套递归调用。为了让 Coq 相信这些都在减少，我们需要定义 coerceVec透明，通过替换 Qed与 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.

在这里， path tree表示成树的索引类型 tree .

Coq 社区中经常对如何以及何时使用依赖类型存在分歧。在这种特殊情况下，我认为使用类型 t 会更容易。原始语法树和非依赖类型 path成一棵树的路径。您可以定义表示路径相对于树的良构性的谓词，并在事后证明您关心的函数尊重良构性的概念。我发现在这种情况下这更灵活，因为您不必担心在函数中操作类型索引并对其进行推理(要理解这意味着什么，请尝试陈述原始 Typ.eq 函数的正确性定理)。