From 8c4c4a6306dfd855daa81560c8e1d09625a29be7 Mon Sep 17 00:00:00 2001
From: Rustan Leino <leino@amazon.com>
Date: Fri, 11 Oct 2024 23:21:26 -0700
Subject: [PATCH 01/16] chore: Improve trigger/induction code

# Conflicts:
#	Source/DafnyCore/Verifier/Statements/BoogieGenerator.TrForallStmt.cs
---
 Source/DafnyCore/Resolver/ModuleResolver.cs   |  2 +-
 Source/DafnyCore/Rewriters/IRewriter.cs       |  2 +-
 .../DafnyCore/Rewriters/InductionRewriter.cs  | 68 ++++++++++---------
 .../Rewriters/TriggerGeneratingRewriter.cs    |  4 +-
 .../Triggers/ComprehensionTriggerGenerator.cs |  2 +-
 .../Triggers/QuantifiersCollector.cs          | 24 ++++---
 .../BoogieGenerator.ExpressionTranslator.cs   |  9 +--
 .../Verifier/BoogieGenerator.Methods.cs       |  1 +
 .../BoogieGenerator.TrForallStmt.cs           | 33 +++++----
 9 files changed, 80 insertions(+), 65 deletions(-)

diff --git a/Source/DafnyCore/Resolver/ModuleResolver.cs b/Source/DafnyCore/Resolver/ModuleResolver.cs
index ae9de04f6b2..c012f2bd652 100644
--- a/Source/DafnyCore/Resolver/ModuleResolver.cs
+++ b/Source/DafnyCore/Resolver/ModuleResolver.cs
@@ -174,7 +174,7 @@ public void ComputeIsRecursiveBit(CompilationData compilation, ModuleDefinition
       }
 
       foreach (var rewriter in rewriters) {
-        rewriter.PostCyclicityResolve(module, Reporter);
+        rewriter.PostCyclicityResolve(module);
       }
     }
 
diff --git a/Source/DafnyCore/Rewriters/IRewriter.cs b/Source/DafnyCore/Rewriters/IRewriter.cs
index 0a16b6fd953..8fd56e4bfef 100644
--- a/Source/DafnyCore/Rewriters/IRewriter.cs
+++ b/Source/DafnyCore/Rewriters/IRewriter.cs
@@ -76,7 +76,7 @@ internal virtual void PostResolveIntermediate(ModuleDefinition moduleDefinition)
     /// <param name="moduleDefinition">A module definition after it
     ///   is resolved, type-checked and SCC/Cyclicity/Recursivity have been performed</param>
     /// <param name="errorReporter"></param>
-    internal virtual void PostCyclicityResolve(ModuleDefinition moduleDefinition, ErrorReporter errorReporter) {
+    internal virtual void PostCyclicityResolve(ModuleDefinition moduleDefinition) {
       Contract.Requires(moduleDefinition != null);
     }
 
diff --git a/Source/DafnyCore/Rewriters/InductionRewriter.cs b/Source/DafnyCore/Rewriters/InductionRewriter.cs
index 03b8e06f0ba..faeb66ebc58 100644
--- a/Source/DafnyCore/Rewriters/InductionRewriter.cs
+++ b/Source/DafnyCore/Rewriters/InductionRewriter.cs
@@ -1,5 +1,6 @@
 using System.Collections.Generic;
 using System.Diagnostics.Contracts;
+using JetBrains.Annotations;
 using static Microsoft.Dafny.RewriterErrors;
 
 namespace Microsoft.Dafny;
@@ -40,12 +41,9 @@ internal override void PostDecreasesResolve(ModuleDefinition m) {
           }
         }
 
-        if (decl is NewtypeDecl) {
-          var nt = (NewtypeDecl)decl;
-          if (nt.Constraint != null) {
-            var visitor = new Induction_Visitor(this);
-            visitor.Visit(nt.Constraint);
-          }
+        if (decl is NewtypeDecl { Constraint: { } constraint }) {
+          var visitor = new InductionVisitor(this);
+          visitor.Visit(constraint);
         }
       }
     }
@@ -53,7 +51,7 @@ internal override void PostDecreasesResolve(ModuleDefinition m) {
 
   void ProcessMethodExpressions(Method method) {
     Contract.Requires(method != null);
-    var visitor = new Induction_Visitor(this);
+    var visitor = new InductionVisitor(this);
     method.Req.ForEach(mfe => visitor.Visit(mfe.E));
     method.Ens.ForEach(mfe => visitor.Visit(mfe.E));
     if (method.Body != null) {
@@ -63,7 +61,7 @@ void ProcessMethodExpressions(Method method) {
 
   void ProcessFunctionExpressions(Function function) {
     Contract.Requires(function != null);
-    var visitor = new Induction_Visitor(this);
+    var visitor = new InductionVisitor(this);
     function.Req.ForEach(visitor.Visit);
     function.Ens.ForEach(visitor.Visit);
     if (function.Body != null) {
@@ -73,20 +71,29 @@ void ProcessFunctionExpressions(Function function) {
 
   void ComputeLemmaInduction(Method method) {
     Contract.Requires(method != null);
-    if (method.Body != null && method.IsGhost && method.Mod.Expressions.Count == 0 && method.Outs.Count == 0 &&
-        !(method is ExtremeLemma)) {
-      var specs = new List<Expression>();
-      method.Req.ForEach(mfe => specs.Add(mfe.E));
-      method.Ens.ForEach(mfe => specs.Add(mfe.E));
-      ComputeInductionVariables(method.tok, method.Ins, specs, method, ref method.Attributes);
+    if (method is Lemma or PrefixLemma && method is { Body: not null, Outs: { Count: 0 } }) {
+      Expression pre = Expression.CreateBoolLiteral(method.tok, true);
+      foreach (var req in method.Req) {
+        pre = Expression.CreateAnd(pre, req.E);
+      }
+      Expression post = Expression.CreateBoolLiteral(method.tok, true);
+      foreach (var ens in method.Ens) {
+        post = Expression.CreateAnd(post, ens.E);
+      }
+      ComputeInductionVariables(method.tok, method.Ins, Expression.CreateImplies(pre, post), method, ref method.Attributes);
     }
   }
 
-  void ComputeInductionVariables<VarType>(IToken tok, List<VarType> boundVars, List<Expression> searchExprs,
-    Method lemma, ref Attributes attributes) where VarType : class, IVariable {
+  /// <summary>
+  /// Look at the command-line options and any {:induction} attribute to determine a good list of induction
+  /// variables. If there are any, then record them in an attribute {:_induction ...} added to "attributes".
+  /// "body" is the condition that the induction would support.
+  /// </summary>
+  void ComputeInductionVariables<TVarType>(IToken tok, List<TVarType> boundVars, Expression body,
+    [CanBeNull] Method lemma, ref Attributes attributes) where TVarType : class, IVariable {
     Contract.Requires(tok != null);
     Contract.Requires(boundVars != null);
-    Contract.Requires(searchExprs != null);
+    Contract.Requires(body != null);
     Contract.Requires(Reporter.Options.Induction != 0);
 
     var args = Attributes.FindExpressions(attributes,
@@ -106,9 +113,9 @@ void ComputeInductionVariables<VarType>(IToken tok, List<VarType> boundVars, Lis
     } else if (args.Count == 0) {
       // {:induction} is treated the same as {:induction true}, which says to automatically infer induction variables
       // GO INFER below (all boundVars)
-    } else if (args.Count == 1 && args[0] is LiteralExpr && ((LiteralExpr)args[0]).Value is bool) {
+    } else if (args.Count == 1 && args[0] is LiteralExpr { Value: bool and var boolValue }) {
       // {:induction false} or {:induction true}
-      if (!(bool)((LiteralExpr)args[0]).Value) {
+      if (!boolValue) {
         // we're told not to infer anything
         return;
       }
@@ -117,12 +124,11 @@ void ComputeInductionVariables<VarType>(IToken tok, List<VarType> boundVars, Lis
       // Here, we're expecting the arguments to {:induction args} to be a sublist of "this;boundVars", where "this" is allowed only
       // if "lemma" denotes an instance lemma.
       var goodArguments = new List<Expression>();
-      var i = lemma != null && !lemma.IsStatic
+      var i = lemma is { IsStatic: false }
         ? -1
         : 0; // -1 says it's okay to see "this" or any other parameter; 0 <= i says it's okay to see parameter i or higher
       foreach (var arg in args) {
-        var ie = arg.Resolved as IdentifierExpr;
-        if (ie != null) {
+        if (arg.Resolved is IdentifierExpr ie) {
           var j = boundVars.FindIndex(v => v == ie.Var);
           if (0 <= j && i <= j) {
             goodArguments.Add(ie);
@@ -163,15 +169,15 @@ void ComputeInductionVariables<VarType>(IToken tok, List<VarType> boundVars, Lis
 
     // Okay, here we go, coming up with good induction setting for the given situation
     var inductionVariables = new List<Expression>();
-    if (lemma != null && !lemma.IsStatic) {
-      if (args != null || searchExprs.Exists(expr => FreeVariablesUtil.ContainsFreeVariable(expr, true, null))) {
+    if (lemma is { IsStatic: false }) {
+      if (args != null || FreeVariablesUtil.ContainsFreeVariable(body, true, null)) {
         inductionVariables.Add(new ThisExpr(lemma));
       }
     }
 
     foreach (IVariable n in boundVars) {
-      if (!(n.Type.IsTypeParameter || n.Type.IsAbstractType || n.Type.IsInternalTypeSynonym) && (args != null ||
-            searchExprs.Exists(expr => InductionHeuristic.VarOccursInArgumentToRecursiveFunction(Reporter.Options, expr, n)))) {
+      if (!(n.Type.IsTypeParameter || n.Type.IsAbstractType || n.Type.IsInternalTypeSynonym) &&
+          (args != null || InductionHeuristic.VarOccursInArgumentToRecursiveFunction(Reporter.Options, body, n))) {
         inductionVariables.Add(new IdentifierExpr(n.Tok, n));
       }
     }
@@ -189,19 +195,17 @@ void ComputeInductionVariables<VarType>(IToken tok, List<VarType> boundVars, Lis
     }
   }
 
-  class Induction_Visitor : BottomUpVisitor {
+  class InductionVisitor : BottomUpVisitor {
     readonly InductionRewriter IndRewriter;
 
-    public Induction_Visitor(InductionRewriter inductionRewriter) {
+    public InductionVisitor(InductionRewriter inductionRewriter) {
       Contract.Requires(inductionRewriter != null);
       IndRewriter = inductionRewriter;
     }
 
     protected override void VisitOneExpr(Expression expr) {
-      var q = expr as QuantifierExpr;
-      if (q != null && q.SplitQuantifier == null) {
-        IndRewriter.ComputeInductionVariables(q.tok, q.BoundVars, new List<Expression>() { q.LogicalBody() }, null,
-          ref q.Attributes);
+      if (expr is QuantifierExpr { SplitQuantifier: null } q) {
+        IndRewriter.ComputeInductionVariables(q.tok, q.BoundVars, q.LogicalBody(), null, ref q.Attributes);
       }
     }
   }
diff --git a/Source/DafnyCore/Rewriters/TriggerGeneratingRewriter.cs b/Source/DafnyCore/Rewriters/TriggerGeneratingRewriter.cs
index e8283ee85e0..e676be5dfcb 100644
--- a/Source/DafnyCore/Rewriters/TriggerGeneratingRewriter.cs
+++ b/Source/DafnyCore/Rewriters/TriggerGeneratingRewriter.cs
@@ -9,8 +9,8 @@ internal TriggerGeneratingRewriter(ErrorReporter reporter, SystemModuleManager s
     this.systemModuleManager = systemModuleManager;
   }
 
-  internal override void PostCyclicityResolve(ModuleDefinition definition, ErrorReporter reporter) {
-    var finder = new Triggers.QuantifierCollector(reporter);
+  internal override void PostCyclicityResolve(ModuleDefinition definition) {
+    var finder = new Triggers.QuantifierCollector(Reporter);
 
     foreach (var decl in ModuleDefinition.AllCallablesIncludingPrefixDeclarations(definition.TopLevelDecls)) {
       finder.Visit(decl, null);
diff --git a/Source/DafnyCore/Triggers/ComprehensionTriggerGenerator.cs b/Source/DafnyCore/Triggers/ComprehensionTriggerGenerator.cs
index be69c3977c4..15b9fc0edb9 100644
--- a/Source/DafnyCore/Triggers/ComprehensionTriggerGenerator.cs
+++ b/Source/DafnyCore/Triggers/ComprehensionTriggerGenerator.cs
@@ -122,7 +122,7 @@ bool DetectAndFilterLoopingCandidates() {
       // In addition, we ignore cases where the only differences between a trigger
       // and a trigger match are places where a variable is replaced with an
       // expression whose free variables do not intersect that of the quantifier
-      // in which that expression is found. For examples of this behavious, see
+      // in which that expression is found. For examples of this behavior, see
       // triggers/literals-do-not-cause-loops.
       // This ignoring logic is implemented by the CouldCauseLoops method.
       bool foundLoop = false;
diff --git a/Source/DafnyCore/Triggers/QuantifiersCollector.cs b/Source/DafnyCore/Triggers/QuantifiersCollector.cs
index 1f169e161ba..869640da766 100644
--- a/Source/DafnyCore/Triggers/QuantifiersCollector.cs
+++ b/Source/DafnyCore/Triggers/QuantifiersCollector.cs
@@ -7,6 +7,7 @@
 using System.Text;
 using System.Collections.ObjectModel;
 using System.Diagnostics.Contracts;
+using JetBrains.Annotations;
 
 namespace Microsoft.Dafny.Triggers {
   internal class QuantifierCollector : TopDownVisitor<OldExpr/*?*/> {
@@ -20,21 +21,24 @@ public QuantifierCollector(ErrorReporter reporter) {
       this.reporter = reporter;
     }
 
+    public void AddComprehension(ComprehensionExpr comprehensionExpr, [CanBeNull] List<Expression> splitQuantifier) {
+      quantifiers.Add(comprehensionExpr);
+      if (splitQuantifier != null) {
+        var collection = splitQuantifier.OfType<ComprehensionExpr>();
+        quantifierCollections.Add(new ComprehensionTriggerGenerator(comprehensionExpr, collection, reporter));
+        quantifiers.UnionWith(splitQuantifier);
+      } else {
+        quantifierCollections.Add(new ComprehensionTriggerGenerator(comprehensionExpr, Enumerable.Repeat(comprehensionExpr, 1), reporter));
+      }
+    }
+
     protected override bool VisitOneExpr(Expression expr, ref OldExpr/*?*/ enclosingOldContext) {
       // only consider quantifiers that are not empty (Bound.Vars.Count > 0)
       if (expr is ComprehensionExpr e && e.BoundVars.Count > 0 && !quantifiers.Contains(e)) {
         if (e is SetComprehension or MapComprehension) {
-          quantifiers.Add(e);
-          quantifierCollections.Add(new ComprehensionTriggerGenerator(e, Enumerable.Repeat(e, 1), reporter));
+          AddComprehension(e, null);
         } else if (e is QuantifierExpr quantifier) {
-          quantifiers.Add(quantifier);
-          if (quantifier.SplitQuantifier != null) {
-            var collection = quantifier.SplitQuantifier.Select(q => q as ComprehensionExpr).Where(q => q != null);
-            quantifierCollections.Add(new ComprehensionTriggerGenerator(e, collection, reporter));
-            quantifiers.UnionWith(quantifier.SplitQuantifier);
-          } else {
-            quantifierCollections.Add(new ComprehensionTriggerGenerator(e, Enumerable.Repeat(quantifier, 1), reporter));
-          }
+          AddComprehension(quantifier, quantifier.SplitQuantifier);
         }
       }
 
diff --git a/Source/DafnyCore/Verifier/BoogieGenerator.ExpressionTranslator.cs b/Source/DafnyCore/Verifier/BoogieGenerator.ExpressionTranslator.cs
index 10d78a37498..4f4b707f9c9 100644
--- a/Source/DafnyCore/Verifier/BoogieGenerator.ExpressionTranslator.cs
+++ b/Source/DafnyCore/Verifier/BoogieGenerator.ExpressionTranslator.cs
@@ -1674,17 +1674,18 @@ public Boogie.Expr TrBoundVariables(List<BoundVar/*!*/> boundVars, List<Variable
         return varsAndAntecedents;
       }
 
-      public Boogie.Expr TrBoundVariablesRename(List<BoundVar> boundVars, List<Variable> bvars, out Dictionary<IVariable, Expression> substMap, out Boogie.Trigger antitriggers) {
+      public Boogie.Expr TrBoundVariablesRename(List<BoundVar> boundVars, List<Variable> bvars, out Dictionary<IVariable, Expression> substMap) {
         Contract.Requires(boundVars != null);
         Contract.Requires(bvars != null);
 
         substMap = new Dictionary<IVariable, Expression>();
-        antitriggers = null;
         Boogie.Expr typeAntecedent = Boogie.Expr.True;
         foreach (BoundVar bv in boundVars) {
           var newBoundVar = new BoundVar(bv.tok, bv.Name, bv.Type);
-          IdentifierExpr ie = new IdentifierExpr(newBoundVar.tok, newBoundVar.AssignUniqueName(BoogieGenerator.currentDeclaration.IdGenerator));
-          ie.Var = newBoundVar; ie.Type = ie.Var.Type;  // resolve ie here
+          IdentifierExpr ie = new IdentifierExpr(newBoundVar.tok, newBoundVar.AssignUniqueName(BoogieGenerator.currentDeclaration.IdGenerator)) {
+            Var = newBoundVar,
+            Type = newBoundVar.Type
+          };
           substMap.Add(bv, ie);
           Boogie.Variable bvar = new Boogie.BoundVariable(newBoundVar.tok, new Boogie.TypedIdent(newBoundVar.tok, newBoundVar.AssignUniqueName(BoogieGenerator.currentDeclaration.IdGenerator), BoogieGenerator.TrType(newBoundVar.Type)));
           bvars.Add(bvar);
diff --git a/Source/DafnyCore/Verifier/BoogieGenerator.Methods.cs b/Source/DafnyCore/Verifier/BoogieGenerator.Methods.cs
index d6fc9b6adaf..130068059fb 100644
--- a/Source/DafnyCore/Verifier/BoogieGenerator.Methods.cs
+++ b/Source/DafnyCore/Verifier/BoogieGenerator.Methods.cs
@@ -759,6 +759,7 @@ private StmtList TrMethodBody(Method m, BoogieStmtListBuilder builder, Variables
         foreach (var pre in m.Req) {
           parRange = Expression.CreateAnd(parRange, Substitute(pre.E, receiverSubst, substMap));
         }
+
         // construct an expression (generator) for:  VF' << VF
         ExpressionConverter decrCheck = delegate (Dictionary<IVariable, Expression> decrSubstMap, ExpressionTranslator exprTran) {
           var decrToks = new List<IToken>();
diff --git a/Source/DafnyCore/Verifier/Statements/BoogieGenerator.TrForallStmt.cs b/Source/DafnyCore/Verifier/Statements/BoogieGenerator.TrForallStmt.cs
index ab7e6ae4a58..f2c402f91bc 100644
--- a/Source/DafnyCore/Verifier/Statements/BoogieGenerator.TrForallStmt.cs
+++ b/Source/DafnyCore/Verifier/Statements/BoogieGenerator.TrForallStmt.cs
@@ -158,15 +158,14 @@ void TrForallStmtCall(IToken tok, List<BoundVar> boundVars, List<BoundedPool> bo
 
       // Note, in the following, we need to do a bit of a song and dance.  The actual arguments of the
       // call should be translated using "initEtran", whereas the method postcondition should be translated
-      // using "callEtran".  To accomplish this, we translate the argument and then tuck the resulting
+      // using "callEtran".  To accomplish this, we translate the arguments and then tuck the resulting
       // Boogie expressions into BoogieExprWrappers that are used in the DafnyExpr-to-DafnyExpr substitution.
       var bvars = new List<Variable>();
       Dictionary<IVariable, Expression> substMap;
-      Bpl.Trigger antitriggerBoundVarTypes;
-      Bpl.Expr ante;
       var argsSubstMap = new Dictionary<IVariable, Expression>();  // maps formal arguments to actuals
       Contract.Assert(s0.Method.Ins.Count == s0.Args.Count);
       var callEtran = new ExpressionTranslator(this, predef, etran.HeapExpr, initHeap, etran.scope);
+      Bpl.Expr ante;
       Bpl.Expr post = Bpl.Expr.True;
       Bpl.Trigger tr;
       if (forallExpressions != null) {
@@ -176,29 +175,35 @@ void TrForallStmtCall(IToken tok, List<BoundVar> boundVars, List<BoundedPool> bo
           expr = (QuantifierExpr)expr.SplitQuantifierExpression;
         }
         boundVars = expr.BoundVars;
-        ante = initEtran.TrBoundVariablesRename(boundVars, bvars, out substMap, out antitriggerBoundVarTypes);
-        ante = BplAnd(ante, initEtran.TrExpr(Substitute(expr.Range, null, substMap)));
+        ante = initEtran.TrBoundVariablesRename(boundVars, bvars, out substMap);
+        tr = TrTrigger(callEtran, expr.Attributes, expr.tok, bvars, substMap, s0.MethodSelect.TypeArgumentSubstitutionsWithParents());
+
+        var p = Substitute(expr.Range, null, substMap);
+        ante = BplAnd(ante, initEtran.TrExpr(p));
         if (additionalRange != null) {
           ante = BplAnd(ante, additionalRange(substMap, initEtran));
         }
         tr = TrTrigger(callEtran, expr.Attributes, expr.tok, bvars, substMap, s0.MethodSelect.TypeArgumentSubstitutionsWithParents());
         post = callEtran.TrExpr(Substitute(expr.Term, null, substMap));
       } else {
-        ante = initEtran.TrBoundVariablesRename(boundVars, bvars, out substMap, out antitriggerBoundVarTypes);
-        for (int i = 0; i < s0.Method.Ins.Count; i++) {
-          var arg = Substitute(s0.Args[i], null, substMap, s0.MethodSelect.TypeArgumentSubstitutionsWithParents());  // substitute the renamed bound variables for the declared ones
-          argsSubstMap.Add(s0.Method.Ins[i], new BoogieWrapper(initEtran.TrExpr(arg), s0.Args[i].Type));
-        }
-        ante = BplAnd(ante, initEtran.TrExpr(Substitute(range, null, substMap)));
+        ante = initEtran.TrBoundVariablesRename(boundVars, bvars, out substMap);
+
+        var p = Substitute(range, null, substMap);
+        ante = BplAnd(ante, initEtran.TrExpr(p));
         if (additionalRange != null) {
           ante = BplAnd(ante, additionalRange(substMap, initEtran));
         }
+
         var receiver = new BoogieWrapper(initEtran.TrExpr(Substitute(s0.Receiver, null, substMap, s0.MethodSelect.TypeArgumentSubstitutionsWithParents())), s0.Receiver.Type);
+        for (int i = 0; i < s0.Method.Ins.Count; i++) {
+          var arg = Substitute(s0.Args[i], null, substMap, s0.MethodSelect.TypeArgumentSubstitutionsWithParents());  // substitute the renamed bound variables for the declared ones
+          argsSubstMap.Add(s0.Method.Ins[i], new BoogieWrapper(initEtran.TrExpr(arg), s0.Args[i].Type));
+        }
         foreach (var ens in s0.Method.Ens) {
-          var p = Substitute(ens.E, receiver, argsSubstMap, s0.MethodSelect.TypeArgumentSubstitutionsWithParents());  // substitute the call's actuals for the method's formals
+          p = Substitute(ens.E, receiver, argsSubstMap, s0.MethodSelect.TypeArgumentSubstitutionsWithParents());  // substitute the call's actuals for the method's formals
           post = BplAnd(post, callEtran.TrExpr(p));
         }
-        tr = antitriggerBoundVarTypes;
+        tr = null;
       }
 
       // TRIG (forall $ih#s0#0: Seq :: $Is($ih#s0#0, TSeq(TChar)) && $IsAlloc($ih#s0#0, TSeq(TChar), $initHeapForallStmt#0) && Seq#Length($ih#s0#0) != 0 && Seq#Rank($ih#s0#0) < Seq#Rank(s#0) ==> (forall i#2: int :: true ==> LitInt(0) <= i#2 && i#2 < Seq#Length($ih#s0#0) ==> char#ToInt(_module.CharChar.MinChar($LS($LZ), $Heap, this, $ih#s0#0)) <= char#ToInt($Unbox(Seq#Index($ih#s0#0, i#2)): char)))
@@ -532,4 +537,4 @@ void TrForallProof(ForallStmt forallStmt, BoogieStmtListBuilder definedness, Boo
       exporter.Add(TrAssumeCmd(forallStmt.Tok, BplAnd(se, ((Bpl.ForallExpr)qq).Body)));
     }
   }
-}
\ No newline at end of file
+}

From e62d2b61b3cec129cd33f40f3838959709a249ec Mon Sep 17 00:00:00 2001
From: Rustan Leino <leino@amazon.com>
Date: Fri, 11 Oct 2024 23:23:09 -0700
Subject: [PATCH 02/16] Compute triggers for automatic induction

# Conflicts:
#	Source/DafnyCore/Verifier/BoogieGenerator.Methods.cs
#	Source/DafnyCore/Verifier/Statements/BoogieGenerator.TrForallStmt.cs
---
 .../DafnyCore/Rewriters/InductionRewriter.cs  | 61 +++++++++++++++++++
 .../Triggers/ComprehensionTriggerGenerator.cs | 14 +++++
 .../Verifier/BoogieGenerator.Methods.cs       | 15 +++--
 .../BoogieGenerator.TrForallStmt.cs           | 20 +++++-
 4 files changed, 101 insertions(+), 9 deletions(-)

diff --git a/Source/DafnyCore/Rewriters/InductionRewriter.cs b/Source/DafnyCore/Rewriters/InductionRewriter.cs
index faeb66ebc58..e782569bde6 100644
--- a/Source/DafnyCore/Rewriters/InductionRewriter.cs
+++ b/Source/DafnyCore/Rewriters/InductionRewriter.cs
@@ -1,5 +1,6 @@
 using System.Collections.Generic;
 using System.Diagnostics.Contracts;
+using System.Linq;
 using JetBrains.Annotations;
 using static Microsoft.Dafny.RewriterErrors;
 
@@ -183,6 +184,23 @@ void ComputeInductionVariables<TVarType>(IToken tok, List<TVarType> boundVars, E
     }
 
     if (inductionVariables.Count != 0) {
+      if (lemma != null) {
+        var triggers = ComputeInductionTriggers(inductionVariables, body, lemma.EnclosingClass.EnclosingModuleDefinition);
+        if (triggers.Count == 0) {
+          var msg = "omitting automatic induction because of lack of triggers";
+          if (args != null) {
+            Reporter.Warning(MessageSource.Rewriter, GenericErrors.ErrorId.none, tok, msg);
+          } else {
+            Reporter.Info(MessageSource.Rewriter, tok, msg);
+          }
+          return;
+        }
+
+        foreach (var trigger in triggers) {
+          attributes = new Attributes("_inductionPattern", trigger, attributes);
+        }
+      }
+
       // We found something usable, so let's record that in an attribute
       attributes = new Attributes("_induction", inductionVariables, attributes);
       // And since we're inferring something, let's also report that in a hover text.
@@ -195,6 +213,49 @@ void ComputeInductionVariables<TVarType>(IToken tok, List<TVarType> boundVars, E
     }
   }
 
+  /// <summary>
+  /// Obtain and return matching patterns for
+  ///     (forall inductionVariables :: body)
+  /// If there aren't any, then return null.
+  /// </summary>
+  List<List<Expression>> ComputeInductionTriggers(List<Expression> inductionVariables, Expression body, ModuleDefinition moduleDefinition) {
+    Contract.Requires(inductionVariables.Count != 0);
+
+    // Construct a quantifier, because that's what the trigger-generating machinery expects.
+    // We start by creating a new BoundVar for each ThisExpr-or-IdentifierExpr in "inductionVariables".
+    var boundVars = new List<BoundVar>();
+    var substMap = new Dictionary<IVariable, Expression>();
+    var reverseSubstMap = new Dictionary<IVariable, Expression>();
+    Expression receiverReplacement = null;
+    foreach (var inductionVariableExpr in inductionVariables) {
+      var tok = inductionVariableExpr.tok;
+      BoundVar boundVar;
+      if (inductionVariableExpr is IdentifierExpr identifierExpr) {
+        boundVar = new BoundVar(tok, identifierExpr.Var.Name, identifierExpr.Var.Type);
+        substMap.Add(identifierExpr.Var, new IdentifierExpr(tok, boundVar));
+      } else {
+        Contract.Assert(inductionVariableExpr is ThisExpr);
+        boundVar = new BoundVar(tok, "this", inductionVariableExpr.Type);
+        receiverReplacement = new IdentifierExpr(tok, boundVar);
+      }
+      boundVars.Add(boundVar);
+      reverseSubstMap.Add(boundVar, inductionVariableExpr);
+    }
+
+    var substituter = new Substituter(receiverReplacement, substMap, new Dictionary<TypeParameter, Type>());
+    var quantifier = new ForallExpr(body.tok, body.RangeToken, boundVars, null, substituter.Substitute(body), null) {
+      Type = Type.Bool
+    };
+
+    var finder = new Triggers.QuantifierCollector(Reporter);
+    var triggersCollector = new Triggers.TriggersCollector(finder.exprsInOldContext, Reporter.Options, moduleDefinition);
+    var quantifierCollection = new Triggers.ComprehensionTriggerGenerator(quantifier, Enumerable.Repeat(quantifier, 1), Reporter);
+    quantifierCollection.ComputeTriggers(triggersCollector);
+    var triggers = quantifierCollection.GetTriggers();
+    var reverseSubstituter = new Substituter(null, reverseSubstMap, new Dictionary<TypeParameter, Type>());
+    return triggers.ConvertAll(trigger => trigger.ConvertAll(reverseSubstituter.Substitute));
+  }
+
   class InductionVisitor : BottomUpVisitor {
     readonly InductionRewriter IndRewriter;
 
diff --git a/Source/DafnyCore/Triggers/ComprehensionTriggerGenerator.cs b/Source/DafnyCore/Triggers/ComprehensionTriggerGenerator.cs
index 15b9fc0edb9..65723ba9829 100644
--- a/Source/DafnyCore/Triggers/ComprehensionTriggerGenerator.cs
+++ b/Source/DafnyCore/Triggers/ComprehensionTriggerGenerator.cs
@@ -230,5 +230,19 @@ internal void CommitTriggers(SystemModuleManager systemModuleManager) {
         triggerWriter.CommitTrigger(reporter, partWriters.Count > 1 ? index : null, systemModuleManager);
       }
     }
+
+    public List<List<Expression>> GetTriggers() {
+      var triggers = new List<List<Expression>>();
+      foreach (var triggerWriter in partWriters) {
+        foreach (var triggerTerms in triggerWriter.Candidates) {
+          var trigger = new List<Expression>();
+          foreach (var triggerTerm in triggerTerms.Terms) {
+            trigger.Add(triggerTerm.Expr);
+          }
+          triggers.Add(trigger);
+        }
+      }
+      return triggers;
+    }
   }
 }
diff --git a/Source/DafnyCore/Verifier/BoogieGenerator.Methods.cs b/Source/DafnyCore/Verifier/BoogieGenerator.Methods.cs
index 130068059fb..7a893ade472 100644
--- a/Source/DafnyCore/Verifier/BoogieGenerator.Methods.cs
+++ b/Source/DafnyCore/Verifier/BoogieGenerator.Methods.cs
@@ -782,14 +782,17 @@ private StmtList TrMethodBody(Method m, BoogieStmtListBuilder builder, Variables
             null, null, false, true);
         };
 
+        var triggers = Attributes.FindAllExpressions(m.Attributes, "_inductionPattern");
 #if VERIFY_CORRECTNESS_OF_TRANSLATION_FORALL_STATEMENT_RANGE
-          var definedness = new BoogieStmtListBuilder(this, options);
-          var exporter = new BoogieStmtListBuilder(this, options);
-          TrForallStmtCall(m.tok, parBoundVars, parRange, decrCheck, null, recursiveCall, definedness, exporter, localVariables, etran);
-          // All done, so put the two pieces together
-          builder.Add(new Bpl.IfCmd(m.tok, null, definedness.Collect(m.tok), null, exporter.Collect(m.tok)));
+        var definedness = new BoogieStmtListBuilder(this, options, builder.Context);
+        var exporter = new BoogieStmtListBuilder(this, options, builder.Context);
+        TrForallStmtCall(m.tok, parBoundVars, parBounds, parRange, decrCheck, null, triggers, recursiveCall, definedness,
+          exporter, localVariables, etran);
+        // All done, so put the two pieces together
+        builder.Add(new Bpl.IfCmd(m.tok, null, definedness.Collect(m.tok), null, exporter.Collect(m.tok)));
 #else
-        TrForallStmtCall(m.tok, parBoundVars, parBounds, parRange, decrCheck, null, recursiveCall, null, builder, localVariables, etran);
+        TrForallStmtCall(m.tok, parBoundVars, parBounds, parRange, decrCheck, null, triggers, recursiveCall, null,
+          builder, localVariables, etran);
 #endif
       }
       // translate the body of the method
diff --git a/Source/DafnyCore/Verifier/Statements/BoogieGenerator.TrForallStmt.cs b/Source/DafnyCore/Verifier/Statements/BoogieGenerator.TrForallStmt.cs
index f2c402f91bc..20c4126c10d 100644
--- a/Source/DafnyCore/Verifier/Statements/BoogieGenerator.TrForallStmt.cs
+++ b/Source/DafnyCore/Verifier/Statements/BoogieGenerator.TrForallStmt.cs
@@ -40,12 +40,14 @@ private void TrForallStmt(BoogieStmtListBuilder builder, Variables locals, Expre
       } else {
         var s0 = (CallStmt)forallStmt.S0;
         if (Attributes.Contains(forallStmt.Attributes, "_trustWellformed")) {
-          TrForallStmtCall(forallStmt.Tok, forallStmt.BoundVars, forallStmt.Bounds, forallStmt.Range, null, forallStmt.EffectiveEnsuresClauses, s0, null, builder, locals, etran);
+          TrForallStmtCall(forallStmt.Tok, forallStmt.BoundVars, forallStmt.Bounds, forallStmt.Range, null,
+            forallStmt.EffectiveEnsuresClauses, null, s0, null, builder, locals, etran);
         } else {
           var definedness = new BoogieStmtListBuilder(this, options, builder.Context);
           DefineFuelConstant(forallStmt.Tok, forallStmt.Attributes, definedness, etran);
           var exporter = new BoogieStmtListBuilder(this, options, builder.Context);
-          TrForallStmtCall(forallStmt.Tok, forallStmt.BoundVars, forallStmt.Bounds, forallStmt.Range, null, forallStmt.EffectiveEnsuresClauses, s0, definedness, exporter, locals, etran);
+          TrForallStmtCall(forallStmt.Tok, forallStmt.BoundVars, forallStmt.Bounds, forallStmt.Range, null,
+            forallStmt.EffectiveEnsuresClauses, null, s0, definedness, exporter, locals, etran);
           // All done, so put the two pieces together
           builder.Add(new Bpl.IfCmd(forallStmt.Tok, null, definedness.Collect(forallStmt.Tok), null, exporter.Collect(forallStmt.Tok)));
         }
@@ -71,13 +73,14 @@ private void TrForallStmt(BoogieStmtListBuilder builder, Variables locals, Expre
 
 
   void TrForallStmtCall(IToken tok, List<BoundVar> boundVars, List<BoundedPool> bounds,
-    Expression range, ExpressionConverter additionalRange, List<Expression> forallExpressions, CallStmt s0,
+    Expression range, ExpressionConverter additionalRange, List<Expression> forallExpressions, List<List<Expression>> triggers, CallStmt s0,
     BoogieStmtListBuilder definedness, BoogieStmtListBuilder exporter, Variables locals, ExpressionTranslator etran) {
     Contract.Requires(tok != null);
     Contract.Requires(boundVars != null);
     Contract.Requires(bounds != null);
     Contract.Requires(range != null);
     // additionalRange is allowed to be null
+    Contract.Requires(forallExpressions == null || triggers == null || triggers.Count == 0);
     Contract.Requires(s0 != null);
     // definedness is allowed to be null
     Contract.Requires(exporter != null);
@@ -203,7 +206,18 @@ void TrForallStmtCall(IToken tok, List<BoundVar> boundVars, List<BoundedPool> bo
           p = Substitute(ens.E, receiver, argsSubstMap, s0.MethodSelect.TypeArgumentSubstitutionsWithParents());  // substitute the call's actuals for the method's formals
           post = BplAnd(post, callEtran.TrExpr(p));
         }
+
         tr = null;
+        if (triggers != null) {
+          foreach (var trigger in triggers) {
+            Contract.Assert(trigger.Count != 0);
+            var terms = trigger.ConvertAll(expr => {
+              expr = Substitute(expr, receiver, argsSubstMap, s0.MethodSelect.TypeArgumentSubstitutionsWithParents());
+              return callEtran.TrExpr(expr);
+            });
+            tr = new Trigger(trigger[0].tok, true, terms, tr);
+          }
+        }
       }
 
       // TRIG (forall $ih#s0#0: Seq :: $Is($ih#s0#0, TSeq(TChar)) && $IsAlloc($ih#s0#0, TSeq(TChar), $initHeapForallStmt#0) && Seq#Length($ih#s0#0) != 0 && Seq#Rank($ih#s0#0) < Seq#Rank(s#0) ==> (forall i#2: int :: true ==> LitInt(0) <= i#2 && i#2 < Seq#Length($ih#s0#0) ==> char#ToInt(_module.CharChar.MinChar($LS($LZ), $Heap, this, $ih#s0#0)) <= char#ToInt($Unbox(Seq#Index($ih#s0#0, i#2)): char)))

From ad1c724c5b5e86459479162d3e9f7ef0f0b71218 Mon Sep 17 00:00:00 2001
From: Rustan Leino <leino@amazon.com>
Date: Sat, 12 Oct 2024 11:38:10 -0700
Subject: [PATCH 03/16] Improve induction heuristics

---
 .../DafnyCore/Rewriters/InductionHeuristic.cs | 22 ++++++++++++++-----
 .../DafnyCore/Rewriters/InductionRewriter.cs  |  2 +-
 2 files changed, 17 insertions(+), 7 deletions(-)

diff --git a/Source/DafnyCore/Rewriters/InductionHeuristic.cs b/Source/DafnyCore/Rewriters/InductionHeuristic.cs
index 3787ab4303b..1ceab8866f2 100644
--- a/Source/DafnyCore/Rewriters/InductionHeuristic.cs
+++ b/Source/DafnyCore/Rewriters/InductionHeuristic.cs
@@ -1,3 +1,4 @@
+#nullable enable
 using System.Diagnostics.Contracts;
 
 namespace Microsoft.Dafny;
@@ -6,6 +7,8 @@ public static class InductionHeuristic {
 
   /// <summary>
   /// Returns 'true' iff by looking at 'expr' the Induction Heuristic determines that induction should be applied to 'n'.
+  /// Variable 'n' can be passed in as 'null', in which case it stands for 'this'.
+  /// 
   /// More precisely:
   ///   DafnyInductionHeuristic      Return 'true'
   ///   -----------------------      -------------
@@ -17,10 +20,15 @@ public static class InductionHeuristic {
   ///        5    if 'n' occurs as   a prominent subexpression of                                                               any                       argument to a recursive function
   ///        6    if 'n' occurs as   a prominent subexpression of                                                               any decreases-influencing argument to a recursive function
   /// </summary>
-  public static bool VarOccursInArgumentToRecursiveFunction(DafnyOptions options, Expression expr, IVariable n) {
+  public static bool VarOccursInArgumentToRecursiveFunction(DafnyOptions options, Expression expr, IVariable? n) {
     switch (options.InductionHeuristic) {
       case 0: return true;
-      case 1: return FreeVariablesUtil.ContainsFreeVariable(expr, false, n);
+      case 1:
+        if (n == null) {
+          return FreeVariablesUtil.ContainsFreeVariable(expr, true, null);
+        } else {
+          return FreeVariablesUtil.ContainsFreeVariable(expr, false, n);
+        }
       default: return VarOccursInArgumentToRecursiveFunction(options, expr, n, false);
     }
   }
@@ -30,16 +38,18 @@ public static bool VarOccursInArgumentToRecursiveFunction(DafnyOptions options,
   /// not 'expr' has prominent status in its context.
   /// DafnyInductionHeuristic cases 0 and 1 are assumed to be handled elsewhere (i.e., a precondition of this method is DafnyInductionHeuristic is at least 2).
   /// </summary>
-  static bool VarOccursInArgumentToRecursiveFunction(DafnyOptions options, Expression expr, IVariable n, bool exprIsProminent) {
+  static bool VarOccursInArgumentToRecursiveFunction(DafnyOptions options, Expression expr, IVariable? n, bool exprIsProminent) {
     Contract.Requires(expr != null);
     Contract.Requires(n != null);
 
     // The following variable is what gets passed down to recursive calls if the subexpression does not itself acquire prominent status.
     var subExprIsProminent = options.InductionHeuristic == 2 || options.InductionHeuristic == 4 ? /*once prominent, always prominent*/exprIsProminent : /*reset the prominent status*/false;
 
-    if (expr is IdentifierExpr) {
+    if (n != null && expr is IdentifierExpr) {
       var e = (IdentifierExpr)expr;
       return exprIsProminent && e.Var == n;
+    } else if (n == null && expr is ThisExpr) {
+      return exprIsProminent;
     } else if (expr is SeqSelectExpr) {
       var e = (SeqSelectExpr)expr;
       var q = options.InductionHeuristic < 4 || subExprIsProminent;
@@ -108,7 +118,7 @@ static bool VarOccursInArgumentToRecursiveFunction(DafnyOptions options, Express
       }
     } else if (expr is DatatypeValue) {
       var e = (DatatypeValue)expr;
-      var q = n.Type.IsDatatype ? exprIsProminent : subExprIsProminent;  // prominent status continues, if we're looking for a variable whose type is a datatype
+      var q = n != null && n.Type.IsDatatype ? exprIsProminent : subExprIsProminent;  // prominent status continues, if we're looking for a variable whose type is a datatype
       return e.Arguments.Exists(exp => VarOccursInArgumentToRecursiveFunction(options, exp, n, q));
     } else if (expr is UnaryExpr) {
       var e = (UnaryExpr)expr;
@@ -145,7 +155,7 @@ static bool VarOccursInArgumentToRecursiveFunction(DafnyOptions options, Express
     } else if (expr is StmtExpr) {
       var e = (StmtExpr)expr;
       // ignore the statement
-      return VarOccursInArgumentToRecursiveFunction(options, e.E, n);
+      return VarOccursInArgumentToRecursiveFunction(options, e.E, n, exprIsProminent);
 
     } else if (expr is ITEExpr) {
       var e = (ITEExpr)expr;
diff --git a/Source/DafnyCore/Rewriters/InductionRewriter.cs b/Source/DafnyCore/Rewriters/InductionRewriter.cs
index e782569bde6..c8ca384bc12 100644
--- a/Source/DafnyCore/Rewriters/InductionRewriter.cs
+++ b/Source/DafnyCore/Rewriters/InductionRewriter.cs
@@ -171,7 +171,7 @@ void ComputeInductionVariables<TVarType>(IToken tok, List<TVarType> boundVars, E
     // Okay, here we go, coming up with good induction setting for the given situation
     var inductionVariables = new List<Expression>();
     if (lemma is { IsStatic: false }) {
-      if (args != null || FreeVariablesUtil.ContainsFreeVariable(body, true, null)) {
+      if (args != null || InductionHeuristic.VarOccursInArgumentToRecursiveFunction(Reporter.Options, body, null)) {
         inductionVariables.Add(new ThisExpr(lemma));
       }
     }

From 29d715a778d8fe9f8d8edefb18d6ac1dfb9b5d78 Mon Sep 17 00:00:00 2001
From: Rustan Leino <leino@amazon.com>
Date: Sat, 12 Oct 2024 11:44:35 -0700
Subject: [PATCH 04/16] =?UTF-8?q?chore:=20Change=20=E2=80=9Cghost=20method?=
 =?UTF-8?q?=E2=80=9D=20to=20=E2=80=9Clemma=E2=80=9D?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 .../TestFiles/LitTests/LitTest/dafny0/LetExpr.dfy             | 4 ++--
 .../TestFiles/LitTests/LitTest/dafny0/Termination.dfy         | 4 ++--
 2 files changed, 4 insertions(+), 4 deletions(-)

diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/LetExpr.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/LetExpr.dfy
index 9cdc06d5040..8b3300900aa 100644
--- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/LetExpr.dfy
+++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/LetExpr.dfy
@@ -127,11 +127,11 @@ method Theorem0(n: int)
   }
 }
 
-ghost method Theorem1(n: int)
+lemma Theorem1(n: int)
   requires 1 <= n;
   ensures 1 <= Fib(n);
 {
-  // in a ghost method, the induction tactic takes care of it
+  // in a lemma, the induction tactic takes care of it
 }
 
 ghost function Theorem2(n: int): int
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/Termination.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/Termination.dfy
index 8ac6f9a37ae..26376f13b2a 100644
--- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/Termination.dfy
+++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/Termination.dfy
@@ -392,7 +392,7 @@ module MultisetTests {
     if n == 0 then 0 else F'(a, n-1)
   }
 
-  ghost method M(n: nat, b: multiset<int>)
+  lemma M(n: nat, b: multiset<int>)
     ensures F(b, n) == 0  // proved via automatic induction
   {
   }
@@ -410,7 +410,7 @@ module MapTests {
     if n == 0 then 0 else F'(a, n-1)
   }
 
-  ghost method M(n: nat, b: map<int,int>)
+  lemma M(n: nat, b: map<int,int>)
     ensures F(b, n) == 0  // proved via automatic induction
   {
   }

From 4cfbe2183a2137639061721e40a806e886fbe35f Mon Sep 17 00:00:00 2001
From: Rustan Leino <leino@amazon.com>
Date: Mon, 14 Oct 2024 01:33:58 -0700
Subject: [PATCH 05/16] chore: Improve C#

---
 Source/DafnyCore/AST/ExtremeCloner.cs         |  2 +-
 .../DafnyCore/AST/ExtremeLemmaBodyCloner.cs   | 61 ++++++-------------
 .../CollectFriendlyCallsInSpec_Visitor.cs     |  6 +-
 Source/DafnyCore/Resolver/ModuleResolver.cs   | 15 ++---
 .../Triggers/SplitPartTriggerWriter.cs        |  4 +-
 5 files changed, 28 insertions(+), 60 deletions(-)

diff --git a/Source/DafnyCore/AST/ExtremeCloner.cs b/Source/DafnyCore/AST/ExtremeCloner.cs
index d4d725e82e3..67cc276bf05 100644
--- a/Source/DafnyCore/AST/ExtremeCloner.cs
+++ b/Source/DafnyCore/AST/ExtremeCloner.cs
@@ -17,7 +17,7 @@ protected ExtremeCloner(Expression k, ErrorReporter reporter) {
     Contract.Requires(reporter != null);
     this.k = k;
     this.reporter = reporter;
-    this.suffix = string.Format("#[{0}]", Printer.ExprToString(reporter.Options, k));
+    this.suffix = $"#[{Printer.ExprToString(reporter.Options, k)}]";
   }
   protected Expression CloneCallAndAddK(ApplySuffix e) {
     Contract.Requires(e != null);
diff --git a/Source/DafnyCore/AST/ExtremeLemmaBodyCloner.cs b/Source/DafnyCore/AST/ExtremeLemmaBodyCloner.cs
index f71835f6ce2..66eda31ca9a 100644
--- a/Source/DafnyCore/AST/ExtremeLemmaBodyCloner.cs
+++ b/Source/DafnyCore/AST/ExtremeLemmaBodyCloner.cs
@@ -11,42 +11,31 @@ namespace Microsoft.Dafny;
 class ExtremeLemmaBodyCloner : ExtremeCloner {
   readonly ExtremeLemma context;
   readonly ISet<ExtremePredicate> focalPredicates;
-  public ExtremeLemmaBodyCloner(ExtremeLemma context, Expression k, ISet<ExtremePredicate> focalPredicates, ErrorReporter reporter)
+  readonly ISet<CoDatatypeDecl> focalCodatatypeEquality;
+  public ExtremeLemmaBodyCloner(ExtremeLemma context, Expression k,
+    ISet<ExtremePredicate> focalPredicates, ISet<CoDatatypeDecl> focalCodatatypeEquality, ErrorReporter reporter)
     : base(k, reporter) {
     Contract.Requires(context != null);
     Contract.Requires(k != null);
     Contract.Requires(reporter != null);
     this.context = context;
     this.focalPredicates = focalPredicates;
+    this.focalCodatatypeEquality = focalCodatatypeEquality;
   }
 
   public override Expression CloneExpr(Expression expr) {
     if (reporter.Options.RewriteFocalPredicates) {
-      if (expr is FunctionCallExpr) {
-        var e = (FunctionCallExpr)expr;
-#if DEBUG_PRINT
-          if (e.Function.Name.EndsWith("#") && Contract.Exists(focalPredicates, p => e.Function.Name == p.Name + "#")) {
-            Options.Writer.WriteLine("{0}({1},{2}): DEBUG: Possible opportunity to rely on new rewrite: {3}", e.tok.filename, e.tok.line, e.tok.col, Printer.ExprToString(e));
-          }
-#endif
+      if (expr is FunctionCallExpr functionCallExpr) {
         // Note, we don't actually ever get here, because all calls will have been parsed as ApplySuffix.
         // However, if something changes in the future (for example, some rewrite that changing an ApplySuffix
         // to its resolved FunctionCallExpr), then we do want this code, so with the hope of preventing
         // some error in the future, this case is included.  (Of course, it is currently completely untested!)
-        var f = e.Function as ExtremePredicate;
-        if (f != null && focalPredicates.Contains(f)) {
-#if DEBUG_PRINT
-            var r = CloneCallAndAddK(e);
-            Options.Writer.WriteLine("{0}({1},{2}): DEBUG: Rewrote extreme predicate into prefix predicate: {3}", e.tok.filename, e.tok.line, e.tok.col, Printer.ExprToString(r));
-            return r;
-#else
-          return CloneCallAndAddK(e);
-#endif
+        if (functionCallExpr.Function is ExtremePredicate f && focalPredicates.Contains(f)) {
+          return CloneCallAndAddK(functionCallExpr);
         }
       } else if (expr is StaticReceiverExpr ee) {
         return new StaticReceiverExpr(Tok(ee.tok), ee.Type, ee.IsImplicit);
-      } else if (expr is ApplySuffix) {
-        var apply = (ApplySuffix)expr;
+      } else if (expr is ApplySuffix apply) {
         if (!apply.WasResolved()) {
           // Since we're assuming the enclosing statement to have been resolved, this ApplySuffix must
           // be part of an ExprRhs that actually designates a method call.  Such an ApplySuffix does
@@ -54,22 +43,9 @@ public override Expression CloneExpr(Expression expr) {
           var mse = (MemberSelectExpr)apply.Lhs.Resolved;
           Contract.Assume(mse.Member is Method);
         } else {
-          var fce = apply.Resolved as FunctionCallExpr;
-          if (fce != null) {
-#if DEBUG_PRINT
-              if (fce.Function.Name.EndsWith("#") && Contract.Exists(focalPredicates, p => fce.Function.Name == p.Name + "#")) {
-                Options.Writer.WriteLine("{0}({1},{2}): DEBUG: Possible opportunity to rely on new rewrite: {3}", fce.tok.filename, fce.tok.line, fce.tok.col, Printer.ExprToString(fce));
-              }
-#endif
-            var f = fce.Function as ExtremePredicate;
-            if (f != null && focalPredicates.Contains(f)) {
-#if DEBUG_PRINT
-                var r = CloneCallAndAddK(fce);
-                Options.Writer.WriteLine("{0}({1},{2}): DEBUG: Rewrote extreme predicate into prefix predicate: {3}", fce.tok.filename, fce.tok.line, fce.tok.col, Printer.ExprToString(r));
-                return r;
-#else
+          if (apply.Resolved is FunctionCallExpr fce) {
+            if (fce.Function is ExtremePredicate f && focalPredicates.Contains(f)) {
               return CloneCallAndAddK(fce);
-#endif
             }
           }
         }
@@ -78,32 +54,31 @@ public override Expression CloneExpr(Expression expr) {
     return base.CloneExpr(expr);
   }
   public override AssignmentRhs CloneRHS(AssignmentRhs rhs) {
-    var r = rhs as ExprRhs;
-    if (r != null && r.Expr is ApplySuffix) {
-      var apply = (ApplySuffix)r.Expr;
-      var mse = apply.Lhs.Resolved as MemberSelectExpr;
-      if (mse != null && mse.Member is ExtremeLemma && ModuleDefinition.InSameSCC(context, (ExtremeLemma)mse.Member)) {
+    if (rhs is ExprRhs { Expr: ApplySuffix apply }) {
+      if (apply.Lhs.Resolved is MemberSelectExpr { Member: ExtremeLemma extremeLemma } && ModuleDefinition.InSameSCC(context, extremeLemma)) {
         // we're looking at a recursive call to an extreme lemma
-        Contract.Assert(apply.Lhs is NameSegment || apply.Lhs is ExprDotName);  // this is the only way a call statement can have been parsed
+        Contract.Assert(apply.Lhs is NameSegment or ExprDotName); // this is the only way a call statement can have been parsed
         // clone "apply.Lhs", changing the least/greatest lemma to the prefix lemma; then clone "apply", adding in the extra argument
         Expression lhsClone;
         if (apply.Lhs is NameSegment) {
           var lhs = (NameSegment)apply.Lhs;
-          lhsClone = new NameSegment(Tok(lhs.tok), lhs.Name + "#", lhs.OptTypeArguments == null ? null : lhs.OptTypeArguments.ConvertAll(CloneType));
+          lhsClone = new NameSegment(Tok(lhs.tok), lhs.Name + "#", lhs.OptTypeArguments?.ConvertAll(CloneType));
         } else {
           var lhs = (ExprDotName)apply.Lhs;
-          lhsClone = new ExprDotName(Tok(lhs.tok), CloneExpr(lhs.Lhs), lhs.SuffixName + "#", lhs.OptTypeArguments == null ? null : lhs.OptTypeArguments.ConvertAll(CloneType));
+          lhsClone = new ExprDotName(Tok(lhs.tok), CloneExpr(lhs.Lhs), lhs.SuffixName + "#", lhs.OptTypeArguments?.ConvertAll(CloneType));
         }
+
         var args = new List<ActualBinding>();
         args.Add(new ActualBinding(null, k));
         apply.Bindings.ArgumentBindings.ForEach(arg => args.Add(CloneActualBinding(arg)));
         var applyClone = new ApplySuffix(Tok(apply.tok), apply.AtTok == null ? null : Tok(apply.AtTok),
           lhsClone, args, Tok(apply.CloseParen));
         var c = new ExprRhs(applyClone, CloneAttributes(rhs.Attributes));
-        reporter.Info(MessageSource.Cloner, apply.Lhs.tok, mse.Member.Name + suffix);
+        reporter.Info(MessageSource.Cloner, apply.Lhs.tok, extremeLemma.Name + suffix);
         return c;
       }
     }
+
     return base.CloneRHS(rhs);
   }
 }
diff --git a/Source/DafnyCore/Resolver/CollectFriendlyCallsInSpec_Visitor.cs b/Source/DafnyCore/Resolver/CollectFriendlyCallsInSpec_Visitor.cs
index 76bccae2139..02b9ba438c1 100644
--- a/Source/DafnyCore/Resolver/CollectFriendlyCallsInSpec_Visitor.cs
+++ b/Source/DafnyCore/Resolver/CollectFriendlyCallsInSpec_Visitor.cs
@@ -19,9 +19,8 @@ protected override bool VisitOneExpr(Expression expr, ref CallingPosition cp) {
       // no friendly calls in "expr"
       return false;  // don't recurse into subexpressions
     }
-    if (expr is FunctionCallExpr) {
+    if (expr is FunctionCallExpr fexp) {
       if (cp == CallingPosition.Positive) {
-        var fexp = (FunctionCallExpr)expr;
         if (IsCoContext ? fexp.Function is GreatestPredicate : fexp.Function is LeastPredicate) {
           if (Context.KNat != ((ExtremePredicate)fexp.Function).KNat) {
             KNatMismatchError(expr.tok, Context.Name, Context.TypeOfK, ((ExtremePredicate)fexp.Function).TypeOfK);
@@ -31,8 +30,7 @@ protected override bool VisitOneExpr(Expression expr, ref CallingPosition cp) {
         }
       }
       return false;  // don't explore subexpressions any further
-    } else if (expr is BinaryExpr && IsCoContext) {
-      var bin = (BinaryExpr)expr;
+    } else if (expr is BinaryExpr bin && IsCoContext) {
       if (cp == CallingPosition.Positive && bin.ResolvedOp == BinaryExpr.ResolvedOpcode.EqCommon && bin.E0.Type.IsCoDatatype) {
         friendlyCalls.Add(bin);
         return false;  // don't explore subexpressions any further
diff --git a/Source/DafnyCore/Resolver/ModuleResolver.cs b/Source/DafnyCore/Resolver/ModuleResolver.cs
index c012f2bd652..05f8b1ebfde 100644
--- a/Source/DafnyCore/Resolver/ModuleResolver.cs
+++ b/Source/DafnyCore/Resolver/ModuleResolver.cs
@@ -1696,17 +1696,14 @@ private void FillInPostConditionsAndBodiesOfPrefixLemmas(List<TopLevelDecl> decl
             var post = subst.CloneExpr(p.E);
             prefixLemma.Ens.Add(new AttributedExpression(post));
             foreach (var e in coConclusions) {
-              var fce = e as FunctionCallExpr;
-              if (fce != null) {
-                // the other possibility is that "e" is a BinaryExpr
+              if (e is FunctionCallExpr fce) {
                 GreatestPredicate predicate = (GreatestPredicate)fce.Function;
                 focalPredicates.Add(predicate);
                 // For every focal predicate P in S, add to S all greatest predicates in the same strongly connected
                 // component (in the call graph) as P
-                foreach (var node in predicate.EnclosingClass.EnclosingModuleDefinition.CallGraph.GetSCC(
-                           predicate)) {
-                  if (node is GreatestPredicate) {
-                    focalPredicates.Add((GreatestPredicate)node);
+                foreach (var node in predicate.EnclosingClass.EnclosingModuleDefinition.CallGraph.GetSCC(predicate)) {
+                  if (node is GreatestPredicate greatestPredicate) {
+                    focalPredicates.Add(greatestPredicate);
                   }
                 }
               }
@@ -1729,8 +1726,8 @@ private void FillInPostConditionsAndBodiesOfPrefixLemmas(List<TopLevelDecl> decl
               // For every focal predicate P in S, add to S all least predicates in the same strongly connected
               // component (in the call graph) as P
               foreach (var node in predicate.EnclosingClass.EnclosingModuleDefinition.CallGraph.GetSCC(predicate)) {
-                if (node is LeastPredicate) {
-                  focalPredicates.Add((LeastPredicate)node);
+                if (node is LeastPredicate leastPredicate) {
+                  focalPredicates.Add(leastPredicate);
                 }
               }
             }
diff --git a/Source/DafnyCore/Triggers/SplitPartTriggerWriter.cs b/Source/DafnyCore/Triggers/SplitPartTriggerWriter.cs
index 4e5eedefb82..49c27770468 100644
--- a/Source/DafnyCore/Triggers/SplitPartTriggerWriter.cs
+++ b/Source/DafnyCore/Triggers/SplitPartTriggerWriter.cs
@@ -84,9 +84,7 @@ public bool RewriteMatchingLoop(ErrorReporter reporter, ModuleDefinition module)
             var entry = substMap.Find(x => ExprExtensions.ExpressionEq(sub, x.Item1));
             if (entry == null) {
               var newBv = new BoundVar(sub.tok, "_t#" + substMap.Count, sub.Type);
-              var ie = new IdentifierExpr(sub.tok, newBv.Name);
-              ie.Var = newBv;
-              ie.Type = newBv.Type;
+              var ie = new IdentifierExpr(sub.tok, newBv.Name) { Var = newBv, Type = newBv.Type };
               substMap.Add(new Tuple<Expression, IdentifierExpr>(sub, ie));
             }
           }

From b17c662b2b520a83a7d08f18b4ce79c0ac63c782 Mon Sep 17 00:00:00 2001
From: Rustan Leino <leino@amazon.com>
Date: Mon, 14 Oct 2024 01:35:44 -0700
Subject: [PATCH 06/16] Also consider codatatype equality as a greatest focal
 predicate

---
 Source/DafnyCore/AST/ExtremeCloner.cs         | 12 ++++++++++++
 .../DafnyCore/AST/ExtremeLemmaBodyCloner.cs   |  4 ++++
 Source/DafnyCore/Resolver/ModuleResolver.cs   | 19 ++++++++++++++-----
 3 files changed, 30 insertions(+), 5 deletions(-)

diff --git a/Source/DafnyCore/AST/ExtremeCloner.cs b/Source/DafnyCore/AST/ExtremeCloner.cs
index 67cc276bf05..96411834bd9 100644
--- a/Source/DafnyCore/AST/ExtremeCloner.cs
+++ b/Source/DafnyCore/AST/ExtremeCloner.cs
@@ -63,4 +63,16 @@ protected Expression CloneCallAndAddK(FunctionCallExpr e) {
     reporter.Info(MessageSource.Cloner, e.tok, e.Name + suffix);
     return fexp;
   }
+
+  protected Expression CloneEqualityAndAndK(BinaryExpr binaryExpr) {
+    if (this.CloneResolvedFields) {
+      throw new NotImplementedException();
+    }
+
+    var eq = new TernaryExpr(Tok(binaryExpr.tok),
+      binaryExpr.ResolvedOp == BinaryExpr.ResolvedOpcode.EqCommon ? TernaryExpr.Opcode.PrefixEqOp : TernaryExpr.Opcode.PrefixNeqOp,
+      k, CloneExpr(binaryExpr.E0), CloneExpr(binaryExpr.E1));
+    reporter.Info(MessageSource.Cloner, binaryExpr.tok, "==" + suffix);
+    return eq;
+  }
 }
diff --git a/Source/DafnyCore/AST/ExtremeLemmaBodyCloner.cs b/Source/DafnyCore/AST/ExtremeLemmaBodyCloner.cs
index 66eda31ca9a..c5763a08f9e 100644
--- a/Source/DafnyCore/AST/ExtremeLemmaBodyCloner.cs
+++ b/Source/DafnyCore/AST/ExtremeLemmaBodyCloner.cs
@@ -49,6 +49,10 @@ public override Expression CloneExpr(Expression expr) {
             }
           }
         }
+      } else if (expr is BinaryExpr { ResolvedOp: BinaryExpr.ResolvedOpcode.EqCommon or BinaryExpr.ResolvedOpcode.NeqCommon } binaryExpr) {
+        if (binaryExpr.E0.Type.AsCoDatatype is { } coDatatypeDecl && focalCodatatypeEquality.Contains(coDatatypeDecl)) {
+          return CloneEqualityAndAndK(binaryExpr);
+        }
       }
     }
     return base.CloneExpr(expr);
diff --git a/Source/DafnyCore/Resolver/ModuleResolver.cs b/Source/DafnyCore/Resolver/ModuleResolver.cs
index 05f8b1ebfde..91398372d1d 100644
--- a/Source/DafnyCore/Resolver/ModuleResolver.cs
+++ b/Source/DafnyCore/Resolver/ModuleResolver.cs
@@ -1685,6 +1685,7 @@ private void FillInPostConditionsAndBodiesOfPrefixLemmas(List<TopLevelDecl> decl
 
         var k = prefixLemma.Ins[0];
         var focalPredicates = new HashSet<ExtremePredicate>();
+        var focalCodatatypeEquality = new HashSet<CoDatatypeDecl>();
         if (com is GreatestLemma) {
           // compute the postconditions of the prefix lemma
           Contract.Assume(prefixLemma.Ens.Count == 0); // these are not supposed to have been filled in before
@@ -1706,6 +1707,9 @@ private void FillInPostConditionsAndBodiesOfPrefixLemmas(List<TopLevelDecl> decl
                     focalPredicates.Add(greatestPredicate);
                   }
                 }
+              } else {
+                var binExpr = (BinaryExpr)e; // each "coConclusion" is either a FunctionCallExpr or a BinaryExpr
+                focalCodatatypeEquality.Add(binExpr.E0.Type.AsCoDatatype ?? binExpr.E1.Type.AsCoDatatype);
               }
             }
           }
@@ -1734,16 +1738,21 @@ private void FillInPostConditionsAndBodiesOfPrefixLemmas(List<TopLevelDecl> decl
           }
         }
 
-        reporter.Info(MessageSource.Resolver, com.tok,
-          focalPredicates.Count == 0
-            ? $"{com.PrefixLemma.Name} has no focal predicates"
-            : $"{com.PrefixLemma.Name} with focal predicate{Util.Plural(focalPredicates.Count)} {Util.Comma(focalPredicates, p => p.Name)}");
+        var focalCount = focalPredicates.Count + focalCodatatypeEquality.Count;
+        if (focalCount == 0) {
+          reporter.Info(MessageSource.Resolver, com.tok, $"{com.PrefixLemma.Name} has no focal predicates");
+        } else {
+          var predicates = Util.Comma(focalPredicates, p => p.Name);
+          var equalities = Util.Comma(focalCodatatypeEquality, decl => $"{decl.Name}.==");
+          var focals = predicates + (predicates.Length != 0 && equalities.Length != 0 ? ", " : "") + equalities;
+          reporter.Info(MessageSource.Resolver, com.tok, $"{com.PrefixLemma.Name} with focal predicate{Util.Plural(focalCount)} {focals}");
+        }
         // Compute the statement body of the prefix lemma
         Contract.Assume(prefixLemma.Body == null); // this is not supposed to have been filled in before
         if (com.Body != null) {
           var kMinusOne = new BinaryExpr(com.tok, BinaryExpr.Opcode.Sub, new IdentifierExpr(k.tok, k.Name),
             new LiteralExpr(com.tok, 1));
-          var subst = new ExtremeLemmaBodyCloner(com, kMinusOne, focalPredicates, this.reporter);
+          var subst = new ExtremeLemmaBodyCloner(com, kMinusOne, focalPredicates, focalCodatatypeEquality, this.reporter);
           var mainBody = subst.CloneBlockStmt(com.Body);
           Expression kk;
           Statement els;

From cee8d58168eb7b7c3d5af495a4c5b151008c75cb Mon Sep 17 00:00:00 2001
From: Rustan Leino <leino@amazon.com>
Date: Mon, 14 Oct 2024 01:37:09 -0700
Subject: [PATCH 07/16] Show tooltips for any quantifier rewrite substitutions

---
 Source/DafnyCore/Triggers/SplitPartTriggerWriter.cs | 6 +++++-
 1 file changed, 5 insertions(+), 1 deletion(-)

diff --git a/Source/DafnyCore/Triggers/SplitPartTriggerWriter.cs b/Source/DafnyCore/Triggers/SplitPartTriggerWriter.cs
index 49c27770468..abb809b9a54 100644
--- a/Source/DafnyCore/Triggers/SplitPartTriggerWriter.cs
+++ b/Source/DafnyCore/Triggers/SplitPartTriggerWriter.cs
@@ -13,6 +13,7 @@ class SplitPartTriggerWriter {
   public List<TriggerTerm> CandidateTerms { get; set; }
   public List<TriggerCandidate> Candidates { get; set; }
   private List<TriggerCandidate> RejectedCandidates { get; }
+  public List<Tuple<Expression, IdentifierExpr>> NamedExpressions { get; }
   private List<TriggerMatch> loopingMatches;
 
   private bool AllowsLoops {
@@ -28,6 +29,7 @@ private bool AllowsLoops {
   internal SplitPartTriggerWriter(ComprehensionExpr comprehension) {
     this.Comprehension = comprehension;
     this.RejectedCandidates = new List<TriggerCandidate>();
+    this.NamedExpressions = new();
   }
 
   internal void TrimInvalidTriggers() {
@@ -96,6 +98,7 @@ public bool RewriteMatchingLoop(ErrorReporter reporter, ModuleDefinition module)
     if (substMap.Count > 0) {
       var s = new ExprSubstituter(substMap);
       expr = s.Substitute(Comprehension) as QuantifierExpr;
+      NamedExpressions.AddRange(substMap);
     } else {
       // make a copy of the expr
       if (expr is ForallExpr) {
@@ -173,7 +176,8 @@ string InfoFirstLineEnd(int count) {
       messages.Add($"Part #{splitPartIndex} is '{Comprehension.Term}'");
     }
     if (Candidates.Any()) {
-      messages.Add($"Selected triggers:{InfoFirstLineEnd(Candidates.Count)}{string.Join(", ", Candidates)}");
+      var subst = Util.Comma("", NamedExpressions, pair => $" where {pair.Item2} := {pair.Item1}");
+      messages.Add($"Selected triggers:{InfoFirstLineEnd(Candidates.Count)}{string.Join(", ", Candidates)}{subst}");
     }
     if (RejectedCandidates.Any()) {
       messages.Add($"Rejected triggers:{InfoFirstLineEnd(RejectedCandidates.Count)}{string.Join("\n  ", RejectedCandidates)}");

From dda37cbcb1478137aaf4b26c29e1fa8b16727a0e Mon Sep 17 00:00:00 2001
From: Rustan Leino <leino@amazon.com>
Date: Mon, 14 Oct 2024 01:55:10 -0700
Subject: [PATCH 08/16] feat!: Auto-induction for twostate lemmas but not ghost
 methods

---
 Source/DafnyCore/Rewriters/InductionRewriter.cs | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

diff --git a/Source/DafnyCore/Rewriters/InductionRewriter.cs b/Source/DafnyCore/Rewriters/InductionRewriter.cs
index c8ca384bc12..8314cc34dc5 100644
--- a/Source/DafnyCore/Rewriters/InductionRewriter.cs
+++ b/Source/DafnyCore/Rewriters/InductionRewriter.cs
@@ -72,15 +72,17 @@ void ProcessFunctionExpressions(Function function) {
 
   void ComputeLemmaInduction(Method method) {
     Contract.Requires(method != null);
-    if (method is Lemma or PrefixLemma && method is { Body: not null, Outs: { Count: 0 } }) {
+    if (method is { IsGhost: true, AllowsAllocation: false, Outs: { Count: 0 }, Body: not null } and not ExtremeLemma) {
       Expression pre = Expression.CreateBoolLiteral(method.tok, true);
       foreach (var req in method.Req) {
         pre = Expression.CreateAnd(pre, req.E);
       }
+
       Expression post = Expression.CreateBoolLiteral(method.tok, true);
       foreach (var ens in method.Ens) {
         post = Expression.CreateAnd(post, ens.E);
       }
+
       ComputeInductionVariables(method.tok, method.Ins, Expression.CreateImplies(pre, post), method, ref method.Attributes);
     }
   }

From fa79ba3a8a85316586bd46ab13f9d08944fe1797 Mon Sep 17 00:00:00 2001
From: Rustan Leino <leino@amazon.com>
Date: Wed, 16 Oct 2024 07:33:22 -0700
Subject: [PATCH 09/16] =?UTF-8?q?fix:=20Don=E2=80=99t=20consider=20arrow-t?=
 =?UTF-8?q?yped=20variables=20for=20auto=20induction?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 Source/DafnyCore/Rewriters/InductionRewriter.cs     |  2 +-
 Source/DafnyCore/Triggers/TriggerExtensions.cs      |  7 +------
 .../LitTest/triggers/InductionWithoutTriggers.dfy   | 13 +++++++++++++
 .../triggers/InductionWithoutTriggers.dfy.expect    |  3 +++
 4 files changed, 18 insertions(+), 7 deletions(-)
 create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/triggers/InductionWithoutTriggers.dfy
 create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/triggers/InductionWithoutTriggers.dfy.expect

diff --git a/Source/DafnyCore/Rewriters/InductionRewriter.cs b/Source/DafnyCore/Rewriters/InductionRewriter.cs
index 8314cc34dc5..0cb37e9fa7c 100644
--- a/Source/DafnyCore/Rewriters/InductionRewriter.cs
+++ b/Source/DafnyCore/Rewriters/InductionRewriter.cs
@@ -179,7 +179,7 @@ void ComputeInductionVariables<TVarType>(IToken tok, List<TVarType> boundVars, E
     }
 
     foreach (IVariable n in boundVars) {
-      if (!(n.Type.IsTypeParameter || n.Type.IsAbstractType || n.Type.IsInternalTypeSynonym) &&
+      if (!(n.Type.IsTypeParameter || n.Type.IsAbstractType || n.Type.IsInternalTypeSynonym || n.Type.IsArrowType) &&
           (args != null || InductionHeuristic.VarOccursInArgumentToRecursiveFunction(Reporter.Options, body, n))) {
         inductionVariables.Add(new IdentifierExpr(n.Tok, n));
       }
diff --git a/Source/DafnyCore/Triggers/TriggerExtensions.cs b/Source/DafnyCore/Triggers/TriggerExtensions.cs
index e1417a6492a..6a79257962e 100644
--- a/Source/DafnyCore/Triggers/TriggerExtensions.cs
+++ b/Source/DafnyCore/Triggers/TriggerExtensions.cs
@@ -268,12 +268,7 @@ private static bool ShallowEq(WildcardExpr expr1, WildcardExpr expr2) {
     }
 
     private static bool ShallowEq(LambdaExpr expr1, LambdaExpr expr2) {
-#if THROW_UNSUPPORTED_COMPARISONS
-      Contract.Assume(false); // This kind of expression never appears in a trigger
-      throw new NotImplementedException();
-#else
-      return false;
-#endif
+      return true;
     }
 
     private static bool ShallowEq(MapComprehension expr1, MapComprehension expr2) {
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/triggers/InductionWithoutTriggers.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/triggers/InductionWithoutTriggers.dfy
new file mode 100644
index 00000000000..82bbf55f80c
--- /dev/null
+++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/triggers/InductionWithoutTriggers.dfy
@@ -0,0 +1,13 @@
+// RUN: %testDafnyForEachResolver "%s" --expect-exit-code=4
+
+ghost function Sum(n: nat, f: int -> int): int
+{
+  if n == 0 then 0 else f(n-1) + Sum(n-1, f)
+}
+
+lemma TestTriggerWithLambdaExpression(n: nat, f: int -> int, g: int -> int)
+{
+  // Once, trigger selection would crash on the following quantifier, which uses a LambdaExpr.
+  assert forall n: nat, f: int -> int :: Sum(n, x => 500 + f(x)) == n + Sum(n, f); // error: this does not hold
+}
+
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/triggers/InductionWithoutTriggers.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/triggers/InductionWithoutTriggers.dfy.expect
new file mode 100644
index 00000000000..dd60a022868
--- /dev/null
+++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/triggers/InductionWithoutTriggers.dfy.expect
@@ -0,0 +1,3 @@
+InductionWithoutTriggers.dfy(17,21): Warning: Could not find a trigger for the induction hypothesis. Without a trigger, this may cause brittle verification. Change or remove the {:induction} attribute to generate a different induction hypothesis, or add {:nowarn} to silence this warning. For more information, see the section quantifier instantiation rules in the reference manual.
+
+Dafny program verifier finished with 2 verified, 1 error

From 0028a3ad0034ccc6b52b072e8663fc76f66ed16d Mon Sep 17 00:00:00 2001
From: Rustan Leino <leino@amazon.com>
Date: Wed, 16 Oct 2024 07:35:15 -0700
Subject: [PATCH 10/16] feat: allow ternary expressions in triggers

---
 Source/DafnyCore/Triggers/TriggersCollector.cs | 1 +
 1 file changed, 1 insertion(+)

diff --git a/Source/DafnyCore/Triggers/TriggersCollector.cs b/Source/DafnyCore/Triggers/TriggersCollector.cs
index a39c6ce38ed..a210052fcab 100644
--- a/Source/DafnyCore/Triggers/TriggersCollector.cs
+++ b/Source/DafnyCore/Triggers/TriggersCollector.cs
@@ -101,6 +101,7 @@ expr is ApplyExpr ||
         expr is DisplayExpression ||
         expr is MapDisplayExpr ||
         expr is DatatypeValue ||
+        expr is TernaryExpr ||
         TranslateToFunctionCall(expr)) {
       return true;
     } else if (expr is BinaryExpr) {

From 394c635b09294f0ba9bc20b24038817aec88ad14 Mon Sep 17 00:00:00 2001
From: Rustan Leino <leino@amazon.com>
Date: Wed, 16 Oct 2024 07:58:24 -0700
Subject: [PATCH 11/16] Compute and use triggers for induction hypotheses

---
 .../DafnyCore/Rewriters/InductionRewriter.cs  | 55 ++++++++++++++++---
 .../LitTest/dafny0/AutoContracts.dfy.expect   |  4 +-
 .../LitTest/dafny0/PrefixTypeSubst.dfy.expect | 12 ++--
 .../LitTests/LitTest/dafny2/Calculations.dfy  |  8 +++
 .../LitTests/LitTest/dafny3/Abstemious.dfy    |  3 +-
 .../LitTests/LitTest/dafny4/Bug170.dfy.expect |  5 +-
 .../LitTests/LitTest/dafny4/GHC-MergeSort.dfy | 11 ++++
 .../LitTest/dafny4/Lucas-up.legacy.dfy        |  4 +-
 .../LitTests/LitTest/dafny4/UnionFind.dfy     |  2 +-
 .../git-issues/git-issue-977.dfy.expect       |  9 +++
 .../LitTest/git-issues/github-issue-4804.dfy  |  2 +-
 .../LitTests/LitTest/hofs/SumSum.dfy          |  6 +-
 .../LitTests/LitTest/lambdas/MatrixAssoc.dfy  |  2 +-
 .../triggers/InductionWithoutTriggers.dfy     |  8 +++
 .../InductionWithoutTriggers.dfy.expect       |  1 +
 15 files changed, 104 insertions(+), 28 deletions(-)

diff --git a/Source/DafnyCore/Rewriters/InductionRewriter.cs b/Source/DafnyCore/Rewriters/InductionRewriter.cs
index 0cb37e9fa7c..e6a8cf4ae4e 100644
--- a/Source/DafnyCore/Rewriters/InductionRewriter.cs
+++ b/Source/DafnyCore/Rewriters/InductionRewriter.cs
@@ -165,8 +165,23 @@ void ComputeInductionVariables<TVarType>(IToken tok, List<TVarType> boundVars, E
         return;
       }
 
-      // The argument list was legal, so let's use it for the _induction attribute
+      // The argument list was legal, so let's use it for the _induction attribute.
+      // Next, look for matching patterns for the induction hypothesis.
+      if (lemma != null) {
+        var triggers = ComputeAndReportInductionTriggers(lemma, ref attributes, goodArguments, body);
+        if (triggers.Count == 0) {
+          var suppressWarnings = Attributes.Contains(attributes, "nowarn");
+          var warningLevel = suppressWarnings ? ErrorLevel.Info : ErrorLevel.Warning;
+
+          Reporter.Message(MessageSource.Rewriter, warningLevel, null, tok,
+            $"Could not find a trigger for the induction hypothesis. Without a trigger, this may cause brittle verification. " +
+            $"Change or remove the {{:induction}} attribute to generate a different induction hypothesis, or add {{:nowarn}} to silence this warning. " +
+            $"For more information, see the section quantifier instantiation rules in the reference manual.");
+        }
+      }
+
       attributes = new Attributes("_induction", goodArguments, attributes);
+
       return;
     }
 
@@ -186,8 +201,9 @@ void ComputeInductionVariables<TVarType>(IToken tok, List<TVarType> boundVars, E
     }
 
     if (inductionVariables.Count != 0) {
+      List<List<Expression>> triggers = null;
       if (lemma != null) {
-        var triggers = ComputeInductionTriggers(inductionVariables, body, lemma.EnclosingClass.EnclosingModuleDefinition);
+        triggers = ComputeInductionTriggers(inductionVariables, body, lemma.EnclosingClass.EnclosingModuleDefinition);
         if (triggers.Count == 0) {
           var msg = "omitting automatic induction because of lack of triggers";
           if (args != null) {
@@ -197,10 +213,6 @@ void ComputeInductionVariables<TVarType>(IToken tok, List<TVarType> boundVars, E
           }
           return;
         }
-
-        foreach (var trigger in triggers) {
-          attributes = new Attributes("_inductionPattern", trigger, attributes);
-        }
       }
 
       // We found something usable, so let's record that in an attribute
@@ -210,8 +222,32 @@ void ComputeInductionVariables<TVarType>(IToken tok, List<TVarType> boundVars, E
       if (lemma is PrefixLemma) {
         s = lemma.Name + " " + s;
       }
-
       Reporter.Info(MessageSource.Rewriter, tok, s);
+
+      if (triggers != null) {
+        ReportInductionTriggers(lemma, ref attributes, triggers);
+      }
+    }
+  }
+
+  List<List<Expression>> ComputeAndReportInductionTriggers(Method lemma, ref Attributes attributes, List<Expression> inductionVariables,
+    Expression body) {
+    var triggers = ComputeInductionTriggers(inductionVariables, body, lemma.EnclosingClass.EnclosingModuleDefinition);
+    ReportInductionTriggers(lemma, ref attributes, triggers);
+    return triggers;
+  }
+
+  private void ReportInductionTriggers(Method lemma, ref Attributes attributes, List<List<Expression>> triggers) {
+    foreach (var trigger in triggers) {
+      attributes = new Attributes("_inductionPattern", trigger, attributes);
+#if DEBUG
+      var ss = Printer.OneAttributeToString(Reporter.Options, attributes, "inductionPattern");
+      if (lemma is PrefixLemma) {
+        ss = lemma.Name + " " + ss;
+      }
+
+      Reporter.Info(MessageSource.Rewriter, lemma.tok, ss);
+#endif
     }
   }
 
@@ -253,7 +289,10 @@ List<List<Expression>> ComputeInductionTriggers(List<Expression> inductionVariab
     var triggersCollector = new Triggers.TriggersCollector(finder.exprsInOldContext, Reporter.Options, moduleDefinition);
     var quantifierCollection = new Triggers.ComprehensionTriggerGenerator(quantifier, Enumerable.Repeat(quantifier, 1), Reporter);
     quantifierCollection.ComputeTriggers(triggersCollector);
-    var triggers = quantifierCollection.GetTriggers();
+    // Get the computed triggers, but only ask for those that do not require additional bound variables. (An alternative to this
+    // design would be to add {:matchinglooprewrite false} to "quantifier" above. However, that would cause certain matching loops
+    // to be ignored, so it is safer to not include triggers that require additional bound variables.)
+    var triggers = quantifierCollection.GetTriggers(false);
     var reverseSubstituter = new Substituter(null, reverseSubstMap, new Dictionary<TypeParameter, Type>());
     return triggers.ConvertAll(trigger => trigger.ConvertAll(reverseSubstituter.Substitute));
   }
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/AutoContracts.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/AutoContracts.dfy.expect
index 50ce7f167c5..934b0a287e3 100644
--- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/AutoContracts.dfy.expect
+++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/AutoContracts.dfy.expect
@@ -248,13 +248,13 @@ module OneModule {
       data < 20
     }
 
-    lemma /*{:_induction this}*/ L()
+    lemma L()
       requires Valid()
       ensures data < 100
     {
     }
 
-    twostate lemma /*{:_induction this}*/ TL()
+    twostate lemma TL()
       requires old(Valid())
       ensures old(data) <= data
     {
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/PrefixTypeSubst.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/PrefixTypeSubst.dfy.expect
index 71102103951..7f1f51f43c1 100644
--- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/PrefixTypeSubst.dfy.expect
+++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/PrefixTypeSubst.dfy.expect
@@ -231,7 +231,7 @@ greatest lemma N<D0, D1, D2>(o: MyClass<D0, D1>)
   N<D0, D1, D2>(o);
 }
 /***
-lemma {:axiom} /*{:_induction _k}*/ N#<D0, D1, D2>[_k: ORDINAL](o: MyClass<D0, D1>)
+lemma {:axiom} /*{:_induction _k}*/ /*{:_inductionPattern o.R#[_k]()}*/ N#<D0, D1, D2>[_k: ORDINAL](o: MyClass<D0, D1>)
   ensures o.R#<D2>[_k]()
   decreases _k, o
 {
@@ -253,7 +253,7 @@ greatest lemma O<D0, D1, D2>()
   O<D0, D1, D2>();
 }
 /***
-lemma {:axiom} /*{:_induction _k}*/ O#<D0, D1, D2>[_k: ORDINAL]()
+lemma {:axiom} /*{:_induction _k}*/ /*{:_inductionPattern MyClass<D0, D1>.S#[_k]()}*/ O#<D0, D1, D2>[_k: ORDINAL]()
   ensures MyClass<D0, D1>.S#<D2>[_k]()
   decreases _k
 {
@@ -448,7 +448,7 @@ greatest lemma RstRst7<alpha, beta, gamma>()
   }
 }
 /***
-lemma {:axiom} /*{:_induction _k}*/ RstRst7#<alpha, beta, gamma>[_k: ORDINAL]()
+lemma {:axiom} /*{:_induction _k}*/ /*{:_inductionPattern MyClass<alpha, beta>.RST#[_k]()}*/ RstRst7#<alpha, beta, gamma>[_k: ORDINAL]()
   ensures MyClass<alpha, beta>.RST#<gamma>[_k]()
   decreases _k
 {
@@ -512,7 +512,7 @@ greatest lemma RstRst10<alpha, beta, gamma>[nat]()
 {
 }
 /***
-lemma {:axiom} /*{:_induction _k}*/ RstRst10#<alpha, beta, gamma>[_k: nat]()
+lemma {:axiom} /*{:_induction _k}*/ /*{:_inductionPattern MyClass<alpha, beta>.RST_Nat#[_k]()}*/ RstRst10#<alpha, beta, gamma>[_k: nat]()
   ensures MyClass<alpha, beta>.RST_Nat#<gamma>[_k]()
   decreases _k
 {
@@ -588,7 +588,7 @@ class MyClass<A, B> {
     L(u, v);
   }
   /***
-  lemma {:axiom} /*{:_induction this, _k}*/ L#<U, V>[_k: ORDINAL](u: U, v: V)
+  lemma {:axiom} /*{:_induction _k}*/ /*{:_inductionPattern P#[_k](u, v)}*/ L#<U, V>[_k: ORDINAL](u: U, v: V)
     ensures P#[_k](u, v)
     decreases _k
   {
@@ -611,7 +611,7 @@ class MyClass<A, B> {
     assert R#<char>[_k - 1]();
   }
   /***
-  lemma {:axiom} /*{:_induction this, _k}*/ M#<W>[_k: ORDINAL]()
+  lemma {:axiom} /*{:_induction _k}*/ /*{:_inductionPattern R#[_k]()}*/ M#<W>[_k: ORDINAL]()
     ensures R#<char>[_k]()
     decreases _k
   {
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny2/Calculations.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny2/Calculations.dfy
index 14926010e4e..ecf9db84e66 100644
--- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny2/Calculations.dfy
+++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny2/Calculations.dfy
@@ -49,6 +49,14 @@ lemma Lemma_ConcatNil(xs : List)
 lemma Lemma_RevCatCommute(xs : List)
   ensures forall ys, zs :: revacc(xs, concat(ys, zs)) == concat(revacc(xs, ys), zs);
 {
+  forall ys, zs
+    ensures revacc(xs, concat(ys, zs)) == concat(revacc(xs, ys), zs)
+  {
+    match xs
+    case Nil =>
+    case Cons(_, xs') =>
+      Lemma_RevCatCommute(xs');
+  }
 }
 
 // Here is a theorem that says "qreverse" and "reverse" calculate the same result.  The proof
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny3/Abstemious.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny3/Abstemious.dfy
index 9645b0cf2f3..5eb338afaa8 100644
--- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny3/Abstemious.dfy
+++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny3/Abstemious.dfy
@@ -143,9 +143,10 @@ greatest lemma OhOnesTail_Correct()
 {
 }
 
-greatest lemma OhOnes_Correct()
+lemma OhOnes_Correct()
   ensures OhOnes() == Cons(0, ones())
 {
+  OhOnesTail_Correct();
 }
 
 lemma OhOnes_Correct'(n: nat)
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny4/Bug170.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny4/Bug170.dfy.expect
index 9b8aeb71c83..976b1a237f1 100644
--- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny4/Bug170.dfy.expect
+++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny4/Bug170.dfy.expect
@@ -14,8 +14,6 @@ Bug170.dfy(10,12): Info: B#[_k - 1]
 Bug170.dfy(15,12): Info: A#[_k - 1]
 Bug170.dfy(18,14): Info: AA# decreases _k, x
 Bug170.dfy(26,14): Info: BB# decreases _k, x
-Bug170.dfy(18,14): Info: AA# {:induction _k, x}
-Bug170.dfy(26,14): Info: BB# {:induction _k, x}
 Bug170.dfy(36,21): Info: _k: ORDINAL
 Bug170.dfy(41,21): Info: _k: ORDINAL
 Bug170.dfy(46,17): Info: _k: ORDINAL
@@ -33,7 +31,9 @@ Bug170.dfy(43,4): Info: A#[_k - 1]
 Bug170.dfy(46,17): Info: AA# decreases _k, x
 Bug170.dfy(53,17): Info: BB# decreases _k, x
 Bug170.dfy(46,17): Info: AA# {:induction _k, x}
+Bug170.dfy(46,17): Info: AA# {:inductionPattern A#[_k](x)}
 Bug170.dfy(53,17): Info: BB# {:induction _k, x}
+Bug170.dfy(53,17): Info: BB# {:inductionPattern B#[_k](x)}
 Bug170.dfy(64,18): Info: _k: ORDINAL
 Bug170.dfy(69,14): Info: _k: ORDINAL
 Bug170.dfy(70,14): Info: A#[_k]
@@ -42,7 +42,6 @@ Bug170.dfy(72,7): Info: A#[_k - 1]
 Bug170.dfy(73,6): Info: AA#[_k - 1]
 Bug170.dfy(66,12): Info: A#[_k - 1]
 Bug170.dfy(69,14): Info: AA# decreases _k, x
-Bug170.dfy(69,14): Info: AA# {:induction _k, x}
 Bug170.dfy(50,11): Info: Some instances of this call are not inlined.
 Bug170.dfy(57,11): Info: Some instances of this call are not inlined.
 
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny4/GHC-MergeSort.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny4/GHC-MergeSort.dfy
index a4022dc988a..bd80b089d5c 100644
--- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny4/GHC-MergeSort.dfy
+++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny4/GHC-MergeSort.dfy
@@ -472,6 +472,17 @@ lemma stable_sequences(g: G, xs: List<G>)
     case Cons(a, ys) =>
       match ys {
         case Nil =>
+          calc {
+            flatten(sequences(xs));
+            // def. sequences, since xs == Cons(a, Nil)
+            flatten(Cons(xs, Nil));
+            // def. flatten
+            append(xs, flatten(Nil));
+            // def. flatten
+            append(xs, Nil);
+            { append_Nil(xs); }
+            xs;
+          }
         case Cons(b, zs) =>
           if !Below(a, b) {
             calc {
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny4/Lucas-up.legacy.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny4/Lucas-up.legacy.dfy
index 38413c3be06..5ba9023a9a7 100644
--- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny4/Lucas-up.legacy.dfy
+++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny4/Lucas-up.legacy.dfy
@@ -66,7 +66,7 @@ ghost function binom(a: nat, b: nat): nat
 // div-2 is applied to both arguments, except in the case where
 // the first argument to "binom" is even and the second argument
 // is odd, in which case "binom" is always even.
-lemma {:resource_limit "8e6"} Lucas_Binary(a: nat, b: nat)
+lemma {:resource_limit "8e6"} {:induction a, b} {:nowarn} Lucas_Binary(a: nat, b: nat)
   ensures EVEN(binom(2*a, 2*b + 1))
   ensures EVEN(binom(2*a, 2*b)) <==> EVEN(binom(a, b))
   ensures EVEN(binom(2*a + 1, 2*b + 1)) <==> EVEN(binom(a, b))
@@ -83,7 +83,7 @@ lemma {:resource_limit "8e6"} Lucas_Binary(a: nat, b: nat)
 }
 
 // Here is an alternative way to phrase the previous lemma.
-lemma {:resource_limit "200e6"} Lucas_Binary'(a: nat, b: nat)
+lemma {:resource_limit "200e6"} {:induction a, b} {:nowarn} Lucas_Binary'(a: nat, b: nat)
   ensures binom(2*a, 2*b) % 2 == binom(a, b) % 2
   ensures binom(2*a, 2*b + 1) % 2 == 0
   ensures binom(2*a + 1, 2*b) % 2 == binom(a, b) % 2
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny4/UnionFind.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny4/UnionFind.dfy
index d80ac5cac0c..3831148a1cc 100644
--- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny4/UnionFind.dfy
+++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny4/UnionFind.dfy
@@ -264,7 +264,7 @@ module M3 refines M2 {
       }
     }
 
-    lemma {:autocontracts false} ReachUnaffectedByChangeFromRoot'(d: nat, e: Element, r: Element, C: CMap, td: nat, r0: Element, r1: Element, C': CMap)
+    lemma {:autocontracts false} {:induction d, e, r, C} {:nowarn} ReachUnaffectedByChangeFromRoot'(d: nat, e: Element, r: Element, C: CMap, td: nat, r0: Element, r1: Element, C': CMap)
       requires GoodCMap(C)
       requires e in C && Reaches(d, e, r, C)
       requires r0 in C && r1 in C && C[r0].Root? && C[r1].Root? && C[r0].depth == C[r1].depth && r0 != r1
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-977.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-977.dfy.expect
index a88c1419457..db3dee30b5b 100644
--- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-977.dfy.expect
+++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-977.dfy.expect
@@ -28,8 +28,17 @@ git-issue-977.dfy(84,16): Info: decreases num
 git-issue-977.dfy(129,16): Info: decreases k, num
 git-issue-977.dfy(146,16): Info: decreases k, num
 git-issue-977.dfy(54,6): Info: {:induction num}
+git-issue-977.dfy(54,6): Info: {:inductionPattern GreatestPredNat(num)}
+git-issue-977.dfy(54,6): Info: {:inductionPattern GreatestPredOrd(num)}
+git-issue-977.dfy(54,6): Info: {:inductionPattern Pred(num)}
 git-issue-977.dfy(61,6): Info: {:induction k, num}
+git-issue-977.dfy(61,6): Info: {:inductionPattern RicochetOrd(k, num)}
+git-issue-977.dfy(61,6): Info: {:inductionPattern GreatestManualOrd(k, num)}
+git-issue-977.dfy(61,6): Info: {:inductionPattern GreatestPredOrd#[k](num)}
 git-issue-977.dfy(77,6): Info: {:induction k, num}
+git-issue-977.dfy(77,6): Info: {:inductionPattern RicochetNat(k, num)}
+git-issue-977.dfy(77,6): Info: {:inductionPattern GreatestManualNat(k, num)}
+git-issue-977.dfy(77,6): Info: {:inductionPattern GreatestPredNat#[k](num)}
 git-issue-977.dfy(71,4): Info: ensures GreatestPredOrd#[m](num)
 git-issue-977.dfy(71,4): Info: ensures GreatestManualOrd(m, num)
 git-issue-977.dfy(71,4): Info: ensures RicochetOrd(m, num)
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/github-issue-4804.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/github-issue-4804.dfy
index 35dc939d8eb..6516b3be1a8 100644
--- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/github-issue-4804.dfy
+++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/github-issue-4804.dfy
@@ -1,4 +1,4 @@
-// RUN: %exits-with 4 %verify --allow-axioms --resource-limit 1000000 %s > %t
+// RUN: %exits-with 4 %verify --allow-axioms --resource-limit 1200 %s > %t
 // RUN: %diff "%s.expect" "%t"
 module Power {
 
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/hofs/SumSum.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/hofs/SumSum.dfy
index 4a7f8894e41..bda1eb00196 100644
--- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/hofs/SumSum.dfy
+++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/hofs/SumSum.dfy
@@ -20,6 +20,7 @@ lemma ExchangeEta(n: nat, f: int -> int, g: int -> int)
   requires forall i :: 0 <= i < n ==> f(i) == g(i)
   ensures Sum(n, x => f(x)) == Sum(n, x => g(x))
 {
+  if n != 0 { ExchangeEta(n - 1, f, g); }
 }
 
 lemma NestedAlphaRenaming(n: nat, g: (int,int) -> int)
@@ -37,10 +38,10 @@ lemma Distribute(n: nat, f: int -> int, g: int -> int)
 {
 }
 
-lemma {:induction false} PrettyBasicBetaReduction(n: nat, g: (int,int) -> int, i: int)
+lemma PrettyBasicBetaReduction(n: nat, g: (int,int) -> int, i: int)
   ensures (x => Sum(n, y => g(x,y)))(i) == Sum(n, y => g(i,y))
 {
-  // NOTE: This proof is by induction on n (it can be done automatically)
+  // NOTE: This proof is by induction on n
   if n == 0 {
     calc {
       (x => Sum(n, y => g(x,y)))(i);
@@ -62,7 +63,6 @@ lemma {:induction false} PrettyBasicBetaReduction(n: nat, g: (int,int) -> int, i
 lemma BetaReduction0(n: nat, g: (int,int) -> int, i: int)
   ensures (x => Sum(n, y => g(x,y)))(i) == Sum(n, y => g(i,y))
 {
-  // automatic proof by induction on n
 }
 
 lemma BetaReduction1(n': nat, g: (int,int) -> int, i: int)
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/lambdas/MatrixAssoc.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/lambdas/MatrixAssoc.dfy
index 0c777579f63..9a528b39724 100644
--- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/lambdas/MatrixAssoc.dfy
+++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/lambdas/MatrixAssoc.dfy
@@ -73,7 +73,7 @@ lemma distr_mult(f: Index -> int, x: int)
 
 /** Σ_k (Σ_l f(k,l))  ==  Σ_l (Σ_k f(k,l)) */
 /** proof by induction */
-lemma sum_assoc_n(m: Matrix, n1: nat, n2: nat)
+lemma {:induction m, n1, n2} {:nowarn} sum_assoc_n(m: Matrix, n1: nat, n2: nat)
   requires n1 <= N && n2 <= N
   ensures Sum_n((k: Index) => Sum_n((l: Index) => m(k)(l), n1), n2)
           ==
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/triggers/InductionWithoutTriggers.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/triggers/InductionWithoutTriggers.dfy
index 82bbf55f80c..171bc0a8612 100644
--- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/triggers/InductionWithoutTriggers.dfy
+++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/triggers/InductionWithoutTriggers.dfy
@@ -11,3 +11,11 @@ lemma TestTriggerWithLambdaExpression(n: nat, f: int -> int, g: int -> int)
   assert forall n: nat, f: int -> int :: Sum(n, x => 500 + f(x)) == n + Sum(n, f); // error: this does not hold
 }
 
+// With an explicit :induction attribute, the induction hypothesis emitted lets the proof of the lemma go through.
+// However, there is no good matching pattern for the induction hypothesis, so a warning is generated.
+// For a manual proof of this lemma, see lemma ExchangeEta in hofs/SumSum.dfy.
+lemma {:induction n} ExchangeEtaWithInductionAttribute(n: nat, f: int -> int, g: int -> int) // warning: no trigger
+  requires forall i :: 0 <= i < n ==> f(i) == g(i)
+  ensures Sum(n, x => f(x)) == Sum(n, x => g(x))
+{
+}
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/triggers/InductionWithoutTriggers.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/triggers/InductionWithoutTriggers.dfy.expect
index dd60a022868..815d9943bf2 100644
--- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/triggers/InductionWithoutTriggers.dfy.expect
+++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/triggers/InductionWithoutTriggers.dfy.expect
@@ -1,3 +1,4 @@
 InductionWithoutTriggers.dfy(17,21): Warning: Could not find a trigger for the induction hypothesis. Without a trigger, this may cause brittle verification. Change or remove the {:induction} attribute to generate a different induction hypothesis, or add {:nowarn} to silence this warning. For more information, see the section quantifier instantiation rules in the reference manual.
+InductionWithoutTriggers.dfy(11,9): Error: assertion might not hold
 
 Dafny program verifier finished with 2 verified, 1 error

From 659d4bada49288f2060bc7028e43be1a8671e5d5 Mon Sep 17 00:00:00 2001
From: Rustan Leino <leino@amazon.com>
Date: Wed, 16 Oct 2024 07:59:42 -0700
Subject: [PATCH 12/16] Tooltip named expressions from trigger selection

---
 .../Triggers/ComprehensionTriggerGenerator.cs     | 15 +++++++++------
 .../LitTest/triggers/let-expressions.dfy.expect   |  4 ++--
 .../loop-detection-is-not-too-strict.dfy.expect   |  6 +++---
 .../loop-detection-looks-at-ranges-too.dfy.expect |  4 ++--
 ...loop-detection-messages--unit-tests.dfy.expect | 10 +++++-----
 .../matrix-accesses-are-triggers.dfy.expect       |  2 +-
 ...t-look-like-the-triggers-they-match.dfy.expect |  6 +++---
 ...ting-triggers-recovers-expressivity.dfy.expect |  4 ++--
 ...ppressing-warnings-behaves-properly.dfy.expect |  2 +-
 9 files changed, 28 insertions(+), 25 deletions(-)

diff --git a/Source/DafnyCore/Triggers/ComprehensionTriggerGenerator.cs b/Source/DafnyCore/Triggers/ComprehensionTriggerGenerator.cs
index 65723ba9829..91b5e565632 100644
--- a/Source/DafnyCore/Triggers/ComprehensionTriggerGenerator.cs
+++ b/Source/DafnyCore/Triggers/ComprehensionTriggerGenerator.cs
@@ -231,15 +231,18 @@ internal void CommitTriggers(SystemModuleManager systemModuleManager) {
       }
     }
 
-    public List<List<Expression>> GetTriggers() {
+    public List<List<Expression>> GetTriggers(bool includeTriggersThatRequireNamedExpressions) {
       var triggers = new List<List<Expression>>();
       foreach (var triggerWriter in partWriters) {
-        foreach (var triggerTerms in triggerWriter.Candidates) {
-          var trigger = new List<Expression>();
-          foreach (var triggerTerm in triggerTerms.Terms) {
-            trigger.Add(triggerTerm.Expr);
+        if (includeTriggersThatRequireNamedExpressions || triggerWriter.NamedExpressions.Count == 0) {
+          foreach (var triggerTerms in triggerWriter.Candidates) {
+            var trigger = new List<Expression>();
+            foreach (var triggerTerm in triggerTerms.Terms) {
+              trigger.Add(triggerTerm.Expr);
+            }
+
+            triggers.Add(trigger);
           }
-          triggers.Add(trigger);
         }
       }
       return triggers;
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/triggers/let-expressions.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/triggers/let-expressions.dfy.expect
index c2731da3a7c..43c6c5c9d54 100644
--- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/triggers/let-expressions.dfy.expect
+++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/triggers/let-expressions.dfy.expect
@@ -1,6 +1,6 @@
 let-expressions.dfy(6,8): Info: Selected triggers: {s[i]}
 let-expressions.dfy(7,8): Info: Selected triggers: {s[i]}
-let-expressions.dfy(8,8): Info: Selected triggers: {s[_t#0], s[i]}
-let-expressions.dfy(9,8): Info: Selected triggers: {s[_t#0], s[i]}
+let-expressions.dfy(8,8): Info: Selected triggers: {s[_t#0], s[i]} where _t#0 := i + 1
+let-expressions.dfy(9,8): Info: Selected triggers: {s[_t#0], s[i]} where _t#0 := i + 1
 
 Dafny program verifier finished with 1 verified, 0 errors
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/triggers/loop-detection-is-not-too-strict.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/triggers/loop-detection-is-not-too-strict.dfy.expect
index aef0837895c..4c9f454a9c4 100644
--- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/triggers/loop-detection-is-not-too-strict.dfy.expect
+++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/triggers/loop-detection-is-not-too-strict.dfy.expect
@@ -2,14 +2,14 @@ loop-detection-is-not-too-strict.dfy(15,9): Info: Selected triggers:
    {P(y, x)}, {P(x, y)}
 loop-detection-is-not-too-strict.dfy(18,9): Info: Selected triggers:
    {P(y, x)}, {P(x, y)}
-loop-detection-is-not-too-strict.dfy(21,9): Info: Selected triggers: {P(x, _t#0), P(x, y)}
+loop-detection-is-not-too-strict.dfy(21,9): Info: Selected triggers: {P(x, _t#0), P(x, y)} where _t#0 := y + 1
 loop-detection-is-not-too-strict.dfy(26,9): Info: Selected triggers: {Q(x)}
 loop-detection-is-not-too-strict.dfy(27,9): Info: Selected triggers: {Q(x)}
 loop-detection-is-not-too-strict.dfy(28,9): Info: Selected triggers:
    {P(x, z)}, {P(x, 1)}
 loop-detection-is-not-too-strict.dfy(33,9): Info: Selected triggers: {Q(x)}
 loop-detection-is-not-too-strict.dfy(34,9): Info: Selected triggers: {Q(x)}
-loop-detection-is-not-too-strict.dfy(36,9): Info: Selected triggers: {Q(_t#0), Q(x)}
-loop-detection-is-not-too-strict.dfy(40,9): Info: Selected triggers: {Q(_t#0), Q(x)}
+loop-detection-is-not-too-strict.dfy(36,9): Info: Selected triggers: {Q(_t#0), Q(x)} where _t#0 := if z > 1 then x else 3 * z + 1
+loop-detection-is-not-too-strict.dfy(40,9): Info: Selected triggers: {Q(_t#0), Q(x)} where _t#0 := x + 1
 
 Dafny program verifier finished with 1 verified, 0 errors
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/triggers/loop-detection-looks-at-ranges-too.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/triggers/loop-detection-looks-at-ranges-too.dfy.expect
index a6679d8c1ea..992d2e551f2 100644
--- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/triggers/loop-detection-looks-at-ranges-too.dfy.expect
+++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/triggers/loop-detection-looks-at-ranges-too.dfy.expect
@@ -1,4 +1,4 @@
-loop-detection-looks-at-ranges-too.dfy(11,17): Info: Selected triggers: {P(_t#0), P(x)}
-loop-detection-looks-at-ranges-too.dfy(13,17): Info: Selected triggers: {P(x), P(_t#0)}
+loop-detection-looks-at-ranges-too.dfy(11,17): Info: Selected triggers: {P(_t#0), P(x)} where _t#0 := x + 1
+loop-detection-looks-at-ranges-too.dfy(13,17): Info: Selected triggers: {P(x), P(_t#0)} where _t#0 := x + 1
 
 Dafny program verifier finished with 1 verified, 0 errors
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/triggers/loop-detection-messages--unit-tests.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/triggers/loop-detection-messages--unit-tests.dfy.expect
index 374f02b7f9b..3d8d9a1765e 100644
--- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/triggers/loop-detection-messages--unit-tests.dfy.expect
+++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/triggers/loop-detection-messages--unit-tests.dfy.expect
@@ -1,21 +1,21 @@
 loop-detection-messages--unit-tests.dfy(11,9): Info: Selected triggers: {f(f(i))}
  Rejected triggers: {f(i)} (may loop with "f(f(i))")
-loop-detection-messages--unit-tests.dfy(12,9): Info: Selected triggers: {f(_t#0), f(i)}
-loop-detection-messages--unit-tests.dfy(13,9): Info: Selected triggers: {f(_t#0), f(i)}
+loop-detection-messages--unit-tests.dfy(12,9): Info: Selected triggers: {f(_t#0), f(i)} where _t#0 := i + 1
+loop-detection-messages--unit-tests.dfy(13,9): Info: Selected triggers: {f(_t#0), f(i)} where _t#0 := i + 1
 loop-detection-messages--unit-tests.dfy(15,9): Info: Quantifier was split into 2 parts. Better verification performance and error reporting may be obtained by splitting the quantifier in source. For more information, see the section quantifier instantiation rules in the reference manual.
 loop-detection-messages--unit-tests.dfy(15,9): Info: Part #0 is 'false ==> f(i) == f(_t#0)'
- Selected triggers: {f(_t#0), f(i)}
+ Selected triggers: {f(_t#0), f(i)} where _t#0 := i + 1
 loop-detection-messages--unit-tests.dfy(15,9): Info: Part #1 is 'false ==> f(i) == g(i)'
  Selected triggers:
    {g(i)}, {f(i)}
 loop-detection-messages--unit-tests.dfy(16,9): Info: Quantifier was split into 2 parts. Better verification performance and error reporting may be obtained by splitting the quantifier in source. For more information, see the section quantifier instantiation rules in the reference manual.
 loop-detection-messages--unit-tests.dfy(16,9): Info: Part #0 is 'false ==> f(i) == f(_t#0)'
- Selected triggers: {f(_t#0), f(i)}
+ Selected triggers: {f(_t#0), f(i)} where _t#0 := i + 1
 loop-detection-messages--unit-tests.dfy(16,9): Info: Part #1 is 'false ==> f(i) == f(i)'
  Selected triggers: {f(i)}
 loop-detection-messages--unit-tests.dfy(17,9): Info: Quantifier was split into 2 parts. Better verification performance and error reporting may be obtained by splitting the quantifier in source. For more information, see the section quantifier instantiation rules in the reference manual.
 loop-detection-messages--unit-tests.dfy(17,9): Info: Part #0 is 'false ==> f(i) == f(_t#0)'
- Selected triggers: {f(_t#0), f(i)}
+ Selected triggers: {f(_t#0), f(i)} where _t#0 := i + 1
 loop-detection-messages--unit-tests.dfy(17,9): Info: Part #1 is 'false ==> f(i) == f(i)'
  Selected triggers: {f(i)}
 loop-detection-messages--unit-tests.dfy(19,9): Info: Selected triggers: {f(i)}
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/triggers/matrix-accesses-are-triggers.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/triggers/matrix-accesses-are-triggers.dfy.expect
index 4dc44f54ccf..4de25509099 100644
--- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/triggers/matrix-accesses-are-triggers.dfy.expect
+++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/triggers/matrix-accesses-are-triggers.dfy.expect
@@ -1,4 +1,4 @@
-matrix-accesses-are-triggers.dfy(7,11): Info: Selected triggers: {m[j, _t#0], m[i, j]}
+matrix-accesses-are-triggers.dfy(7,11): Info: Selected triggers: {m[j, _t#0], m[i, j]} where _t#0 := i + 1
 matrix-accesses-are-triggers.dfy(7,82): Error: index 0 out of range
 matrix-accesses-are-triggers.dfy(7,86): Error: index 1 out of range
 
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/triggers/some-terms-do-not-look-like-the-triggers-they-match.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/triggers/some-terms-do-not-look-like-the-triggers-they-match.dfy.expect
index 592b2b34dcd..ccd871551da 100644
--- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/triggers/some-terms-do-not-look-like-the-triggers-they-match.dfy.expect
+++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/triggers/some-terms-do-not-look-like-the-triggers-they-match.dfy.expect
@@ -1,9 +1,9 @@
-some-terms-do-not-look-like-the-triggers-they-match.dfy(12,17): Info: Selected triggers: {s[_t#0], s[x]}
+some-terms-do-not-look-like-the-triggers-they-match.dfy(12,17): Info: Selected triggers: {s[_t#0], s[x]} where _t#0 := x + 1
 some-terms-do-not-look-like-the-triggers-they-match.dfy(15,17): Info: Quantifier was split into 2 parts. Better verification performance and error reporting may be obtained by splitting the quantifier in source. For more information, see the section quantifier instantiation rules in the reference manual.
 some-terms-do-not-look-like-the-triggers-they-match.dfy(15,17): Info: Part #0 is 'x in s ==> s[_t#0] > 0'
- Selected triggers: {s[_t#0], s[x]}
+ Selected triggers: {s[_t#0], s[x]} where _t#0 := x + 1
 some-terms-do-not-look-like-the-triggers-they-match.dfy(15,17): Info: Part #1 is 'x in s ==> _t#0 !in s'
- Selected triggers: {s[_t#0], s[x]}
+ Selected triggers: {s[_t#0], s[x]} where _t#0 := x + 2
 some-terms-do-not-look-like-the-triggers-they-match.dfy(24,18): Info: Selected triggers: {x in s + t}
 some-terms-do-not-look-like-the-triggers-they-match.dfy(25,18): Info: Selected triggers:
    {x in t}, {x in s}
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/triggers/splitting-triggers-recovers-expressivity.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/triggers/splitting-triggers-recovers-expressivity.dfy.expect
index e66366bd3ec..b06c081fc7a 100644
--- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/triggers/splitting-triggers-recovers-expressivity.dfy.expect
+++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/triggers/splitting-triggers-recovers-expressivity.dfy.expect
@@ -1,7 +1,7 @@
 splitting-triggers-recovers-expressivity.dfy(12,10): Info: Selected triggers:
-   {P(_t#0), Q(i)}, {P(_t#0), P(i)}
+   {P(_t#0), Q(i)}, {P(_t#0), P(i)} where _t#0 := i + 1
 splitting-triggers-recovers-expressivity.dfy(17,11): Info: Selected triggers:
-   {P(_t#0), Q(j)}, {P(_t#0), P(j)}
+   {P(_t#0), Q(j)}, {P(_t#0), P(j)} where _t#0 := j + 1
 splitting-triggers-recovers-expressivity.dfy(26,10): Info: Selected triggers: {Q(i)}
  Rejected triggers: {P(i)} (may loop with "P(i + 1)")
 splitting-triggers-recovers-expressivity.dfy(33,11): Info: Selected triggers: {Q(j)}
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/triggers/suppressing-warnings-behaves-properly.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/triggers/suppressing-warnings-behaves-properly.dfy.expect
index 4abcebe8941..80c6a424512 100644
--- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/triggers/suppressing-warnings-behaves-properly.dfy.expect
+++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/triggers/suppressing-warnings-behaves-properly.dfy.expect
@@ -5,7 +5,7 @@ suppressing-warnings-behaves-properly.dfy(14,9): Info: Selected triggers: {f(n)}
 suppressing-warnings-behaves-properly.dfy(15,9): Info: Selected triggers: {f(n)}
 suppressing-warnings-behaves-properly.dfy(16,9): Info: The attribute {:autotriggers false} may cause brittle verification. It's better to remove this attribute, or as a second option, manually define a trigger using {:trigger}. For more information, see the section quantifier instantiation rules in the reference manual.
 suppressing-warnings-behaves-properly.dfy(18,9): Info: Selected triggers:
-   {g(n), f(_t#0)}, {f(_t#0), f(n)}
+   {g(n), f(_t#0)}, {f(_t#0), f(n)} where _t#0 := n + 1
 suppressing-warnings-behaves-properly.dfy(19,9): Info: Selected triggers: {f(n)}
 suppressing-warnings-behaves-properly.dfy(20,9): Info: The attribute {:autotriggers false} may cause brittle verification. It's better to remove this attribute, or as a second option, manually define a trigger using {:trigger}. For more information, see the section quantifier instantiation rules in the reference manual.
 

From 6b5b207386f57a6329714bb5ad5eceb4db678b85 Mon Sep 17 00:00:00 2001
From: Rustan Leino <leino@amazon.com>
Date: Wed, 16 Oct 2024 08:00:18 -0700
Subject: [PATCH 13/16] chore: Remove deprecated semi-colons

---
 .../LitTest/dafny3/SimpleCoinduction.dfy      | 23 ++++++++++---------
 1 file changed, 12 insertions(+), 11 deletions(-)

diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny3/SimpleCoinduction.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny3/SimpleCoinduction.dfy
index 352efe03eab..5ac106cae58 100644
--- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny3/SimpleCoinduction.dfy
+++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny3/SimpleCoinduction.dfy
@@ -1,4 +1,4 @@
-// RUN: %testDafnyForEachResolver "%s" -- --allow-deprecation
+// RUN: %testDafnyForEachResolver "%s"
 
 
 codatatype Stream<T> = Cons(head: T, tail: Stream)
@@ -22,7 +22,7 @@ ghost function Inc(s: Stream<int>): Stream<int>
 }
 
 lemma {:induction false} UpLemma(k: nat, n: int)
-  ensures Inc(Up(n)) ==#[k] Up(n+1);
+  ensures Inc(Up(n)) ==#[k] Up(n+1)
 {
   if (k != 0) {
     UpLemma(k-1, n+1);
@@ -30,18 +30,18 @@ lemma {:induction false} UpLemma(k: nat, n: int)
 }
 
 greatest lemma {:induction false} CoUpLemma(n: int)
-  ensures Inc(Up(n)) == Up(n+1);
+  ensures Inc(Up(n)) == Up(n+1)
 {
   CoUpLemma(n+1);
 }
 
 lemma UpLemma_Auto(k: nat, n: int, nn: int)
-  ensures nn == n+1 ==> Inc(Up(n)) ==#[k] Up(nn);  // note: it would be nice to do an automatic rewrite (from "ensures Inc(Up(n)) ==#[k] Up(n+1)") to obtain the good trigger here
+  ensures nn == n+1 ==> Inc(Up(n)) ==#[k] Up(nn)  // note: it would be nice to do an automatic rewrite (from "ensures Inc(Up(n)) ==#[k] Up(n+1)") to obtain the good trigger here
 {
 }
 
 greatest lemma CoUpLemma_Auto(n: int, nn: int)
-  ensures nn == n+1 ==> Inc(Up(n)) == Up(nn);  // see comment above
+  ensures nn == n+1 ==> Inc(Up(n)) == Up(nn)  // see comment above
 {
 }
 
@@ -53,8 +53,9 @@ ghost function Repeat(n: int): Stream<int>
 }
 
 greatest lemma RepeatLemma(n: int)
-  ensures Inc(Repeat(n)) == Repeat(n+1);
+  ensures Inc(Repeat(n)) == Repeat(n+1)
 {
+  RepeatLemma(n);
 }
 
 // -----------------------------------------------------------------------
@@ -65,7 +66,7 @@ greatest predicate True(s: Stream)
 }
 
 greatest lemma AlwaysTrue(s: Stream)
-  ensures True(s);
+  ensures True(s)
 {
 }
 
@@ -75,7 +76,7 @@ greatest predicate AlsoTrue(s: Stream)
 }
 
 greatest lemma AlsoAlwaysTrue(s: Stream)
-  ensures AlsoTrue(s);
+  ensures AlsoTrue(s)
 {
 }
 
@@ -85,7 +86,7 @@ greatest predicate TT(y: int)
 }
 
 greatest lemma AlwaysTT(y: int)
-  ensures TT(y);
+  ensures TT(y)
 {
 }
 
@@ -116,11 +117,11 @@ greatest predicate AtMost(a: IList<int>, b: IList<int>)
 }
 
 greatest lemma ZerosAndOnes_Theorem0()
-  ensures AtMost(zeros(), ones());
+  ensures AtMost(zeros(), ones())
 {
 }
 
 greatest lemma ZerosAndOnes_Theorem1()
-  ensures Append(zeros(), ones()) == zeros();
+  ensures Append(zeros(), ones()) == zeros()
 {
 }

From 3fc56d3d4e5b13fba010b3720cd6253dae95828c Mon Sep 17 00:00:00 2001
From: Rustan Leino <leino@amazon.com>
Date: Wed, 16 Oct 2024 08:01:01 -0700
Subject: [PATCH 14/16] Add tests for ternary expressions in triggers

---
 .../LitTests/LitTest/dafny0/CoPrefix.dfy      |  2 +-
 .../LitTest/dafny0/CoPrefix.dfy.expect        |  3 +--
 .../LitTests/LitTest/dafny3/Abstemious.dfy    | 22 +++++++++++++++++++
 3 files changed, 24 insertions(+), 3 deletions(-)

diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/CoPrefix.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/CoPrefix.dfy
index 708f0291219..f23c066103c 100644
--- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/CoPrefix.dfy
+++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/CoPrefix.dfy
@@ -135,7 +135,7 @@ greatest lemma {:induction false} Compare<T>(h: T)
   Compare(Next(h));
   if {
     case true =>
-      assert FF(h).tail == GG(h).tail;  // error: full equality is not known here
+      assert FF(h).tail == GG(h).tail;  // yes, this full equality is a focal predicate, so it's rewritten into ==#[_k - 1]
     case true =>
       assert FF(h) ==#[_k] GG(h);  // yes, this is the postcondition to be proved, and it is known to hold
     case true =>
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/CoPrefix.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/CoPrefix.dfy.expect
index dd2100b12db..d5f27399a5a 100644
--- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/CoPrefix.dfy.expect
+++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/CoPrefix.dfy.expect
@@ -3,7 +3,6 @@ CoPrefix.dfy(76,55): Error: cannot prove termination; try supplying a decreases
 CoPrefix.dfy(114,0): Error: a postcondition could not be proved on this return path
 CoPrefix.dfy(113,10): Related location: this is the postcondition that could not be proved
 CoPrefix.dfy(101,16): Related location: this proposition could not be proved
-CoPrefix.dfy(138,24): Error: assertion might not hold
 CoPrefix.dfy(142,24): Error: assertion might not hold
 CoPrefix.dfy(117,22): Related location: this proposition could not be proved
 CoPrefix.dfy(151,0): Error: a postcondition could not be proved on this return path
@@ -17,4 +16,4 @@ CoPrefix.dfy(205,6): Error: the calculation step between the previous line and t
 CoPrefix.dfy(207,6): Error: the calculation step between the previous line and this line could not be proved
 CoPrefix.dfy(220,12): Error: ORDINAL subtraction might underflow a limit ordinal (that is, RHS might be too large)
 
-Dafny program verifier finished with 13 verified, 12 errors
+Dafny program verifier finished with 13 verified, 11 errors
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny3/Abstemious.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny3/Abstemious.dfy
index 5eb338afaa8..258e7be2e6f 100644
--- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny3/Abstemious.dfy
+++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny3/Abstemious.dfy
@@ -206,3 +206,25 @@ lemma Fib_Correct(n: nat)
     }
   }
 }
+
+// --------------- ternary expression is a trigger ---------------
+
+lemma OrdinalLemma(k: ORDINAL)
+  ensures OhOnes().tail ==#[k] ones()
+{
+  // automatic induction on k
+}
+
+lemma NaturalLemma(k: nat)
+  ensures OhOnes().tail ==#[k] ones()
+{
+  // automatic induction on k
+}
+
+lemma Quantifier()
+  // the following quantifiers use the entire body as a trigger (previously, ternary expressions
+  // had not been considered as trigger candidates)
+  requires forall k: nat :: OhOnes().tail ==#[k] ones()
+  requires forall k: ORDINAL :: OhOnes().tail ==#[k] ones()
+{
+}

From 73d2d61568350f650471d7fc2f4703fb063d2a07 Mon Sep 17 00:00:00 2001
From: Rustan Leino <leino@amazon.com>
Date: Wed, 16 Oct 2024 08:01:13 -0700
Subject: [PATCH 15/16] Adjust resource count in test

---
 .../LitTests/LitTest/dafny0/CoinductiveProofs.dfy.expect        | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/CoinductiveProofs.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/CoinductiveProofs.dfy.expect
index d56b584921a..2730c4fe541 100644
--- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/CoinductiveProofs.dfy.expect
+++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/CoinductiveProofs.dfy.expect
@@ -31,5 +31,5 @@ CoinductiveProofs.dfy(208,21): Related location: this is the postcondition that
 CoinductiveProofs.dfy(4,23): Related location: this proposition could not be proved
 
 Dafny program verifier finished with 23 verified, 12 errors
-Total resources used is 770796
+Total resources used is 770576
 Max resources used by VC is 60436

From f4815f45def8c8e98b276dca679ec0722c9decaa Mon Sep 17 00:00:00 2001
From: Rustan Leino <leino@amazon.com>
Date: Wed, 16 Oct 2024 08:31:43 -0700
Subject: [PATCH 16/16] Add release notes

---
 docs/dev/news/5835.feat | 5 +++++
 1 file changed, 5 insertions(+)
 create mode 100644 docs/dev/news/5835.feat

diff --git a/docs/dev/news/5835.feat b/docs/dev/news/5835.feat
new file mode 100644
index 00000000000..d9fb6f80a25
--- /dev/null
+++ b/docs/dev/news/5835.feat
@@ -0,0 +1,5 @@
+Fill in matching patterns for the quantifiers introduced by automatic induction to represent the induction hypothesis. Suppress the generation of the induction hypothesis if no such matching patterns are found. Enhance tooltips accordingly. This feature is added to make stabilize verification, but by sometimes not generating induction hypotheses, some automatic proofs may no longer go through.
+
+Improve the selection of induction variables.
+
+Allow codatatype equality in matching patterns and as a focal predicate for extreme predicates.