Coq平等实施 [英] Coq equality implementation

问题描述

我正在写一种玩具语言，其中AST中的节点可以有任意数量的子代（ Num 的值为0， Arrow 有2，依此类推）。您可以致电这些运营商。此外，AST中的一个节点可能被聚焦。如果数据类型具有焦点，则使用 Z 为数据类型建立索引，如果没有焦点，则使用 H 为数据类型建立索引。

I'm writing a toy language where nodes in the AST can have any number of children (Num has 0, Arrow has 2, etc). You might call these operators. Additionally, exactly one node in the AST might be "focused". We index the data type with Z if it has a focus, or H if it doesn't.

我需要一些代码建议。希望可以一​​次询问所有这些，因为它们都是相关的。

I need advice on a few parts of the code. Hopefully it's alright to ask all of these at once, since they're related.

1. 您将如何定义内部类型一个焦点， InternalZ 的节点？现在我说：我们有 S n 个孩子-其中 n 个孩子没有重点关注，有一个（在给定的索引下） InternalZ：forall nm，arityCode（n + 1 + m）-> Vector.t（t H）n->更直观的选择（看起来像拉链）。 ; t Z-> Vector.t（t H）m-> t Z 。我知道我不想处理这种加法。

1. How would you define the type of internal nodes with one focus, InternalZ? Right now I say "we have S n children -- n of them are unfocused and one (at some given index) is focused. A slightly more intuitive option (which looks zipper-like) would be InternalZ : forall n m, arityCode (n + 1 + m) -> Vector.t (t H) n -> t Z -> Vector.t (t H) m -> t Z. I know I don't want to deal with that addition, though.

修饰类型：在两种有趣的情况下，在 eq 中，我比较两个 n s（孩子的数量）。如果它们相同，我应该能够强迫 arityCode s和 Vector.t s具有相同的类型，现在我用两个引理砍掉了它，应该如何正确执行呢？好像亚当·克利帕拉（Adam Chlipala）的车队模式 可能有帮助，但我无法解决。

Refining types: In both interesting cases in eq I compare the two ns (number of children). If they're the same, I should be able to "coerce" the arityCodes and Vector.ts to have the same type. Right now I hacked this with two lemmas. How should I do this properly? It seems like Adam Chlipala's "convoy pattern" might help but I couldn't work out how.

如果我取消任何 Vector.eqb 调用的注释，则Coq会抱怨无法猜测减少修正的论点。。我了解此错误，但不确定如何解决。首先想到的是，我可能必须按 t 的子项深度对其进行索引。

If I uncomment either of the Vector.eqb calls, Coq complains "Cannot guess decreasing argument of fix.". I understand the error but I'm not sure how to circumvent it. The first thing that comes to mind is that I might have to index t by its depth of children.

我的代码：

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.eqb 在其第一个参数上执行嵌套的递归调用。为了使Coq确信这些数量正在减少，我们需要通过将 Qed 替换为<$，使 coerceVec 的定义透明化c $ c>已定义：

Let's start with your third question. Vector.eqb performs nested recursive calls on its first argument. To convince Coq that these are decreasing, we need to make the definition of coerceVec transparent, by replacing 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 做的。但是，在这种特殊情况下，更容易避免使用具有不同索引的元素的强制转换和编写比较函数：

As for your second question: in general, you do need to implement cast operations with equality proofs, like you did with coerceVec. In this particular case, however, it is easier to avoid the cast and write comparison functions that take elements with different indices:

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.

问题中最困难，最开放的是第一个。我认为对类型进行建模的最简单方法是将其分为两类：一种是原始语法树，另一种是由树索引的路径。例如：

The hardest and most open-ended of your questions is the first one. I think the easiest way to model your type would be by splitting it in two: a type of raw syntax trees, and a type of paths indexed by trees. For example:

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 represents the type of indices into a tree tree.

在Coq社区中，关于如何以及何时使用依赖类型常常存在分歧。 。在这种特殊情况下，我认为具有原始语法树的类型 t 和非依赖类型的 path 进入树的路径。您可以定义表示相对于树的路径的格式正确性的谓词，并在您关心的功能尊重格式正确性这一事实之后证明。我发现这种方法更加灵活，因为您不必担心在函数中操作类型索引并对其进行推理（要了解这意味着什么，请尝试为原始声明正确性定理。 Typ.eq 函数）。

There is often disagreement in the Coq community about how and when to use dependent types. In this particular case, I think it would be easier to have a type t of raw syntax trees and a non-dependent type path of paths into a tree. You can define predicates that express the well-formedness of a path with respect to a tree, and prove after the fact that the functions you care about respect that notion of well-formedness. I find this more flexible in this case because you don't have to worry about manipulating type indices in your functions and reasoning about them (to understand what this means, try to state a the correctness theorem for the original Typ.eq function).

这篇关于Coq平等实施的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！