Coq平等实施

Question

我正在写一种玩具语言,其中AST中的节点可以有任意数量的子节点(Num有0,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我比较两个ns(孩子的数量).如果它们是相同的,我应该能够"强制" arityCodes和Vector.ts具有相同的类型.现在我用两个引理来攻击这个.我该怎么做呢？似乎Adam Chlipala的"护航模式"可能有所帮助,但我无法弄清楚如何.

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.

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功能).