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

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);
  }
}

dafny-lang / dafny

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