Ошибка программы Fixpoint с Admit Obligations и вложенной рекурсией - PullRequest
Новая
       11

Ошибка программы Fixpoint с Admit Obligations и вложенной рекурсией

0 голосов
/ 17 декабря 2018

Я пытался определить функцию, используя 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.

IВозможно, я могу определить это по-другому, но мне все еще интересно, почему это происходит.

1 Ответ

0 голосов
/ 17 декабря 2018

Читая сообщение об ошибке далее, обратите внимание, что 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.
...