CODEWITHSUNDEEP
coq
iamwhoiam
iamwhoiam

Reputation: 287

Coq - overriding notion of equality to add elements to set

I was trying to use Coq's listSet to create a set of nats. However, I run into problems when adding members to the set.

Here is the code I'm running.

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)).

When run, the output is

= if eq_dec 0 0 then (0 :: nil)%list else (0 :: 0 :: nil)%list : set nat

Now, I know why I am getting the if-else statements in the output. It's because I have only told Coq that equality on nats is decidable but nothing about evaluating the equality. I also know how to compare two nats. The code for that is below.

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.

However, I am unable to string the two together to get the desired output which is

(0 :: nil)%list : set nat

I'd appreciate any help on this.

Upvotes: 1

Views: 689

Answers (1)

Tej Chajed
Tej Chajed

Reputation: 3948

Your function nats_equal isn't literally an implementation of the eq_dec axiom you wrote, since it returns a boolean without an associated proof. You can turn your axiom into a definition, using Coq's tactics to create the definition. Putting Defined. at the end means the definition is transparent, so that Coq can compute with it, but otherwise this is the same thing as when you start a Theorem, prove it, and end it with Qed.

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

In this case the proof was easy because Coq has a built-in tactic for proving decidable equality, which works even for recursive types.

That said, decidable equality for nats is already in the standard library, so you don't need to define it yourself:

(* 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} + {_ <> _}).

If you import PeanoNat you can refer to it with the nicer name Nat.eq_dec.

Upvotes: 8

Related Questions