logo标签列表

Coq的相等性实现

coq
7
我正在编写一种玩具语言，其中AST中的节点可以有任意数量的子节点（Num没有，Arrow有2个等）。您可以将这些称为运算符。此外，AST中恰好有一个节点可能是“聚焦”的。如果数据类型具有焦点，则使用Z索引，否则使用H索引。
我需要关于代码的一些建议。希望一次性询问所有相关问题是否没问题。

  1. 如何定义只有一个焦点的内部节点类型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。虽然我知道我不想处理那个加法。

  2. 完善类型：在eq的两种有趣情况中，我都要比较两个n(孩子数量)。如果它们相同，我应该能够将arityCodes和Vector.ts "强制转换"为相同的类型。现在我用了两个引理来解决这个问题。我应该怎么做才能得到正确的结果？似乎Adam Chlipala的"convoy pattern"可以帮助，但我没有搞清楚怎么做。

  3. 如果我取消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.
1
标准库中有Vector.cast，它本质上与coerceVec相同。 - Anton Trunov
1个回答
6

让我们从第三个问题开始。 Vector.eqb 在其第一个参数上执行嵌套递归调用。为了使Coq相信这些是递减的，我们需要使coerceVec的定义透明化，即用Defined替换Qed：

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.

这里，“路径树”表示对树“tree”的索引类型。

在Coq社区中，通常会就何时以及如何使用依赖类型产生分歧。在这种情况下，我认为更容易使用原始语法树的类型t和非依赖类型path的路径类型。您可以定义表达与树相关联的路径的良好形式的谓词，并且事实上证明您关心的函数符合该良好形式的概念。在这种情况下，我发现这更加灵活，因为您不必担心在函数中操作类型索引并推理它们（要了解这意味着什么，请尝试陈述原始Typ.eq函数的正确性定理）。

我认为，不仅是“分歧”，不同的人确实偏爱非常不同的风格。每种风格都有一些特定的优点和特色，现在像精益这样的新工具正在创造新的风格。当然，拥有某种风格词典将有助于人们了解每种风格的好坏与丑陋之处，这将是很酷的事情。 - ejgallego
@Joel Burget 您根本不需要 coerceVec -- 您完全可以完全摆脱长度强制转换，因为 Vector.eqb 具有类型 forall A: Type，（A-> A-> bool）-> forall m n：nat，VectorDef.t A m -> VectorDef.t A n -> bool，因此它不关心向量是否具有相同的长度。评估结果仍然是相同的。 - Anton Trunov
网页内容由stack overflow 提供, 点击上面的
可以查看英文原文，
原文链接