Coq - Überschreiben von Gleichheit zum Hinzufügen von Elementen zum Set

Question

Ich habe versucht, Coq listSet verwenden, um eine setnats zu erstellen. Ich habe jedoch Probleme beim Hinzufügen von Mitgliedern zum Set.

Hier ist der Code, den ich verwende.

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

Wenn er gestartet wird, ist der Ausgang

= if eq_dec 0 0 then (0 :: nil)% Liste sonst (0 :: 0 :: nil)% Liste : set nat

Jetzt weiß ich, warum ich die if-else Aussagen in der Ausgabe immer bin. Es ist, weil ich Coq nur gesagt habe, dass die Gleichheit auf nats entscheidbar ist, aber nichts über die Bewertung der Gleichheit. Ich weiß auch wie zwei nats zu vergleichen. Der Code dafür ist unten.

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. 

Allerdings bin ich die beiden zusammen zu String nicht in der Lage die gewünschte Ausgabe zu erhalten, die

ist

(0 :: nil)% Liste: set nat

Ich würde schätze jede Hilfe zu diesem Thema.

Answer 1

Ihre Funktion nats_equal ist nicht wörtlich eine Implementierung des eq_dec Axioms, die Sie geschrieben haben, da sie einen Booleschen Wert ohne einen zugehörigen Beweis zurückgibt. Sie können Ihr Axiom in eine Definition umwandeln, indem Sie Coqs Taktiken verwenden, um die Definition zu erstellen. Putting Defined. am Ende bedeutet, dass die Definition transparent ist, so dass Coq damit berechnen kann, aber ansonsten ist das das gleiche wie wenn Sie eine Theorem starten, beweisen Sie es, und beenden Sie es mit Qed.

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

In diesem Fall war der Beweis, einfach, weil Coq eine eingebaute in Taktik für den Nachweis entscheidbar Gleichheit hat, die auch für rekursive Typen arbeitet.

Das heißt, entscheidbar Gleichheit für NATs ist bereits in der Standardbibliothek, so brauchen Sie nicht, es selbst zu definieren:

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

Wenn Sie importieren PeanoNat Sie Nat.eq_dec, um es mit dem schöneren Namen verweisen .