feat: Compute matching patterns for automatic induction

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 =>

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

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()
+{
+}