From 2ec5eeca83a7233ec85e2a8e96232c1a5a4b8621 Mon Sep 17 00:00:00 2001
From: "Juan C." <38925412+JuanCoRo@users.noreply.github.com>
Date: Tue, 21 Jan 2025 18:02:53 +0100
Subject: [PATCH] Add uninterpreted `List` implementation to `Prelude.lean`
 (#4740)

Tackling #4725, this PR adds an uninterpreted implementation for the
`List` sort.

It also adds minor improvements to the `SetHookDef` module.
---
 pyk/src/pyk/k2lean4/Prelude.lean | 85 +++++++++++++++++++++++++++-----
 pyk/src/pyk/k2lean4/k2lean4.py   |  2 +-
 2 files changed, 74 insertions(+), 13 deletions(-)

diff --git a/pyk/src/pyk/k2lean4/Prelude.lean b/pyk/src/pyk/k2lean4/Prelude.lean
index ca8a3ff003..d8b5de0e97 100644
--- a/pyk/src/pyk/k2lean4/Prelude.lean
+++ b/pyk/src/pyk/k2lean4/Prelude.lean
@@ -108,23 +108,23 @@ If you intend to add an element to a set that might already be present in the se
  -/
 
 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
+  set          : Type -- Carrier, such as `T → Prop`
+  unit         : set
+  concat       : set → set → Option set
+  element      : 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
+  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 elementAx      : T → setCAx
 axiom unionAx        : setCAx → setCAx → setCAx
 axiom intersectionAx : setCAx → setCAx → setCAx
 axiom differenceAx   : setCAx → setCAx → setCAx
@@ -137,7 +137,7 @@ noncomputable def SetHook (T : Type) : SetHookSig T :=
   { set          := setCAx,
     unit         := unitAx,
     concat       := concatAx,
-    setItem      := setItemAx T,
+    element      := elementAx T,
     union        := unionAx,
     intersection := intersectionAx,
     difference   := differenceAx,
@@ -148,6 +148,67 @@ noncomputable def SetHook (T : Type) : SetHookSig T :=
 
 end SetHookDef
 
+namespace ListHookDef
+/-
+The `List` sort is an ordered collection that may contain duplicate elements.
+ -/
+
+structure listHookSig (T : Type) where
+  list      : Type -- Carrier, such as `T → Prop`
+  unit      : list
+  concat    : list → list → Option list
+  element   : T → list
+  push      : T → list → list
+  get       : Int → list → Option T
+  updte     : Int → T → list → Option list
+  -- create a list with `length` elements, each containing  `value`. `Option` return type from `Int` parameter
+  make      : Int → T → Option list
+  -- create a new `List` which is equal to `dest` except the  `N` elements starting at `index` are replaced with the   contents of `src`
+  -- Having `index + size(src) > size(dest)` is undefined
+  -- updateList(dest: List, index: Int, src: List)
+  updateAll : list → Int → list → Option list
+  -- create a new `List` where the `length` elements starting   at `index` are replaced with `value`
+  fill      : list → Int → T → Option list
+  -- compute a new `List` by removing `fromFront` elements from   the front of the list and `fromBack` elements from the back   of the list
+  -- range(List, fromFront: Int, fromBack: Int)
+  range     : list → Int → Int → Option list
+  -- compute whether an element is in a list
+  -- the hook is `in`, but clashes with Lean syntax
+  inList    : T → list → Bool
+  size      : list → Int
+
+variable (T : Type)
+axiom listCAx     : Type
+axiom unitAx      : listCAx
+axiom concatAx    : listCAx → listCAx → Option listCAx
+axiom elementAx   : T → listCAx
+axiom pushAx      : T → listCAx → listCAx
+axiom getAx       : Int → listCAx → Option T
+axiom updteAx     : Int → T → listCAx → Option listCAx
+axiom makeAx      : Int → T → Option listCAx
+axiom updateAllAx : listCAx → Int → listCAx → Option listCAx
+axiom fillAx      : listCAx → Int → T → Option listCAx
+axiom rangeAx     : listCAx → Int → Int → Option listCAx
+axiom inListAx    : T → listCAx → Bool
+axiom sizeAx      : listCAx → Int
+
+noncomputable def ListHook (T : Type) : listHookSig T :=
+  { list      := listCAx,
+    unit      := unitAx,
+    concat    := concatAx,
+    element   := elementAx T,
+    push      := pushAx T,
+    get       := getAx T,
+    updte     := updteAx T,
+    make      := makeAx T,
+    updateAll := updateAllAx,
+    fill      := fillAx T,
+    range     := rangeAx,
+    inList    := inListAx T,
+    size      := sizeAx }
+
+end ListHookDef
+
 class Inj (From To : Type) : Type where
   inj (x : From) : To
 
diff --git a/pyk/src/pyk/k2lean4/k2lean4.py b/pyk/src/pyk/k2lean4/k2lean4.py
index 194e81b416..b05f0a02f9 100644
--- a/pyk/src/pyk/k2lean4/k2lean4.py
+++ b/pyk/src/pyk/k2lean4/k2lean4.py
@@ -150,7 +150,7 @@ def _collection(self, sort: str) -> Structure:
         match coll.kind:
             case CollectionKind.LIST:
                 (item,) = sorts
-                val = Term(f'List {item}')
+                val = Term(f'(ListHook {item}).list')
             case CollectionKind.SET:
                 (item,) = sorts
                 val = Term(f'(SetHook {item}).set')