Топологическое определение непрерывного в Coq

Итак, я действительно новичок в coq, функциональном программировании в целом, и я пытаюсь выразить топологическое определение непрерывности в coq. Я использую этот код для определения топологии в coq. Моя лучшая попытка выразить преемственность данной конкретной функции:

    Definition Continuous (X:Type)(TX:Topology X)(Y:Type)(TY:Topology Y)(f:X->Y):=
        forall V, exists U, all y:V, some x:U, f x = y.

Я получаю ошибку

Термин «f x» имеет тип «Y», тогда как предполагается, что он имеет тип «Prop».

Не знаю, что делать, любая помощь приветствуется.


topology coq
person aaron    schedule 19.05.2016    source источник

Ответы (1)


arrow_upward
1
arrow_downward

Проблема в том, что синтаксический анализатор Coq неправильно интерпретировал y. Мне удалось решить проблему, немного изменив обозначения для all и some:

Notation "'all' x 'in' U , P" := (forall x, U x -> P) (at level 200).
Notation "'some' x 'in' U , P" := (exists x, U x /\ P) (at level 200).

Definition continuous (X:Type)(TX:topology X)(Y:Type)(TY:topology Y)(f:X->Y):=
  forall V, exists U, all y in V, some x in U, f x = y.

Обратите внимание, как различаются уровни нотации и как используется ключевое слово in вместо :. Я не знаю, есть ли способ заставить : работать; Coq 8.5 продолжал жаловаться, если я пытался.

person Arthur Azevedo De Amorim    schedule 19.05.2016
comment
Блестяще! Большое спасибо. - person aaron; 19.05.2016