Support multi-binding var expressions in Lean backend

Source/Provers/LeanAuto/LeanAutoGenerator.cs

@@ -364,17 +364,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;
   }
 

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» {

Test/lean-auto/lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:v4.9.0
+leanprover/lean4:v4.11.0

Test/lean-auto/multi-let.bpl

@@ -0,0 +1,10 @@
+// RUN: %parallel-boogie "%s" > "%t"
+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;
+}