auto- proof searchLtac- automated forward reasoning (hypothesis matching machinery)eauto,eapply- deferred instantiation of existentials
Ltac macro
Ltac inv H := inversion H; subst; clear H.
(** later in the proof... **)
inv H5.
The auto Tactic
autocan free us by searching for a sequence of applications that will prove the goal:
intros P Q R H1 H2 H3.
apply H2. apply H1. assumption.
(** can be replaced by... **)
auto.
auto solves goals that are solvable by any combination of
introsapply(of hypotheses from the local context, by default)
使用 auto 一定是“安全”的，它不会失败，也不会改变当前证明的状态： auto 要么完全解决它，要么什么也不做。
Proof search could, in principle, take an arbitrarily long time, so there are limits to how far auto will search by default. (i.e.
5)
Example auto_example_3 : ∀(P Q R S T U: Prop),
(P → Q) →
(Q → R) →
(R → S) →
(S → T) →
(T → U) →
P →
U.
Proof.
(* 当 auto 无法解决此目标时，它就什么也不做 *)
auto.
(* 可选的参数用来控制它的搜索深度（默认为 5）, 6 就刚好能解决了！ *)
auto 6.
Qed.
Hint Database 提示数据库
autoauto considers a hint database of other lemmas and constructors. common lemmas about equality and logical operators are installed by default.
just for the purposes of one application of
auto我们可以为某次auto的调用扩展提示数据库，auto using ...
Example auto_example_6 : ∀n m p : nat,
(n ≤ p → (n ≤ m ∧ m ≤ n)) →
n ≤ p →
n = m.
Proof.
intros.
auto using le_antisym.
Qed.
Global Hint Database 添加到全局提示数据库
Hint Resolve T.
Hint Constructors c.
Hint Unfold d.
Proof with auto.
Under Proof with t, t1... == t1; t.
Searching For Hypotheses
对于很常见的一种矛盾情形：
H1: beval st b = false
H2: beval st b = true
contradiction 并不能解决，必须 rewrite H1 in H2; inversion H2.
- 宏：
Ltac rwinv H1 H2 := rewrite H1 in H2; inv H2.
(** later in the proof... **)
rwinv H H2.
match goal调用宏
Ltac find_rwinv :=
match goal with
H1: ?E = true,
H2: ?E = false
⊢ _ ⇒ rwinv H1 H2
end.
(** later in the proof... **)
induction E1; intros st2 E2; inv E2; try find_rwinv; auto. (** 直接解决所有矛盾 case **)
- (* E_Seq *)
rewrite (IHE1_1 st'0 H1) in *. auto.
- (* E_WhileTrue *)
+ (* b 求值为 true *)
rewrite (IHE1_1 st'0 H3) in *. auto. Qed.
可以看到最后只剩这种改写形式…我们也把他们自动化了：
Ltac find_eqn :=
match goal with
H1: ∀x, ?P x → ?L = ?R,
H2: ?P ?X
⊢ _ ⇒ rewrite (H1 X H2) in *
end.
配合上 repeat…我们可以 keep doing useful rewrites until only trivial ones are left.
最终效果：
Theorem ceval_deterministic''''': ∀c st st1 st2,
st =[ c ]⇒ st1 →
st =[ c ]⇒ st2 →
st1 = st2.
Proof.
intros c st st1 st2 E1 E2.
generalize dependent st2;
induction E1; intros st2 E2; inv E2;
try find_rwinv;
repeat find_eqn; auto.
Qed.
即使我们给 IMP 加上一个 CRepeat（其实就是 DO c WHILE b)，
会发现颠倒一下自动化的顺序就能 work 了
induction E1; intros st2 E2; inv E2;
repeat find_eqn;
try find_rwinv; auto.
当然，这种「超级自动化」(hyper-automation) 并不总是现实，也不好调试…
The eapply and eauto variants
推迟量词的实例化
比如对于
Example ceval_example1:
empty_st =[
X ::= 2;;
TEST X ≤ 1
THEN Y ::= 3
ELSE Z ::= 4
FI
]⇒ (Z !-> 4 ; X !-> 2).
Proof.
(* 我们补充了中间状态 st'... *)
apply E_Seq with (X !-> 2).
- apply E_Ass. reflexivity.
- apply E_IfFalse. reflexivity. apply E_Ass. reflexivity.
Qed.
没有 with 就会 Error: Unable to find an instance for the variable st'
但其实 st' 的取值在后面的步骤是很明显（很好 infer/unify）的，所以 eapply works.
What readers say
先看读者反馈，再直接在当前页面继续讨论。公共留言需要 Waline 服务端；配置后访客只填昵称即可发布。
这类长文如果结构清楚，我会一路读到底。这里最好的地方是把概念、公式和代码示例放在同一篇里。
数据库和工程文档的风格很实用，截图、SQL 和说明都能直接拿去复盘项目。
强化学习相关文章密度很高，但排版如果更清楚，回看体验会更好。这个新版方向是对的。
我更喜欢能快速扫到标签、修改时间和文章重点的首页，现在这种卡片视图会比纯列表更容易选读。
代码块只要语言标识和层级做好，技术博客的专业感会立刻上来。
评论区不用社交账号强绑定会更愿意留言，尤其是这种偏学习记录的网站。
Quick Identity
Pick a preset and leave a note
留言方式：先选择一个预设身份，再在下方输入评论。当前若显示“需要配置 Waline”，说明站点还缺少可写评论后端。
当前未选择预设身份