0

我想用我能想到的Mizar数学定理证明器语言编写最简单的证明。所以我想到了以下几点：

存在 x \in Nat : 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

但正如你所见，Mizar 不喜欢我的证明。我错过了什么？

这仍然不起作用：

::: 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
4

2 回答 2

1

您可以尝试以下方法：

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;

希望这可以帮助。

于 2018-11-28T05:43:04.377 回答
1

做这件事有很多种方法：

虽然这不是您的陈述，但这里只是一个示例（这不是您的陈述，因为您使用了“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;

这 3 个陈述经 mizar 验证为有效、真实、证明。

如果这没有被证明（在 mizar 的意义上），它会指示 *4 错误，甚至有时是 *1 错误。

对于此处的 3 项陈述，没有明确说明证据。它包含在环境中，因为 Mizar 不需要您指示所有步骤，其中一些是自动的。

以这种方式呈现是可能的，开泽也可以接受。

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;
于 2018-11-28T05:29:59.137 回答