如何对 Coq 中的重复假设进行分组？

Question

我有

1 subgoals, subgoal 1
n : nat
b : bool
m : nat
H1: P1
H2: P2
H3: P1
H4: P2
=========
some_goal

在我运行战术auto_group_duplicates之后，它将变成

1 subgoals, subgoal 1
n, m : nat
b : bool
H1, H3: P1
H2, H4: P2
=========
some_goal

有这样的战术吗？

Answer 1

您可以手动使用 move 策略（参见 https://coq.inria.fr/refman/proof-engine/tactics.html?highlight=top#coq:tacn.move-%E2%80%A6-after-%E2%80%A6）来重新排列假设。

我怀疑是否存在像您正在寻找的那样的通用自动策略，但人们可能会想出一种基于 match-goal 的奇特策略，以使用该策略作为基本块来自动重新排列假设，虽然这超出了我的能力范围。

Answer 2

我不认为有这样的策略。但是你总是可以使用 Ltac 想出一些东西。

From Coq Require Import Utf8.

Definition mark {A : Type} (x : A) := x.

Ltac bar :=
  match goal with
  | x : ?A, y : ?A |- _ =>
    lazymatch A with
    | context [ mark ] => fail
    | _ =>
      move y after x ;
      change A with (mark A) in x
    end
  end.

Ltac remove_marks :=
  repeat match goal with
  | x : mark ?A |- _ =>
    change (mark A) with A in x
  end.

Ltac auto_group_duplicates :=
  repeat bar ; remove_marks.

Lemma foo :
  ∀ (n : nat) (b : bool) (m : nat) (c : bool),
    n = m →
    b = c →
    n = m →
    b = c →
    n = m →
    True.
Proof.
  intros n b m c e1 e2 e3 e4 e5.
  auto_group_duplicates.
  auto_group_duplicates.

这里我不得不应用这个策略两次，因为 Ltac 将 A 与 mark A 统一起来很烦人。

如何对 Coq 中的重复假设进行分组？

How to group duplicated hypothesis in Coq?

coq

coq-tactic