Как можно доказать, что в Mizar есть натуральное число, равное 1 (язык доказательства математических теорем)? - PullRequest
Новая
       26

Как можно доказать, что в Mizar есть натуральное число, равное 1 (язык доказательства математических теорем)?

0 голосов
/ 28 ноября 2018

Я хотел написать простейшее доказательство на Mizar языке доказательства математических теорем, о котором я только мог подумать.Поэтому я подумал о следующем:

в Nat существует x \: x = 1

нет ничего проще, чем я мог бы придумать.Я предпринял следующую попытку: 

:: example of a comment
environ
  vocabularies MY_MIZAR;
  :: adding Natural Numbers
  requirments SUBSET, NUMERALS, ARITHM;
::>         *210
begin

theorem Th1:
    ex x being Nat st x=1
proof
    ::consider x = 1
    :: proof is done
    x = 1;
    thus Th1;
end;
::>
::> 210: Wrong item in environment declaration

, но, как вы видите, Мицар не любит мое доказательство.Чего мне не хватает?

Это все еще не работает: 

::: example of a comment
environ
  vocabularies MY_MIZAR;
  ::: adding Natural Numbers
  requirements SUBSET, NUMERALS, ARITHM;
::>                 *856      *825
begin

theorem Th1:
    ex x being Nat st x=1
proof
    :::consider x = 1
    ::: proof is done
    set x=1;
    take x;
    thus thesis;
end;
::>
::> 825: Cannot find constructors name on constructor list
::> 856: Inaccessible requirements directive

Ответы [ 2 ]

0 голосов
/ 28 ноября 2018

Вы можете попробовать следующее:

1) Исправить ошибку 210: 

x  requirments (wrong spelling)
o  requirements

2) Вероятно, теперь появятся некоторые новые ошибки в содержании этой строки, поэтомукогда вы начинаете, обычно полезно «позаимствовать» среду, которая уже работает, например, вы можете использовать строки среды из одной из статей Mizar о натуральных числах, таких как NAT_1.miz: 

environ
:: adding Natural Numbers
vocabularies NUMBERS, ORDINAL1, REAL_1, SUBSET_1, CARD_1, ARYTM_3, TARSKI,
  RELAT_1, XXREAL_0, XCMPLX_0, ARYTM_1, XBOOLE_0, FINSET_1, FUNCT_1, NAT_1,
  FUNCOP_1, PBOOLE, PARTFUN1, FUNCT_7, SETFAM_1, ZFMISC_1;
notations TARSKI, XBOOLE_0, ENUMSET1, ZFMISC_1, SUBSET_1, SETFAM_1, ORDINAL1,
  FINSET_1, CARD_1, PBOOLE, NUMBERS, XCMPLX_0, XREAL_0, XXREAL_0, RELAT_1,
  FUNCT_1, PARTFUN1, FUNCOP_1, FUNCT_2, BINOP_1;
constructors NUMBERS, XCMPLX_0, XXREAL_0, XREAL_0, CARD_1, WELLORD2, FUNCT_2,
  PARTFUN1, FUNCOP_1, FUNCT_4, ENUMSET1, RELSET_1, PBOOLE, ORDINAL1,
  SETFAM_1, ZFMISC_1, BINOP_1;
registrations SUBSET_1, ORDINAL1, NUMBERS, XXREAL_0, XREAL_0, CARD_1,
  RELSET_1, FUNCT_2, PBOOLE;
requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM;
definitions SETFAM_1, TARSKI, XBOOLE_0, RELAT_1;
equalities ORDINAL1, XBOOLE_0, CARD_1;
expansions SETFAM_1, ORDINAL1, TARSKI, XBOOLE_0;
theorems AXIOMS, ORDINAL1, XCMPLX_1, XREAL_1, XXREAL_0, TARSKI, ORDINAL2,
  XBOOLE_0, CARD_1, FUNCT_2, FUNCT_1, FUNCOP_1, PBOOLE, RELSET_1, RELAT_1,
  PARTFUN1, SUBSET_1, NUMBERS, ENUMSET1, XBOOLE_1;
schemes SUBSET_1, ORDINAL2, FUNCT_2, PBOOLE, BINOP_1;

3) Чтобы использовать «1» в качестве примера, вы можете использовать «set», «take»: 

proof
  set x=1;
  take x;
  thus thesis;
end;

Надеюсь, это поможет.

0 голосов
/ 28 ноября 2018

Есть несколько способов сделать это:

Хотя это не совсем ваше утверждение, вот пример (это не совсем ваше утверждение, потому что вы используете тип "Nat").

environ

 vocabularies NUMBERS;
 constructors ARYTM_0;
 notations NUMBERS;
 registrations ORDINAL1;
 requirements NUMERALS, SUBSET, BOOLE;

begin

1 in NAT;

ex x be object st x = 1;

ex x be object st x in NAT & x = 1;

Mizar подтвердил 3 утверждения как действительные, истинные, демонстрирующие.

Если это не продемонстрировано (в смысле Мицара), это будет означать ошибку * 4 или даже иногда ошибку * 1.

В случае 3 утверждений здесь доказательствоне указано явно.Он содержится в среде, потому что Мицар не требует, чтобы вы указывали все шаги, некоторые из них являются автоматическими.

Можно представить таким образом, что приемлемо и для Мицара. 

environ

 vocabularies NUMBERS;
 constructors ARYTM_0;
 notations NUMBERS;
 registrations ORDINAL1;
 requirements NUMERALS, SUBSET, BOOLE;

begin

1 in NAT
proof
  thus thesis;
end;

ex x be object st x = 1
proof
  thus thesis;
end;

ex x be object st x in NAT & x = 1
proof
  thus thesis;
end;

Но в этой ситуации полное выражение 

proof
  thus thesis;
end;

является избыточным.

Чтобы вернуться к исходной проблеме и использовать предложение (user10715283 & user10715216).«Можем ли мы взять среду, которая меньше [...]»: да, с помощью специального инструмента (clearenv.pl, предоставьте Mizar-System) 

environ

 vocabularies NAT_1;
 constructors NUMBERS, XCMPLX_0, XREAL_0, BINOP_1;
 notations ORDINAL1;
 registrations ORDINAL1;
 requirements NUMERALS, SUBSET;

begin

theorem Th1:
    ex x being Nat st x=1
proof
    set x=1;
    take x;
    thus thesis;
end;
...