程序fixpoint误差带有接纳义务和嵌套递归

Question

i试图使用Program Fixpoint定义一个函数，该函数在其体内使用另一个（匿名）递归函数。我目前尝试使用Admit Obligations，以查看其他问题是否有意义，但我遇到了错误。

这是一个简单的示例，显示相同的错误（也许有一个简单的错误...）。

Require Import List.
Import ListNotations.
Require Import Program.
Section Test.
  Inductive FType : Type :=
  | Base : RType -> FType
  | Cons : RType -> FType -> FType
  with RType : Type :=
  | Empty : RType  
  | Nested : nat -> FType -> RType
  | NestedList : nat -> list FType -> RType.

  Variable ftype_size : FType -> nat.

  Program Fixpoint failing (ft : FType) {measure (ftype_size ft)} : FType :=
    match ft with
    | Base _ => ft
    | Cons hd tl =>
      match hd with
      | NestedList l rs =>
        let fix loop (rs : list FType) (i : nat) : list FType :=
            match rs with
            | [] => []
            | r' :: rs' => (failing r') :: (loop rs' (i + 1))
            end
        in
        Base (NestedList l (loop rs 0))                                  
      | _ => ft
      end
    end.
  Admit Obligations.
End Test.

所以，运行此操作时，请说Recursive call to loop has not enough arguments.。我想知道为什么会发生这种情况？它与此问题有点相关吗？

另外，如果我定义了索引映射并重复此图，则没有任何错误。

 Section Map.
        Variables (T1 T2 : Type) (f : nat -> T1 -> T2).
Definition indexed_map (s : list T1) :=
  let fix imap s index : list T2 :=
      match s with
      | [] => []
      | hd :: tl =>  (f index hd) :: imap tl (index + 1)
      end
  in
  imap s 0.
  End Map.
  Arguments indexed_map [T1 T2].
  Program Fixpoint failing (ft : FType) {measure (ftype_size ft)} : FType :=
    match ft with
    | Base _ => ft
    | Cons hd tl =>
      match hd with
      | NestedList l rs => Base (NestedList l (indexed_map (fun i r' => (failing r')) rs))                             
      | _ => ft
      end
    end.
  Admit Obligations.

我可能可以以不同的方式定义它，但是我仍然想知道为什么会发生这种情况。

Answer 1

进一步阅读错误消息，请注意loop在打印功能中发生两次。第二个事件是您写的，但第一个（有问题的）是Admit Obligations生成的公理的参数。

Recursive call to loop has not enough arguments.
Recursive definition is:
"fun (rs0 : list FType) (i : nat) =>
 let program_branch_0 := fun _ : [] = rs0 => [] in
 let program_branch_1 :=
   fun (r' : FType) (rs' : list FType) (Heq_rs : r' :: rs' = rs0) =>
   failing r'
     (failing_obligation_1 ft failing hd tl Heq_ft l rs Heq_hd loop
        rs0 i r' rs' Heq_rs) :: loop rs' (i + 1) in
 match rs0 as rs' return (rs' = rs0 -> list FType) with
 | [] => program_branch_0
 | r' :: rs' => program_branch_1 r' rs'
 end eq_refl".

为了避免这种情况，您可以手动跨越相应的义务，并将自己的公理不依赖于loop。

Parameter TODO : forall {A : Prop}, A.
Program Fixpoint failing ... (* Your definition *)
Next Obligation.
  apply TODO.
Qed.
(* Now the rest can still be Admitted. *)
Admit Obligations.