Я смотрел на IndProp и видел:
Fail Inductive wrong_ev (n : nat) : Prop :=
| wrong_ev_0 : wrong_ev 0
| wrong_ev_SS : ∀ n, wrong_ev n → wrong_ev (S (S n)).
(* ===> Error: A parameter of an inductive type n is not
allowed to be used as a bound variable in the type
of its constructor. *)
за исключением того, что он ведет себя точно так же, как если бы он принимал аргумент, но, похоже, выдает ошибку.Почему это так?
В тексте содержится какое-то объяснение, но я его не понимаю:
что я не совсем понимаю.Часть, которую я не понимаю, это часть, в которой говорится:
разрешено принимать различные значения в типах
почему это так?говоря "в прообразе"?Типы НЕ входные, значения есть.Почему это говорит это?Это кажется очень запутанным.Я знаю (весьма расплывчато), что существует такая вещь, как «зависимые типы», но на это ли она ссылается?Разве это не должны быть аргументы?Разве конструкторы не принимают значения или «вещи» и не возвращают объект какого-либо типа?
Почему кажется, что сигнатура индуктивного типа (которую я просто рассматриваю как функцию, создающую вещи, возвращаетобъекты некоторого типа) пропущенные аргументы ?
Больше контекста из текста, где, кажется, появляется объяснение:
Это определение отличается в одном решающемуважение к предыдущему использованию Inductive: его результатом является не Type, а скорее функция от nat до Prop, то есть свойство чисел.Обратите внимание, что мы уже видели другие индуктивные определения, которые приводят к появлению функций, таких как list, тип которых Type → Type.Новым здесь является то, что, поскольку аргумент nat ev появляется без имени, справа от двоеточия разрешено принимать разные значения в типах различных конструкторов: 0 в типе ev_0 и S (S n) втип ev_SS.Напротив, определение списка называет параметр X глобально, слева от двоеточия, что приводит к тому, что результат nil и cons будет одинаковым (список X).Если бы мы попытались вывести nat влево при определении ev, мы бы увидели ошибку ... Мы можем думать об определении ev как о определении свойства Coq ev: nat → Prop вместе с примитивными теоремами ev_0: ev 0 иev_SS: ∀n, ev n → ev (S (S n)).Такие «теоремы конструктора» имеют тот же статус, что и доказанные теоремы.