Как говорят Ив и Галле, за исключением ошибок в системе, каждый термин Галлина, принятый Coq, имеет тип.Это почти по определению;сказать, что термин t принят Coq, означает, что Check t не является ошибкой, и мы можем заметить, что Check t всегда будет печатать тип t.Теперь может быть так, что тип, напечатанный самим Check t, неправильно напечатан, но это, опять же, будет ошибкой в системе, и я никогда не видел, чтобы это произошло (до тех пор, пока нотации не получаются)в способе обратимости печати).
Однако есть пара вещей, близких к тому, что вы просите, которые могут вас заинтересовать.
Юниверсы
В Coq мы можем написать
Universe i.
Check Type@{i}.
Однако, хотя i является допустимым юниверсом, Check i завершается ошибкой, а i не имеет типа вощущение, что термины Галлина имеют типы.
Обратите внимание, что в Agda мы можем написать
postulate foo : (i : Level) → Set i
, и средство проверки Agda принимает это, но если мы напишем
bar = (i : Level) → Set i
мы получаем сообщение об ошибке Setω is not a valid type.У Coq нет этой проблемы, потому что юниверсы не являются терминами в Coq, а полиморфизм юниверсов в Coq - это prenex.
Потеря субъекта сокращения
Coq имеет несколько угловслучаи (возможно, также называемые ошибками), когда предметное сокращение потеряно.То есть есть некоторые хорошо напечатанные термины, которые становятся плохо напечатанными, когда вы их сокращаете.См., Например, ошибка # 6768 , которая дает код
CoInductive I := C : I -> I.
CoFixpoint infty := C infty.
Definition unfold : infty = C infty :=
match infty as x return match x with C n => x = C n end with
| C n => eq_refl (C n)
end.
Fail Definition nf_unfold : infty = C infty := Eval lazy in unfold.
Обратите внимание, что мы можем получить такую ошибку даже без аннотаций типа, например с
Axiom id : forall {T}, T -> T.
Definition nf_unfold := Eval lazy in id unfold.
(*Error: Illegal application:
The term "@id" of type "forall T : Type, T -> T"
cannot be applied to the terms
"(cofix infty : I := C infty) = C (cofix infty : I := C infty)" : "Prop"
"eq_refl"
: "C (cofix infty : I := C infty) = C (cofix infty : I := C infty)"
The 2nd term has type
"C (cofix infty : I := C infty) = C (cofix infty : I := C infty)"
which should be coercible to
"(cofix infty : I := C infty) = C (cofix infty : I := C infty)".
*)
Это не совсем то, о чем вы спрашиваете, но, похоже, это связано.
Самоссылочные типы
Все термины имеют типы, но не все термины имеюттипы, которые вы хотите их.Например, учитывая A : Type и B : A -> Type, вы можете записать тип терминов f, которые имеют тип
forall b : bool, if b then A else B (f true)
Конечно, это не принимается Coq, но мы можемопределить термины, которые имеют этот тип.Например, если дано A, B и x : @sigT A B, Coq принимает
Definition f := fun b : bool => if b return if b then _ else _
then projT1 x else projT2 x.
Check f : forall b : bool, if b then A else B (f true).
Доказательства теорем, которые нельзя сформулировать
Назад до CoqЯ имел явные переменные юниверса, и я хотел доказать, что расширение функций закрыто вниз.То есть я хотел доказать теорему
Set Universe Polymorphism.
Definition funext_at@{i} := forall (A B : Type@{i}) (f g : A -> B),
(forall x, f x = g x) -> f = g.
Universes i j.
Constraint j <= i.
Theorem funext_downward_closed : funext_at@{i} -> funext_at@{j}.
Однако не было возможности сформулировать эту теорему.Я мог только написать
Theorem funext_downward_closed : funext -> funext.
Мне все еще удалось доказать эту теорему (см. этот коммит и этот коммит и этот вопрос в HoTT / HoTT библиотека), однако, записав проверочный термин и впоследствии проверив теорему, чтобы увидеть, были ли ограничения юниверса правильными.Я в шутку сказал, что доказал невероятную теорему.