Why3: induction

Table of Contents

Proving by induction

There are different ways to prove something, in math one of them is proving by induction. Its idea is: prove that a statement is true for every natural number n.

  • Identify the cases. The theorem, lemma, or claim usually has many cases. We want to prove that the statement is true for all of them.
  • Number the cases. We describe the cases using a natural number n. For example, if the cases are 2x, 4x, 6x, 8x, ... we can describe the n-th case as 2*n*x. So instead of proving infinitely many separate cases, we can talk about them using one number n.
  • Prove the base case. We prove that the statement is true for the first case, usually n=0 or n=1 (it can be any n but it must be the first one).
  • Prove the induction step. We prove a general rule: I͟f͟ t͟h͟e͟ s͟t͟a͟t͟e͟m͟e͟n͟t͟ i͟s͟ t͟r͟u͟e͟ f͟o͟r͟ s͟o͟m͟e͟ c͟a͟s͟e͟ n͟,͟ t͟h͟e͟n͟ i͟t͟ i͟s͟ a͟l͟s͟o͟ t͟r͟u͟e͟ f͟o͟r͟ t͟h͟e͟ n͟e͟x͟t͟ c͟a͟s͟e͟,͟ n͟+͟1͟. And EVERY case has previous, next case, so it means ALL cases are true AFTER THE FIRST ("next is true" automatically means "ALL" after some zero, initial case) The important word is some. We are not proving some case n=5 leading to case n=6. We prove the rule for every possible n: P(n) => P(n+1)
  • Put the two parts together. We know the first case is true (let's say the first is n=1): P(1) and we know that every true case leads to the next true case: P(n) => P(n+1). Therefore: P(1) => P(2) => P(3)...
  • So: every case AFTER THE BASE CASE is true.:
P(1) => P(2)
P(2) => P(3)
P(3) => P(4)
...
P(n) => P(n+1)

PROVE THE FIRST CASE, THEN PROVE THAT EVERY CASE (IF IT IS TRUE) LEADS TO THE NEXT CASE. THEREFORE ALL CASES AFTER THE BASE - ARE TRUE.

Again, we don't prove that P(n) is true, we prove that IF P(n) is true, then P(n+1) is true, but it does not prove that P(n) is true, maybe IT IS NOT. We prove only logical connection between them - "IF one true, the next (any) true too" . But... if among them we see at least one case true - then ALL are: 

          oh, true!
             |
            \v/ 
   ? -> ? -> O -> o -> ... -> o -> o -> o
            /|\   |
             |    |
            base  `-- if the previous is true
            case      then the next is true

What about cases BEFORE the first/BASE case? We don't know, maybe they are true, maybe no - look at the implication logical function:

U V U => V
0 0 1
0 1 1
1 0 0
1 1 1

and lets think that the base case is V and the previous one, unknown (?) - is U. If V=1 then U can be 0 and the implication (=> or ->) will be true too. It means that if we proved P(n) => P(n+1) and if the base case if true (1), then there is only one case for the next case - when both are true. But for the previous it is not true: 0 => 1 is true and if the base is this 1 then the previous could be 0. So, the math. induction is based on the idea of the NEXT cases only:

Mathematical induction is fundamentally about propagating truth from a starting point toward the next cases: P(base-case) => P(base-case + 1) => P(base-case + 2) => ...

See more in Wikipedia.

Induction in Why3

Lets prove this formula:

\begin{aligned} P(n \in \mathbb{N}): 0 + 1 + 2 + \ldots + n = \sum_{i=1}^{n} i = \frac{n(n+1)}{2} \text{ , formula (1)} \end{aligned}

It is proven by induction as...

Induction case if want to prove that IF it is true for some n (some... hmmm, let's call it k, i.e., when n = k), then it is true for the next (i.e., k + 1). What do we know? We know only that formula (1). We chose some PARTICULAR NUMBER among the series natural numbers, we designed it as k. The formula (not proven yet!) is the same (1) but imagine the particular k instead of abstract n. OK. The step is to prove that P(k+1) is true too - when P(k) is true: P(k) => P(k+1). How? Look:

\begin{aligned} 0 + 1 + \ldots + k = \frac{k(k+1)}{2} \text{ , for k} \\ 0 + 1 + \ldots + k + (k + 1) = ? \text{ , for k + 1} \end{aligned}

Well, ? is our formula (1) plus this new addend - (k + 1):

\begin{aligned} 0 + 1 + \ldots + k + (k + 1) = \frac{k(k+1)}{2} + (k + 1) \end{aligned}

After simplification this formula became:

\begin{aligned} 0 + 1 + \ldots + k + (k + 1) = \frac{(k+1)((k+1)+1)}{2} \end{aligned}

If to rename (k + 1) as some... X: \(\frac{X(X+1)}{2}\), wow! We see again the formula (1) ! What is our conclusion after this mathematical exercise? It is:

If formula (1) is true (we don't know: maybe it is not!), but if (1) is true, for some k then it is true for k+1 too because IT IS THE SAME FORMULA AGAIN! So, we proved that if P(k) is true then P(k + 1) will be true too.

Base case ok, now lets select the "base" case - n=0 (or 1, etc):

\begin{aligned} \text{Base case : }P(0) = \frac{0(0+1)}{2} = 0 \end{aligned}

Conclusion: Since both the base case and the induction step have been proved as true, by mathematical induction the statement P(n) holds for every natural number n ≥ 0 !

Proven! This is the method, approach of math. induction - an example of its usage.

See more on Wikipedia.

First attempt (unsuccessful)

Lets repeat this approach in Why3: 

module MySum

  use int.Int                  (* for ints and operation *)
  use int.EuclideanDivision    (* for div operation *)

  let rec function sum (n: int) : int
    requires { n>=0 }
    variant { n }
  =
    if n = 0 then 0
    else n + sum (n - 1)
  
  lemma sum_formula:
    forall n: int. n >= 0 ->
      sum n = div (n * (n + 1)) 2

end

and if to try to prove it: 

$ why3 prove -Pz3 MySum1.mlw
File MySum1.mlw:
Goal sum'vc.
Prover result is: Valid (0.00s, 299 steps).

File "MySum1.mlw", line 26, character 4 to line 27, character 33:
Goal sum_formula.
Prover result is: Timeout (5.00s, 710885547 steps).

Ops!

In math we had a sum equals to... In Why3 we should express the sum in some way, we did it using a recursive function (we a termination/DECREASING measure n) and a kind of "refinement type" (actually just a contract n>=0):

mathematics Why3
\(\sum_{i=1}^{n} i\) let rec function sum...
\(\frac{n(n+1)}{2}\) lemma sum_formula...

So, the sum is expressed through a recursion, OK, but the result (right hand side) of the formula ... Why3 cannot prove it by default!

Lemma with a body

We wrote: 

module MySum

  use int.Int
  use int.EuclideanDivision

  let rec function sum (n: int) : int
    requires { n>=0 }
    variant { n }
  =
    if n = 0 then 0
    else n + sum (n - 1)

  let rec lemma sum_formula (n: int)
    requires { n >= 0 }
    ensures { sum n = div (n * (n + 1)) 2 }
    variant { n }
  =
    if n = 0 then
      ()
    else
      sum_formula (n - 1)

end

And the proving now: 

$ why3 prove -Pz3 MySum1.mlw
File MySum1.mlw:
Goal sum'vc.
Prover result is: Valid (0.00s, 431 steps).

File MySum1.mlw:
Goal sum_formula'vc.
Prover result is: Valid (0.00s, 6485 steps).

How does it prove the formula (1) by induction?!

First, the "lemma" is our theorem, our formula (1). Second, it has "a contract": precondition, postcondition and an argument n: 

  requires { U(n) }       \_____  U(n) -> V(n): Assuming U(n), prove V(n).
  ensures { V(n) }        /

U is n ≥ 0. And the V is exactly \(\frac{n(n+1)}{2}\) ! But... our lemma is not only proposition-based, it has a body. And the body is this: 

    if n = 0 then
      ()
    else
      sum_formula (n - 1)

So, the base case is n=0 - the lemma-with-a-body returns (), i.e., a unit which means "proven!", then - the induction step: else - follow recursion. By the way, this can be rewritten lesser explicit and shorter, it is the same: 

    if n > 0 then
      sum_formula (n - 1)

What does Why3 do with all these? Using induction it has to check that P(n) => P(n+1) and to find the base case. Our lemma is:

\begin{aligned} P(n) \equiv \sum_{i=1}^{n} i = \frac{n(n+1)}{2} \end{aligned}

P(n-1) is, then:

\begin{aligned} P(n - 1) \equiv \sum_{i=1}^{n - 1} i = \frac{(n-1)n}{2} \end{aligned}

Two different propositions. We can assume \(P(n - 1) = \sum_{i=1}^{n - 1} i\) as true - it will be our induction hypothesis. Our goal is P(n) which is \(\sum_{i=1}^{n} i = \frac{n(n+1)}{2}\) (the postcondition of our lemma is).

From the recursive definition of the sum (let rec function sum) Why3 knows that when n > 0:

\begin{aligned} \sum_{i=1}^{n} i = n + \sum_{i=1}^{n - 1} i \end{aligned}

and Why3 use it in our goal P(n), replacing \(\sum_{i=1}^{n} i\) by \(n + \sum_{i=1}^{n - 1} i\) :

\begin{aligned} n + \sum_{i=1}^{n - 1} i = \frac{n(n + 1)}{2} \end{aligned}

Why3 uses the \(\sum_{i=1}^{n - 1} i\) from the induction hypothesis and:

\begin{aligned} n + \frac{(n - 1)n}{2} = \frac{n(n + 1)}{2} \end{aligned}

This is passed to SMT solver and it easy proves it (n is in a numerical domain - a task as for SMT).

Conceptually, the induction step is P(n - 1) => P(n), but Why3 doesn't necessarily hand Z3 one giant formula literally written in this way. Instead, Why3 creates a verification condition (VC) with P(n - 1) as an assumption \(P(n-1) \vdash P(n)\) which means:

Assuming P(n - 1) as true, prove P(n)

Bigger picture: 

Assume:
  n >= 0
  n > 0

Induction hypothesis (from the lemma "sum_formula",
                      substituting "n" by "n-1"):
                      
          n-1    (n-1)n
 P(n-1) ≡  ∑ i = ──────   ····························.
          i=1      2                                  :
                                                      :
Prove ("ensures" of the lemma "sum_formula"):         :
                                                      :
         n     n(n+1)                                 :
 P(n) ≡  ∑ i = ──────                                 :     
        i=1      2                                    :  
                                                      :
Why3 unfolds sum (from "sum" definition):             :
                                                      :
                              then Why3               :
         n        n-1 ⋰˙˙⋱   substitutes        by this from
 P(n) ≡  ∑ i = n + ∑ i     `····this····.          P(n-1)   
        i=1       i=1                   :          /  :   
                                        :         /   :
                                        :       SO    :
                                        :     ASSUME  :
         n         (n-1)n               :     P(n-1)  :
 P(n) ≡  ∑ i = n + ──────   <···········:·············'
        i=1          2

Now the goal is effectively:

                 n     n(n+1)
  by "ensures"   ∑ i = ──────                -- V(n)
                i=1      2                      or precond.
                
  by unfolds     n         (n-1)n
  and subst.     ∑ i = n + ──────            -- P(n)
                i=1          2                  assuming
                                                P(n-1)

So, to prove P(n), ie, whole lemma - that V(n) = transform result,
we send this to SMT:

   n(n+1)  ?      (n-1)n                   easy proves
   ──────  =  n + ──────   ···> SMT ···>  that they are
     2              2                      really equal

QED: assuming P(n-1), we proved P(n).

This is sent to SMT - SMT can establish it very easy (numbers!):

\begin{aligned} \forall n \in \mathbb{Z}, \frac{n(n+1)}{2} = \frac{n(n-1)}{2} + n \end{aligned}

Again, to prove P(n), we assumed P(n-1) - this is the induction step and finally we came to some new formula. Then we sent to SMT request to prove V(n) or ensures {..} and this new formula.

Assuming that P(n-1) is true, we proved true of P(n), so we established P(n-1) => P(n). Base case is for n = 0 ("unit" - trivial, even if it is implicit): 

...
  if n = 0 then ()
...

This is how Why3 presumably operated in this instance.

P(n-1) came from recursion of the lemma - we "forced" Why3 to be based on P(n-1) - so to become "inductive"!

By the way, n + ... came from recursion of the sum definition.

The combination of the recursive call and the decreasing variant is what makes the recursive lemma usable inductively.

The question here is:

Why does not Why3 prove P(n-1) case?

When Why3 sees that some goal (a lemma in the case) is recursive and it has a variant (decreasing measure) it "think" in this way:

I (Why3) sees: 

let rec lemma foo (n: int)         GOAL:       P(n)
  ensures { P(n) }                 -----
  variant { n }                    AVAILABLE:  P(n-1)
=                                  ----------    :
  if n = 0 then ()                               :
  else foo (n-1)               From recursive call/SPECIFICATION

Why3 doesn't recursively open another proof obligation saying "now prove P(n-1)". It uses the induction mechanism instead.

But if we write: 

let lemma bar (n: int)
  ensures { P(n-1) }
=
  ...without recursive call supplying P(n-1), and no variant too

then the goal is plain P(n-1) from ensures {..}. And Why3 in this case will prove P(n-1). When Why3 sees induction, it proves the base case, and then proves the connection/IMPLICATION between P(n) => P(n+1) - it is "smart" enough. To do it Why3 needs:

  • recursion
  • variant (decreasing measure)

When Why3 sees something like: foo(smaller_argument) then what does the ensures clause of foo give it? If it gives Why3: P(smaller_argument) then Why3 can use that as an induction hypothesis while proving the current invocation.

The variant answers a different question:

Why am I allowed to use the recursive call?

Answer:

Because the recursive argument/measure is smaller.

Why3 proves P(n-1) when P(n-1) is the current verification goal; it ASSUMES/uses P(n-1) when a valid recursive call to a lemma whose CONTRACT (ensures {..}) guarantees P(n-1) is available while proving P(n).

Transformations

What are transformations in Why3?

A transformation rewrites a proof goal into one or more new goals, usually in a predictable, logic-level way. In Why3, a transformation might introduce an implication’s premises as hypotheses, split a conjunction, or simplify a formula. It generally doesn’t construct a proof by itself; it changes the task that a prover must solve.

Why3 transformations are typically reusable goal-to-goal operations, often used to prepare verification conditions for automated provers.

"Reusable" means that you can save them in a session file if you applied them interactively in IDE (as commands: IDE has an edit box for typing of "commands"). Also you can pass them as options in command line as --apply-transform - one by one.

A transformation can resemble a simple "tactic": for instance, Why3’s introducepremises is similar in effect to introducing assumptions in Rocq or LEAN. But tactics are a broader mechanism and can include search, branching, and proof construction.

Transformations are best thought of as goal transformations; tactics are proof-state programs. The boundary isn’t absolute---some tactics merely transform goals, and some systems expose transformations through tactic-like interfaces.

Transformation is REWRITING of the initial WhyML happening "in the memory".

Simple example: split_vc splits a verification condition into separate goals, typically by decomposing a top-level conjunction in the goal. For example, a goal P /\ Q becomes 2 goals, P and Q. This lets Why3 send each obligation to SMT prover separately. It does not prove them; it restructures the proof task. I.e., split_vc is a transformation: it takes a verification condition and produces separate proof goals, rather than proving them itself. If you think that it looks as an "optimization" then yes - it affects the performance of the proving and if you has hit timeout or similar, then sometimes split_vc can help.

Usually you use transformations exactly for this: you cannot prove some goal, using transformations you solve this problem. Well, sometimes you need rewriting of WhyML too... anyway, this is the idea of "transformations".

You can see all supported transformations by the simple command: 

$ why3 show transformations
abstract_quantifiers
  Abstract quantifiers in the axioms of the context and the goals.

abstract_unknown_lsymbols
  Abstract applications of non-built-in symbols with constants. Used by the
  Gappa pretty-printer.

apply
  type: prsymbol -> ?with -> list term -> list task
  apply <prop> [with] <term list> applies premise <prop> to the goal and uses
  the list of terms to instantiate the variables that are not found.

assert
  type: formula -> ?as -> string -> list task
  assert <term> [name] makes an assertion with a hypothesis 'name: term'.

case
  type: formula -> ?as -> string -> list task
  case <term> [name] generates hypothesis 'name: term' in a first goal and
  'name: ~ term' in a second one.
...

For example, Why3 1.8.0 has 128 transformations. They are available as an interactive command in IDE and as menu items in IDE: "Tools/Transformations".

Transformations cannot be written in WhyML program - to be "called"/applied from there. But you can "hint" then from WhyML program (with arguments).

Now lets return to the initial WhyML: 

module MySum

  use int.Int                  (* for ints and operation *)
  use int.EuclideanDivision    (* for div operation *)

  let rec function sum (n: int) : int
    requires { n>=0 }
    variant { n }
  =
    if n = 0 then 0
    else n + sum (n - 1)
  
  lemma sum_formula:
    forall n: int. n >= 0 ->
      sum n = div (n * (n + 1)) 2

end

And let's open it in IDE with why3 ide MySum1.mlw. We have an edit box for entering of commands, put the cursor on sum_formula in the left tree. And enter in the command box intros n. It will create there new sub-goals. Put the cursor on the last one "0" and enter the next command: introduce_premises. New sub-goal, and a new command: induction n. Put the cursor for example, on the induction n sub-goal and call the SMT proving with the menu "Tools/Provers/CVC4". You show see green checks in the tree. Now put the cursor on the sum'vc and call the prover again - everything is green now and the tree looks like: 

Status | Theories/Goals                         | Time
  ✔      ▼ 🗁  MySum1.mlw         
  ✔        ▼ 🗁  MySum
  ✔          ▼ 🗎 sum'vc [VC for sum]
  ✔              \ CVC4 1.8                       0.01 (steps: 246)
  ✔          ▼ 🗎 sum_formula
  ✔            ▼ 🛠 intros n
  ✔              ▼ 🗎 0
  ✔                ▼ 🛠 introduce_premises
  ✔                  ▼ 🗎 0
  ✔                    ▼ 🛠 induction n
  ✔                      ▼ 🗎 0 [base case]
  ✔                          \ CVC4 1.8           0.02 (steps: 3597)
  ✔                      ▼ 🗎 1 [recursive case]
  ✔                          \ CVC4 1.8           0.02 (steps: 4821)

Entered commands are transformations. Now, save the session (menu "File/Save session"). And exit. Put the session directory (./MySum1/) to Git control (all its files). And you can re-check it from the command line with this command line in the console: 

$ why3 replay -q MySum1
 2/2 (replay OK)

For unchanged goals, existing proofs remain attached. For goals affected by the source modification, the existing proof attempts become obsolete. This is explicitly how Why3 is designed to work.

If the modification changes the actual proof structure, we may need to edit the transformation tree - for example, change, add, remove transformations - just as we did originally, in the IDE.

Why3 specifically provides the replay valid obsolete proofs operation for this situation.

By the way, another scenario is to use just 2 transformations - they also work fine:

  1. intros n
  2. induction n

Lets explore little what we are seeing in the IDE.

▒▒▒▒▒▒▒▒▒▒ Cursor on sum_formula - the "Task" tab is: 

 1  --------------------------- Local Context ---------------------------
 2  
 3  function sum int : int
 4  
 5  sum'def :
 6    forall n:int.
 7     n >= 0 -> (if n = 0 then sum n = 0 else sum n = (n + sum (n - 1)))
 8  
 9  ------------------------------- Goal --------------------------------
10  
11  goal sum_formula : forall n:int. n >= 0 -> sum n = div (n * (n + 1)) 2

Our initial WhyML.

▒▒▒▒▒▒▒▒▒▒ Cursor on intros n / 0 - the "Task" tab is: 

 1  --------------------------- Local Context ---------------------------
 2  
 3  function sum int : int
 4  
 5  sum'def :
 6    forall n1:int.
 7     n1 >= 0 -> (if n1 = 0 then sum n1 = 0 else sum n1 = (n1 + sum (n1 - 1)))
 8  
 9  constant n : int
10  
11  ------------------------------- Goal --------------------------------
12  
13  goal sum_formula : n >= 0 -> sum n = div (n * (n + 1)) 2

intros n introduced (extracted) n constant (line 9) in the logical context (in the top level) - it was applied on sum_formula so forall n was removed as redundant now - now n is on the top level. Also, to avoid names clashing, in sum'def the variable n was renamed to n1 (line 6).

▒▒▒▒▒▒▒▒▒▒ Cursor on induction n / 0 [base case] - the "Task" tab is: 

 1  --------------------------- Local Context ---------------------------
 2  
 3  function sum int : int
 4  
 5  sum'def :
 6    forall n1:int.
 7     n1 >= 0 -> (if n1 = 0 then sum n1 = 0 else sum n1 = (n1 + sum (n1 - 1)))
 8  
 9  constant n : int
10  
11  Init : n <= 0
12  
13  ------------------------------- Goal --------------------------------
14  
15  goal sum_formula : n >= 0 -> sum n = div (n * (n + 1)) 2

Base case. Init is simply the name Why3 gives to the induction-range assumption.

It is not an assumption from the original .mlw source, and it is not something that changed between the 2 cases. Rather, each branch gets a different generated assumption.

▒▒▒▒▒▒▒▒▒▒ Cursor on induction n / 1 [recursive case] - the "Task" tab is: 

 1  --------------------------- Local Context ---------------------------
 2  
 3  function sum int : int
 4  
 5  sum'def :
 6    forall n1:int.
 7     n1 >= 0 -> (if n1 = 0 then sum n1 = 0 else sum n1 = (n1 + sum (n1 - 1)))
 8  
 9  constant n : int
10  
11  Init : 0 < n
12  
13  Hrec : forall n1:int. n1 < n -> n1 >= 0 -> sum n1 = div (n1 * (n1 + 1)) 2
14  
15  ------------------------------- Goal --------------------------------
16  
17  goal sum_formula : n >= 0 -> sum n = div (n * (n + 1)) 2

Hrec was added (line 13) - it is the STRONG induction hypothesis: 

                                  I N D U C T I O N   H Y P O T H E S I S:
                                          
                                                  n     n(n+1)
                                           P(n) ≡ ∑ i = ──────
Hrec :                                           i=1      2
  forall n1:int.
    n1 < n ->                       ⟷     ∀n, n < n1 /\ n ≥ 0  ⟹  P(n).
    n1 >= 0 ->
    sum n1 = div (n1 * (n1 + 1)) 2        For every nonnegative integer
                                          smaller than n, the theorem
                                          is already known.

Conceptually: 

             P(n)
               │
        induction on n
          /         \
     n <= 0          n > 0
       │               │
     Base          Recursive

Weak (ordinary) induction

In ordinary induction, the recursive step gives you only the immediately preceding case: P(n−1) ⟹ P(n), i.e., "if P holds in the previous case, then in the current, it holds too." In Why3 it could look as: 

Hrec : P(n - 1)           if const n=4: P(3) ◀ known
                                        P(4)   ?
● I know the theorem for exactly n-1

Strong induction

Hrec :                    if const n=4: P(0) ◀ known
  forall n1:int.                        P(1) ◀ known
    n1 < n ->                           P(2) ◀ known
    n1 >= 0 ->                          P(3) ◀ known
    P(n1)                               P(4)   ?

● I know the theorem for every nonnegative integer smaller than n

                           I.e.,

                  ● ordinary induction:

                          P(n-1)

                  ● strong induction:

              P(0) /\ P(1) /\ ... /\ P(n-1)

For many proofs, strong induction isn't actually more powerful in terms of what can ultimately be proved.

Why did STRONG induction appear? This is how the transformation induction... works: 

$ why3 show transformations | grep -A 2 induction
induction
  type: term -> ?from -> term -> env -> list task
  induction <term1> [from] <term2> performs a strong induction on the integer
  <term1> starting from the integer <term2>. <term2> is optional and defaults
  to 0.
--
...

The mental model is: 

Transformation "induction n":

        "induction n"
             │
             ├── base:     n <= 0
             │
             └── recursive: 0 < n
                            +
                            ∀ n1 < n, P(n1)

Inductive predicate and transformations

module MySum2
  use int.Int

  inductive sum_def int int =
    | Zero:
        sum_def 0 0
    | More:
        forall n s: int.
          sum_def n s ->
          sum_def (n + 1) (s + n + 1)

  lemma sum_formula:
    forall n s: int.
      sum_def n s ->
      2 * s = n * (n + 1)

end

Here sum_def n s is read as "s is the sum of the first n numbers.", So, 

constructor/case|                      TRUE IS THAT...
----------------+----------------------------------------------------------------
     Zero       |                       sum_def 0 0
                |                             ↓
                |                "sum of first 0 nums is 0"
----------------+----------------------------------------------------------------
     More       | forall n s: int.  sum_def n s   ->   sum_def (n + 1) (s + n + 1)
                |        ↓               ↓        ↓                  ↓
                |    "For any       "if s is    "then"    "s + (n + 1) is the sum
                |    integers        the sum                   for n + 1"
                |      n, s"       for n nums"

Yes, literally it is read for Zero: "IT IS TRUE THAT SUM OF FIRST 0 NUMBERS IS 0".

It is a recursive definition of the sum, expressed as an inductive predicate.

Why does sum_def have 2 arguments? Imagine: 

inductive sum_def int =
  | Zero: sum_def 0
  | More:
      forall n:int.
        sum_def n ->
        sum_def (n+1)

Then sum_def n would only tell us: "n is reachable from zero." It would not tell us what the sum is. For example, all we know is: sum_def 3 BUT WHERE IS 6 - THE SUM VALUE?

It reminds Prolog's predicate...

Then the lemma. It says: 

forall n s: int.       sum_def n s       ->       2 * s = n * (n + 1)
       ↓                    ↓            ↓                ↓
                                                                 n(n+1)
  "for any         "if s is the sum    "then"   "sum is equal to ------ "
n,s integers"       of first n nums"                                2

And to avoid games with div, we just multiplied both side by 2 (so, you see 2 * s = ...).

What is "inductive" ?

Why3 supports "predicate" - something returning true or false. The construction using the keyword inductive means "define this predicate by rules" (sum_def). It has 2 arguments: 

sum_def : int -> int -> Prop

and when it is used as sum_def 3 6 then it is a PROPOSITION, saying "6 is the sum associated with 3."

And because it is an inductive predicate, you don't define it with a Boolean expression such as predicate sum_def (n,s:int) = .... Instead, you define RULES FOR CONSTRUCTING PROOFS OF IT. Yes, the CONSTRUCTORS ARE RULES FOR PROVING THE PREDICATE: 

                                 sum_def n s
   ───────────              ─────────────────────
   sum_def 0 0              sum_def (n+1) (s+n+1)

If you already have a proof that sum_def n s, you are allowed to construct a proof that sum_def (n+1) (s+n+1).

this is the induction step:

THE WORD I͟N͟D͟U͟C͟T͟I͟V͟E͟ MEANS THAT THE PREDICATE IS DEFINED BY HOW ITS PROOFS CAN BE CONSTRUCTED FROM EARLIER PROOFS. 

        Zero
sum_def 0 0
      ↓ More
sum_def 1 1
      ↓ More
sum_def 2 3
      ↓ More
sum_def 3 6
      ↓ More
sum_def 4 10

And the surprise part is that if to try to prove it with Why3, then it will... timeout! And it can be overcome with the help of transformations.

Applying transformation

We can do it in CLI with this command applying transformation induction_pr: 

$ why3 prove -Pz3 MySum2.mlw --apply-transform 'induction_pr'
File MySum2.mlw:
Goal sum_formula.
Prover result is: Valid (0.00s, 80 steps).

File "MySum2.mlw", line 11, character 8 to line 13, character 37:
Goal sum_formula.
Prover result is: Valid (0.01s, 1763 steps).

If to open it in IDE: why3 ide MyList2.mlw and to apply the same transformation induction_pr from the menu, then you will see new "sub-goals" labeled by "0" and "1" in the left panel ("tree"). If to put the cursor on the "0" and to open in the right panel the tab "Task", then you will see there: 

--------------------------- Local Context ---------------------------

inductive sum_def int int =
  | Zero : sum_def 0 0
  | More : forall n:int, s:int. sum_def n s -> sum_def (n + 1) ((s + n) + 1)

------------------------------- Goal --------------------------------

goal sum_formula :
  forall n:int, s:int. s = 0 -> n = 0 -> (2 * s) = (n * (n + 1))

The "0" sub-goal is proving of our lemma sum_formula for Zero constructor only. It can be read as "assuming sum_def 0 0, prove sum_formula". But sum_def 0 0 means s (sum) is 0, and n (numbers) is 0 too, and Why3 writes exactly this: 

          ASSUMING THIS...            PROVE          THIS
forall n:int, s:int. s = 0 -> n = 0    ->    (2 * s) = (n * (n + 1))

s = 0 -> n = 0 is read as "Assuming that if s=0 and if n=0..."

If - on "1", then the content of "Task" tab will be: 

--------------------------- Local Context ---------------------------

inductive sum_def int int =
  | Zero : sum_def 0 0
  | More : forall n:int, s:int. sum_def n s -> sum_def (n + 1) ((s + n) + 1)

------------------------------- Goal --------------------------------

goal sum_formula :
  forall n:int, s:int.
   sum_def n s /\
   (forall n1:int, s1:int. s1 = s -> n1 = n -> (2 * s1) = (n1 * (n1 + 1))) ->
   (forall n1:int, s1:int.
     s1 = ((s + n) + 1) -> n1 = (n + 1) -> (2 * s1) = (n1 * (n1 + 1)))

It is the next sub-goal for proving (of sum_formula lemma). Well, the second sub-goal is for More obviously (though it is not written somewhere). This long goal consists actually of 3 parts - they are induction step written in More constructor:

  1. sum_def n s
  2. (forall n1:int, s1:int. s1 = s -> n1 = n -> (2 * s1) = (n1 * (n1 + 1))) -> ...
  3. (forall n1:int, s1:int. s1 = ((s + n) + 1) -> n1 = (n + 1) -> (2 * s1) = (n1 * (n1 + 1)))

1st is read as "assuming that the predecessor is a valid sum_def n s..."

2nd is read as "we introduce the INDUCTION HYPOTHESIS IH: 2 * s = n * (n + 1)". Why3 writes it in the "Task" tab as (2 * s1) = (n1 * (n1 + 1))) -> ... with quantified variables (more on them later). Can be read also: "Induction hypothesis: the formula is true for the predecessor n,s."

3rd represents the property for the result of the More constructor sum_def (n + 1) (s + n + 1) - this. This is so called the "INDUCTION STEP" - the lemma should be true on the next step too - P(n+1).

Now, why does induction_pr introduce n1 and s1? It generalizes the variables, forming always: 

(for any X,Y,Z: phrase-1...) -> (for any T,U,V: phrase-2...) -> ...

it does it always, even if variables the same. If they are the same, they are "fixed" with top-scope value (forall i1, but i1 = i): 

   for i in ...      →    forall i
     for i1 in ...   →      forall i1.
       if i1:        →        i1 = i ->
         ...         →          ...

Or in more human readable form: 

--------BASE--------

n = 0
s = 0

Prove:
    2*s = n*(n+1)

    
---INDUCTION-CASE---

Assume:
    sum_def n s

Induction hypothesis:
    2*s = n*(n+1)

Prove:
    2*(s+n+1) = (n+1)*(n+2)

SMT can proves the last easy (assuming P(1) - what 2*s is, from the "BASE" case): 

2*(s+n+1)
= 2*s + 2*n + 2
= n*(n+1) + 2*n + 2       [IH]
= n² + 3*n + 2
= (n+1)*(n+2)

Why did the transformation help?

Without induction_pr Z3 got: 

 we know : sum_def 0 0
     and : sum_def n s -> sum_def (n+1) (s+n+1)
lemma is : sum_def n s -> 2*s = n*(n+1)

and Z3 has to discover the RELATIONSHIP between our recursive/inductive definition sum_def and the lemma sum_formula. Being different numerical, boolean domains constrained. It is not easy for SMT usually and it hits timeout:

Z3 is very good at arithmetic and first-order SMT reasoning, but it isn't automatically performing the structural induction that a human mathematician sees immediately.

It will discover it for long WITHOUT FINDING THE INDUCTION ARGUMENT.

But with induction_pr, Why3 performs the induction BEFORE Z3 sees the problem and it transforms: 

       f r o m                    t o  -  Z 3  (n o w   O K)

∀ n s.                     →      BASE:  P(0, 0)
sum_def n s -> P(n,s)      →      STEP:  P(n,s) -> P(n+1,s+n+1)

𝘸𝘩𝘦𝘳𝘦 𝘗(𝘯,𝘴) ≡ 2*𝘴 = 𝘯*(𝘯+1)
                                           ↓ ↓ ↓
                                              

                                 n=0, s=0            2s = n(n+1)
                               ───────────  ,   ─────────────────────
                               2s = n(n+1)      2(s+n+1) = (n+1)(n+2)

                                        (𝘫𝘶𝘴𝘵 𝘢𝘳𝘪𝘵𝘩𝘮𝘦𝘵𝘪𝘤)

Why3 transformations is a kind of proof-problem preprocessing, rewriting, it helped Why3 to recognize INDUCTION STRUCTURE and to reduce it to "arithmetic" - good for SMT.

What is sent to SMT?

Actually, you can watch what Why3 sends to SMT solver using its -o <DIRECTORY> option, for example: 

$ why3 prove -Pz3 MySum2.mlw -o .

It saves in the <DIRECTORY> files sent to SMT. During my different experiments, I got 2 files: 

                ----- File MySum2-MySum2-sum_formula.smt2 -----

;;; generated by SMT-LIB2 driver
;;; SMT-LIB2 driver: bit-vectors, common part
;;; generated by SMT-LIB strings
;;; SMT-LIB2: integer arithmetic
;; Goal "sum_formula"
;; File "MySum2.mlw", line 20, characters 6-17
(assert
  (not
  (forall ((n Int) (s Int))
    (=> (= s 0) (=> (= n 0) (= (* 2 s) (* n (+ n 1))))))))

(check-sat)

                ----- File MySum2-MySum2-sum_formula1.smt2 -----

;;; generated by SMT-LIB2 driver
;;; SMT-LIB2 driver: bit-vectors, common part
;;; generated by SMT-LIB strings
;;; SMT-LIB2: integer arithmetic
;; "sum_def"
(declare-fun sum_def (Int
  Int) Bool)

;; "Zero"
(assert (sum_def 0 0))

;; "More"
(assert
  (forall ((n Int) (s Int))
    (=> (sum_def n s) (sum_def (+ n 1) (+ (+ s n) 1)))))

;; "sum_def_inversion"
(assert
  (forall ((z Int) (z1 Int))
    (=>
      (sum_def z z1)
      (or
        (and (= z 0) (= z1 0))
        (exists ((n Int) (s Int))
          (and (sum_def n s) (and (= z (+ n 1)) (= z1 (+ (+ s n) 1)))))))))

;; Goal "sum_formula"
;; File "MySum2.mlw", line 20, characters 6-17
(assert
  (not
  (forall ((n Int) (s Int))
    (=>
      (and
        (sum_def n s)
        (forall ((n1 Int) (s1 Int))
          (=> (= s1 s) (=> (= n1 n) (= (* 2 s1) (* n1 (+ n1 1)))))))
      (forall ((n1 Int) (s1 Int))
        (=>
          (= s1 (+ (+ s n) 1))
          (=> (= n1 (+ n 1)) (= (* 2 s1) (* n1 (+ n1 1))))))))))

(check-sat)