Предположим, что 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.
но я не знаю, как пойти дальше оттуда.
Любые идеи поощряются.
Вы не можете 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, что я и сделал выше, но вы можете адаптировать его по своему усмотрению.
Я думаю, что эту гипотезу можно упростить с помощью тривиальной гипотезы, которая верна для любого P в классической логике. Hypothesis PProperty : forall (t : T), {k : nat | (P k t) /\ forall n, (n < k -> ~ P n t)} + {forall k, ~ P k t}.
В общем, если вы не знаете, что что-то делает, вы можете Check proj1_sig
увидеть его тип, Print proj1_sig
увидеть его определение или даже Locate proj1_sig
узнать, где оно определено. Последнее полезно, чтобы увидеть, есть ли полезные комментарии в коде рядом с определением. В данном случае есть: мы видим, что proj1_sig
— это первая проекция sig
, которая является Type
версией exists _, _
. Итак, proj1_sig kH
дает вам k
, для которого выполняется свойство.
Это зависит от того, что вы подразумеваете под «классической логикой». Обычно я бы сказал, что это означает «Coq + forall P : Prop, P / ~ P
». Обратите внимание, что это слабее, чем forall P : Prop, {P} + {~ P}
, что, как я считаю, вам нужно принять, чтобы получить PProperty
. Вы все еще можете работать с более сильным предположением, но помните, какие аксиомы вы используете.
В дополнение к отличному ответу Аны, я думаю, стоит отметить, что option nat
по сути то же самое, что и {k : nat | ...} + {forall k, ~ P k t}
, если стереть доказательства последнего типа: в первом случае (Some
или inleft
) вы получите натуральное число; во втором (None
или inright
) вы вообще ничего не получаете.
Ух ты. Я не смотрел на это таким образом! Спасибо, что указали на этот момент. Но я изо всех сил пытаюсь понять, что значит быть одним и тем же. Я думаю, что ...
в левой части должно быть правдой, если мы хотим, чтобы это было все nat
?
@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
.
Спасибо за ваш ответ. Могу ли я попросить ссылку, чтобы узнать больше о
proj1_sig
?