When a lemma has an ensures clause starting with forall, suggest making that into a lemma parameter

[keyboardDrummer]

Given

lemma LemmaPAuto()
  ensures forall x: int: P(x) {
  forall x: int 
    ensures P(x)
  {
     ...proof...
  }
}

suggest writing

lemma LemmaP(x: int)
  ensures P(x) {
     ...proof...
}

We might not include the changes in the body as part of the suggestion, and leave figuring that out up to the customer.

If there is a range, such as in:

lemma {:induction false} LemmaLogSAuto()
  ensures forall base: nat, pow: nat {:trigger Log(base, pow / base)}
            | base > 1 && pow >= base 
            :: pow / base >= 0 && Log(base, pow) == 1 + Log(base, pow / base)

We can suggest making the range part of the requires clause:

lemma {:induction false} LemmaLogS(base: nat, pow: nat)
  requires base > 1 && pow >= base 
  ensures pow / base >= 0 && Log(base, pow) == 1 + Log(base, pow / base)  

I think the suggestion should only be given if all ensures clauses of the lemma start for all forall that has a parameter of this type and range. For example, for:

lemma LemmaDivBasicsAuto()
  ensures forall x {:trigger 0 / x} :: x != 0 ==> 0 / x == 0
  ensures forall x {:trigger x / 1} :: x / 1 == x
  ensures forall x, y {:trigger x / y} :: x >= 0 && y > 0 ==> x / y >= 0
  ensures forall x, y {:trigger x / y} :: x >= 0 && y > 0 ==> x / y <= x
{

I do not think there should be a suggestion to make y a parameter.

---

I think ideally we introduce warning instead of suggestions, but we can only introduce warnings if they can always be resolved. I think here we might be able to introduce a warning if we introduce a way not to need the Auto version.

Suppose we allow:

method Caller() {
  LemmaP(_);
}

which translates to:

method Caller() {
  forall x: Int ensures P(x) { LemmaP(x); }
}

There would be no way to specify triggers for the generated forall, so in case you want those you have to manually write the forall without using the _ syntax. We would then also not give a warning/suggestion for the "Auto" type lemmas if their quantifiers include custom triggers.

Some cases from the standard library that could be removed if we introduce the _ syntax:

lemma LemmaToNatLeftEqToNatRightAuto()
  ensures forall xs: seq<digit> :: ToNatRight(xs) == ToNatLeft(xs)
{
  forall xs: seq<digit>
    ensures ToNatRight(xs) == ToNatLeft(xs)
  {
    LemmaToNatLeftEqToNatRight(xs);
  }
}

lemma LemmaMulIsMulRecursiveAuto()
  ensures forall x: int, y: int :: x * y == MulRecursive(x, y)
{
  forall x: int, y: int
    ensures x * y == MulRecursive(x, y)
  {
    LemmaMulIsMulRecursive(x, y);
  }
}

[keyboardDrummer]

There are many cases of Auto lemmas in the Dafny standard library, and it seems all of them should be kept. Most of them introduce triggers, so they contain valuable information as well. I'm hesitant about introducing this suggestion since it would be given for many common valid cases.