Coq `Pfad` Implementierung

Question

Dies ist eine Folge bis Coq equality implementation (obwohl diese Frage in sich abgeschlossen ist).

Ich habe eine einfache induktive Art von Bäumen (t) mit einem festen Satz von Tags (arityCode), jeweils mit einer festen Anzahl von Kindern. Ich habe einen Typ (path) von Pfaden in einen Baum. Ich versuche einige Manipulationen zu implementieren. Insbesondere möchte ich einen Cursor in ein paar Richtungen bewegen können. Das scheint ziemlich einfach zu sein, aber ich stoße in eine Straßensperre.

Das ist alles im Code, aber eine kurze Erklärung, wo ich stecke: Um einen there Pfad zu erstellen, muss ich eine path (Vector.nth v i) (ein Pfad in einem der Kinder) produzieren. Aber die einzigen path Konstruktoren (here und there) produzieren eine path (Node c v). In gewisser Weise muss ich dem Compiler zeigen, dass ein Pfad gleichzeitig den Typ path (Node c v) und path (Vector.nth v i) hat, aber Coq ist nicht clever genug, um (Vector.nth children fin_n) ->Node c v zu berechnen. Wie kann ich davon überzeugen, dass das in Ordnung ist?

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

Sie könnten einen Smart-Konstruktor für Here definieren, die auf die Form des t Wert wird es keine Einschränkung hat angewendet:

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

Anschließend können Sie schreiben:

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