COQ-覆盖平等的概念以添加设置的元素

Question

我试图使用COQ的listSet创建nats的set。但是，在将成员添加到集合时，我会遇到问题。

这是我正在运行的代码。

Require Import ListSet Nat.
Axiom eq_dec : forall x y : nat, {x = y} + {x <> y}.
Compute (set_add eq_dec 0 (set_add eq_dec 0 nil)).

运行时，输出为

=如果eq_dec 0 0，则（0 :: nil）％列表else（0 :: 0 :: nil）％列表 ：设置nat

现在，我知道为什么我在输出中获取if-else语句。这是因为我只告诉COQ，nats上的平等是可决定的，但没有评估平等的平等。我也知道如何比较两个nats。该代码在下面。

Fixpoint nats_equal (m n : nat) : bool :=
  match m, n with
    | 0, 0 => true
    | 0, _ => false
    | _, 0 => false
    | S m', S n' => nats_equal m' n'
  end.

但是，我无法将两者串在一起以获取所需的输出

（0 :: nil）％列表：设置nat

我感谢对此的任何帮助。

Answer 1

您的函数nats_equal实际上不是您编写的eq_dec Axiom的实现，因为它返回了没有相关证明的布尔值。您可以使用COQ的策略来创建定义，将公理变成定义。将Defined.放在末尾意味着定义是透明的，因此Coq可以使用它进行计算，但是否则，这与启动Theorem时相同，证明并用Qed结束。

。

Definition eq_dec : forall x y : nat, {x = y} + {x <> y}.
  decide equality.
Defined.

在这种情况下，证明很容易，因为COQ具有证明可决定平等的内置策略，即使适用于递归类型。

也就是说，NAT的可决定性平等已经在标准库中，因此您无需自己定义它：

(* how to even search for the type in eq_dec? *)
Locate "{".
(* Notation
"{ A } + { B }" := sumbool A B : type_scope (default interpretation)
*)
(* now we know what the notation means and can search for it: *)
Search sumbool nat.
(* PeanoNat.Nat.eq_dec: forall n m : nat, {n = m} + {n <> m} *)
(* alternately, we can use some more specific searches: *)
Search (forall (_ _:nat), {_ = _} + {_ <> _}).
Search ({@eq nat _ _} + {_ <> _}).
(* same as above, but use special notation for equality at a specific type *)
Search ({_ = _ :> nat} + {_ <> _}).

如果导入peanonat，则可以使用较好的名称Nat.eq_dec。