Coq - 覆盖相等概念以添加要设置的元素

Question

我试图用勒柯克的listSet创建set的nats.但是,在向集合添加成员时遇到问题.

这是我正在运行的代码.

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)%list else(0 :: 0 :: nil)%list:set 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)%list:set nat

我很感激你的帮助.

Answer 1

你的函数nats_equal实际上并不是eq_dec你写的公理的实现,因为它返回一个没有相关证明的布尔值.你可以使用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.