为什么 Coqsolve_in_Union 策略直接失败，但通过断言相同目标起作用？

Question

我在 Coq 中遇到了一个令人困惑的情况，我正在与关系和合奏团合作。我已经定义了他们之间的强制以及解决会员目标的策略：

Require Import Lia Reals Lra Classical_sets List Ensembles Relations_1.
Import ListNotations.

Notation "x ∈ A" := (In _ A x) (at level 40).
Notation "A ⋃ B" := (Union _ A B) (at level 30).
Notation "⦃⦄" := (Empty_set _).
Notation ℝ := R.

Fixpoint list_to_ensemble {U : Type} (l : list U) : Ensemble U :=
  match l with
  | [] => ⦃⦄
  | x :: xs => Union U (Singleton U x) (list_to_ensemble xs)
  end.

Notation "⦃ x ⦄" := (Singleton _ x).
Notation "⦃ x , y , .. , z ⦄" :=
  (@list_to_ensemble _ (cons x (cons y .. (cons z nil) ..)))
  (format "⦃ x , y , .. , z ⦄").

Lemma In_Union_def : forall (U : Type) (A B : Ensemble U) (x : U),
  x ∈ (A ⋃ B) <-> x ∈ A \/ x ∈ B.
Proof.
  intros; split; [apply Union_inv | intros [H1 | H1]; [apply Union_introl; auto | apply Union_intror; auto]].
Qed.

Coercion rel_to_ens {A} (R : Relation A) : Ensemble (A * A) := 
  fun p => R (fst p) (snd p).

Coercion ens_to_rel {A} (E : Ensemble (A * A)) : Relation A := 
  fun x y => E (x,y).

Lemma x_y_In_implies_rel : forall A (R : Relation A) x y, (x, y) ∈ R <-> R x y.
Proof.
  intros; split; auto.
Qed.

Ltac solve_in_Union :=
  simpl; auto;
  match goal with
  | [ |- ?x ∈ Singleton _ _ ] => 
      apply Singleton_intro; (try reflexivity; try nia; try nra)
  | [ |- ?x ∈ Union _ ?A ?B ] => 
      apply In_Union_def; solve [ left; solve_in_Union | right; solve_in_Union ]
  | [ |- ?G ] => fail "Goal not solvable"
  end.

证明简单隶属属性时：

Section Example.
  Open Scope R_scope.
  Let R : Relation ℝ := ⦃ (1,1),(1,2),(1,3),(1,4),(2,3),(2,5),(2,6),(3,5),(4,5),(4,6) ⦄.

  Lemma lemma_example : R 1 1.
  Proof.
    apply x_y_In_implies_rel. unfold R. try solve_in_Union.
    assert ((1, 1) ∈ ⦃ (1,1),(1,2),(1,3),(1,4),(2,3),(2,5),(2,6),(3,5),(4,5),(4,6) ⦄) as H1 by solve_in_Union.
    auto.
  Qed.
End Example.

当我尝试使用 trysolve_in_Union 解决目标时，我的目标正是：

(1, 1) ∈ ⦃(1,1),(1,2),(1,3),(1,4),(2,3),(2,5),(2,6),(3,5),(4,5),(4,6)⦄

奇怪的是，直接使用solve_in_Union来实现这个目标失败了。但是，如果我断言完全相同的目标文本并尝试使用solve_in_Union 来证明它，它就会起作用：

更令人费解的是，如果我模式匹配目标并打印它：

match goal with
| [ |- ?G ] => idtac G
end.

它显示的文本与断言中的文本完全相同。 为什么solve_in_Union在最初的目标上失败了，但在同一目标的断言上却成功了？这两种看似相同的情况有什么根本区别？

对于我正在使用的 Coq 版本，当我在终端中输入 coqc -v 时，我得到

coqc-v Coq 证明助手，版本 8.19.2 使用 OCaml 5.2.0 编译

Answer 1

做

Set Printing All.

并敏锐地审视我们看到的目标 在第一种（非工作）情况下，目标是

In (prod RbaseSymbolsImpl.R RbaseSymbolsImpl.R)
  (@rel_to_ens RbaseSymbolsImpl.R
  (@ens_to_rel RbaseSymbolsImpl.R
  (@list_to_ensemble (prod RbaseSymbolsImpl.R RbaseSymbolsImpl.R)
  (@cons (prod RbaseSymbolsImpl.R RbaseSymbolsImpl.R)
  (@pair RbaseSymbolsImpl.R RbaseSymbolsImpl.R
  (IZR (Zpos xH)) (IZR (Zpos xH)))

  ....

在第二种（工作）情况下，目标是

In (prod RbaseSymbolsImpl.R RbaseSymbolsImpl.R)
  (@list_to_ensemble (prod RbaseSymbolsImpl.R RbaseSymbolsImpl.R)
  (@cons (prod RbaseSymbolsImpl.R RbaseSymbolsImpl.R)
  (@pair RbaseSymbolsImpl.R RbaseSymbolsImpl.R (IZR (Zpos xH))
  (IZR (Zpos xH)))

因此，强制

ens_to_rel

和

rel_to_ens

似乎以某种方式妨碍了匹配工作所需的展开。