消除Coq中案例分析生成的冗余子目标 [英] Eliminate redundant sub-goals generated by case analysis in Coq

问题描述

简单定义

Inductive B := bb.
Inductive C := cc.

Inductive A :=
 | mkA1 : B -> A
 | mkA2 : C -> A.

Definition id (a: A) : A :=
 match a with 
  | mkA1 b => mkA1 b 
  | mkA2 c => mkA2 c
end.

我尝试通过案例分析（销毁）来做证明，例如：

I try to do proofs by case analysis (destruct), something like:

Theorem Foo :
  forall  a1 a2 : A , a1 <> a2 -> id a1 <> id a2.
Proof.
 destruct a1; destruct a2.
 Abort.

不出所料，当前证明状态包含两个等效的子目标：

Unsurprisingly, the current prove state contains two equivalent sub-goals:

b: B
c: C
______________________________________(2/4)
mkA1 b <> mkA2 c -> id (mkA1 b) <> id (mkA2 c)
______________________________________(3/4)
mkA2 c <> mkA1 b -> id (mkA2 c) <> id (mkA1 b)

在我看来，重复的子目标在进行结构化案例时很常见分析。有一些通用的方法可以删除这些重复项吗？

It seems to me that duplicated sub-goals are quite often when doing structural case analysis. Is there some common way to remove these duplicates?

我要做的是按摩第二个子目标，使其看起来像第三个目标：

What I did is to massage the second sub-goal to look like the third:

Focus 2; 
intro; apply not_eq_sym in H; apply not_eq_sym; revert H;
Unfocus.

尽管我仍然没有办法要求Coq删除重复项。现在，我可以为第二个子目标证明引理，并在第三个子目标中重用它。但是我想知道一些替代方法。

Although I still have no way to ask Coq to remove the duplicates. Now I can prove a lemma for my second sub-goal, and reuse it in my third sub-goal. But I would like to know some alternatives.

推荐答案

以下是一些策略自动化，可以对子目标进行重复数据删除。请注意，不仅目标必须完全匹配，而且上下文的顺序也必须匹配。在进行案例分析之前，您还需要运行初始化策略。这是Coq> = 8.5的代码。

Here is some tactic automation that de-duplicates subgoals. Note that not only must the goals match exactly, but the ordering of the contexts must also match. You also need to run the initialization tactic before you do case analysis. This is code for Coq >= 8.5.

Inductive B := bb.
Inductive C := cc.

Inductive A :=
| mkA1 : B -> A
| mkA2 : C -> A.

Definition id (a: A) : A :=
  match a with
  | mkA1 b => mkA1 b
  | mkA2 c => mkA2 c
  end.

Record duplicate_prod (A B : Type) := duplicate_conj { duplicate_fst : A ; duplicate_snd : B }.
Definition HERE := True.

Ltac start_remove_duplicates H :=
  simple refine (let H___duplicates := @duplicate_conj _ _ I _ in _);
  [ shelve | | ]; cycle 1.
Ltac find_dup H G :=
  lazymatch type of H with
  | duplicate_prod G _ => constr:(@duplicate_fst _ _ H)
  | duplicate_prod _ _ => find_dup (@duplicate_snd _ _ H) G
  end.
Ltac find_end H :=
  lazymatch type of H with
  | duplicate_prod _ _ => find_end (@duplicate_snd _ _ H)
  | _ => H
  end.
Ltac revert_until H :=
  repeat lazymatch goal with
         | [ H' : _ |- _ ]
           => first [ constr_eq H H'; fail 1
                    | revert H' ]
         end.
Ltac remove_duplicates :=
  [ > lazymatch goal with
      | [ |- duplicate_prod _ _ ] => idtac
      | [ H : duplicate_prod _ _ |- _ ]
        => generalize (I : HERE);
           revert_until H;
           let G := match goal with |- ?G => G end in
           lazymatch type of H with
           | context[duplicate_prod G]
             => let lem := find_dup H G in exact lem
           | _ => let lem := find_end H in
                  refine (@duplicate_fst _ _ lem); clear H; (* clear to work around a bug in Coq *)
                  shelve
           end
      end.. ].
Ltac finish_duplicates :=
  [ > lazymatch goal with
      | [ H : duplicate_prod _ _ |- _ ] => clear H
      end..
  | repeat match goal with
           | [ |- duplicate_prod _ ?e ]
             => split;
                [ repeat lazymatch goal with
                         | [ |- HERE -> _ ] => fail
                         | _ => intro
                         end;
                  intros _
                | try (is_evar e; exact I) ]
           end ].


Theorem Foo :
  forall  a1 a2 : A , a1 <> a2 -> id a1 <> id a2.
Proof.
  start_remove_duplicates.
  destruct a1; destruct a2.
  2:intro; apply not_eq_sym in H; apply not_eq_sym; revert c b H; intros c b.
  all:remove_duplicates.
  all:finish_duplicates.

这个想法是，您首先创建一个evar，它将保存解决方案以实现独特的目标。然后您进行案例分析。然后，您要完成目标，并使用evar的最新预测来解决这些目标，或者，如果发现目标已经存在解决方案，则可以使用该解决方案。最后，您将evar分为多个（去重复的）目标。关于创建evar时不存在的假设的还原，还有一些其他样板（需要为适当类型的术语安抚变量作用域），记住最初来自上下文的内容，最后将这些内容重新引入上下文中

The idea is that you first create an evar that will hold the solutions to unique goals. Then you do the case analysis. Then you go through the goals, and solve them either with a fresh projection from the evar, or, if you see that there's already a solution to the goal you're looking at, you use that solution. Finally, you split up the evar into multiple (deduplicated) goals. There's some additional boilerplate around reverting hypotheses that didn't exist when you created the evar (necessary to appease variable scoping for well-typed terms), remembering which things came from the context originally, and reintroducing those things back into the context at the end.

这篇关于消除Coq中案例分析生成的冗余子目标的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！