From df5f771f29972b05650cbfd8d9e0e83c5295a737 Mon Sep 17 00:00:00 2001
From: Aaron Tomb <aarotomb@amazon.com>
Date: Wed, 28 Aug 2024 15:05:43 -0700
Subject: [PATCH 1/3] Allow multi-binding let expressions in Lean

---
 Source/Provers/LeanAuto/LeanAutoGenerator.cs | 20 ++++++++++++--------
 1 file changed, 12 insertions(+), 8 deletions(-)

diff --git a/Source/Provers/LeanAuto/LeanAutoGenerator.cs b/Source/Provers/LeanAuto/LeanAutoGenerator.cs
index 7bd3c533f..2b59cce28 100644
--- a/Source/Provers/LeanAuto/LeanAutoGenerator.cs
+++ b/Source/Provers/LeanAuto/LeanAutoGenerator.cs
@@ -369,17 +369,21 @@ public override Expr VisitLambdaExpr(LambdaExpr node)
 
   public override Expr VisitLetExpr(LetExpr node)
   {
-    if (node.Dummies.Count > 1) {
+    if (node.Dummies.Count != node.Rhss.Count) {
       throw new LeanConversionException(node.tok,
-        "Unsupported: LetExpr with more than one binder");
+        "Unsupported: LetExpr with differing LHS and RHS counts.");
+    }
+
+    var bindings = node.Dummies.Zip(node.Rhss);
+    foreach (var (x, e) in bindings) {
+      WriteText("(let ");
+      Visit(x.TypedIdent);
+      WriteText(" := ");
+      Visit(e);
+      WriteText("; ");
     }
-    WriteText("(let");
-    node.Dummies.ForEach(x => Visit(x.TypedIdent));
-    WriteText(" := ");
-    node.Rhss.ForEach(e => Visit(e));
-    WriteText("; ");
     Visit(node.Body);
-    WriteText(")");
+    bindings.ForEach(b => WriteText(")"));
     return node;
   }
 

From 8629183289e50a8b9c84f5192c05bacee90a6f87 Mon Sep 17 00:00:00 2001
From: Aaron Tomb <aarotomb@amazon.com>
Date: Wed, 13 Nov 2024 13:54:20 -0800
Subject: [PATCH 2/3] Add test for multiple let bindings

Also bump version of lean and lean-auto
---
 Test/lean-auto/lakefile.lean  | 2 +-
 Test/lean-auto/lean-toolchain | 2 +-
 Test/lean-auto/multi-let.bpl  | 9 +++++++++
 3 files changed, 11 insertions(+), 2 deletions(-)
 create mode 100644 Test/lean-auto/multi-let.bpl

diff --git a/Test/lean-auto/lakefile.lean b/Test/lean-auto/lakefile.lean
index 8d422d5e3..ae3b2c2d0 100644
--- a/Test/lean-auto/lakefile.lean
+++ b/Test/lean-auto/lakefile.lean
@@ -6,7 +6,7 @@ package «test» {
 }
 
 require auto from git
-  "https://github.com/leanprover-community/lean-auto"@"0831a6eff8cbb456e90c616bd2f4db51aefea3d0"
+  "https://github.com/leanprover-community/lean-auto"@"60e546ca7a9d40d508e58847a9d0630406835178"
 
 @[default_target]
 lean_lib «ToBuild» {
diff --git a/Test/lean-auto/lean-toolchain b/Test/lean-auto/lean-toolchain
index 4ef27c472..5a9c76dc9 100644
--- a/Test/lean-auto/lean-toolchain
+++ b/Test/lean-auto/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:v4.9.0
+leanprover/lean4:v4.11.0
diff --git a/Test/lean-auto/multi-let.bpl b/Test/lean-auto/multi-let.bpl
new file mode 100644
index 000000000..841e5e761
--- /dev/null
+++ b/Test/lean-auto/multi-let.bpl
@@ -0,0 +1,9 @@
+procedure P(x: int, y: int) {
+    var z: int;
+    var w: int;
+
+    z := (var a, b := x+1, y+1; a);
+    w := (var a, b := x+1, y+1; b);
+    assert (z - 1) == x;
+    assert (w - 1) == y;
+}

From 77f6a6a3b1b7aa94c7124867c96f44e84abea774 Mon Sep 17 00:00:00 2001
From: Aaron Tomb <aarotomb@amazon.com>
Date: Wed, 13 Nov 2024 14:26:31 -0800
Subject: [PATCH 3/3] Add lit header to new test

---
 Test/lean-auto/multi-let.bpl | 1 +
 1 file changed, 1 insertion(+)

diff --git a/Test/lean-auto/multi-let.bpl b/Test/lean-auto/multi-let.bpl
index 841e5e761..c93686468 100644
--- a/Test/lean-auto/multi-let.bpl
+++ b/Test/lean-auto/multi-let.bpl
@@ -1,3 +1,4 @@
+// RUN: %parallel-boogie "%s" > "%t"
 procedure P(x: int, y: int) {
     var z: int;
     var w: int;