9.13

幽灵行者 2

玩了第一关，花了半个多小时，死了 86 次。跑酷天才这一块

你也干这个？

几周前学长试图发放 john.sjtu.app 论坛邀请码到邮箱，但是由于邮件管理系统故障，发不出邮件。今天突然想到此事，问了问情况，才知道这个系统居然是 21 级去耶鲁的钟有为学长维护的，这段时间一直没回邮件，所以系统没人修。

搜了一下他的名字，看到了 https://news.sjtu.edu.cn/zhxw/20241216/205575.html 这个通报，看到 SPLASH2024 几个字就蚌埠住了，你怎么也干这个？

2023年4月起，钟有为在约翰·霍普克罗夫特中心曹钦翔副教授和计算机系助理教授胡云聪等老师的指导下开始了对零知识虚拟机进行形式化验证的研究。在曹老师的支持和指导下，钟有为独立完成了零知识以太坊虚拟机中约束生成算法的正确性证明，并在交互式定理证明器 Coq 中实现了该证明。

曹神，原来这也是你带的兵？🥰

最后，个人主页 里的 Awards and Honors 属实抽象，把致远每年每人 5000 的低保写里面了

＋吃－跑

原宿舍每到校一人，就约一次饭。作为最早到校的，这三天连着出去吃三顿了🐖，分别是烤肉，炒肉和火锅。

那还说啥了，后面几天少吃点不就得了。

今晚下雨了，跑不了步，暂停一天！👍

那年今日（并非今日）

Theorem plus_sym: (forall n m, n + m = m + n).
Proof.
  intros n m.
  elim n.
    (** base case for n *)
    elim m.
      (** base case for m *)
      exact (eq_refl (O + O)).

      (** inductive case for m *)
      intros m'.      
      simpl.
      intros inductive_hyp_m.
      rewrite <- inductive_hyp_m.
      exact (eq_refl (S m')).

    (** inductive case for n *)
    intros n'.
    intros inductive_hyp_n.
    simpl.
    rewrite inductive_hyp_n.
    elim m.
      (** base case for m *)
      simpl.
      exact (eq_refl (S n')).

      intros m'.
      intros inductive_hyp_m.
      simpl.
      rewrite inductive_hyp_m.
      simpl.
      exact (eq_refl (S (m' + S n'))).
Qed.

四年前的夏天，在看加法交换律的证明，还发了 QQ 动态；今天，还在看加法交换律的证明。

傻逼定理 1：如果发现过去的自己是一个傻逼，说明自己在进步。
傻逼定理 2：如果自己很久没有当傻逼了， 说明自己在原地踏步或者退步

引理 1：智商没有比四年前成长多少，还在学差不多的东西
引理 2：居然没觉得当时发 QQ 动态的行为有多傻逼

由 引理 1 和 引理 2 立刻可得：
引理 3：自己很久没有当傻逼了

引理 4：自己在原地踏步或者退步

Proof.
	exact (傻逼定理1 引理3).
Qed.

引理 5：四年前的自己是傻逼

命题：我是傻逼

Proof.
	trivial.
Qed.

总结：不管怎么样，能在日记里写出这么一坨东西出来的，确实是傻逼了！

最后，边刷水源边把 Coq 教程读完了，顺手挂一个题解：

Theorem app_cons_not_nil : forall A (x y:list A) (a:A), nil <> x ++ a :: y.
Proof.
  unfold not.
  intros A x y a.
  case x.
    simpl.
    intros H.
    discriminate H.
    
    intros a' l.
    simpl.
    intros H.
    discriminate H.
Qed.

豪丸！👍