Блог

Главная - Вопросы по программированию - Избегайте того, чтобы неявные аргументы Fixpoint становились явными в режиме проверки

Избегайте того, чтобы неявные аргументы Fixpoint становились явными в режиме проверки

#coq

#coq

Вопрос:

Есть ли способ заставить неявные аргументы Fixpoint оставаться неявными в режиме проверки?

Пример:

 Fixpoint foo {a : Set} (l : list a) : nat :=
  match l with
  | nil => 1
  | _ :: xs => ltac:(exact (1   foo _ xs))
                                   ^^^  
end.

Но я хотел бы написать

 Fixpoint foo {a : Set} (l : list a) : nat :=
  match l with
  | nil => 1
  | _ :: xs => ltac:(exact (1   foo xs))
  end.

Комментарии:

1. Я испытываю искушение сказать «нет», но меня не удивило бы, если бы ни у кого раньше не было этой проблемы. Вероятно, вам лучше опубликовать проблему на GitHub ( github.com/coq/coq/issues ).

2. Кто-то, похоже, спрашивал об этом раньше. Он был закрыт как wontfix. Причина, указанная для этого сбоя, заключается в том, что «локальные определения не содержат никакой информации об их аргументах», и не ожидалось, что это когда-либо изменится.

3. @HTNW Ваш комментарий выглядит как ответ для меня 🙂

Ответ №1:

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

 From Coq Require Import List.
Import ListNotations.

Section Foo.

  Context {a : Set}.

  Fixpoint foo (l : list a) : nat :=
    match l with
    | nil => 1
    | _ :: xs => ltac:(exact (1   foo xs))
    end.

End Foo.

Обратите внимание, что это эквивалентно (в том смысле, что оно создает то же определение), что и:

 Definition foo' {a : Set} :=
  fix foo' (l : list a) : nat :=
    match l with
    | nil => 1
    | _ :: xs => ltac:(exact (1   foo' xs))
    end.

Здесь трюк более явный, вы принимаете аргумент a : Set перед выполнением операции с фиксированной точкой.

Конечно, это работает только тогда, когда рассматриваемый неявный аргумент является единообразным в определении.