[返回主页面](https://hackmd.io/@LVcpSNoxQAim3tB5Xaj-gg/H1IpnzxAU)

# 形式证明方案设计

[题目1证明代码设计](/pfpNy5K5QAuCneUP-jjSTQ)

[历史垃圾](/4JDgiLJOSFqA39oZLD_O0g)

### 设计方案说明

[更详细的设计方案](/v4TB7vIzQnqdp1ygPO4XXg)

形式逻辑推导的过程和不等式、等式的推导过程一样，是可以被严格格式化的。

#### claim 建议词汇

structure:
detail:
expression:
wehave:高票

#### so 建议词汇
latest

#### 有限元素求和设计

在表达式形势下，我们会使用 $a+b+c$ 的格式去表达，然而，如果需要对每一项分别去进行推理、验算，我们将把它写成如下形式

claim:
    a
+
    b
+
    c

在这种写法中，看不到任何这么做的必要性。我们的目的不是为了表达$a+b+c$本身，而是为了表达一个动态推导的过程。例如，已知 $a=d$, $b=e$, $c=f$, 我们如何知道 $a+b+c = d+e+f$ 呢？ 我们可以写成如下形式

claim:
    a
    = d
+
    b
    = e
+
    c
    = f

wehave:
    forsome c. c is an integer:
        c = a
and
    forsome d. d is an integer:
        d = b
these implies forsome c,d. c,d are integers:
    c = a and d = b

这就代表 $a+b+c$ 和 $d+e+f$ 两个表达式中，我们分别有 $a=d$, $b=e$ 和 $c=f$。

同样的例子也可以用于逻辑表达中，比如

claim:
    我是个大呆瓜
    implies 我看起来憨憨的
and
    我没有女朋友
    implies 我很自由

其实这个句子作为一个整体，从 我是个没有女朋友的大呆瓜 推出了 我是一个看起来憨憨的自由人。因此，claim 的设计是一个起头，其主要作用是用于<span style="color:red">局部演算和推导</span>

#### 无限元素求和设计（量词）
虽然claim 可以把一个表达式拆成有限的部分并进行局部推导，但很多情况下我们需要对无穷个情形进行局部演算和推导，这时，我们要借助量词来帮我们实现

首先看计算上的例子。如何说明
$$
\sum_{n\in\mathbb N}\frac1{n^2}>\sum_{n\in\mathbb N}\frac1{n^3}
$$

sumover n. n is integer:
    \frac1{n^2}
    > \frac1{n^3}

其实上面的这样的表达式可能电脑还是看不懂，因此如果需要告诉电脑 $\frac1{n^2}>\frac1{n^3}$ 是因为 $n^3>n^2$，可以这么写

sumover n. n is integer:
    claim:
        1
    divide
        n^2
        < n^3

上面便是局部推导的例子。我们再回到逻辑：

forall x. x is a girl:
    x is not my girlfriend

这句话的意思是 任何女生都不是我的女朋友

以下是一个逻辑上局部推导的例子

forall x. x is a girl:
    x is not my girlfriend
    implies I am not a boyfriend of x

## 形式推导

True implies 我是个大呆瓜

这句话的意思表示 “我是个大呆瓜” 是个永远成立的命题。一般的 True implies p 是代表 p 成立的意思。逻辑推导有很多种例子，以下列举一些常见的

## 参数消失处理原则

当一个量词声明发生后，子句没有用到该量词声明的变量，这时我们称之为 参数消失 情形。面对参数消失情形，数学上有很多处理
$$
\sum_{x\in A}n = n\# A
$$
$$
\prod_{x\in A}n = n^{\#A}
$$

$$
\text{forall} \quad x, p \iff p
$$

$$
\text{forsome} \quad x, p \iff p
$$

这时，我们用so 关键字来处理此事，比如

sumover x. x in A:
    y
= so // an obvious matter

等价于

y times #A

又如

forall x. x in A:
    p
implies so

等价于

p

#### 分类讨论

这是运用 True => p or not p 来完成的，比如证明一个平方数必须有4k+1 或 4k 形式

forany n. n is an integer:
    True implies claim:
        n is an odd number
        implies forsome m. m is an integer:
            n = 2m + 1
            implies claim:
                n = 2m+1
                implies n^2 = 4m(m+1)+1
            and
                True
                implies forsome k. k is an integer:
                    k = 4m(m+1)
            implies forsome k. k is an integer:
                n^2 = 4k+1
        implies so//用于将implies 的最后一个命题直接传递到此处
    or
        n is an even number
        implies forsome m. m is an integer:
            claim:
                n = 2m
                implies n^2 = 4m^2
            and
                True
                implies forsome k. k is an integer:
                    k=4m^2
            implies for some k. k is an integer:
                n^2 = 4k
        implies so
    implies for some k. k is an integer:
        n^2 = 4k+1 or n^2 = 4k

#### 反证法

反证法也是一样。比如，设3个球放进2个抽屉，证明必然有一个抽屉有至少两个球

True implies claim:
    True implies claim:
        所有抽屉中只有一个球
        implies 一共最多两个球
        implies False
    or
        必然有一个抽屉有至少两个球
implies so

$$
True \implies (\text{所有抽屉只有一球} or \text{至少有一个抽屉有俩球})
$$

又因为 所有抽屉只有一球 => False
因此

$$
True\implies (False \text{ or } \text{至少有一个抽屉有俩球})
$$

这个表达式可以直接化简成

至少有一个抽屉有俩球

### 哈

(True => p or q) and (p=>r), then (True => r or q)

(True => (False or p)), then p

False or p = p

False or True = True
Flase or False = False

False or p = p