主页 / coding / 问题 / 79139888
Accepted
Sterling1111
Asked: 2024-10-30 14:32:35 +0800 CST

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

  • 772

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

coq

1 个回答

  1. Best Answer

    仔细观察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了匹配工作所需的展开。

    事实上，所有这些都相当拗口，当我们发现了问题之后，最好直接做Set Printing Coercions.

    因此 R 是Relation具有强制的，但断言中的术语是Ensemble。

    Definition your_R : Relation R := ⦃ (1,1), (1,2) ⦄.
Definition your_assert  := ⦃ (1,1), (1,2) ⦄.
Set Printing All.
Print X.
Print Y.

    印刷

    X = ens_to_rel ⦃(1, 1),(1, 2)⦄
 : Relation ℝ

Y = ⦃(1, 1),(1, 2)⦄
 : Ensemble (ℝ * ℝ)

    没有与前者相匹配的规则，这就是 Ltacsolve_in_Union失败的原因。

    具体来说，你的目标是

    (1, 1) ∈ rel_to_ens (ens_to_rel ⦃(1, 1),(1, 2)⦄)

    由于这两个强制不是定义上的逆，因此无法简化。它们是部分应用函数，无法进一步简化。

    • 1

相关问题