From 74cec6eefc055c769123db6d4919fe5054aa4387 Mon Sep 17 00:00:00 2001 From: Juan Conejero Date: Mon, 20 Jan 2025 16:29:30 +0100 Subject: [PATCH 1/4] Remove vacuous parenthesis in `MapHook` --- pyk/src/pyk/k2lean4/Prelude.lean | 22 +++++++++++----------- 1 file changed, 11 insertions(+), 11 deletions(-) diff --git a/pyk/src/pyk/k2lean4/Prelude.lean b/pyk/src/pyk/k2lean4/Prelude.lean index d0aed86a96..e4fb889c07 100644 --- a/pyk/src/pyk/k2lean4/Prelude.lean +++ b/pyk/src/pyk/k2lean4/Prelude.lean @@ -81,22 +81,22 @@ 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 From 49c5e17e3e75905a49f6f1ab41a33790c772580c Mon Sep 17 00:00:00 2001 From: Juan Conejero Date: Mon, 20 Jan 2025 16:29:53 +0100 Subject: [PATCH 2/4] Add `SetHookDef` module --- pyk/src/pyk/k2lean4/Prelude.lean | 51 ++++++++++++++++++++++++++++++++ 1 file changed, 51 insertions(+) diff --git a/pyk/src/pyk/k2lean4/Prelude.lean b/pyk/src/pyk/k2lean4/Prelude.lean index e4fb889c07..3d0788b2de 100644 --- a/pyk/src/pyk/k2lean4/Prelude.lean +++ b/pyk/src/pyk/k2lean4/Prelude.lean @@ -100,6 +100,57 @@ noncomputable def MapHook (K V : Type) : MapHookSig K V := 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 From 07f80c7a197d6baeb240bdba14a394388cc48dcc Mon Sep 17 00:00:00 2001 From: Juan Conejero Date: Mon, 20 Jan 2025 16:30:21 +0100 Subject: [PATCH 3/4] Change generated `Set` implementation --- pyk/src/pyk/k2lean4/k2lean4.py | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/pyk/src/pyk/k2lean4/k2lean4.py b/pyk/src/pyk/k2lean4/k2lean4.py index 7653c89c8a..194e81b416 100644 --- a/pyk/src/pyk/k2lean4/k2lean4.py +++ b/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') From 64d8adf6ec2be8ba66c00f9e7aceb6069743b7c1 Mon Sep 17 00:00:00 2001 From: Juan Conejero Date: Mon, 20 Jan 2025 16:53:03 +0100 Subject: [PATCH 4/4] Better typesetting of `SetHookDef` description --- pyk/src/pyk/k2lean4/Prelude.lean | 9 +++------ 1 file changed, 3 insertions(+), 6 deletions(-) diff --git a/pyk/src/pyk/k2lean4/Prelude.lean b/pyk/src/pyk/k2lean4/Prelude.lean index 3d0788b2de..ca8a3ff003 100644 --- a/pyk/src/pyk/k2lean4/Prelude.lean +++ b/pyk/src/pyk/k2lean4/Prelude.lean @@ -102,12 +102,9 @@ 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. +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