From PLF Require Import LibTactics.
LibTactics vs. SSReflect (another tactics package)
- for PL vs. for math
- traditional vs. rethinks..so harder
Tactics for Naming and Performing Inversion
introv
Theorem ceval_deterministic: ∀c st st1 st2,
st =[ c ]⇒ st1 →
st =[ c ]⇒ st2 →
st1 = st2.
intros c st st1 st2 E1 E2. (* 以往如果想给 Hypo 命名必须说全 *)
introv E1 E2. (* 现在可以忽略 forall 的部分 *)
inverts
(* was... 需要 subst, clear *)
- inversion H. subst. inversion H2. subst.
(* now... *)
- inverts H. inverts H2.
(* 可以把 invert 出来的东西放在 goal 的位置让你自己用 intro 命名！*)
inverts E2 as.
Tactics for N-ary Connectives
Because Coq encodes conjunctions and disjunctions using binary constructors ∧ and ∨… to work with a
N-ary logical connectives…
splits
n-ary conjunction
n-ary split
branch
n-ary disjunction
faster destruct?
Tactics for Working with Equality
asserts_rewrite and cuts_rewrite
substs
better subst - not fail on circular eq
fequals
vs f_equal?
applys_eq
variant of eapply
Some Convenient Shorthands
unfolds
better unfold
false and tryfalse
better exfalso
gen
shorthand for generalize dependent, multiple arg.
(* old *)
intros Gamma x U v t S Htypt Htypv.
generalize dependent S. generalize dependent Gamma.
(* new...so nice!!! *)
introv Htypt Htypv. gen S Gamma.
admits, admit_rewrite and admit_goal
wrappers around admit
sort
proof context more readable
vars -> top hypotheses -> bottom
What readers say
先看读者反馈，再直接在当前页面继续讨论。公共留言需要 Waline 服务端；配置后访客只填昵称即可发布。
这类长文如果结构清楚，我会一路读到底。这里最好的地方是把概念、公式和代码示例放在同一篇里。
数据库和工程文档的风格很实用，截图、SQL 和说明都能直接拿去复盘项目。
强化学习相关文章密度很高，但排版如果更清楚，回看体验会更好。这个新版方向是对的。
我更喜欢能快速扫到标签、修改时间和文章重点的首页，现在这种卡片视图会比纯列表更容易选读。
代码块只要语言标识和层级做好，技术博客的专业感会立刻上来。
评论区不用社交账号强绑定会更愿意留言，尤其是这种偏学习记录的网站。
Quick Identity
Pick a preset and leave a note
留言方式：先选择一个预设身份，再在下方输入评论。当前若显示“需要配置 Waline”，说明站点还缺少可写评论后端。
当前未选择预设身份