Induction

While techniques such as unrolling and simplification can get us a long way towards formally verifying our software, variants of mathematical induction are in general required for verifying properties of systems with infinite state-spaces.

Induction is a proof technique that can be used to prove that some property φ(x) holds for all the elements x of a recursively defined structure (e.g. natural numbers, lists, trees, execution traces, etc). The proof consists of:

  • a proof that φ(base) is true for each base case
  • a proof that if φ(c) is true (called the inductive hypothesis), then φ(step(c)) is also true, for all the recursive steps of the property we're trying to prove

Induction can be done in many ways, and finding the "right" way to induct is often the key to difficult problems. Imandra has deep automation for finding and applying the "right" induction for a problem. If this fails, the user can instruct Imandra how to induct, with various forms of instructions.

A method of induction is given by an induction scheme.

Induction schemes can automatically be derived by Imandra in many ways. By default, with [@@auto] or [@@induct], Imandra analyses the recursive functions involved in the conjecture and constructs a functional induction scheme derived from their recursive structure, in a manner that is justified by the ordinal measures used to prove their termination. Imandra also supports structural induction principles derived from the definitions of (well-founded) algebraic datatypes such as lists and trees.

Some example induction schemes are:

  • for the natural numbers, φ(Zero) && φ(n) ==> φ(Succ(n))
  • for lists, φ([]) && (lst <> [] && φ(List.tl(lst)) ==> φ (lst))
  • for the function repeat as defined below, n <= 0 ==> φ(n, c) && (n > 0 && φ(n - 1, c)) ==> φ(n, c)
In [1]:
let rec repeat c n =
  if n <= 0 then
    []
  else
    c :: (repeat c (n-1))
Out[1]:
val repeat : 'a -> int -> 'a list = <fun>
termination proof

Termination proof

call `repeat c (n - 1)` from `repeat c n`
originalrepeat c n
subrepeat c (n - 1)
original ordinalOrdinal.Int (if n >= 0 then n else 0)
sub ordinalOrdinal.Int (if (n - 1) >= 0 then n - 1 else 0)
path[not (n <= 0)]
proof
detailed proof
ground_instances1
definitions0
inductions0
search_time
0.010s
details
Expand
smt_stats
num checks3
arith assert lower8
arith pivots2
rlimit count1027
mk clause4
datatype occurs check2
mk bool var20
arith assert upper3
decisions2
arith add rows3
propagations2
conflicts2
arith fixed eqs2
datatype accessor ax2
arith conflicts1
num allocs930100473
final checks1
added eqs6
del clause4
arith eq adapter2
memory15.040000
max memory17.870000
Expand
  • start[0.010s]
      not (n <= 0)
      && (if n >= 0 then n else 0) >= 0
         && (if (n - 1) >= 0 then n - 1 else 0) >= 0
      ==> (n - 1) <= 0
          || Ordinal.<< (Ordinal.Int (if (n - 1) >= 0 then n - 1 else 0))
             (Ordinal.Int (if n >= 0 then n else 0))
  • simplify
    into
    (not
     ((not (n <= 0) && (if n >= 0 then n else 0) >= 0)
      && (if n >= 1 then -1 + n else 0) >= 0)
     || n <= 1)
    || Ordinal.<< (Ordinal.Int (if n >= 1 then -1 + n else 0))
       (Ordinal.Int (if n >= 0 then n else 0))
    expansions
    []
    rewrite_steps
      forward_chaining
      • unroll
        expr
        (|Ordinal.<<_116| (|Ordinal.Int_107| (ite (>= n_1479 1) (+ (- 1) n_1479) 0))
                          (|Ord…
        expansions
        • unsat
          (let ((a!1 (not (= n_1479 (ite (>= n_1479 0) n_1479 0))))
                (a!2 (+ n_1479 (* (- 1) (ite (>= n_1…

        In Imandra, induction schemes are "destructor style." So, an actual scheme Imandra would produce for a goal involving n : nat (where type nat = Zero | Succ of nat) is:

         (n = Zero ==> φ n)
         && (not (n = Zero) && φ (Destruct(Succ, 0, n)) ==> φ n).

        Let us see a few example inductions.

        In [2]:
        lemma assoc_append x y z =
         x @ (y @ z) = (x @ y) @ z [@@auto] [@@rw]
        
        Out[2]:
        val assoc_append : 'a list -> 'a list -> 'a list -> bool = <fun>
        Goal:
        
        x @ y @ z = (x @ y) @ z.
        
        1 nontautological subgoal.
        
        Subgoal 1:
        
        |---------------------------------------------------------------------------
         List.append x (List.append y z) = List.append (List.append x y) z
        
        
        Must try induction.
        
        The recursive terms in the conjecture suggest 3 inductions.
        Subsumption and merging reduces this to 2.
        
        Only 1 of those schemes are unflawed.
        We shall induct according to a scheme derived from List.append.
        
        Induction scheme:
        
         (x = [] ==> φ z y x) && (not (x = []) && φ z y (List.tl x) ==> φ z y x).
        
        2 nontautological subgoals.
        
        Subgoal 1.2:
        
         H0. x = []
        |---------------------------------------------------------------------------
         List.append x (List.append y z) = List.append (List.append x y) z
        
        But simplification reduces this to true, using the definition of List.append.
        
        Subgoal 1.1:
        
         H0. not (x = [])
         H1. List.append (List.tl x) (List.append y z) =
             List.append (List.append (List.tl x) y) z
        |---------------------------------------------------------------------------
         List.append x (List.append y z) = List.append (List.append x y) z
        
        But simplification reduces this to true, using the definition of List.append.
        
         Rules:
            (:def List.append)
            (:induct List.append)
        
        
        Proved
        proof
        ground_instances0
        definitions5
        inductions1
        search_time
        0.074s
        Expand
        • start[0.074s, "Goal"]
            List.append :var_0: (List.append :var_1: :var_2:) =
            List.append (List.append :var_0: :var_1:) :var_2:
        • subproof

          List.append x (List.append y z) = List.append (List.append x y) z
          • start[0.073s, "1"]
              List.append x (List.append y z) = List.append (List.append x y) z
          • induction on (functional )
            :scheme (x = [] ==> φ z y x)
                    && (not (x = []) && φ z y (List.tl x) ==> φ z y x)
          • Split ((not (x = [])
                    || List.append x (List.append y z) = List.append (List.append x y) z)
                   && (not
                       (not (x = [])
                        && List.append (List.tl x) (List.append y z) =
                           List.append (List.append (List.tl x) y) z)
                       || List.append x (List.append y z) =
                          List.append (List.append x y) z)
                   :cases [not (x = [])
                           || List.append x (List.append y z) =
                              List.append (List.append x y) z;
                           (x = []
                            || not
                               (List.append (List.tl x) (List.append y z) =
                                List.append (List.append (List.tl x) y) z))
                           || List.append x (List.append y z) =
                              List.append (List.append x y) z])
            • subproof
              (x = [] || not (List.append (List.tl x) (List.append y z) = List.append (List.append (List.tl x) y) z)) || List.append x (List.append y z) = List.append (List.append x y) z
              • start[0.034s, "1.1"]
                  (x = []
                   || not
                      (List.append (List.tl x) (List.append y z) =
                       List.append (List.append (List.tl x) y) z))
                  || List.append x (List.append y z) = List.append (List.append x y) z
              • simplify
                into
                true
                expansions
                [List.append, List.append, List.append]
                rewrite_steps
                  forward_chaining
                • subproof
                  not (x = []) || List.append x (List.append y z) = List.append (List.append x y) z
                  • start[0.034s, "1.2"]
                      not (x = [])
                      || List.append x (List.append y z) = List.append (List.append x y) z
                  • simplify
                    into
                    true
                    expansions
                    [List.append, List.append]
                    rewrite_steps
                      forward_chaining
                In [3]:
                lemma rev_append x y =
                 List.rev (x @ y) = List.rev y @ List.rev x
                 [@@auto]
                
                Out[3]:
                val rev_append : 'a list -> 'a list -> bool = <fun>
                Goal:
                
                List.rev (x @ y) = List.rev y @ List.rev x.
                
                1 nontautological subgoal.
                
                Subgoal 1:
                
                |---------------------------------------------------------------------------
                 List.rev (List.append x y) = List.append (List.rev y) (List.rev x)
                
                
                Must try induction.
                
                The recursive terms in the conjecture suggest 3 inductions.
                Subsumption and merging reduces this to 2.
                
                Only 1 of those schemes are unflawed.
                We shall induct according to a scheme derived from List.append.
                
                Induction scheme:
                
                 (x = [] ==> φ y x) && (not (x = []) && φ y (List.tl x) ==> φ y x).
                
                2 nontautological subgoals.
                
                Subgoal 1.2:
                
                 H0. x = []
                |---------------------------------------------------------------------------
                 List.rev (List.append x y) = List.append (List.rev y) (List.rev x)
                
                But simplification reduces this to true, using the definitions of List.append
                and List.rev, and the rewrite rule List.append_to_nil.
                
                Subgoal 1.1:
                
                 H0. not (x = [])
                 H1. List.rev (List.append (List.tl x) y) =
                     List.append (List.rev y) (List.rev (List.tl x))
                |---------------------------------------------------------------------------
                 List.rev (List.append x y) = List.append (List.rev y) (List.rev x)
                
                This simplifies, using the definitions of List.append and List.rev to:
                
                Subgoal 1.1':
                
                 H0. x <> []
                 H1. List.rev (List.append (List.tl x) y) =
                     List.append (List.rev y) (List.rev (List.tl x))
                |---------------------------------------------------------------------------
                 List.append (List.rev (List.append (List.tl x) y)) [List.hd x] =
                 List.append (List.rev y) (List.append (List.rev (List.tl x)) [List.hd x])
                
                But simplification reduces this to true, using the rewrite rule assoc_append.
                
                 Rules:
                    (:def List.append)
                    (:def List.rev)
                    (:rw List.append_to_nil)
                    (:rw assoc_append)
                    (:induct List.append)
                
                
                Proved
                proof
                ground_instances0
                definitions6
                inductions1
                search_time
                0.161s
                Expand
                • start[0.161s, "Goal"]
                    List.rev (List.append :var_0: :var_1:) =
                    List.append (List.rev :var_1:) (List.rev :var_0:)
                • subproof

                  List.rev (List.append x y) = List.append (List.rev y) (List.rev x)
                  • start[0.161s, "1"]
                      List.rev (List.append x y) = List.append (List.rev y) (List.rev x)
                  • induction on (functional )
                    :scheme (x = [] ==> φ y x) && (not (x = []) && φ y (List.tl x) ==> φ y x)
                  • Split ((not (x = [])
                            || List.rev (List.append x y) = List.append (List.rev y) (List.rev x))
                           && (not
                               (not (x = [])
                                && List.rev (List.append (List.tl x) y) =
                                   List.append (List.rev y) (List.rev (List.tl x)))
                               || List.rev (List.append x y) =
                                  List.append (List.rev y) (List.rev x))
                           :cases [not (x = [])
                                   || List.rev (List.append x y) =
                                      List.append (List.rev y) (List.rev x);
                                   (x = []
                                    || not
                                       (List.rev (List.append (List.tl x) y) =
                                        List.append (List.rev y) (List.rev (List.tl x))))
                                   || List.rev (List.append x y) =
                                      List.append (List.rev y) (List.rev x)])
                    • subproof
                      (x = [] || not (List.rev (List.append (List.tl x) y) = List.append (List.rev y) (List.rev (List.tl x)))) || List.rev (List.append x y) = List.append (List.rev y) (List.rev x)
                      • start[0.111s, "1.1"]
                          (x = []
                           || not
                              (List.rev (List.append (List.tl x) y) =
                               List.append (List.rev y) (List.rev (List.tl x))))
                          || List.rev (List.append x y) = List.append (List.rev y) (List.rev x)
                      • simplify
                        into
                        (x = []
                         || not
                            (List.rev (List.append (List.tl x) y) =
                             List.append (List.rev y) (List.rev (List.tl x))))
                        || List.append (List.rev (List.append (List.tl x) y)) [List.hd x] =
                           List.append (List.rev y) (List.append (List.rev (List.tl x)) [List.hd x])
                        expansions
                        [List.rev, List.rev, List.append]
                        rewrite_steps
                          forward_chaining
                          • simplify
                            into
                            true
                            expansions
                            []
                            rewrite_steps
                            assoc_append
                            forward_chaining
                          • subproof
                            not (x = []) || List.rev (List.append x y) = List.append (List.rev y) (List.rev x)
                            • start[0.111s, "1.2"]
                                not (x = [])
                                || List.rev (List.append x y) = List.append (List.rev y) (List.rev x)
                            • simplify
                              into
                              true
                              expansions
                              [List.append, List.rev, List.append]
                              rewrite_steps
                              List.append_to_nil
                              forward_chaining
                        In [4]:
                        verify (fun lst ->
                          List.for_all (fun x -> x > 0) lst ==>
                            List.fold_right (+) ~base:1 lst > 0)
                        [@@auto]
                        
                        Out[4]:
                        - : int list -> bool = <fun>
                        Goal:
                        
                        List.for_all (fun x -> x > 0) lst ==> List.fold_right + 1 lst > 0.
                        
                        1 nontautological subgoal.
                        
                        Subgoal 1:
                        
                         H0. List.for_all (fun x -> x > 0) lst
                         H1. List.fold_right + 1 lst <= 0
                        |---------------------------------------------------------------------------
                         false
                        
                        
                        Must try induction.
                        
                        The recursive terms in the conjecture suggest 2 inductions.
                        Subsumption and merging reduces this to 1.
                        
                        We shall induct according to a scheme derived from List.for_all.
                        
                        Induction scheme:
                        
                         (lst = [] ==> φ lst) && (not (lst = []) && φ (List.tl lst) ==> φ lst).
                        
                        2 nontautological subgoals.
                        
                        Subgoal 1.2:
                        
                         H0. lst = []
                         H1. List.for_all (fun x -> x > 0) lst
                         H2. List.fold_right + 1 lst <= 0
                        |---------------------------------------------------------------------------
                         false
                        
                        But simplification reduces this to true, using the definition of
                        List.fold_right.
                        
                        Subgoal 1.1:
                        
                         H0. not (lst = [])
                         H1. not (List.for_all (fun x -> x > 0) (List.tl lst))
                             || not (List.fold_right + 1 (List.tl lst) <= 0)
                         H2. List.for_all (fun x -> x > 0) lst
                         H3. List.fold_right + 1 lst <= 0
                        |---------------------------------------------------------------------------
                         false
                        
                        But simplification reduces this to true, using the definitions of
                        List.fold_right and List.for_all.
                        
                         Rules:
                            (:def List.fold_right)
                            (:def List.for_all)
                            (:induct List.for_all)
                        
                        
                        Proved
                        proof
                        ground_instances0
                        definitions3
                        inductions1
                        search_time
                        0.092s
                        Expand
                        • start[0.092s, "Goal"]
                            List.for_all (fun x -> x > 0) :var_0: ==> List.fold_right + 1 :var_0: > 0
                        • subproof

                          not (List.for_all (fun x -> x > 0) lst) || not (List.fold_right + 1 lst <= 0)
                          • start[0.091s, "1"]
                              not (List.for_all (fun x -> x > 0) lst)
                              || not (List.fold_right + 1 lst <= 0)
                          • induction on (functional )
                            :scheme (lst = [] ==> φ lst)
                                    && (not (lst = []) && φ (List.tl lst) ==> φ lst)
                          • Split (((not (lst = []) || not (List.for_all (fun x -> x > 0) lst))
                                    || not (List.fold_right + 1 lst <= 0))
                                   && ((not
                                        (not (lst = [])
                                         && (not (List.for_all (fun x -> x > 0) (List.tl lst))
                                             || not (List.fold_right + 1 (List.tl lst) <= 0)))
                                        || not (List.for_all (fun x -> x > 0) lst))
                                       || not (List.fold_right + 1 lst <= 0))
                                   :cases [(not (lst = []) || not (List.for_all (fun x -> x > 0) lst))
                                           || not (List.fold_right + 1 lst <= 0);
                                           ((lst = []
                                             || not
                                                (not (List.for_all (fun x -> x > 0) (List.tl lst))
                                                 || not (List.fold_right + 1 (List.tl lst) <= 0)))
                                            || not (List.for_all (fun x -> x > 0) lst))
                                           || not (List.fold_right + 1 lst <= 0)])
                            • subproof
                              ((lst = [] || not (not (List.for_all (fun x -> x > 0) (List.tl lst)) || not (List.fold_right + 1 (List.tl lst) <= 0))) || not (List.for_all (fun x -> x > 0) lst)) || not (List.fold_right + 1 lst <= 0)
                              • start[0.030s, "1.1"]
                                  ((lst = []
                                    || not
                                       (not (List.for_all (fun x -> x > 0) (List.tl lst))
                                        || not (List.fold_right + 1 (List.tl lst) <= 0)))
                                   || not (List.for_all (fun x -> x > 0) lst))
                                  || not (List.fold_right + 1 lst <= 0)
                              • simplify
                                into
                                true
                                expansions
                                [List.for_all, List.fold_right]
                                rewrite_steps
                                  forward_chaining
                                • subproof
                                  (not (lst = []) || not (List.for_all (fun x -> x > 0) lst)) || not (List.fold_right + 1 lst <= 0)
                                  • start[0.030s, "1.2"]
                                      (not (lst = []) || not (List.for_all (fun x -> x > 0) lst))
                                      || not (List.fold_right + 1 lst <= 0)
                                  • simplify
                                    into
                                    true
                                    expansions
                                    List.fold_right
                                    rewrite_steps
                                      forward_chaining

                                Functional Induction

                                By default, Imandra uses functional induction (also known as recursion induction).

                                A functional induction scheme is one derived from the recursive structure of a function definition. The termination measure used to admit the function is also used to justify the soundness of the functional induction scheme. Unless instructed otherwise, Imandra will consider all recursive functions in a goal, analyse their recursions and instances, and apply various heuristics to merge and score them and adapt them to the conjecture being proved. In general, there may be more than one plausible induction scheme to choose from, and selecting the "right" way to induct can often be a key step in difficult proofs. Imandra will often make the "right" decision. However, in case it doesn't, it is also possible to manually specify the induction that Imandra should do.

                                Let us return to the function repeat above and see functional induction in action.

                                In [5]:
                                lemma repeat_len c n =
                                  n >= 0 ==>
                                  List.length (repeat c n) = n [@@auto]
                                
                                Out[5]:
                                val repeat_len : 'a -> int -> bool = <fun>
                                Goal:
                                
                                n >= 0 ==> List.length (repeat c n) = n.
                                
                                1 nontautological subgoal.
                                
                                Subgoal 1:
                                
                                 H0. n >= 0
                                |---------------------------------------------------------------------------
                                 List.length (repeat c n) = n
                                
                                
                                Must try induction.
                                
                                We shall induct according to a scheme derived from repeat.
                                
                                Induction scheme:
                                
                                 (n <= 0 ==> φ c n) && (not (n <= 0) && φ c (n - 1) ==> φ c n).
                                
                                2 nontautological subgoals.
                                
                                Subgoal 1.2:
                                
                                 H0. n <= 0
                                 H1. n >= 0
                                |---------------------------------------------------------------------------
                                 List.length (repeat c n) = n
                                
                                But simplification reduces this to true, using the definitions of List.length
                                and repeat.
                                
                                Subgoal 1.1:
                                
                                 H0. not (n <= 0)
                                 H1. n >= 1 ==> List.length (repeat c (-1 + n)) = -1 + n
                                 H2. n >= 0
                                |---------------------------------------------------------------------------
                                 List.length (repeat c n) = n
                                
                                But simplification reduces this to true, using the definitions of List.length
                                and repeat.
                                
                                 Rules:
                                    (:def List.length)
                                    (:def repeat)
                                    (:fc List.len_nonnegative)
                                    (:induct repeat)
                                
                                
                                Proved
                                proof
                                ground_instances0
                                definitions4
                                inductions1
                                search_time
                                0.089s
                                Expand
                                • start[0.089s, "Goal"]
                                    :var_0: >= 0 ==> List.length (repeat :var_1: :var_0:) = :var_0:
                                • subproof

                                  not (n >= 0) || List.length (repeat c n) = n
                                  • start[0.088s, "1"] not (n >= 0) || List.length (repeat c n) = n
                                  • induction on (functional )
                                    :scheme (n <= 0 ==> φ c n) && (not (n <= 0) && φ c (n - 1) ==> φ c n)
                                  • Split (((not (n <= 0) || not (n >= 0)) || List.length (repeat c n) = n)
                                           && ((not
                                                (not (n <= 0)
                                                 && (not (n >= 1) || List.length (repeat c (-1 + n)) = -1 + n))
                                                || not (n >= 0))
                                               || List.length (repeat c n) = n)
                                           :cases [(not (n <= 0) || not (n >= 0)) || List.length (repeat c n) = n;
                                                   ((n <= 0
                                                     || not
                                                        (not (n >= 1) || List.length (repeat c (-1 + n)) = -1 + n))
                                                    || not (n >= 0))
                                                   || List.length (repeat c n) = n])
                                    • subproof
                                      ((n <= 0 || not (not (n >= 1) || List.length (repeat c (-1 + n)) = -1 + n)) || not (n >= 0)) || List.length (repeat c n) = n
                                      • start[0.025s, "1.1"]
                                          ((n <= 0 || not (not (n >= 1) || List.length (repeat c (-1 + n)) = -1 + n))
                                           || not (n >= 0))
                                          || List.length (repeat c n) = n
                                      • simplify
                                        into
                                        true
                                        expansions
                                        [List.length, repeat]
                                        rewrite_steps
                                          forward_chaining
                                          • List.len_nonnegative
                                          • List.len_nonnegative
                                      • subproof
                                        (not (n <= 0) || not (n >= 0)) || List.length (repeat c n) = n
                                        • start[0.025s, "1.2"]
                                            (not (n <= 0) || not (n >= 0)) || List.length (repeat c n) = n
                                        • simplify
                                          into
                                          true
                                          expansions
                                          [List.length, repeat]
                                          rewrite_steps
                                            forward_chaining
                                            List.len_nonnegative

                                    Functional induction schemes tailored to a problem can also be manually specified.

                                    In order to manually specify a functional induction, one must define a recursive function encoding the recursion scheme one wants available in induction (Imandra doesn't care what the function does, it only looks at how it recurses). As always, Imandra must be able to prove that the recursive function terminates in order for it to be admitted into the logic. The ordinal measures used in the termination proof are then used to justify subsequent functional induction schemes derived from the function.

                                    Let's see a simple example. Note that we could trivially prove this goal with [@@auto], but we shall use it to illustrate the process of manual induction schemes nevertheless! For fun, we'll make our custom induction scheme have two base-cases.

                                    In [6]:
                                    let rec sum n =
                                     if n <= 0 then 0
                                     else n + sum (n-1)
                                    
                                    let rec induct_scheme (n : int) =
                                     if n <= 0 then true
                                     else if n = 1 then true
                                     else induct_scheme (n-1)
                                    
                                    Out[6]:
                                    val sum : int -> Z.t = <fun>
                                    val induct_scheme : int -> bool = <fun>
                                    
                                    termination proof

                                    Termination proof

                                    call `sum (n - 1)` from `sum n`
                                    originalsum n
                                    subsum (n - 1)
                                    original ordinalOrdinal.Int (if n >= 0 then n else 0)
                                    sub ordinalOrdinal.Int (if (n - 1) >= 0 then n - 1 else 0)
                                    path[not (n <= 0)]
                                    proof
                                    detailed proof
                                    ground_instances1
                                    definitions0
                                    inductions0
                                    search_time
                                    0.011s
                                    details
                                    Expand
                                    smt_stats
                                    num checks3
                                    arith assert lower8
                                    arith pivots2
                                    rlimit count1027
                                    mk clause4
                                    datatype occurs check2
                                    mk bool var20
                                    arith assert upper3
                                    decisions2
                                    arith add rows3
                                    propagations2
                                    conflicts2
                                    arith fixed eqs2
                                    datatype accessor ax2
                                    arith conflicts1
                                    num allocs2448738349
                                    final checks1
                                    added eqs6
                                    del clause4
                                    arith eq adapter2
                                    memory20.360000
                                    max memory38.170000
                                    Expand
                                    • start[0.011s]
                                        not (n <= 0)
                                        && (if n >= 0 then n else 0) >= 0
                                           && (if (n - 1) >= 0 then n - 1 else 0) >= 0
                                        ==> (n - 1) <= 0
                                            || Ordinal.<< (Ordinal.Int (if (n - 1) >= 0 then n - 1 else 0))
                                               (Ordinal.Int (if n >= 0 then n else 0))
                                    • simplify
                                      into
                                      (not
                                       ((not (n <= 0) && (if n >= 0 then n else 0) >= 0)
                                        && (if n >= 1 then -1 + n else 0) >= 0)
                                       || n <= 1)
                                      || Ordinal.<< (Ordinal.Int (if n >= 1 then -1 + n else 0))
                                         (Ordinal.Int (if n >= 0 then n else 0))
                                      expansions
                                      []
                                      rewrite_steps
                                        forward_chaining
                                        • unroll
                                          expr
                                          (|Ordinal.<<_116| (|Ordinal.Int_107| (ite (>= n_1766 1) (+ (- 1) n_1766) 0))
                                                            (|Ord…
                                          expansions
                                          • unsat
                                            (let ((a!1 (not (= n_1766 (ite (>= n_1766 0) n_1766 0))))
                                                  (a!2 (+ n_1766 (* (- 1) (ite (>= n_1…

                                          termination proof

                                          Termination proof

                                          call `induct_scheme (n - 1)` from `induct_scheme n`
                                          originalinduct_scheme n
                                          subinduct_scheme (n - 1)
                                          original ordinalOrdinal.Int (if n >= 0 then n else 0)
                                          sub ordinalOrdinal.Int (if (n - 1) >= 0 then n - 1 else 0)
                                          path[not (n = 1) && not (n <= 0)]
                                          proof
                                          detailed proof
                                          ground_instances1
                                          definitions0
                                          inductions0
                                          search_time
                                          0.014s
                                          details
                                          Expand
                                          smt_stats
                                          num checks3
                                          arith assert lower10
                                          arith pivots2
                                          rlimit count1133
                                          mk clause7
                                          datatype occurs check2
                                          mk bool var24
                                          arith assert upper3
                                          decisions2
                                          arith add rows3
                                          propagations3
                                          conflicts2
                                          arith fixed eqs2
                                          datatype accessor ax2
                                          arith conflicts1
                                          arith assert diseq3
                                          num allocs2530488807
                                          final checks1
                                          added eqs6
                                          del clause7
                                          arith eq adapter4
                                          memory20.670000
                                          max memory38.170000
                                          Expand
                                          • start[0.014s]
                                              not (n = 1)
                                              && not (n <= 0)
                                                 && (if n >= 0 then n else 0) >= 0
                                                    && (if (n - 1) >= 0 then n - 1 else 0) >= 0
                                              ==> not (not (n - 1 = 1) && not ((n - 1) <= 0))
                                                  || Ordinal.<< (Ordinal.Int (if (n - 1) >= 0 then n - 1 else 0))
                                                     (Ordinal.Int (if n >= 0 then n else 0))
                                          • simplify
                                            into
                                            (not
                                             (((not (n = 1) && not (n <= 0)) && (if n >= 0 then n else 0) >= 0)
                                              && (if n >= 1 then -1 + n else 0) >= 0)
                                             || not (not (n = 2) && not (n <= 1)))
                                            || Ordinal.<< (Ordinal.Int (if n >= 1 then -1 + n else 0))
                                               (Ordinal.Int (if n >= 0 then n else 0))
                                            expansions
                                            []
                                            rewrite_steps
                                              forward_chaining
                                              • unroll
                                                expr
                                                (|Ordinal.<<_116| (|Ordinal.Int_107| (ite (>= n_1777 1) (+ (- 1) n_1777) 0))
                                                                  (|Ord…
                                                expansions
                                                • unsat
                                                  (let ((a!1 (not (= n_1777 (ite (>= n_1777 0) n_1777 0))))
                                                        (a!2 (+ n_1777 (* (- 1) (ite (>= n_1…

                                                In [7]:
                                                verify (fun n -> n >= 0 ==> sum n = (n * (n+1)) / 2) [@@induct functional induct_scheme]
                                                
                                                Out[7]:
                                                - : int -> bool = <fun>
                                                Goal:
                                                
                                                n >= 0 ==> sum n = (n * (n + 1)) / 2.
                                                
                                                1 nontautological subgoal.
                                                
                                                Note: Thank you for your explicit request for a non-present functional
                                                induction!
                                                
                                                We shall induct according to a scheme derived from induct_scheme.
                                                
                                                Induction scheme:
                                                
                                                 (not (not (n = 1) && not (n <= 0)) ==> φ n)
                                                 && (not (n <= 0) && not (n = 1) && φ (n - 1) ==> φ n).
                                                
                                                2 nontautological subgoals.
                                                
                                                Subgoal 2:
                                                
                                                 H0. n >= 0
                                                |---------------------------------------------------------------------------
                                                 C0. not (n = 1) && not (n <= 0)
                                                 C1. sum n = (n * (1 + n)) / 2
                                                
                                                This simplifies to the following 2 subgoals:
                                                
                                                Subgoal 2.2:
                                                
                                                 H0. n = 1
                                                |---------------------------------------------------------------------------
                                                 sum n = (n * (1 + n)) / 2
                                                
                                                But simplification reduces this to true, using the definition of sum.
                                                
                                                Subgoal 2.1:
                                                
                                                 H0. n >= 0
                                                 H1. n <= 0
                                                |---------------------------------------------------------------------------
                                                 C0. n = 1
                                                 C1. sum n = (n * (1 + n)) / 2
                                                
                                                But simplification reduces this to true, using the definition of sum.
                                                
                                                Subgoal 1:
                                                
                                                 H0. not (n <= 0)
                                                 H1. not (n = 1)
                                                 H2. n >= 1 ==> sum (-1 + n) = (n * (-1 + n)) / 2
                                                 H3. n >= 0
                                                |---------------------------------------------------------------------------
                                                 sum n = (n * (1 + n)) / 2
                                                
                                                But simplification reduces this to true, using the definition of sum.
                                                
                                                 Rules:
                                                    (:def sum)
                                                    (:induct induct_scheme)
                                                
                                                
                                                Proved
                                                proof
                                                ground_instances0
                                                definitions4
                                                inductions1
                                                search_time
                                                0.087s
                                                Expand
                                                • start[0.087s, "Goal"]
                                                    :var_0: >= 0 ==> sum :var_0: = (:var_0: * (:var_0: + 1)) / 2
                                                • subproof

                                                  not (n >= 0) || sum n = (n * (1 + n)) / 2
                                                  • start[0.086s, "1"] not (n >= 0) || sum n = (n * (1 + n)) / 2
                                                  • induction on (functional induct_scheme)
                                                    :scheme (not (not (n = 1) && not (n <= 0)) ==> φ n)
                                                            && (not (n <= 0) && not (n = 1) && φ (n - 1) ==> φ n)
                                                  • Split (((not (n = 1) && not (n <= 0) || not (n >= 0))
                                                            || sum n = (n * (1 + n)) / 2)
                                                           && ((not
                                                                ((not (n <= 0) && not (n = 1))
                                                                 && (not (n >= 1) || sum (-1 + n) = (n * (-1 + n)) / 2))
                                                                || not (n >= 0))
                                                               || sum n = (n * (1 + n)) / 2)
                                                           :cases [(not (n >= 0) || not (n = 1) && not (n <= 0))
                                                                   || sum n = (n * (1 + n)) / 2;
                                                                   (((n <= 0 || n = 1)
                                                                     || not (not (n >= 1) || sum (-1 + n) = (n * (-1 + n)) / 2))
                                                                    || not (n >= 0))
                                                                   || sum n = (n * (1 + n)) / 2])
                                                    • subproof
                                                      (((n <= 0 || n = 1) || not (not (n >= 1) || sum (-1 + n) = (n * (-1 + n)) / 2)) || not (n >= 0)) || sum n = (n * (1 + n)) / 2
                                                      • start[0.083s, "1"]
                                                          (((n <= 0 || n = 1)
                                                            || not (not (n >= 1) || sum (-1 + n) = (n * (-1 + n)) / 2))
                                                           || not (n >= 0))
                                                          || sum n = (n * (1 + n)) / 2
                                                      • simplify
                                                        into
                                                        true
                                                        expansions
                                                        sum
                                                        rewrite_steps
                                                          forward_chaining
                                                        • subproof
                                                          (not (n >= 0) || not (n = 1) && not (n <= 0)) || sum n = (n * (1 + n)) / 2
                                                          • start[0.083s, "2"]
                                                              (not (n >= 0) || not (n = 1) && not (n <= 0)) || sum n = (n * (1 + n)) / 2
                                                          • simplify
                                                            into
                                                            (not (n = 1) || sum n = (n * (1 + n)) / 2)
                                                            && (((not (n >= 0) || not (n <= 0)) || n = 1) || sum n = (n * (1 + n)) / 2)
                                                            expansions
                                                            []
                                                            rewrite_steps
                                                              forward_chaining
                                                                • Subproof
                                                                • Subproof

                                                        Note that it's rare to have to manually instruct Imandra how to induct in this way. Usually, if you need to instruct Imandra to use a different scheme than the one it automatically picked, you'll simply need to give Imandra the hint of "inducting following key recursive function foo" in your goal. For example, if Imandra had made a wrong selection in a goal involving sum and some other recursive functions, we might tell Imandra [@@induct functional sum] to get it to select a scheme derived from the recursive structure of sum.

                                                        Structural Induction

                                                        Imandra also supports structural induction. Unlike functional induction schemes which are derived from recursive functions, structural induction schemes are derived from type definitions.

                                                        For example, we can define a type of binary trees and prove a property about them by structural induction.

                                                        In [8]:
                                                        type 'a tree = Node of 'a * 'a tree * 'a tree | Leaf
                                                        
                                                        Out[8]:
                                                        type 'a tree = Node of 'a * 'a tree * 'a tree | Leaf
                                                        
                                                        In [9]:
                                                        let rec size (x : 'a tree) =
                                                         match x with
                                                         | Node (_, a,b) -> size a + size b
                                                         | Leaf -> 1
                                                        
                                                        Out[9]:
                                                        val size : 'a tree -> Z.t = <fun>
                                                        
                                                        termination proof

                                                        Termination proof

                                                        call `size (Destruct(Node, 1, x))` from `size x`
                                                        originalsize x
                                                        subsize (Destruct(Node, 1, x))
                                                        original ordinalOrdinal.Int (Ordinal.count x)
                                                        sub ordinalOrdinal.Int (Ordinal.count (Destruct(Node, 1, x)))
                                                        path[Is_a(Node, x)]
                                                        proof
                                                        detailed proof
                                                        ground_instances3
                                                        definitions0
                                                        inductions0
                                                        search_time
                                                        0.013s
                                                        details
                                                        Expand
                                                        smt_stats
                                                        num checks8
                                                        arith assert lower12
                                                        arith pivots12
                                                        rlimit count5064
                                                        mk clause17
                                                        datatype occurs check12
                                                        mk bool var68
                                                        arith gcd tests4
                                                        arith assert upper10
                                                        datatype splits3
                                                        decisions15
                                                        arith add rows22
                                                        propagations11
                                                        arith patches1
                                                        conflicts6
                                                        arith fixed eqs4
                                                        datatype accessor ax7
                                                        arith conflicts2
                                                        datatype constructor ax11
                                                        num allocs3185482010
                                                        final checks5
                                                        added eqs42
                                                        del clause10
                                                        arith ineq splits1
                                                        arith eq adapter7
                                                        memory27.470000
                                                        max memory38.170000
                                                        Expand
                                                        • start[0.013s]
                                                            Is_a(Node, x)
                                                            && Ordinal.count x >= 0 && Ordinal.count (Destruct(Node, 1, x)) >= 0
                                                            ==> not Is_a(Node, Destruct(Node, 1, x))
                                                                && not Is_a(Node, Destruct(Node, 1, x))
                                                                || Ordinal.<< (Ordinal.Int (Ordinal.count (Destruct(Node, 1, x))))
                                                                   (Ordinal.Int (Ordinal.count x))
                                                        • simplify
                                                          into
                                                          (not
                                                           ((Is_a(Node, x) && Ordinal.count x >= 0)
                                                            && Ordinal.count (Destruct(Node, 1, x)) >= 0)
                                                           || not Is_a(Node, Destruct(Node, 1, x)))
                                                          || Ordinal.<< (Ordinal.Int (Ordinal.count (Destruct(Node, 1, x))))
                                                             (Ordinal.Int (Ordinal.count x))
                                                          expansions
                                                          []
                                                          rewrite_steps
                                                            forward_chaining
                                                            • unroll
                                                              expr
                                                              (|Ordinal.<<_116| (|Ordinal.Int_107|
                                                                                  (|count_`ty_0 tree`_1850| (|get.Node.1_1833…
                                                              expansions
                                                              • unroll
                                                                expr
                                                                (|count_`ty_0 tree`_1850| (|get.Node.1_1833| x_1839))
                                                                expansions
                                                                • unroll
                                                                  expr
                                                                  (|count_`ty_0 tree`_1850| x_1839)
                                                                  expansions
                                                                  • unsat
                                                                    (let ((a!1 (ite (>= (|count_`ty_0 tree`_1850| (|get.Node.2_1834| x_1839)) 0)
                                                                                    (|count…

                                                                  call `size (Destruct(Node, 2, x))` from `size x`
                                                                  originalsize x
                                                                  subsize (Destruct(Node, 2, x))
                                                                  original ordinalOrdinal.Int (Ordinal.count x)
                                                                  sub ordinalOrdinal.Int (Ordinal.count (Destruct(Node, 2, x)))
                                                                  path[Is_a(Node, x)]
                                                                  proof
                                                                  detailed proof
                                                                  ground_instances3
                                                                  definitions0
                                                                  inductions0
                                                                  search_time
                                                                  0.013s
                                                                  details
                                                                  Expand
                                                                  smt_stats
                                                                  num checks8
                                                                  arith assert lower12
                                                                  arith pivots12
                                                                  rlimit count2532
                                                                  mk clause17
                                                                  datatype occurs check12
                                                                  mk bool var68
                                                                  arith gcd tests4
                                                                  arith assert upper10
                                                                  datatype splits3
                                                                  decisions15
                                                                  arith add rows22
                                                                  propagations11
                                                                  arith patches1
                                                                  conflicts6
                                                                  arith fixed eqs4
                                                                  datatype accessor ax7
                                                                  arith conflicts2
                                                                  datatype constructor ax11
                                                                  num allocs3133764657
                                                                  final checks5
                                                                  added eqs42
                                                                  del clause10
                                                                  arith ineq splits1
                                                                  arith eq adapter7
                                                                  memory24.570000
                                                                  max memory38.170000
                                                                  Expand
                                                                  • start[0.013s]
                                                                      Is_a(Node, x)
                                                                      && Ordinal.count x >= 0 && Ordinal.count (Destruct(Node, 2, x)) >= 0
                                                                      ==> not Is_a(Node, Destruct(Node, 2, x))
                                                                          && not Is_a(Node, Destruct(Node, 2, x))
                                                                          || Ordinal.<< (Ordinal.Int (Ordinal.count (Destruct(Node, 2, x))))
                                                                             (Ordinal.Int (Ordinal.count x))
                                                                  • simplify
                                                                    into
                                                                    (not
                                                                     ((Is_a(Node, x) && Ordinal.count x >= 0)
                                                                      && Ordinal.count (Destruct(Node, 2, x)) >= 0)
                                                                     || not Is_a(Node, Destruct(Node, 2, x)))
                                                                    || Ordinal.<< (Ordinal.Int (Ordinal.count (Destruct(Node, 2, x))))
                                                                       (Ordinal.Int (Ordinal.count x))
                                                                    expansions
                                                                    []
                                                                    rewrite_steps
                                                                      forward_chaining
                                                                      • unroll
                                                                        expr
                                                                        (|Ordinal.<<_116| (|Ordinal.Int_107|
                                                                                            (|count_`ty_0 tree`_1850| (|get.Node.2_1834…
                                                                        expansions
                                                                        • unroll
                                                                          expr
                                                                          (|count_`ty_0 tree`_1850| (|get.Node.2_1834| x_1839))
                                                                          expansions
                                                                          • unroll
                                                                            expr
                                                                            (|count_`ty_0 tree`_1850| x_1839)
                                                                            expansions
                                                                            • unsat
                                                                              (let ((a!1 (ite (>= (|count_`ty_0 tree`_1850| (|get.Node.1_1833| x_1839)) 0)
                                                                                              (|count…

                                                                            In [10]:
                                                                            verify (fun x -> size x > 0) [@@induct structural x]
                                                                            
                                                                            Out[10]:
                                                                            - : 'a tree -> bool = <fun>
                                                                            Goal:
                                                                            
                                                                            size x > 0.
                                                                            
                                                                            1 nontautological subgoal.
                                                                            
                                                                            Induction scheme:
                                                                            
                                                                             φ Leaf
                                                                             && (Is_a(Node, x) && φ (Destruct(Node, 1, x)) && φ (Destruct(Node, 2, x))
                                                                                 ==> φ x).
                                                                            
                                                                            2 nontautological subgoals.
                                                                            
                                                                            Subgoal 2:
                                                                            
                                                                            |---------------------------------------------------------------------------
                                                                             not (size Leaf <= 0)
                                                                            
                                                                            But simplification reduces this to true, using the definition of size.
                                                                            
                                                                            Subgoal 1:
                                                                            
                                                                             H0. Is_a(Node, x)
                                                                             H1. not (size (Destruct(Node, 1, x)) <= 0)
                                                                             H2. not (size (Destruct(Node, 2, x)) <= 0)
                                                                             H3. size x <= 0
                                                                            |---------------------------------------------------------------------------
                                                                             false
                                                                            
                                                                            But simplification reduces this to true, using the definition of size.
                                                                            
                                                                             Rules:
                                                                                (:def size)
                                                                                (:induct struct tree)
                                                                            
                                                                            
                                                                            Proved
                                                                            proof
                                                                            ground_instances0
                                                                            definitions2
                                                                            inductions1
                                                                            search_time
                                                                            0.015s
                                                                            Expand
                                                                            • start[0.015s, "Goal"] size :var_0: > 0
                                                                            • subproof

                                                                              not (size x <= 0)
                                                                              • start[0.014s, "1"] not (size x <= 0)
                                                                              • induction on (structural+ x)
                                                                                :scheme φ Leaf
                                                                                        && (Is_a(Node, x)
                                                                                            && φ (Destruct(Node, 1, x)) && φ (Destruct(Node, 2, x))
                                                                                            ==> φ x)
                                                                              • Split (not (size Leaf <= 0)
                                                                                       && (not
                                                                                           ((Is_a(Node, x) && not (size (Destruct(Node, 1, x)) <= 0))
                                                                                            && not (size (Destruct(Node, 2, x)) <= 0))
                                                                                           || not (size x <= 0))
                                                                                       :cases [not (size Leaf <= 0);
                                                                                               ((not Is_a(Node, x) || size (Destruct(Node, 1, x)) <= 0)
                                                                                                || size (Destruct(Node, 2, x)) <= 0)
                                                                                               || not (size x <= 0)])
                                                                                • subproof
                                                                                  ((not Is_a(Node, x) || size (Destruct(Node, 1, x)) <= 0) || size (Destruct(Node, 2, x)) <= 0) || not (size x <= 0)
                                                                                  • start[0.014s, "1"]
                                                                                      ((not Is_a(Node, x) || size (Destruct(Node, 1, x)) <= 0)
                                                                                       || size (Destruct(Node, 2, x)) <= 0)
                                                                                      || not (size x <= 0)
                                                                                  • simplify
                                                                                    into
                                                                                    true
                                                                                    expansions
                                                                                    size
                                                                                    rewrite_steps
                                                                                      forward_chaining
                                                                                    • subproof
                                                                                      not (size Leaf <= 0)
                                                                                      • start[0.014s, "2"] not (size Leaf <= 0)
                                                                                      • simplify
                                                                                        into
                                                                                        true
                                                                                        expansions
                                                                                        size
                                                                                        rewrite_steps
                                                                                          forward_chaining

                                                                                    Structural induction comes in both additive and multiplicative flavors.

                                                                                    This distinction only manifests when one is performing structural induction over multiple variables simultaneously. It affects the way base cases and inductive steps are mixed. Let's assume one needs to do induction on x, y:

                                                                                    • addictive structural induction gives you 3 cases: two base cases φ(x_base, y), φ(x, y_base) and one inductive step φ(x,y) ==> φ(step(x), step(y))

                                                                                    • multiplicative structural induction gives you 4 cases: one base case φ(x_base, y_base) and three inductive steps φ(x, y_base) ==> φ(step(x), y_base), φ(x_base, y) ==> φ(x_base, step(y)) and φ(x,y) ==> φ(step(x), step(y))

                                                                                    We can see the difference using the following function:

                                                                                    In [11]:
                                                                                    let rec interleave_strict x y = match x, y with
                                                                                      | [], _ | _ , [] -> []
                                                                                      | x::xs, y::ys -> x::y::(interleave_strict xs ys)
                                                                                    
                                                                                    Out[11]:
                                                                                    val interleave_strict : 'a list -> 'a list -> 'a list = <fun>
                                                                                    
                                                                                    termination proof

                                                                                    Termination proof

                                                                                    call `interleave_strict (List.tl x) (List.tl y)` from `interleave_strict x y`
                                                                                    originalinterleave_strict x y
                                                                                    subinterleave_strict (List.tl x) (List.tl y)
                                                                                    original ordinalOrdinal.Int (Ordinal.count x)
                                                                                    sub ordinalOrdinal.Int (Ordinal.count (List.tl x))
                                                                                    path[not (x = [] || y = [])]
                                                                                    proof
                                                                                    detailed proof
                                                                                    ground_instances3
                                                                                    definitions0
                                                                                    inductions0
                                                                                    search_time
                                                                                    0.012s
                                                                                    details
                                                                                    Expand
                                                                                    smt_stats
                                                                                    num checks7
                                                                                    arith assert lower5
                                                                                    arith pivots3
                                                                                    rlimit count2053
                                                                                    mk clause3
                                                                                    datatype occurs check27
                                                                                    mk bool var70
                                                                                    arith assert upper5
                                                                                    datatype splits6
                                                                                    decisions15
                                                                                    arith add rows7
                                                                                    propagations1
                                                                                    conflicts11
                                                                                    arith fixed eqs4
                                                                                    datatype accessor ax7
                                                                                    arith conflicts1
                                                                                    datatype constructor ax17
                                                                                    num allocs3431534076
                                                                                    final checks6
                                                                                    added eqs57
                                                                                    del clause1
                                                                                    arith eq adapter3
                                                                                    memory25.300000
                                                                                    max memory38.170000
                                                                                    Expand
                                                                                    • start[0.012s]
                                                                                        not (x = [] || y = [])
                                                                                        && Ordinal.count x >= 0 && Ordinal.count (List.tl x) >= 0
                                                                                        ==> (List.tl x = [] || List.tl y = [])
                                                                                            || Ordinal.<< (Ordinal.Int (Ordinal.count (List.tl x)))
                                                                                               (Ordinal.Int (Ordinal.count x))
                                                                                    • simplify
                                                                                      into
                                                                                      ((not
                                                                                        ((not (x = [] || y = []) && Ordinal.count x >= 0)
                                                                                         && Ordinal.count (List.tl x) >= 0)
                                                                                        || List.tl x = [])
                                                                                       || List.tl y = [])
                                                                                      || Ordinal.<< (Ordinal.Int (Ordinal.count (List.tl x)))
                                                                                         (Ordinal.Int (Ordinal.count x))
                                                                                      expansions
                                                                                      []
                                                                                      rewrite_steps
                                                                                        forward_chaining
                                                                                        • unroll
                                                                                          expr
                                                                                          (|Ordinal.<<_116| (|Ordinal.Int_107|
                                                                                                              (|count_`ty_0 list`_1915| (|get.::.1_1896| …
                                                                                          expansions
                                                                                          • unroll
                                                                                            expr
                                                                                            (|count_`ty_0 list`_1915| (|get.::.1_1896| x_1904))
                                                                                            expansions
                                                                                            • unroll
                                                                                              expr
                                                                                              (|count_`ty_0 list`_1915| x_1904)
                                                                                              expansions
                                                                                              • unsat
                                                                                                (let ((a!1 (= (|count_`ty_0 list`_1915| x_1904)
                                                                                                              (+ 1 (|count_`ty_0 list`_1915| (|get.:…

                                                                                              Let's prove that the length of interleave_strict x y is always less than or equal to the sum of the lengths of x and y. We'll do it first using additive and then using multiplicative structural induction:

                                                                                              In [12]:
                                                                                              verify (fun x y ->
                                                                                                List.length @@ interleave_strict x y <= List.length x + List.length y)
                                                                                              [@@induct structural_add (x,y)]
                                                                                              
                                                                                              Out[12]:
                                                                                              - : 'a list -> 'a list -> bool = <fun>
                                                                                              Goal:
                                                                                              
                                                                                              (List.length @@ interleave_strict x y) <= (List.length x + List.length y).
                                                                                              
                                                                                              1 nontautological subgoal.
                                                                                              
                                                                                              Induction scheme:
                                                                                              
                                                                                               φ y []
                                                                                               && φ [] x && (x <> [] && y <> [] && φ (List.tl y) (List.tl x) ==> φ y x).
                                                                                              
                                                                                              3 nontautological subgoals.
                                                                                              
                                                                                              Subgoal 3:
                                                                                              
                                                                                              |---------------------------------------------------------------------------
                                                                                               List.length (interleave_strict [] y) <= (List.length [] + List.length y)
                                                                                              
                                                                                              But simplification reduces this to true, using the definitions of List.length
                                                                                              and interleave_strict.
                                                                                              
                                                                                              Subgoal 2:
                                                                                              
                                                                                              |---------------------------------------------------------------------------
                                                                                               List.length (interleave_strict x []) <= (List.length x + List.length [])
                                                                                              
                                                                                              But simplification reduces this to true, using the definitions of List.length
                                                                                              and interleave_strict.
                                                                                              
                                                                                              Subgoal 1:
                                                                                              
                                                                                               H0. x <> []
                                                                                               H1. y <> []
                                                                                               H2. List.length (interleave_strict (List.tl x) (List.tl y)) <=
                                                                                                   (List.length (List.tl x) + List.length (List.tl y))
                                                                                              |---------------------------------------------------------------------------
                                                                                               List.length (interleave_strict x y) <= (List.length x + List.length y)
                                                                                              
                                                                                              This simplifies, using the definitions of List.length and interleave_strict
                                                                                              to:
                                                                                              
                                                                                              Subgoal 1':
                                                                                              
                                                                                               H0. x <> []
                                                                                               H1. y <> []
                                                                                               H2. List.length (interleave_strict (List.tl x) (List.tl y)) <=
                                                                                                   (List.length (List.tl x) + List.length (List.tl y))
                                                                                              |---------------------------------------------------------------------------
                                                                                               List.length ((List.hd y) :: (interleave_strict (List.tl x) (List.tl y))) <=
                                                                                               ((1 + List.length (List.tl x)) + List.length (List.tl y))
                                                                                              
                                                                                              But simplification reduces this to true, using the definition of List.length.
                                                                                              
                                                                                               Rules:
                                                                                                  (:def List.length)
                                                                                                  (:def interleave_strict)
                                                                                                  (:fc List.len_nonnegative)
                                                                                                  (:induct struct list)
                                                                                              
                                                                                              
                                                                                              Proved
                                                                                              proof
                                                                                              ground_instances0
                                                                                              definitions11
                                                                                              inductions1
                                                                                              search_time
                                                                                              0.119s
                                                                                              Expand
                                                                                              • start[0.119s, "Goal"]
                                                                                                  List.length (interleave_strict :var_0: :var_1:) <=
                                                                                                  (List.length :var_0: + List.length :var_1:)
                                                                                              • subproof

                                                                                                List.length (interleave_strict x y) <= (List.length x + List.length y)
                                                                                                • start[0.119s, "1"]
                                                                                                    List.length (interleave_strict x y) <= (List.length x + List.length y)
                                                                                                • induction on (structural+ x, y)
                                                                                                  :scheme φ y []
                                                                                                          && φ [] x
                                                                                                             && (x <> [] && y <> [] && φ (List.tl y) (List.tl x) ==> φ y x)
                                                                                                • Split ((List.length (interleave_strict [] y) <=
                                                                                                          (List.length [] + List.length y)
                                                                                                          && List.length (interleave_strict x []) <=
                                                                                                             (List.length x + List.length []))
                                                                                                         && (not
                                                                                                             ((x <> [] && y <> [])
                                                                                                              && List.length (interleave_strict (List.tl x) (List.tl y)) <=
                                                                                                                 (List.length (List.tl x) + List.length (List.tl y)))
                                                                                                             || List.length (interleave_strict x y) <=
                                                                                                                (List.length x + List.length y))
                                                                                                         :cases [List.length (interleave_strict [] y) <=
                                                                                                                 (List.length [] + List.length y);
                                                                                                                 List.length (interleave_strict x []) <=
                                                                                                                 (List.length x + List.length []);
                                                                                                                 ((not (x <> []) || not (y <> []))
                                                                                                                  || not
                                                                                                                     (List.length (interleave_strict (List.tl x) (List.tl y))
                                                                                                                      <= (List.length (List.tl x) + List.length (List.tl y))))
                                                                                                                 || List.length (interleave_strict x y) <=
                                                                                                                    (List.length x + List.length y)])
                                                                                                  • subproof
                                                                                                    ((not (x <> []) || not (y <> [])) || not (List.length (interleave_strict (List.tl x) (List.tl y)) <= (List.length (List.tl x) + List.length (List.tl y)))) || List.length (interleave_strict x y) <= (List.length x + List.length y)
                                                                                                    • start[0.117s, "1"]
                                                                                                        ((not (x <> []) || not (y <> []))
                                                                                                         || not
                                                                                                            (List.length (interleave_strict (List.tl x) (List.tl y)) <=
                                                                                                             (List.length (List.tl x) + List.length (List.tl y))))
                                                                                                        || List.length (interleave_strict x y) <= (List.length x + List.length y)
                                                                                                    • simplify
                                                                                                      into
                                                                                                      ((not (x <> []) || not (y <> []))
                                                                                                       || not
                                                                                                          (List.length (interleave_strict (List.tl x) (List.tl y)) <=
                                                                                                           (List.length (List.tl x) + List.length (List.tl y))))
                                                                                                      || List.length ((List.hd y) :: (interleave_strict (List.tl x) (List.tl y)))
                                                                                                         <= ((1 + List.length (List.tl x)) + List.length (List.tl y))
                                                                                                      expansions
                                                                                                      [List.length, List.length, List.length, interleave_strict]
                                                                                                      rewrite_steps
                                                                                                        forward_chaining
                                                                                                        • List.len_nonnegative
                                                                                                        • List.len_nonnegative
                                                                                                        • List.len_nonnegative
                                                                                                        • List.len_nonnegative
                                                                                                        • List.len_nonnegative
                                                                                                        • List.len_nonnegative
                                                                                                        • List.len_nonnegative
                                                                                                        • List.len_nonnegative
                                                                                                        • List.len_nonnegative
                                                                                                        • List.len_nonnegative
                                                                                                        • List.len_nonnegative
                                                                                                        • List.len_nonnegative
                                                                                                        • List.len_nonnegative
                                                                                                        • List.len_nonnegative
                                                                                                        • List.len_nonnegative
                                                                                                        • List.len_nonnegative
                                                                                                        • List.len_nonnegative
                                                                                                        • List.len_nonnegative
                                                                                                        • List.len_nonnegative
                                                                                                      • simplify
                                                                                                        into
                                                                                                        true
                                                                                                        expansions
                                                                                                        List.length
                                                                                                        rewrite_steps
                                                                                                          forward_chaining
                                                                                                          • List.len_nonnegative
                                                                                                          • List.len_nonnegative
                                                                                                          • List.len_nonnegative
                                                                                                          • List.len_nonnegative
                                                                                                      • subproof
                                                                                                        List.length (interleave_strict x []) <= (List.length x + List.length [])
                                                                                                        • start[0.118s, "2"]
                                                                                                            List.length (interleave_strict x []) <= (List.length x + List.length [])
                                                                                                        • simplify
                                                                                                          into
                                                                                                          true
                                                                                                          expansions
                                                                                                          [List.length, List.length, interleave_strict]
                                                                                                          rewrite_steps
                                                                                                            forward_chaining
                                                                                                            • List.len_nonnegative
                                                                                                            • List.len_nonnegative
                                                                                                            • List.len_nonnegative
                                                                                                        • subproof
                                                                                                          List.length (interleave_strict [] y) <= (List.length [] + List.length y)
                                                                                                          • start[0.118s, "3"]
                                                                                                              List.length (interleave_strict [] y) <= (List.length [] + List.length y)
                                                                                                          • simplify
                                                                                                            into
                                                                                                            true
                                                                                                            expansions
                                                                                                            [List.length, List.length, interleave_strict]
                                                                                                            rewrite_steps
                                                                                                              forward_chaining
                                                                                                              • List.len_nonnegative
                                                                                                              • List.len_nonnegative
                                                                                                              • List.len_nonnegative
                                                                                                      In [13]:
                                                                                                      verify (fun x y ->
                                                                                                        List.length @@ interleave_strict x y <= List.length x + List.length y)
                                                                                                      [@@induct structural_mult (x,y)]
                                                                                                      
                                                                                                      Out[13]:
                                                                                                      - : 'a list -> 'a list -> bool = <fun>
                                                                                                      Goal:
                                                                                                      
                                                                                                      (List.length @@ interleave_strict x y) <= (List.length x + List.length y).
                                                                                                      
                                                                                                      1 nontautological subgoal.
                                                                                                      
                                                                                                      Induction scheme:
                                                                                                      
                                                                                                       φ [] []
                                                                                                       && (x <> [] && φ [] (List.tl x) ==> φ [] x)
                                                                                                          && (y <> [] && φ (List.tl y) [] ==> φ y [])
                                                                                                             && (x <> [] && y <> [] && φ (List.tl y) (List.tl x) ==> φ y x).
                                                                                                      
                                                                                                      4 nontautological subgoals.
                                                                                                      
                                                                                                      Subgoal 4:
                                                                                                      
                                                                                                      |---------------------------------------------------------------------------
                                                                                                       List.length (interleave_strict [] []) <= (2 * List.length [])
                                                                                                      
                                                                                                      But simplification reduces this to true, using the definitions of List.length
                                                                                                      and interleave_strict.
                                                                                                      
                                                                                                      Subgoal 3:
                                                                                                      
                                                                                                       H0. x <> []
                                                                                                       H1. List.length (interleave_strict (List.tl x) []) <=
                                                                                                           (List.length (List.tl x) + List.length [])
                                                                                                      |---------------------------------------------------------------------------
                                                                                                       List.length (interleave_strict x []) <= (List.length x + List.length [])
                                                                                                      
                                                                                                      But simplification reduces this to true, using the definitions of List.length
                                                                                                      and interleave_strict.
                                                                                                      
                                                                                                      Subgoal 2:
                                                                                                      
                                                                                                       H0. y <> []
                                                                                                       H1. List.length (interleave_strict [] (List.tl y)) <=
                                                                                                           (List.length [] + List.length (List.tl y))
                                                                                                      |---------------------------------------------------------------------------
                                                                                                       List.length (interleave_strict [] y) <= (List.length [] + List.length y)
                                                                                                      
                                                                                                      But simplification reduces this to true, using the definitions of List.length
                                                                                                      and interleave_strict.
                                                                                                      
                                                                                                      Subgoal 1:
                                                                                                      
                                                                                                       H0. x <> []
                                                                                                       H1. y <> []
                                                                                                       H2. List.length (interleave_strict (List.tl x) (List.tl y)) <=
                                                                                                           (List.length (List.tl x) + List.length (List.tl y))
                                                                                                      |---------------------------------------------------------------------------
                                                                                                       List.length (interleave_strict x y) <= (List.length x + List.length y)
                                                                                                      
                                                                                                      This simplifies, using the definitions of List.length and interleave_strict
                                                                                                      to:
                                                                                                      
                                                                                                      Subgoal 1':
                                                                                                      
                                                                                                       H0. x <> []
                                                                                                       H1. y <> []
                                                                                                       H2. List.length (interleave_strict (List.tl x) (List.tl y)) <=
                                                                                                           (List.length (List.tl x) + List.length (List.tl y))
                                                                                                      |---------------------------------------------------------------------------
                                                                                                       List.length ((List.hd y) :: (interleave_strict (List.tl x) (List.tl y))) <=
                                                                                                       ((1 + List.length (List.tl x)) + List.length (List.tl y))
                                                                                                      
                                                                                                      But simplification reduces this to true, using the definition of List.length.
                                                                                                      
                                                                                                       Rules:
                                                                                                          (:def List.length)
                                                                                                          (:def interleave_strict)
                                                                                                          (:fc List.len_nonnegative)
                                                                                                          (:induct struct list)
                                                                                                      
                                                                                                      
                                                                                                      Proved
                                                                                                      proof
                                                                                                      ground_instances0
                                                                                                      definitions16
                                                                                                      inductions1
                                                                                                      search_time
                                                                                                      0.130s
                                                                                                      Expand
                                                                                                      • start[0.130s, "Goal"]
                                                                                                          List.length (interleave_strict :var_0: :var_1:) <=
                                                                                                          (List.length :var_0: + List.length :var_1:)
                                                                                                      • subproof

                                                                                                        List.length (interleave_strict x y) <= (List.length x + List.length y)
                                                                                                        • start[0.130s, "1"]
                                                                                                            List.length (interleave_strict x y) <= (List.length x + List.length y)
                                                                                                        • induction on (structural* x, y)
                                                                                                          :scheme φ [] []
                                                                                                                  && (x <> [] && φ [] (List.tl x) ==> φ [] x)
                                                                                                                     && (y <> [] && φ (List.tl y) [] ==> φ y [])
                                                                                                                        && (x <> [] && y <> [] && φ (List.tl y) (List.tl x) ==> φ y x)
                                                                                                        • Split (((List.length (interleave_strict [] []) <= (2 * List.length [])
                                                                                                                   && (not
                                                                                                                       (x <> []
                                                                                                                        && List.length (interleave_strict (List.tl x) []) <=
                                                                                                                           (List.length (List.tl x) + List.length []))
                                                                                                                       || List.length (interleave_strict x []) <=
                                                                                                                          (List.length x + List.length [])))
                                                                                                                  && (not
                                                                                                                      (y <> []
                                                                                                                       && List.length (interleave_strict [] (List.tl y)) <=
                                                                                                                          (List.length [] + List.length (List.tl y)))
                                                                                                                      || List.length (interleave_strict [] y) <=
                                                                                                                         (List.length [] + List.length y)))
                                                                                                                 && (not
                                                                                                                     ((x <> [] && y <> [])
                                                                                                                      && List.length (interleave_strict (List.tl x) (List.tl y)) <=
                                                                                                                         (List.length (List.tl x) + List.length (List.tl y)))
                                                                                                                     || List.length … <= …)
                                                                                                                 :cases [List.length (interleave_strict [] []) <= (2 * List.length []);
                                                                                                                         (not (x <> [])
                                                                                                                          || not
                                                                                                                             (List.length (interleave_strict (List.tl x) []) <=
                                                                                                                              (List.length (List.tl x) + List.length [])))
                                                                                                                         || List.length (interleave_strict x []) <=
                                                                                                                            (List.length x + List.length []);
                                                                                                                         (not (y <> [])
                                                                                                                          || not
                                                                                                                             (List.length (interleave_strict [] (List.tl y)) <=
                                                                                                                              (List.length [] + List.length (List.tl y))))
                                                                                                                         || List.length (interleave_strict [] y) <=
                                                                                                                            (List.length [] + List.length y);
                                                                                                                         ((not (x <> []) || not (y <> []))
                                                                                                                          || not
                                                                                                                             (List.length (interleave_strict (List.tl x) (List.tl y))
                                                                                                                              <= (List.length (List.tl x) + List.length (List.tl y))))
                                                                                                                         || List.length (interleave_strict x y) <=
                                                                                                                            (List.length x + List.length y)])
                                                                                                          • subproof
                                                                                                            ((not (x <> []) || not (y <> [])) || not (List.length (interleave_strict (List.tl x) (List.tl y)) <= (List.length (List.tl x) + List.length (List.tl y)))) || List.length (interleave_strict x y) <= (List.length x + List.length y)
                                                                                                            • start[0.126s, "1"]
                                                                                                                ((not (x <> []) || not (y <> []))
                                                                                                                 || not
                                                                                                                    (List.length (interleave_strict (List.tl x) (List.tl y)) <=
                                                                                                                     (List.length (List.tl x) + List.length (List.tl y))))
                                                                                                                || List.length (interleave_strict x y) <= (List.length x + List.length y)
                                                                                                            • simplify
                                                                                                              into
                                                                                                              ((not (x <> []) || not (y <> []))
                                                                                                               || not
                                                                                                                  (List.length (interleave_strict (List.tl x) (List.tl y)) <=
                                                                                                                   (List.length (List.tl x) + List.length (List.tl y))))
                                                                                                              || List.length ((List.hd y) :: (interleave_strict (List.tl x) (List.tl y)))
                                                                                                                 <= ((1 + List.length (List.tl x)) + List.length (List.tl y))
                                                                                                              expansions
                                                                                                              [List.length, List.length, List.length, interleave_strict]
                                                                                                              rewrite_steps
                                                                                                                forward_chaining
                                                                                                                • List.len_nonnegative
                                                                                                                • List.len_nonnegative
                                                                                                                • List.len_nonnegative
                                                                                                                • List.len_nonnegative
                                                                                                                • List.len_nonnegative
                                                                                                                • List.len_nonnegative
                                                                                                                • List.len_nonnegative
                                                                                                                • List.len_nonnegative
                                                                                                                • List.len_nonnegative
                                                                                                                • List.len_nonnegative
                                                                                                                • List.len_nonnegative
                                                                                                                • List.len_nonnegative
                                                                                                                • List.len_nonnegative
                                                                                                                • List.len_nonnegative
                                                                                                                • List.len_nonnegative
                                                                                                                • List.len_nonnegative
                                                                                                                • List.len_nonnegative
                                                                                                                • List.len_nonnegative
                                                                                                                • List.len_nonnegative
                                                                                                              • simplify
                                                                                                                into
                                                                                                                true
                                                                                                                expansions
                                                                                                                List.length
                                                                                                                rewrite_steps
                                                                                                                  forward_chaining
                                                                                                                  • List.len_nonnegative
                                                                                                                  • List.len_nonnegative
                                                                                                                  • List.len_nonnegative
                                                                                                                  • List.len_nonnegative
                                                                                                              • subproof
                                                                                                                (not (y <> []) || not (List.length (interleave_strict [] (List.tl y)) <= (List.length [] + List.length (List.tl y)))) || List.length (interleave_strict [] y) <= (List.length [] + List.length y)
                                                                                                                • start[0.126s, "2"]
                                                                                                                    (not (y <> [])
                                                                                                                     || not
                                                                                                                        (List.length (interleave_strict [] (List.tl y)) <=
                                                                                                                         (List.length [] + List.length (List.tl y))))
                                                                                                                    || List.length (interleave_strict [] y) <= (List.length [] + List.length y)
                                                                                                                • simplify
                                                                                                                  into
                                                                                                                  true
                                                                                                                  expansions
                                                                                                                  [List.length, List.length, List.length, interleave_strict]
                                                                                                                  rewrite_steps
                                                                                                                    forward_chaining
                                                                                                                    • List.len_nonnegative
                                                                                                                    • List.len_nonnegative
                                                                                                                    • List.len_nonnegative
                                                                                                                    • List.len_nonnegative
                                                                                                                    • List.len_nonnegative
                                                                                                                • subproof
                                                                                                                  (not (x <> []) || not (List.length (interleave_strict (List.tl x) []) <= (List.length (List.tl x) + List.length []))) || List.length (interleave_strict x []) <= (List.length x + List.length [])
                                                                                                                  • start[0.126s, "3"]
                                                                                                                      (not (x <> [])
                                                                                                                       || not
                                                                                                                          (List.length (interleave_strict (List.tl x) []) <=
                                                                                                                           (List.length (List.tl x) + List.length [])))
                                                                                                                      || List.length (interleave_strict x []) <= (List.length x + List.length [])
                                                                                                                  • simplify
                                                                                                                    into
                                                                                                                    true
                                                                                                                    expansions
                                                                                                                    [List.length, List.length, List.length, interleave_strict]
                                                                                                                    rewrite_steps
                                                                                                                      forward_chaining
                                                                                                                      • List.len_nonnegative
                                                                                                                      • List.len_nonnegative
                                                                                                                      • List.len_nonnegative
                                                                                                                      • List.len_nonnegative
                                                                                                                      • List.len_nonnegative
                                                                                                                  • subproof
                                                                                                                    List.length (interleave_strict [] []) <= (2 * List.length [])
                                                                                                                    • start[0.126s, "4"]
                                                                                                                        List.length (interleave_strict [] []) <= (2 * List.length [])
                                                                                                                    • simplify
                                                                                                                      into
                                                                                                                      true
                                                                                                                      expansions
                                                                                                                      [List.length, List.length, interleave_strict]
                                                                                                                      rewrite_steps
                                                                                                                        forward_chaining
                                                                                                                        • List.len_nonnegative
                                                                                                                        • List.len_nonnegative

                                                                                                                Imandra was able to prove the property using both flavors of structural induction, but we can see that the proof using the additive flavor was shorter. Multiplicative schemes will often result in longer proofs than additive schemes, and thus Imandra uses the additive flavor by default when [@@induct structural ...] is used.