Блог

Я создал следующие индуктивные типы данных и рекурсивные функции.

 Require Coq.Lists.List.

Inductive PairTree : Type :=
| PTLeaf : PairTree
| PTBranch : (nat*nat) -> PairTree -> PairTree -> PairTree.

Fixpoint smush (r m : list nat) : list nat :=
  match m with
    | nil => r
    | h :: t => smush (h :: r) t
  end.
  

Я определил следующую функцию, используя их, со вспомогательным параметром «gas», чтобы правила завершения Coq легко выполнялись.

 Fixpoint fueled_prefix_part (gas : nat) (r m : list nat) : PairTree :=
  match gas with
    | 0 => PTLeaf
    | S gas' =>
      match r with
        | nil => PTLeaf
        | f :: fs =>
          match fs with
            | nil => PTLeaf
            | f' :: fs' =>
              PTBranch (f, f')
                       (fueled_prefix_part gas' (smush fs' m) nil)
                       (fueled_prefix_part gas' (f :: fs') (f' :: m))
          end
      end
  end.
  

Тем не менее, я хотел извлечь фактический код из этого и запустить его. Таким образом, вместо структурной рекурсии в gas я мог бы получить более приятный извлеченный код, если бы вместо этого я мог использовать следующий код, поскольку тогда я мог бы использовать какой-либо другой nat-подобный тип данных с < (например, целые числа Haskell).

 Require Import Recdef.
Require Export Coq.omega.Omega.
Require Export Coq.Lists.List.

(* Insert definitions of PairTree and smush here. *)

Function fpp' (gas: nat) (r m: list nat) {measure (fun x => x) gas}: PairTree :=
  match 0 <? gas with
    | false => PTLeaf
    | true =>
      match r with
        | nil => PTLeaf
        | f :: fs =>
          match fs with
            | nil => PTLeaf
            | f' :: fs' =>
              let gas' := gas - 1 in
              PTBranch (f, f')
                       (fpp' gas' (smush fs' m) nil)
                       (fpp' gas' (f :: fs') (f' :: m))
          end
      end
  end.
  

Конечно, мы не можем на этом закончить; мы должны доказать, что это заканчивается. Следующее, по-видимому, доказывает завершение…

 Proof.
  intro gas. destruct gas; intros _ _ teq _ _ _ _ _ _.
  inversion teq.
  omega.
  intro gas. destruct gas; intros _ _ teq _ _ _ _ _ _.
  inversion teq.
  omega.
  

На данный момент в ProofGeneral я не вижу целей на экране цели, а на экране ответа я вижу сообщение

 No more subgoals.
(dependent evars:)
  

Итак, я ввожу

 Defined.
  

и получите сообщение об ошибке

 Toplevel input, characters 0-8:
Error: Attempt to save a proof with shelved goals (in proof fpp'_terminate)
  

Что, черт возьми, происходит? Если я наберу

 Unshelve.
Defined.
  

Я получаю ту же ошибку.