(** 这里统一回答几个上机课中同学提出的问题。 *)

(* 问题 1 *)

(* swapping_by_arith 一题为何不能写下面的假设并在证明中用(x+y)带入这里的x？*)

Hypothesis triple2: forall x y: Z,
  {{ {[X]} == x AND {[Y]} == y }}
  Y ::= X - Y
  {{ {[X]} == x AND {[Y]} == x - y }}.

(* 这一点是由于我们课程的Imp库在语法较为严格。前面的课程中我们已经严格的定理了程序语言：

    (integer expression)
    a ::= Z
        | var
        | a + a
        | a - a
        | a * a

    (boolean expression)
    b ::= true
        | false
        | a == a
        | a <= a
        | ! b
        | b && b

    (command)
    c ::= Skip
        | var ::= a
        | c ;; c
        | If b Then c Else c Endif
        | While b Do c EndWhile

我们也可以严格定义断言（下面仅仅指Imp库所允许的断言，一般的程序语言理论中可以在断言内使用任意数学语言）：

    (term)
    t ::= Z
        | {[a]}
        | logic_var
        | t + t
        | t - t
        | t * t

    (Assertion)
    P ::= {[b]}
        | t <= t
        | t < t
        | t== t
        | True
        | False
        | P OR P
        | P AND P
        | NOT P
        | EXISTS var, P
        | FORALL var, P

因此，(x+y)能否带入上面 triple2 中的 x 呢？取决于(x+y)是一个整数(Z)还是断言中的整数项(Term)。Coq自动将(x+y)
理解成为了一个 term，并将其中的加法理解成了 term 中的加号，因此不能带入。如果让Coq将(x+y)理解称为一个整数(Z)
呢？我们只需要写(x+y)%Z就可以了。课程网站上上传的Lab_Answer里有“swapping_by_arith_alter”这个不同的解法（它
把原本文件中给出的triple1也改掉了，做作业时请不要这样改动原有文件的内容）。*)

(* 问题 2 *)

(* 断言中问什么不能写大于号">"。如前面所说，暂时Imp中规定的断言语言中没有大于号和大于等于号。如果你想表达
(x>y)，那么可以用(y<x)表示。 *)

(* 问题 3 *)

(* Coq为什么不能识别(P AND Q)和(Q AND P)相同这件事？(P AND Q)和(Q AND P)确实是相互等价的断言，但是如果把每个
断言看作一个语法树，那么这两个断言对应的语言树确实不一致。断言是一个描述程序状态的命题，而不是一个布尔函数，
不能完全用“布尔函数值是否相等”来判断“两个断言是否是同一个断言”。类似的{[0]}和0不是同一个整数项(Term)，但
是他们的值永远相等。*)

(* 问题 4 *)

(* 如果已经证明的(1) {{P}} c1 {{Q}} (2) {{Q}} c2 {{R} (3) {{R}} c3 {{S}}，那么为什么不能在Coq中如下证明
 {{P}} c1;;c2;;c3 {{S}}?
 
   在Coq中失败的证明思路：先用hoare_seq和(1)、(2)一起得出结论：(4) {{P}} c1;;c2 {{R}}；再用hoare_seq和(4)、(3)
   一起证明{{P}} c1;;c2;;c3 {{S}}。

原因是Coq中c1;;c2;;c3表达的意思实际上是(c1;;(c2;;c3))而不是((c1;;c2);;c3)。因此，只能在Coq中如下证明：

   在Coq中成功的证明思路：先用hoare_seq和(2)、(3)一起得出结论：(5) {{Q}} c2;;c3 {{S}}；再用hoare_seq和(1)、(5)
   一起证明{{P}} c1;;c2;;c3 {{S}}。
*)