9.10

Coq

找到了一份不错的入门教程 迈克·纳哈斯的 Coq 教程（中文翻译） ，可惜的是，尽管作者从 2021.10.4 就开始翻译，最终只翻译了不到一半，只能看原文 Mike Nahas's Rocq (formerly known as Coq) Tutorial，好处是它提供了 Coq 源代码版本，可以边读边证明 —— 这一点和 Software Foundations 是一样的。

Coq 基于柯里-霍华德同构（Curry-Howard Isomorphism），在 Coq 里，命题是类型，命题的证明是这个类型的实例（在 Coq 里不叫 instance，而是 inhabitant）。要证明一个命题，就是要构造出一个该类型的实例。理解了这个底层逻辑后，就是学习各种策略（Tactics），同时了解各种类型的命题如何证明。然而，深入理解某些部分或许需要一点类型系统基础，例如依赖类型，Cic。

第一个自己写的证明：

Theorem negb_is_not : (forall a, Is_true (negb a) <-> (~(Is_true a))).
Proof.
  intros a.
  unfold iff.
  refine(conj _ _).

    case a.
      simpl.
      intro f.
      case f.

      simpl.
      intros t f.
      case f.

  
    case a.
      simpl.
      intros H.
      exact (H I).
      
      simpl.
      intros H.
      exact I.
Qed.

在知乎上看到一篇文章 Coq 里的排中律，由此了解到 PKU 开了一门 软件科学基础，就是仿了 CIS 5000，课程页面提供了 Software Foundations 的 中文版，并且同样开放了所有讲义！

最后，对 Mike Nahas's Rocq Tutorial 提出改进意见：

在定理 thm_exists_basics 的证明中，simpl. 一步是无效的，因为没有提前 unfold basic_predicate，导致 simpl. 什么都做不了，据 GPT 所说，最后 exact I. 有效是因为 exact 策略会自动做内核的可换算性检查（convertibility check），听不懂~

教材

作为和班长熟悉的后果，中午被叫去教材科搬教材。说是搬教材，实际上就是清点数量，然后把教材搬到一米远的平板货车上。抽象的是，每个班都要派一个同学 “跟车”，就是爬上装书的栏板式货箱，跟着车一起到各个宿舍楼下分书。

最终我承担了这个岗位，“跟车” 看起来和游街没什么区别，或许一个更现代的说法是 “公开处刑”，但我想取该词的本意，所以在这里反而不是很适合。

每当抵达目的地时，都有一些同学在宿舍门前等待。在这个批次中，一共有 5 个班的教材，也就有 5 个 “跟车” 的同学。我的目的地 D19 被排在第二个，还有一个同学的目的地也是 D19，于是在宿舍门前等待的同学就更多。

到这里，短暂的游街算是结束了，我们能听见其中有些同学称这种车为 “翻斗车”。我因此兴奋了一会儿：自己居然坐上所谓的 “翻斗车” 了！可是上网查了才知道，翻斗车并不长这样，相差甚远，非常失望。

这学期只买了三本教材：《数学分析（上）》，《数学分析（中）》和 《国家安全教育读本》，程序设计课用的是上学期的数据结构教材，看来课程不会太简单。数学分析教材和微积分教材一样，是交大自编的，封面和封底都是蓝色硬壳，别具特色。

为了赶上搬教材，没空吃一顿正经的早中饭，结果是吃了两袋小浣熊方便面——宿舍唯一的零食。搬完书去水果店买了香蕉和一瓶荔枝味味全每日。当然，吃一堑长一智，这次把香蕉挂在了自行车把手上，没有再发生爆炸。

唯时代尔

在水源上刷今年的保研帖，一个电院 AI 的楼主因为 rank 不够，无缘推免，开始备战考研。今年的推免情况比往年惨烈，一大原因就是出国比例减少，顺延下来的推免名额就减少了。在帖子里看到，“我认识的北大图灵rank1都被鸽完了，正在找港新，清华智班的同学也可能去港新”，诶，cxs，带我走吧！

隔壁互联网秋招则是都在吐槽只发实习 offer，不太了解，不好评价

跑

今天是六分配，在【体测】中能够获得【10 分】的好成绩！