Add uninterpreted Set implementation to Prelude.lean

pyk/src/pyk/k2lean4/Prelude.lean

@@ -81,25 +81,73 @@ axiom nodupAx      : forall m, List.Nodup (keysAx K m)
 noncomputable def MapHook (K V : Type) : MapHookSig K V :=
   { map        := mapCAx,
     unit       := unitAx,
-    cons       := (consAx K V),
-    lookup     := (lookupAx K V),
-    lookup?    := (lookupAx? K V),
-    update     := (updateAx K V),
-    delete     := (deleteAx K),
+    cons       := consAx K V,
+    lookup     := lookupAx K V,
+    lookup?    := lookupAx? K V,
+    update     := updateAx K V,
+    delete     := deleteAx K,
     concat     := concatAx,
     difference := differenceAx,
     updateMap  := updateMapAx,
-    removeAll  := (removeAllAx K),
-    keys       := (keysAx K),
-    in_keys    := (in_keysAx K),
-    values     := (valuesAx V),
+    removeAll  := removeAllAx K,
+    keys       := keysAx K,
+    in_keys    := in_keysAx K,
+    values     := valuesAx V,
     size       := sizeAx,
     includes   := includesAx,
-    choice     := (choiceAx K),
-    nodup      := (nodupAx K) }
+    choice     := choiceAx K,
+    nodup      := nodupAx K }
 
 end MapHookDef
 
+namespace SetHookDef
+/-
+Implementation of immutable, associative, commutative sets of `KItem`.
+The sets are nilpotent, i.e., the concatenation of two sets containing elements in common is `#False` (note however, this may be silently allowed during concrete execution).
+If you intend to add an element to a set that might already be present in the set, use the `|Set` operator instead.
+ -/
+
+structure SetHookSig (T : Type) where
+  set : Type -- Carrier, such as `T → Prop`
+  unit : set
+  concat : set → set → Option set
+  setItem : T → set
+  union : set → set → set
+  intersection : set → set → set
+  difference : set → set → set
+  inSet : T → set → Bool
+  inclusion : set → set → Bool
+  size : set → Int
+  choice : set → T
+
+variable (T : Type)
+axiom setCAx         : Type
+axiom unitAx         : setCAx
+axiom concatAx       : setCAx → setCAx → Option setCAx
+axiom setItemAx      : T → setCAx
+axiom unionAx        : setCAx → setCAx → setCAx
+axiom intersectionAx : setCAx → setCAx → setCAx
+axiom differenceAx   : setCAx → setCAx → setCAx
+axiom inSetAx        : T → setCAx → Bool
+axiom inclusionAx    : setCAx → setCAx → Bool
+axiom sizeAx         : setCAx → Int
+axiom choiceAx       : setCAx → T
+
+noncomputable def SetHook (T : Type) : SetHookSig T :=
+  { set          := setCAx,
+    unit         := unitAx,
+    concat       := concatAx,
+    setItem      := setItemAx T,
+    union        := unionAx,
+    intersection := intersectionAx,
+    difference   := differenceAx,
+    inSet        := inSetAx T,
+    inclusion    := inclusionAx,
+    size         := sizeAx,
+    choice       := choiceAx T }
+
+end SetHookDef
+
 class Inj (From To : Type) : Type where
   inj (x : From) : To
 

pyk/src/pyk/k2lean4/k2lean4.py

@@ -153,7 +153,7 @@ def _collection(self, sort: str) -> Structure:
                 val = Term(f'List {item}')
             case CollectionKind.SET:
                 (item,) = sorts
-                val = Term(f'List {item}')
+                val = Term(f'(SetHook {item}).set')
             case CollectionKind.MAP:
                 key, value = sorts
                 val = Term(f'(MapHook {key} {value}).map')