Coq`path` 구현

Question

다음은 최대 Coq equality implementation입니다 (이 질문은 자체 포함되어 있음).

고정 된 수의 자식이있는 고정 된 태그 집합 (arityCode)을 가진 간단한 유도 형 나무 (t)가 있습니다. 트리 형태의 경로 (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

당신은이에 적용되는 t 값의 형태에 어떤 제약이없는 Here위한 스마트 생성자 정의 할 수 있습니다 :

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