形式化理论证明任务：求证⊢x ≤ min(x, max(x,y))

先把我们用到的基础定义、公理和推理规则整理清楚：

基础要素 #

• 公理：$A \leq A$（任何表达式都小于等于自身）
• 推理规则：
  • 规则1：$\frac{A\leq C}{\text{min}(A,B)\leq C}$（若A小于等于C，则A和B的最小值也小于等于C）
  • 规则2：$\frac{A\leq C; B\leq C}{\text{max}(A,B)\leq C}$（若A、B都小于等于C，则它们的最大值也小于等于C）
  • 规则3：$\frac{\text{min}(A,B)\leq C}{\text{min}(B,A)\leq C}$（min操作满足交换律，顺序不影响推导）
  • 规则4：$\frac{A\leq \text{max}(B,C)}{A\leq \text{max}(C,B)}$（max操作满足交换律，顺序不影响推导）
  • 规则5：$\frac{A\leq B; A\leq C}{A\leq \text{min}(B, C)}$（若A同时小于等于B和C，则A小于等于B和C的最小值）
  • 规则6：$\frac{A\leq B}{A\leq \text{max}(B,C)}$（若A小于等于B，则A必然小于等于B和任意C的最大值）
  • 规则7（传递性）：$\frac{A\leq B; B\leq C}{A\leq C} $（不等式的传递性）
• 字母表：$\Sigma= { F, P, I, x, y, z, /, \text{min}, \text{max}, \leq }$
• 语法规则：
  • $P \rightarrow x \mid y \mid z \mid P/$（P代表基本变量或带"/"的扩展变量）
  • $I\rightarrow P \mid \text{min}(I,I) \mid \text{max}(I,I)$（I代表合法的表达式，包括变量、min组合、max组合）
  • $F\rightarrow I\leq I$（F代表合法的不等式公式）

具体证明过程 #

我们一步步来推导目标结论$\vdash x\leq \text{min}(x, \text{max}(x,y))$：

1. 第一步：获取基础自反不等式
   根据公理$A \leq A$，直接代入$A=x$，得到：
   $$x \leq x \tag{1}$$

2. 第二步：推导$x$与$\text{max}(x,y)$的不等式
   应用规则6：$\frac{A\leq B}{A\leq \text{max}(B,C)}$，这里我们取$A=x$，$B=x$，$C=y$，把(1)作为前提代入，就能得到：
   $$x \leq \text{max}(x,y) \tag{2}$$

3. 第三步：组合两个不等式得到目标结论
   现在我们有两个前提：(1) $x \leq x$ 和 (2) $x \leq \text{max}(x,y)$，这正好匹配规则5的前提条件$\frac{A\leq B; A\leq C}{A\leq \text{min}(B, C)}$。我们令$A=x$，$B=x$，$C=\text{max}(x,y)$，代入规则5后，直接得出：
   $$x \leq \text{min}(x, \text{max}(x,y))$$

这样就完成了整个证明，目标结论得证！

备注：内容来源于stack exchange，提问作者Danilo Jonić