我在 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 编译