「SF-LC」16 Auto

auto - proof search
Ltac - 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

auto can 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

intros
apply (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 提示数据库

auto auto 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

对于很常见的一种矛盾情形：

1 2	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 了

1
2
3

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.

Ltac macro

The auto Tactic