# Tactics

More tactics and more properties of functional programs.

• how to use auxiliary lemmas in both “forward-“ and “backward-style” proofs; “正推”“逆推”中使用辅助引理；
• how to reason about data constructors — in particular, how to use the fact that they are injective and disjoint; 如何对数据构造子进行论证，特别是，如何利用它们单射且不交的事实；
• how to strengthen an induction hypothesis, and when such strengthening is required; 如何增强归纳假设，以及何时需要增强；
• more details on how to reason by case analysis. 还有通过分类讨论进行论证的更多细节。

## The [apply] Tactic

The goal to be proved is the same as some hypothesis in the context or some proved lemma, so we can apply them to finish the proof.

Finish with [apply H.] instead of [rewrite H. reflexivity.]

When we [apply] some statements with $\forall$, Coq will try to find appropriate values.

## The [apply with] Tactic

Proof the theorem trans_eq first, and proof by using [apply trans_eq with (m:=[c;d])] (gives an instantiation of [X]). Trans_eq use abstract type so we can “with” the actual type.

Coq also has a tactic [transitivity] that accomplishes the same purpose as applying [trans_eq]. The tactic requires us to state the instantiation we want, just like [apply with] does.

Like:

## The [injection] and [discriminate] Tactics

• 构造子$S$是单射（Injective） 或“一一对应”的。即，如果$S n = S m$，那么$n=m$必定成立。
• 构造子$O$和$S$是不相交（Disjoint）的。即，对于任何$n$，$O$都不等于$S n$

If you jest say [injection XX] with no [as] clause, then all the equations will be turned into hypotheses at the beginning of the goal. (We can follow with [intros] tactics).

one exercise

Two terms beginning with different constructors (like [0] ans [S], or [true] and [false]) can never be equal.

Nonsensial to anything: Beginning with different constructors, any time we find ourselves in a context where we’ve _assumed_ that two such terms are equal, we are justified in concluding anything we want.

The [discriminate] tactic embodies this principle: It is used on a hypothesis involving an equality between different constructors.

Example

The injectivity (one to one) allows us to use [f_equal] tactic to reason form like [n = m -> f x = f y].

Given a goal of the form [f a1 … an = g b1 … bn], the tactic [f_equal] will produce subgoals of the form [f = g], [a1 = b1], …, [an = bn]. At the same time, any of these subgoals that are simple enough (e.g., immediately provable by [reflexivity]) will be automatically discharged by [f_equal].

## Using Tactics on Hypotheses

Change the goal -> change the context.

For example, [simple in H], [apply L in H].

! [apply L in H]会针对 $X$ 匹配 $H$，如果成功，就将其替换为 $Y$ 。换言之，

• [apply L in H] 给了我们一种“正向推理（forward reasoning）” ：
• 根据 $X \rightarrow Y$ 和一个匹配 $X$ 的假设， 它会产生一个匹配 $Y$ 的假设。
• Forward reasoning starts from what is _given_ (premises, previously proven theorems) and iteratively draws conclusions from them until the goal is reached
• [apply L]是一种“反向推理”：
• 如果我们指导 $X \rightarrow Y$ 并且试图证明 $Y$, 那么证明 $X$ 就足够了。
• Backward reasoning starts from
the _goal_ and iteratively reasons about what would imply the goal, until premises or previously proven theorems are reached.

## Varying the Induction Hypothesis

[intros m] in the wrong places.

What’s wrong in the second-second case.

Trying to carry out this proof by induction on [n] when [m] is already in the context doesn’t work because we are then trying to prove a statement involving _every_ [n] but just a _single_ [m].

We get a more general context.

What you should take away from all this is that we need to be careful, when using induction, that we are not trying to prove something too specific: When proving a property involving two variables [n] and [m] by induction on [n], it is sometimes crucial to leave [m] generic.

One of my exercises.

Another

### Rearrangement of quantified variables

What can we do?

• works but not nice: rewrite the statement of the lemma so that [m] is quantified before [n].
• work and nice: first intro duce all and then _re-generalize_ one or more with tactic [generalize dependent].

An exercise

## Unfolding Definitions

Manually unfold a name that has been introduced by a [Definition].

As for automatic unfolding (with tactic [simpl]), Coq is not smart enough…

Use [unfold] to explicitly tell Coq what to do.

As for automatic unfolding the definition, if [simpl] meet a function involving a pattern match with an application of an variable. It is not smart enough to notice whether the two branches of are identical or not.

Two ways to make progress

• Destruct the variable (depends on recognizing the dependencis)
• Tell Coq to unfold the function and show directly, and then …

## Using [destruct] on Compound Expressions

We have used this for the case analysis before.

When [destruct]ing compound expressions, the information recorded by the [eqn:] can actually be critical: if we leave it out, then [destruct] can erase information we need to complete a proof.

So becareful to add [eqn:] when destructing compound expressions.

exercise

## Review

Review 部分摘录翻译版。

• intros：将前提/变量从证明目标移到上下文中
• reflexivity：（当目标形如 e = e 时）结束证明
• apply：用前提、引理或构造子证明目标
• apply... in H：将前提、引理或构造子应用到上下文中的假设上（正向推理）
• apply... with...：为无法被模式匹配确定的变量显式指定值
• simpl：化简目标中的计算
• simpl in H：化简前提中的计算
• rewrite：使用相等关系假设（或引理）来改写目标
• rewrite ... in H：使用相等关系假设（或引理）来改写前提
• symmetry：将形如 t=u 的目标改为 u=t
• symmetry in H：将形如 t=u 的前提改为 u=t
• unfold：用目标中的右式替换定义的常量
• unfold... in H：用前提中的右式替换定义的常量
• destruct... as...：对归纳定义类型的值进行情况分析
• destruct... eqn:...：为添加到上下文中的等式指定名字， 记录情况分析的结果
• induction... as...: 对归纳定义类型的值进行归纳
• injection: reason by injectivity on equalities between values of inductively defined types
• discriminate: reason by disjointness of constructors on equalities between values of inductively defined types
• assert (H: e)（或 assert (e) as H）：引入“局部引理”e 并称之为 H
• generalize dependent x：将变量 x（以及任何依赖它的东西） 从上下文中移回目标公式内的前提中