Coq中分号链局部子目标的策略

Question

假设我们有了定义

Inductive sillyA : nat -> Prop :=
| sA0 : sillyA 0
| sA1 : sillyA 1.

Inductive sillyB : nat -> Prop :=
| sB0 : sillyB 0
| sB1 : sillyB 1.

Inductive sillyC (n : nat) : Prop :=
| sC0 : sillyA n -> sillyC n
| sC1 : sillyA n -> sillyC n.

想要证明

Theorem silly : forall n, sillyC n -> sillyB n.

通过案例分析可以得到一个简单的证明

intros. inversion H; inversion H0.
apply sB0. apply sB1.
apply sB0. apply sB1.

但是这里有一个明显重复的apply sB0. apply sB1.。

问:除了定义一种新的战术符号外，什么才是最佳的筛选方法呢？

使用T; [T1 | ... Tn]是没有帮助的，因为

intros. inversion H; inversion H0;
[apply sB0 | apply sB1].

有错误的战术数量，正确的形式

intros. inversion H; inversion H0;
[apply sB0 | apply sB1 | apply sB0 | apply sB1].

一点也不进步。我们需要的是一种类似于T; [T1 | ... Tn]的策略，但只将[T1 | ... Tn]应用于由前面的策略T生成的子目标，而不是整个分号链。如果我们有这样一个战术T; <T1 | ... Tn>，我们可以进一步缩短上述证据

intros. inversion H; inversion H0;
<apply sB0 | apply sB1>.

这个是可能的吗？

Answer 1

分组将做到这一点：

Theorem silly : forall n, sillyC n -> sillyB n.
intros. inversion H; (inversion H0; [apply sB0 | apply sB1]).