时间戳

首页 > 解决方案 > Ltac：在每个目标中做一些不同的事情

coq - Ltac：在每个目标中做一些不同的事情

问题描述

我有一个证明脚本，我正在探索多个案例，目前速度很慢，因为我有许多解决目标的策略，并且我正在尝试每个案例中的每一个。

我知道在某些情况下我需要应用某些策略，但我不确定如何做到这一点。

这是我现在拥有的：

induction e;
    intros;
    pose (bool_dec (is_v_of_expr e1)) as ve1; destruct ve1;
    [> thing1 | thing 2].

这给出了错误Incorrect number of goals (expected 26 tactics, was given 2)。

对于归纳产生的每种情况，我都试图thing1在第一个目标destruct和thing2第二个目标中做。destruct

问题是，induction生成 13 个子目标，每个子目标被分成 2 个destruct。本地选择器[> thing1 | thing2 ]试图匹配所有子目标，而不仅仅是特定破坏产生的子目标。

我如何对策略进行排序，以便destruct在归纳生成的每个案例上thing1运行，然后在第一个破坏生成的目标上thing2运行，然后在第二个生成的目标上运行，对于每个归纳案例。

标签： coqdependent-typetheorem-provingcoq-tacticltac

解决方案

你有两个问题：（1）分号默认是左结合的，（2）[> ]语法适用于所有重点目标，而不仅仅是前一种策略产生的目标。 （正如杰森所指出的，这种解释是不正确的，但答案仍然有效：）

您可以通过将分号与括号更改并右关联[> ]来解决这些问题：[ ]

Goal ((True /\ True) /\ (True /\ True) /\ (True /\ True)).
  Fail (split; [|split]); split; [> exact I | exact I].
  (split; [|split]); (split; [exact I | exact I]).
Qed.

在您的示例中：

induction e; intros;
  pose (bool_dec (is_v_of_expr e1)) as ve1;
  (destruct ve1; [thing1 | thing 2]).

推荐阅读