Определение рекурсивной функции в coq с ограничением на множество возможных входов - PullRequest
Новая
       3

Определение рекурсивной функции в coq с ограничением на множество возможных входов

1 голос
/ 05 июля 2011

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

Использование меры (inpspacesize - (length l)) в основном работает, но я застрял в одном случае. Кажется, мне не хватает информации о том, что предыдущие слои l были построены правильно, т.е. е. дубликатов нет, и все записи действительно из пространства ввода.

Теперь я ищу замену списка, которая делает то, что мне нужно.

Редактировать Я уменьшил это до следующего:

У меня на nat меньше заданного max, и я должен убедиться, что функция вызывается не более одного раза для каждого числа. Я придумал следующее: 

(* the condition imposed *)
Inductive limited_unique_list (max : nat) : list nat -> Prop :=
  | LUNil  : limited_unique_list max nil
  | LUCons : forall x xs, limited_unique_list max xs
             -> x <= max
             -> ~ (In x xs)
             -> limited_unique_list max (x :: xs).

(* same as function *)
Fixpoint is_lulist (max : nat) (xs0 : list nat) : bool :=
  match xs0 with
  | nil     => true
  | (x::xs) => if (existsb (beq_nat x) xs) || negb (leb x max)
                 then false
                 else is_lulist max xs
  end.

(* really equivalent *)
Theorem is_lulist_iff_limited_unique_list : forall (max:nat) (xs0 : list nat),
    true = is_lulist max xs0 <-> limited_unique_list max xs0.
Proof. ... Qed.

(* used in the recursive function's step *)
Definition lucons {max : nat} (x : nat) (xs : list nat) : option (list nat) :=
  if is_lulist max (x::xs)
    then Some (x :: xs)
    else None.

(* equivalent to constructor *)
Theorem lucons_iff_LUCons : forall max x xs, limited_unique_list max xs ->
    (@lucons max x xs = Some (x :: xs) <-> limited_unique_list max (x::xs)).
Proof. ... Qed.

(* unfolding one step *)
Theorem lucons_step : forall max x xs v, @lucons max x xs = v ->
  (v = Some (x :: xs) /\ x <= max /\ ~ (In x xs)) \/ (v = None).
Proof. ... Qed.

(* upper limit *)
Theorem lucons_toobig : forall max x xs, max < x
    -> ~ limited_unique_list max (x::xs).
Proof. ... Qed.

(* for induction: increasing max is ok *)
Theorem limited_unique_list_increasemax : forall max xs,
  limited_unique_list max xs -> limited_unique_list (S max) xs.
Proof. ... Qed.

Я застреваю, когда пытаюсь убедительно доказать, что не могу вставить элемент в полный список (либо IH выходит из строя, либо я не могу найти нужную мне информацию). Поскольку я считаю, что эта не-вставляемость имеет решающее значение для отображения завершения, я до сих пор не нашел рабочего решения.

Любые предложения о том, как доказать это по-другому, или о реструктуризации выше?

1 Ответ

1 голос
/ 05 июля 2011

Трудно сказать много без подробностей (уточните!), Но:

  • Используете ли вы команду Program ? Это, безусловно, очень полезно для определения функций с помощью нетривиальных мер.
  • Для уникальности это не сработает, если вы попробуете сеты? Я помню, как писал функцию, которая звучит очень похоже на то, что вы говорите: у меня была функция, для которой аргумент содержал набор элементов. Этот набор предметов монотонно рос и ограничивался ограниченным пространством предметов, что давало аргумент завершения.
...