feat: Compute matching patterns for automatic induction

[RustanLeino]

This PR aims to help stabilize verification by filling in matching patterns for the quantifiers introduced by automatic induction to represent the induction hypothesis. It also suppresses the generation of the induction hypothesis if no such matching patterns are found.

Full description

This PR computes matching patterns for the quantification that's about to be used with automatic induction. If there are no matching patterns, the induction hypothesis is not added. Tooltips or warnings show the patterns or announce the lack thereof.

The PR no longer uses arrow-typed variables as induction variables. (If a user really wants them, an {:induction ...} attribute can be given manually.)

Treat this more like other parameters when computing induction variables.

With this PR, ternary expressions (that is, _ ==#[_] _ and _ !=#[_] _) are considered as candidate trigger expressions. In addition, a codatatype == (which is defined by Dafny as a greatest predicate) is considered as a focal predicate for extreme predicates.

The PR also fixes a crash in trigger selection when the candidate expression has a lambda expression.

Finally, the "selected trigger" tooltip is extended to also show the t := e binding for any bound variable added as part of a quantifier rewrite.

By submitting this pull request, I confirm that my contribution is made under the terms of the MIT license.

[RustanLeino]

Thanks for your useful comments, @cpitclaudel . I have addressed many and commented on others. For the good suggestion of making sure there is a way to support customers who want to keep their old possibly-trigger-less inductions, I started writing a specification in the release notes (5835.feat), adding some corresponding test cases to $TEST/triggers/InductionWithoutTriggers.dfy. However, I did not finish this. Here are some questions:

Currently, {:induction} (and equivalently {:induction true}) take the list of all variables (provided their types are reasonable types for induction). Is that what {:induction} should do? I would seem better to let {:induction} pick the list of variables heuristically, just like the absence of an :induction attribute would. That would make sense by itself, and it would also mean that one can get backward compatibility by {:induction} {:nowarn}.

[cpitclaudel]

Using {:induction} for backwards compatibility is tempting but I'm not sure it works: we have many cases of {:induction} already appearing in sources (mostly in quantifiers) in quantifiers.

We could use {:induction "auto"} to use the heuristic, plus {:nowarn}. Alternatively, we could use {:induction_triggers false} to indicate that no triggers should be generated. Or better, since you already generate an {:inductionPattern …}, we could allow users to write an explicit trigger and pass {:inductionPattern} (no terms) to recover the legacy behavior?

I'm not sure how much I like the power that {:inductionPattern …} would give in this case: one we have a way to generate the forall statement in the code, we might ask users to just use that instead?

[cpitclaudel]

Another thing: Should we have a warning specific to induction when we don't generate a trigger for the induction part of a quantifier expression? For example:

predicate f(n: nat)
method ExprInduction() {
  assert forall n: nat {:induction n} :: f(n + 1);
}

In this case we generate this Boogie:

    assert {:id "id1"} {:subsumption 0} (forall n#1: int :: 
      LitInt(0) <= n#1
           && (forall n$ih#0#0: int :: 
            LitInt(0) <= n$ih#0#0
               ==> 
              0 <= n$ih#0#0 && n$ih#0#0 < n#1
               ==> _module.__default.f(n$ih#0#0 + 1))
           && true
         ==> _module.__default.f(n#1 + 1));

Arguably this is fine, because we warn about the top-level quantifier.

[cpitclaudel]

I've made a pass through this:

• I renamed :inductionPattern to :inductionTrigger
• Passing {:inductionTrigger} (no trigger terms) restores the legacy behavior
• I moved the attribute generation to ComputeInductionTriggers.

Here are some examples:

predicate f(n: nat) { if n == 0 then true else f(n-1) }
predicate g(n: nat) { false }

// Default: auto-generated trigger. Proof works.
lemma Default(n: nat) ensures f(n) {}

// Manual list of variables. Proof works.
lemma {:induction n} ListOfVars(n: nat) ensures f(n) {}

// No induction. Proof fails.
lemma {:induction false} NoInduction(n: nat) ensures f(n) {}

// No induction, with manual proof. Proof works.
lemma {:induction false} ManualInduction(n: nat)
  ensures f(n)
{
  forall ih_n: nat | (n decreases to ih_n) {
    ManualInduction(ih_n);
  }
}

// No triggers, so no auto induction ⇒ Proof fails
lemma NoTriggers(n: nat) ensures f(n + 0) {}

// No triggers but forced induction, so warning. Proof works.
lemma {:induction} InductionWarning(n: nat) ensures f(n + 0) {}

// Explicit triggers, so no warning.  Proof works.
lemma {:induction} {:inductionTrigger f(n)} NoWarning2(n: nat) ensures f(n + 0) {}

// Legacy mode: auto induction with no triggers.  Proof works.
lemma {:inductionTrigger} Legacy(n: nat) ensures f(n) {}
lemma {:inductionTrigger} Legacy1(n: nat) ensures f(n + 0) {}
lemma {:induction} {:inductionTrigger} Legacy2(n: nat) ensures f(n + 0) {}

I updated the spec accordingly. I still need to fix a printing issue.

[cpitclaudel]

I think this is ready for review. We can do the forall statement generation in a separate PR. I tried to split things into relevant commits, so reviewing them one by one might be best.

Also: I'm not sure how to regenerate the .doo files: running the recommended make command creates errors:

$ make -C Source/DafnyStandardLibraries update-binary
make: Entering directory 'Source/DafnyStandardLibraries'
dotnet run --project ../Dafny --no-build --roll-forward LatestMajor -- build -t:lib --hidden-no-verify=false  src/Std/dfyconfig.toml --output:build/DafnyStandardLibraries.doo
[…]
src/Std/Arithmetic/LittleEndianNat.dfy[ParametricConversion](113,30): Error: member 'First' does not exist in top-level module declaration '_default'
    |
113 |     ensures ToNatRight(xs) == First(xs)
    |                               ^^^^^

[RustanLeino]

@cpitclaudel Thanks for your help. I think everything has been addressed now.