Определение путем минимизации в Coq

Предположим, что P: nat -> T -> Prop — это утверждение, что для любого заданного t: T

  • либо существует k: nat такое, что P выполняется для всех чисел, больших или равных k, и ни для одного числа меньше k.
  • или P k t ложно для всех k : nat.

Я хочу определить min_k : T -> nat + undef как минимальное число k такое, что P k t выполняется, и undef в противном случае.

Это вообще возможно? Я попытался определить что-то вроде

Definition halts (t : T) := exists k : nat, P k t.

Или, может быть

Definition halts (t : T) := exists! k : nat, (~ P k t /\ P (S k) t).

а затем используйте его как

Definition min_k (t : T) := match halts T with
  | True => ??
  | False => undef
end.

но я не знаю, как пойти дальше оттуда.

Любые идеи поощряются.

Стоит ли изучать PHP в 2023-2024 годах?
Стоит ли изучать PHP в 2023-2024 годах?
Привет всем, сегодня я хочу высказать свои соображения по поводу вопроса, который я уже много раз получал в своем сообществе: "Стоит ли изучать PHP в...
Поведение ключевого слова "this" в стрелочной функции в сравнении с нормальной функцией
Поведение ключевого слова "this" в стрелочной функции в сравнении с нормальной функцией
В JavaScript одним из самых запутанных понятий является поведение ключевого слова "this" в стрелочной и обычной функциях.
Приемы CSS-макетирования - floats и Flexbox
Приемы CSS-макетирования - floats и Flexbox
Здравствуйте, друзья-студенты! Готовы совершенствовать свои навыки веб-дизайна? Сегодня в нашем путешествии мы рассмотрим приемы CSS-верстки - в...
Тестирование функциональных ngrx-эффектов в Angular 16 с помощью Jest
В системе управления состояниями ngrx, совместимой с Angular 16, появились функциональные эффекты. Это здорово и делает код определенно легче для...
Концепция локализации и ее применение в приложениях React ⚡️
Концепция локализации и ее применение в приложениях React ⚡️
Локализация - это процесс адаптации приложения к различным языкам и культурным требованиям. Это позволяет пользователям получить опыт, соответствующий...
Пользовательский скаляр GraphQL
Пользовательский скаляр GraphQL
Листовые узлы системы типов GraphQL называются скалярами. Достигнув скалярного типа, невозможно спуститься дальше по иерархии типов. Скалярный тип...
1
0
66
2
Перейти к ответу Данный вопрос помечен как решенный

Ответы 2

Ответ принят как подходящий

Вы не можете match на Prop. Если вы хотите провести анализ случая, вам нужно что-то в Type, обычно bool или что-то вроде sumbool или sumor. Другими словами, вы можете делать все, что хотите, пока у вас есть достаточно сильная гипотеза.

Variable T : Type.
Variable P : nat -> T -> Prop.

Hypothesis PProperty : forall (t : T),
  {k : nat | forall n, (k <= n -> P n t) /\ (n < k -> ~ P n t)}
  +
  {forall k, ~ P k t}.

Definition min_k (t : T) : option nat :=
  match PProperty t with
  | inleft kH => Some (proj1_sig kH)
  | inright _ => None
  end.

Важно отметить, что это не сработало бы, если бы PProperty было дизъюнктом Prop, то есть если бы оно имело форму _ / _, а не форму _ + { _ }.

Кстати, идиоматический способ описания foo + undef в Coq заключается в использовании option foo, что я и сделал выше, но вы можете адаптировать его по своему усмотрению.

Спасибо за ваш ответ. Могу ли я попросить ссылку, чтобы узнать больше о proj1_sig?

Kamyar Mirzavaziri 06.11.2022 09:46

Я думаю, что эту гипотезу можно упростить с помощью тривиальной гипотезы, которая верна для любого P в классической логике. Hypothesis PProperty : forall (t : T), {k : nat | (P k t) /\ forall n, (n < k -> ~ P n t)} + {forall k, ~ P k t}.

Kamyar Mirzavaziri 06.11.2022 10:42

В общем, если вы не знаете, что что-то делает, вы можете Check proj1_sig увидеть его тип, Print proj1_sig увидеть его определение или даже Locate proj1_sig узнать, где оно определено. Последнее полезно, чтобы увидеть, есть ли полезные комментарии в коде рядом с определением. В данном случае есть: мы видим, что proj1_sig — это первая проекция sig, которая является Type версией exists _, _. Итак, proj1_sig kH дает вам k, для которого выполняется свойство.

Ana Borges 06.11.2022 15:58

Это зависит от того, что вы подразумеваете под «классической логикой». Обычно я бы сказал, что это означает «Coq + forall P : Prop, P / ~ P». Обратите внимание, что это слабее, чем forall P : Prop, {P} + {~ P}, что, как я считаю, вам нужно принять, чтобы получить PProperty. Вы все еще можете работать с более сильным предположением, но помните, какие аксиомы вы используете.

Ana Borges 06.11.2022 16:07

В дополнение к отличному ответу Аны, я думаю, стоит отметить, что option nat по сути то же самое, что и {k : nat | ...} + {forall k, ~ P k t}, если стереть доказательства последнего типа: в первом случае (Some или inleft) вы получите натуральное число; во втором (None или inright) вы вообще ничего не получаете.

Ух ты. Я не смотрел на это таким образом! Спасибо, что указали на этот момент. Но я изо всех сил пытаюсь понять, что значит быть одним и тем же. Я думаю, что ... в левой части должно быть правдой, если мы хотим, чтобы это было все nat?

Kamyar Mirzavaziri 08.11.2022 10:41

@KamyarMirzavaziri Для простоты рассмотрим следующее объявление: Inductive t (P : nat -> Prop) : Type := inleft : forall n, P n -> t P | inright : (forall n, ~ P n) -> t P. Выбрав значение P соответствующим образом, вы можете получить тип, очень похожий на тот, который у вас был в PProperty. Каждый конструктор этого типа принимает в качестве аргумента доказательство того, что некоторое утверждение верно. Если вы удалите эти два аргумента из объявления, вы получите определение, изоморфное option nat.

Arthur Azevedo De Amorim 13.11.2022 20:36

Другие вопросы по теме