Coq `path`实现

Question

这是Coq equality implementation的后续问题(尽管这个问题是自包含的)。

我有一个简单归纳类型的树(t)，它有一组固定的标签(arityCode)，每个标签都有固定数量的子树。我有一种类型(path)的路径到树中。我正在尝试实现一些操作。特别是，我希望能够在几个方向上移动光标。这看起来很简单，但我遇到了一个障碍。

这些都在代码中，但我要快速解释一下我遇到的问题:要构造一个there路径，我需要生成一个path (Vector.nth v i) (其中一个子节点中的路径)。但是唯一的path构造函数(here和there)会产生一个path (Node c v)。因此，在某种意义上，我需要向编译器展示一条路径同时具有类型path (Node c v)和path (Vector.nth v i)，但是Coq还不够聪明，不足以计算(Vector.nth children fin_n) -> Node c v。我怎么才能让它相信这是可以的呢？

Require Coq.Bool.Bool. Open Scope bool.
Require Coq.Strings.String. Open Scope string_scope.
Require Coq.Arith.EqNat.
Require Coq.Arith.PeanoNat. Open Scope nat_scope.
Require Coq.Arith.Peano_dec.
Require Coq.Lists.List. Open Scope list_scope.
Require Coq.Vectors.Vector. Open Scope vector_scope.
Require Fin.

Module Export LocalVectorNotations.
Notation " [ ] " := (Vector.nil _) (format "[ ]") : vector_scope.
Notation " [ x ; .. ; y ] " := (Vector.cons _ x _ .. (Vector.cons _ y _ (Vector.nil _)) ..) : vector_scope.
Notation " [ x ; y ; .. ; z ] " := (Vector.cons _ x _ (Vector.cons _ y _ .. (Vector.cons _ z _ (Vector.nil _)) ..)) : vector_scope.
End LocalVectorNotations.

Module Core.

    Module Typ.
      Set Implicit Arguments.

      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 : 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).

      Example node1 := Node Num [].
      Example children : Vector.t t 2 := [node1; Node Hole []].
      Example node2 := Node Arrow children.

      (* This example can also be typed simply as `path node`, but we type it this way
         to use it as a subath in the next example.
       *)
      Example here  : path (*node1*) (Vector.nth children Fin.F1) := Here _ _.
      Example there : path node2 := There _ children Fin.F1 here.

      Inductive direction : Type :=
      | Child : nat -> direction
      | PrevSibling : direction
      | NextSibling : direction
      | Parent : direction.

      Fixpoint move_in_path
               (node : t)
               (dir : direction)
               (the_path : path node)
        : option (path node) :=
        match node with
        | @Node num_children code children =>
          match the_path with
          | There _ _ i sub_path => move_in_path (Vector.nth children i) dir sub_path
          | Here _ _ =>
            match dir with
            | Child n =>
              match Fin.of_nat n num_children with
              | inleft fin_n =>
                  (* The problem:

                      The term "Here ?a@{n0:=n; n:=n0} ?t@{n0:=n; n:=n0}" has type
                      "path (Node ?a@{n0:=n; n:=n0} ?t@{n0:=n; n:=n0})" while it is expected to have type
                      "path (Vector.nth children fin_n)".

                      How can I convince Coq that `Vector.nth children fin_n`
                      has type `path (Node a t)`?
                    *)
                  let here : path (Vector.nth children fin_n) := Here _ _ in
                  let there : path node := There _ children fin_n here in
                    Some there
              | inright _ => None
              end
            | _ => None (* TODO handle other directions *)
            end
          end
        end.

    End Typ.
End Core.

Answer 1

您可以为Here定义一个智能构造函数，该构造函数对应用它的t值的形状没有任何约束：

 Definition Here' (v : t) : path v := match v return path v with
   | Node c vs => Here c vs
 end.

然后，您可以编写：

let here : path (Vector.nth children fin_n) := Here' _ in