Определение параметризованной фиксированной точки в Coq - PullRequest
Новая
       10

Определение параметризованной фиксированной точки в Coq

0 голосов
/ 22 ноября 2018

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

Я свернул определение доэто: 

Require Import Coq.Init.Notations.
Require Import Coq.Init.Datatypes.

Inductive Wrapper (T : Type) :=
  | Wrap : T -> Wrapper T
  .
Inductive Unwrapper :=
  | Empty : Unwrapper
  | Unwrap : Wrapper Unwrapper -> Unwrapper
  .

Fixpoint Unwrapper_size (u : Unwrapper) {struct u} : nat :=
  match u with
  | Empty => O
  | Unwrap w => Wrapper_size w
  end

with Wrapper_size (w : Wrapper Unwrapper) {struct w} : nat :=
  match w with
  | Wrap _ t => Unwrapper_size t
  end.

, что приводит к этой ошибке: 

Recursive definition of Wrapper_size is ill-formed.
In environment
Unwrapper_size : Unwrapper -> nat
Wrapper_size : Wrapper Unwrapper -> nat
w : Wrapper Unwrapper
t : Unwrapper
Recursive call to Unwrapper_size has principal argument equal to
"t" instead of a subterm of "w".
Recursive definition is:
"fun w : Wrapper Unwrapper =>
match w with
| Wrap _ t => Unwrapper_size t
end".

Здесь, t, очевидно, является подтермой w - w, с которым мы сопоставляемчтобы получить t, но Кок не принимает это.В чем здесь ошибка, и как я могу ее обойти?

1 Ответ

0 голосов
/ 23 ноября 2018

Предположим, вы используете Wrapper также для других аргументов.Затем вам нужно разорвать взаимную рекурсию и сделать функции «параллельными» типу данных.Итак, вы хотите написать Wrapper_size: Wrapper T -> (T -> nat) -> nat.

Затем вы можете использовать Wrapper_size Unwrapper_size в Unwrapper_size: Coq должен сделать достаточно встраивания при проверке завершения, чтобы признать, что это безопасно.

В этом примеретакже легко сделать это вручную: Unwrapper_size будет соответствовать Unwrap (Wrap _ t) и рекурсивно t.

...