Simplification

At the heart of Imandra is a powerful symbolic simplifier and partial evaluator. The simplifier is integrated with the inductive waterfall (e.g., [@@auto]), and is the main way in which previously proved lemmas are used during proofs, through the automatic application of rules. The simplifier can also be used as a pre-processing step before unrolling, via the [@@simp] attribute.

As the name suggests, simplification is a process that attempts to transform a formula into a "simpler" form, bringing the salient features of a formula or conjecture to the surface. Simplification can also prove goals by reducing them to true, and refute them by reducing them to false.

Notably, because the symbolic evaluation semantics of the simplifier operate on a compact digraph representation of formulas and function definitions, simplification can be thought as having memoized semantics for free.

We can see an example of this by using the following naive recursive version of the fibonacci function:

In [1]:
let rec fib n =
  if n <= 1 then
    1
  else
    fib (n-1) + fib (n-2)
Out[1]:
val fib : int -> Z.t = <fun>
termination proof

Termination proof

call `fib (n - 1)` from `fib n`
originalfib n
subfib (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)]
proof
detailed proof
ground_instances1
definitions0
inductions0
search_time
0.028s
details
Expand
smt_stats
num checks3
arith assert lower8
arith pivots2
rlimit count2058
mk clause5
datatype occurs check2
mk bool var20
arith assert upper3
decisions2
arith add rows3
propagations2
conflicts2
arith fixed eqs2
datatype accessor ax2
arith conflicts1
num allocs958751259
final checks1
added eqs6
del clause5
arith eq adapter2
memory17.960000
max memory17.960000
Expand
  • start[0.028s]
      not (n <= 1)
      && (if n >= 0 then n else 0) >= 0
         && (if (n - 1) >= 0 then n - 1 else 0) >= 0
      ==> (n - 1) <= 1 && (n - 1) <= 1
          || 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) && (if n >= 0 then n else 0) >= 0)
      && (if n >= 1 then -1 + n else 0) >= 0)
     || n <= 2)
    || 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_1470 1) (+ (- 1) n_1470) 0))
                          (|Ord…
        expansions
        • unsat
          (let ((a!1 (not (= n_1470 (ite (>= n_1470 0) n_1470 0))))
                (a!2 (+ n_1470 (* (- 1) (ite (>= n_1…

        call `fib (n - 2)` from `fib n`
        originalfib n
        subfib (n - 2)
        original ordinalOrdinal.Int (if n >= 0 then n else 0)
        sub ordinalOrdinal.Int (if (n - 2) >= 0 then n - 2 else 0)
        path[not (n <= 1)]
        proof
        detailed proof
        ground_instances1
        definitions0
        inductions0
        search_time
        0.104s
        details
        Expand
        smt_stats
        num checks3
        arith assert lower8
        arith pivots2
        rlimit count1029
        mk clause5
        datatype occurs check2
        mk bool var20
        arith assert upper3
        decisions2
        arith add rows3
        propagations2
        conflicts2
        arith fixed eqs2
        datatype accessor ax2
        arith conflicts1
        num allocs930097021
        final checks1
        added eqs6
        del clause5
        arith eq adapter2
        memory15.040000
        max memory17.870000
        Expand
        • start[0.104s]
            not (n <= 1)
            && (if n >= 0 then n else 0) >= 0
               && (if (n - 2) >= 0 then n - 2 else 0) >= 0
            ==> (n - 2) <= 1 && (n - 2) <= 1
                || Ordinal.<< (Ordinal.Int (if (n - 2) >= 0 then n - 2 else 0))
                   (Ordinal.Int (if n >= 0 then n else 0))
        • simplify
          into
          (not
           ((not (n <= 1) && (if n >= 0 then n else 0) >= 0)
            && (if n >= 2 then -2 + n else 0) >= 0)
           || n <= 3)
          || Ordinal.<< (Ordinal.Int (if n >= 2 then -2 + 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_1470 2) (+ (- 2) n_1470) 0))
                                (|Ord…
              expansions
              • unsat
                (let ((a!1 (not (= n_1470 (ite (>= n_1470 0) n_1470 0))))
                      (a!2 (+ n_1470 (* (- 1) (ite (>= n_1…

              If we try to use Imandra's simplification to search for a solution for fib 200, Imandra comes back to us with a solution immediately:

              In [2]:
              #check_models false;;
              instance (fun x -> x = fib 200) [@@simp];;
              #check_models true;;
              
              Out[2]:
              - : Z.t -> bool = <fun>
              module CX : sig val x : int end
              
              Instance (after 0 steps, 0.113s):
               let (x : int) = 453973694165307953197296969697410619233826
              
              Instance
              proof attempt
              ground_instances0
              definitions201
              inductions0
              search_time
              0.113s
              details
              Expand
              smt_stats
              eliminated vars1
              rlimit count7759
              mk bool var5
              num allocs1115600185
              memory15.810000
              max memory17.960000
              Expand
              • start[0.113s] :var_0: = fib 200
              • simplify

                into
                x = 453973694165307953197296969697410619233826
                expansions
                [fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib,
                 fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib,
                 fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib,
                 fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib,
                 fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib,
                 fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib,
                 fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib,
                 fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib,
                 fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib,
                 fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib,
                 fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib,
                 fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib,
                 fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib, fib,
                 fib, fib, fib, fib, fib, fib]
                rewrite_steps
                  forward_chaining
                  • Sat (Some let (x : int) = 453973694165307953197296969697410619233826 )

                  If, however, we tried to use normal OCaml evaluation to compute fib 200, OCaml would take over 10 minutes in order to come back with a response (the #check_models false command here is used to tell Imandra not to check the instance Imandra computed using OCaml evaluation, as that requires the expensive computation of fib 200 via standard OCaml evaluation, which is not memoized).

                  Now that we know what simplification does, let's learn about how to influence it using rewrite and forward chaining rules.

                  Rewrite Rules

                  A rewrite rule is a theorem of the form

                  h_1 && ... && h_k ==> lhs = rhs

                  which Imandra can use in further proofs to replace terms that match with lhs (the "left hand side") with the appropriate instantiation of rhs (the "right hand side"), provided that the instantiations of the hypotheses can be established. Observe that rewrite rules are both conditional (requiring in general the establishment of hypotheses) and directed (replacing lhs with rhs). The lhs is also called the "pattern" of the rule.

                  An enabled rewrite rule causes Imandra to look for matches of the lhs, replacing the matched term with the (suitably instantiated) rhs, provided that Imandra can establish ("relieve") the (suitably instantiated) hypotheses of the rule.

                  For example, consider the lemma rev_len below. This lemma expresses the fact that the length of a list x is equal to the length of List.rev x, i.e., if we reverse a list, we end up with a list of the same length. This rule is unconditional: it has no hypotheses. Thus, it will always be able to fire on terms that match its left-hand side. Notice that Imandra uses a previously defined rewrite rule in order to prove this lemma! The lemma rev_len would make an excellent rewrite rule, so we use the [@@rw] annotation to install it:

                  In [3]:
                  lemma rev_len x =
                    List.length (List.rev x) = List.length x
                  [@@auto] [@@rw]
                  
                  Out[3]:
                  val rev_len : 'a list -> bool = <fun>
                  Goal:
                  
                  List.length (List.rev x) = List.length x.
                  
                  1 nontautological subgoal.
                  
                  Subgoal 1:
                  
                  |---------------------------------------------------------------------------
                   List.length (List.rev x) = List.length x
                  
                  
                  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.length.
                  
                  Induction scheme:
                  
                   (x = [] ==> φ x) && (not (x = []) && φ (List.tl x) ==> φ x).
                  
                  2 nontautological subgoals.
                  
                  Subgoal 1.2:
                  
                   H0. x = []
                  |---------------------------------------------------------------------------
                   List.length (List.rev x) = List.length x
                  
                  But simplification reduces this to true, using the definitions of List.length
                  and List.rev.
                  
                  Subgoal 1.1:
                  
                   H0. not (x = [])
                   H1. List.length (List.rev (List.tl x)) = List.length (List.tl x)
                  |---------------------------------------------------------------------------
                   List.length (List.rev x) = List.length x
                  
                  This simplifies, using the definitions of List.length and List.rev to:
                  
                  Subgoal 1.1':
                  
                   H0. x <> []
                   H1. List.length (List.rev (List.tl x)) = List.length (List.tl x)
                  |---------------------------------------------------------------------------
                   List.length (List.append (List.rev (List.tl x)) [List.hd x]) =
                   1 + List.length (List.tl x)
                  
                  
                  We can eliminate destructors by the following substitution:
                   x -> x1 :: x2
                  
                  This produces the modified subgoal:
                  
                  Subgoal 1.1'':
                  
                   H0. List.length (List.rev x2) = List.length x2
                  |---------------------------------------------------------------------------
                   List.length (List.append (List.rev x2) [x1]) = 1 + List.length x2
                  
                  
                  Cross-fertilizing with:
                  
                   List.length (List.rev x2) = List.length x2
                  
                  This produces the modified subgoal:
                  
                  Subgoal 1.1''':
                  
                  |---------------------------------------------------------------------------
                   List.length (List.append (List.rev x2) [x1]) = 1 + List.length (List.rev x2)
                  
                  
                  Candidates for generalization:
                  
                   List.rev x2
                  
                  This produces the modified subgoal:
                  
                  Subgoal 1.1'''':
                  
                  |---------------------------------------------------------------------------
                   List.length (List.append gen_1 [x1]) = 1 + List.length gen_1
                  
                  
                  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.append.
                  
                  Induction scheme:
                  
                   (gen_1 = [] ==> φ gen_1 x1)
                   && (not (gen_1 = []) && φ (List.tl gen_1) x1 ==> φ gen_1 x1).
                  
                  2 nontautological subgoals.
                  
                  Subgoal 1.1''''.2:
                  
                   H0. gen_1 = []
                  |---------------------------------------------------------------------------
                   List.length (List.append gen_1 [x1]) = 1 + List.length gen_1
                  
                  But simplification reduces this to true, using the definitions of List.append
                  and List.length.
                  
                  Subgoal 1.1''''.1:
                  
                   H0. not (gen_1 = [])
                   H1. List.length (List.append (List.tl gen_1) [x1]) =
                       1 + List.length (List.tl gen_1)
                  |---------------------------------------------------------------------------
                   List.length (List.append gen_1 [x1]) = 1 + List.length gen_1
                  
                  But simplification reduces this to true, using the definitions of List.append
                  and List.length.
                  
                   Rules:
                      (:def List.append)
                      (:def List.length)
                      (:def List.rev)
                      (:fc List.len_nonnegative)
                      (:induct List.append)
                      (:induct List.length)
                  
                  
                  Proved
                  proof
                  ground_instances0
                  definitions11
                  inductions2
                  search_time
                  1.051s
                  Expand
                  • start[1.051s, "Goal"] List.length (List.rev :var_0:) = List.length :var_0:
                  • subproof

                    List.length (List.rev x) = List.length x
                    • start[1.051s, "1"] List.length (List.rev x) = List.length x
                    • induction on (functional )
                      :scheme (x = [] ==> φ x) && (not (x = []) && φ (List.tl x) ==> φ x)
                    • Split ((not (x = []) || List.length (List.rev x) = List.length x)
                             && (not
                                 (not (x = [])
                                  && List.length (List.rev (List.tl x)) = List.length (List.tl x))
                                 || List.length (List.rev x) = List.length x)
                             :cases [not (x = []) || List.length (List.rev x) = List.length x;
                                     (x = []
                                      || not
                                         (List.length (List.rev (List.tl x)) =
                                          List.length (List.tl x)))
                                     || List.length (List.rev x) = List.length x])
                      • subproof
                        (x = [] || not (List.length (List.rev (List.tl x)) = List.length (List.tl x))) || List.length (List.rev x) = List.length x
                        • start[0.981s, "1.1"]
                            (x = []
                             || not (List.length (List.rev (List.tl x)) = List.length (List.tl x)))
                            || List.length (List.rev x) = List.length x
                        • simplify
                          into
                          (x = [] || not (List.length (List.rev (List.tl x)) = List.length (List.tl x)))
                          || List.length (List.append (List.rev (List.tl x)) [List.hd x]) =
                             1 + List.length (List.tl x)
                          expansions
                          [List.length, List.rev]
                          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
                          • Elim_destructor (:cstor :: :replace x1 :: x2 :context [])
                          • Generalize (List.length (List.append (List.rev x2) [x1]) =
                                        1 + List.length (List.rev x2) :as (gen_1 : sko_ty_0 list))
                          • induction on (functional )
                            :scheme (gen_1 = [] ==> φ gen_1 x1)
                                    && (not (gen_1 = []) && φ (List.tl gen_1) x1 ==> φ gen_1 x1)
                          • Split ((not (gen_1 = [])
                                    || List.length (List.append gen_1 [x1]) = 1 + List.length gen_1)
                                   && (not
                                       (not (gen_1 = [])
                                        && List.length (List.append (List.tl gen_1) [x1]) =
                                           1 + List.length (List.tl gen_1))
                                       || List.length (List.append gen_1 [x1]) = 1 + List.length gen_1)
                                   :cases [not (gen_1 = [])
                                           || List.length (List.append gen_1 [x1]) =
                                              1 + List.length gen_1;
                                           (gen_1 = []
                                            || not
                                               (List.length (List.append (List.tl gen_1) [x1]) =
                                                1 + List.length (List.tl gen_1)))
                                           || List.length (List.append gen_1 [x1]) =
                                              1 + List.length gen_1])
                            • Subproof
                            • Subproof
                        • subproof
                          not (x = []) || List.length (List.rev x) = List.length x
                          • start[0.981s, "1.2"] not (x = []) || List.length (List.rev x) = List.length x
                          • simplify
                            into
                            true
                            expansions
                            [List.length, List.length, List.rev]
                            rewrite_steps
                              forward_chaining
                              • List.len_nonnegative
                              • List.len_nonnegative

                      With this rule installed and enabled, if Imandra's simplifier encounters a term of the form List.length (List.rev <term>), it will replace it with the simpler form List.length <term>.

                      Both the hypotheses and rhs can be omitted, in which case Imandra will default them to true. That is, h_1 && ... && h_k ==> lhs is equivalent to h_1 && h_k ==> lhs = true and lhs = rhs is equal to true ==> lhs = rhs.

                      Imandra's rewriting is:

                      • conditional: rewrite rules may contain conditions (hypotheses), and eligible rules are only applied when their hypotheses are established. Once the pattern of a rule has been matched, Imandra uses backward-chaining ("backchaining") to relieve the rule's hypotheses, recursively attempting to simplify them to true modulo the current simplification context. This is important to keep in mind when developing your theories: rewrite rules will not fire unless Imandra can simplify their instantiated hypotheses to true.

                      • oriented: given a rule whose conclusion is of the form lhs = rhs, rewriting happens by replacing the (instantiated) lhs with the (instantiated) rhs.

                      When adding a new rewrite rule, users should take care to orient the equality so that rhs is simpler or more canonical than lhs. If it's not clear what it means for an rhs to be "better" than the lhs, e.g., in the case of the proof for the associativity of append x @ (y @ z) = (x @ y) @ z, a canonical form should typically be chosen (e.g., associating to the left in this case) and kept in mind for further rules.

                      By default, the lhs must contain all the top-level variables of the theorem (i.e. the arguments to the lambda term representing the goal). There is an exception to this rule: if the lhs does not contain all the variables of the theorem but the rule hypotheses have subterms containing the remaining free variables, these terms can be annotated with [@trigger rw], signaling Imandra that the annotated terms should be used to complete the matching.

                      It's helpful to see an example where the use of [@trigger rw] is necessary. Let's first define a subset function on lists:

                      In [4]:
                      let rec subset x y =
                        match x with
                        | [] -> true
                        | x :: xs ->
                          if List.mem x y then subset xs y
                          else false
                      
                      Out[4]:
                      val subset : 'a list -> 'a list -> bool = <fun>
                      
                      termination proof

                      Termination proof

                      call `subset (List.tl x) y` from `subset x y`
                      originalsubset x y
                      subsubset (List.tl x) y
                      original ordinalOrdinal.Int (Ordinal.count x)
                      sub ordinalOrdinal.Int (Ordinal.count (List.tl x))
                      path[List.mem (List.hd x) y && not (x = [])]
                      proof
                      detailed proof
                      ground_instances4
                      definitions0
                      inductions0
                      search_time
                      0.020s
                      details
                      Expand
                      smt_stats
                      num checks9
                      arith assert lower9
                      arith pivots5
                      rlimit count2487
                      mk clause10
                      datatype occurs check35
                      mk bool var78
                      arith assert upper6
                      datatype splits6
                      decisions18
                      arith add rows7
                      arith bound prop1
                      propagations9
                      conflicts10
                      arith fixed eqs5
                      datatype accessor ax6
                      arith conflicts1
                      arith assert diseq1
                      datatype constructor ax14
                      num allocs2410432096
                      final checks9
                      added eqs48
                      del clause4
                      arith eq adapter5
                      memory20.360000
                      max memory35.210000
                      Expand
                      • start[0.020s]
                          List.mem (List.hd x) y
                          && not (x = []) && Ordinal.count x >= 0 && Ordinal.count (List.tl x) >= 0
                          ==> not (List.mem (List.hd (List.tl x)) y && not (List.tl x = []))
                              || Ordinal.<< (Ordinal.Int (Ordinal.count (List.tl x)))
                                 (Ordinal.Int (Ordinal.count x))
                      • simplify
                        into
                        (not
                         (((List.mem (List.hd x) y && not (x = [])) && Ordinal.count x >= 0)
                          && Ordinal.count (List.tl x) >= 0)
                         || not (List.mem (List.hd (List.tl x)) y && not (List.tl x = [])))
                        || 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`_1698| (|get.::.1_1676| …
                            expansions
                            • unroll
                              expr
                              (|List.mem_1682| (|get.::.0_1675| (|get.::.1_1676| x_1687)) y_1688)
                              expansions
                              • unroll
                                expr
                                (|count_`ty_0 list`_1698| (|get.::.1_1676| x_1687))
                                expansions
                                • unroll
                                  expr
                                  (|count_`ty_0 list`_1698| x_1687)
                                  expansions
                                  • unsat
                                    (let ((a!1 (= (|count_`ty_0 list`_1698| x_1687)
                                                  (+ 1 (|count_`ty_0 list`_1698| (|get.:…

                                  Let's now suppose that we want to verify the transitivity of subset:

                                  In [5]:
                                  #max_induct 1;;
                                  verify (fun x y z -> subset x y && subset y z ==> subset x z) [@@auto]
                                  #max_induct 3;;
                                  
                                  Out[5]:
                                  - : 'a list -> 'a list -> 'a list -> bool = <fun>
                                  Goal:
                                  
                                  subset x y && subset y z ==> subset x z.
                                  
                                  1 nontautological subgoal.
                                  
                                  Subgoal 1:
                                  
                                   H0. subset x y
                                   H1. subset y z
                                  |---------------------------------------------------------------------------
                                   subset x 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 subset.
                                  
                                  Induction scheme:
                                  
                                   (not (List.mem (List.hd x) y && not (x = [])) ==> φ z y x)
                                   && (not (x = []) && List.mem (List.hd x) y && φ z y (List.tl x)
                                       ==> φ z y x).
                                  
                                  2 nontautological subgoals.
                                  
                                  Subgoal 1.2:
                                  
                                   H0. subset x y
                                   H1. subset y z
                                  |---------------------------------------------------------------------------
                                   C0. List.mem (List.hd x) y && not (x = [])
                                   C1. subset x z
                                  
                                  This simplifies, using the definition of subset to the following 2 subgoals:
                                  
                                  Subgoal 1.2.2:
                                  
                                   H0. x = []
                                   H1. subset y z
                                  |---------------------------------------------------------------------------
                                   C0. List.mem (List.hd x) y
                                   C1. subset x z
                                  
                                  But simplification reduces this to true, using the definition of subset.
                                  
                                  Subgoal 1.2.1:
                                  
                                   H0. subset y z
                                   H1. x = []
                                   H2. List.mem (List.hd x) y
                                  |---------------------------------------------------------------------------
                                   subset x z
                                  
                                  But simplification reduces this to true, using the definition of subset.
                                  
                                  Subgoal 1.1:
                                  
                                   H0. not (x = [])
                                   H1. List.mem (List.hd x) y
                                   H2. subset (List.tl x) y && subset y z ==> subset (List.tl x) z
                                   H3. subset x y
                                   H4. subset y z
                                  |---------------------------------------------------------------------------
                                   subset x z
                                  
                                  This simplifies, using the definition of subset to:
                                  
                                  Subgoal 1.1':
                                  
                                   H0. x <> []
                                   H1. List.mem (List.hd x) y
                                   H2. subset (List.tl x) z
                                   H3. subset (List.tl x) y
                                   H4. subset y z
                                  |---------------------------------------------------------------------------
                                   List.mem (List.hd x) z
                                  
                                  
                                  We can eliminate destructors by the following substitution:
                                   x -> x1 :: x2
                                  
                                  This produces the modified subgoal:
                                  
                                  Subgoal 1.1'':
                                  
                                   H0. List.mem x1 y
                                   H1. subset x2 z
                                   H2. subset x2 y
                                   H3. subset y z
                                  |---------------------------------------------------------------------------
                                   List.mem x1 z
                                  
                                  
                                  Must try induction.
                                  
                                   Aborting proof attempt for _verify_target.
                                  
                                   Rules:
                                      (:def subset)
                                      (:induct subset)
                                  
                                  Checkpoints:
                                  
                                   H0. List.mem x1 y
                                   H1. subset x2 z
                                   H2. subset x2 y
                                   H3. subset y z
                                  |---------------------------------------------------------------------------
                                   List.mem x1 z
                                  
                                  Error[/server]: Maximum induction depth reached (1). You can set this with #max_induct.
                                  

                                  It looks like Imandra needs an additional lemma in order to prove this. By inspecting the checkpoint, it looks like all we need is a rule relating subset and List.mem. Let's attempt to prove it:

                                  In [6]:
                                  lemma mem_subset x y z =
                                    List.mem x y && subset y z ==> List.mem x z
                                  [@@auto] [@@rewrite]
                                  
                                  Out[6]:
                                  val mem_subset : 'a -> 'a list -> 'a list -> bool = <fun>
                                  Goal:
                                  
                                  List.mem x y && subset y z ==> List.mem x z.
                                  
                                  1 nontautological subgoal.
                                  
                                  Subgoal 1:
                                  
                                   H0. List.mem x y
                                   H1. subset y z
                                  |---------------------------------------------------------------------------
                                   List.mem x z
                                  
                                  
                                  Must try induction.
                                  
                                  The recursive terms in the conjecture suggest 3 inductions.
                                  Subsumption and merging reduces this to 2.
                                  
                                  However, scheme scoring gives us a clear winner.
                                  We shall induct according to a scheme derived from List.mem.
                                  
                                  Induction scheme:
                                  
                                   (y = [] ==> φ z y x) && (not (y = []) && φ z (List.tl y) x ==> φ z y x).
                                  
                                  2 nontautological subgoals.
                                  
                                  Subgoal 1.2:
                                  
                                   H0. y = []
                                   H1. List.mem x y
                                   H2. subset y z
                                  |---------------------------------------------------------------------------
                                   List.mem x z
                                  
                                  But simplification reduces this to true, using the definitions of List.mem
                                  and subset.
                                  
                                  Subgoal 1.1:
                                  
                                   H0. not (y = [])
                                   H1. List.mem x (List.tl y) && subset (List.tl y) z ==> List.mem x z
                                   H2. List.mem x y
                                   H3. subset y z
                                  |---------------------------------------------------------------------------
                                   List.mem x z
                                  
                                  But simplification reduces this to true, using the definitions of List.mem
                                  and subset.
                                  
                                   Rules:
                                      (:def List.mem)
                                      (:def subset)
                                      (:induct List.mem)
                                  
                                  File "jupyter cell 6", line 1, characters 6-91:
                                  Error: in rewrite rule,
                                  variable (y : 'a list) does not occur in left-hand side of the rule
                                  or in `[@trigger rw]` terms
                                  See https://docs.imandra.ai/imandra-docs/notebooks/verification-simplification/#Rewrite-Rules
                                  
                                  Proved
                                  proof
                                  ground_instances0
                                  definitions4
                                  inductions1
                                  search_time
                                  0.333s
                                  Expand
                                  • start[0.333s, "Goal"]
                                      List.mem :var_0: :var_1: && subset :var_1: :var_2:
                                      ==> List.mem :var_0: :var_2:
                                  • subproof

                                    (not (List.mem x y) || not (subset y z)) || List.mem x z
                                    • start[0.332s, "1"] (not (List.mem x y) || not (subset y z)) || List.mem x z
                                    • induction on (functional )
                                      :scheme (y = [] ==> φ z y x)
                                              && (not (y = []) && φ z (List.tl y) x ==> φ z y x)
                                    • Split ((((not (y = []) || not (List.mem x y)) || not (subset y z))
                                              || List.mem x z)
                                             && (((not
                                                   (not (y = [])
                                                    && ((not (List.mem x (List.tl y)) || not (subset (List.tl y) z))
                                                        || List.mem x z))
                                                   || not (List.mem x y))
                                                  || not (subset y z))
                                                 || List.mem x z)
                                             :cases [((not (y = []) || not (List.mem x y)) || not (subset y z))
                                                     || List.mem x z;
                                                     (((y = []
                                                        || not
                                                           (not (List.mem x (List.tl y) && subset (List.tl y) z)
                                                            || List.mem x z))
                                                       || not (List.mem x y))
                                                      || not (subset y z))
                                                     || List.mem x z])
                                      • subproof
                                        (((y = [] || not (not (List.mem x (List.tl y) && subset (List.tl y) z) || List.mem x z)) || not (List.mem x y)) || not (subset y z)) || List.mem x z
                                        • start[0.102s, "1.1"]
                                            (((y = []
                                               || not
                                                  (not (List.mem x (List.tl y) && subset (List.tl y) z) || List.mem x z))
                                              || not (List.mem x y))
                                             || not (subset y z))
                                            || List.mem x z
                                        • simplify
                                          into
                                          true
                                          expansions
                                          [List.mem, subset]
                                          rewrite_steps
                                            forward_chaining
                                          • subproof
                                            ((not (y = []) || not (List.mem x y)) || not (subset y z)) || List.mem x z
                                            • start[0.102s, "1.2"]
                                                ((not (y = []) || not (List.mem x y)) || not (subset y z)) || List.mem x z
                                            • simplify
                                              into
                                              true
                                              expansions
                                              [List.mem, subset]
                                              rewrite_steps
                                                forward_chaining

                                          While Imandra was successful in proving this lemma, it raised an error while trying to turn this lemma into a rewrite rule. As Imandra tells us, this is because the free variable y does not appear in the lhs term List.mem x z. If we, however, annotate the subset y z term with the appropriate [@trigger rw] attribute, Imandra can then successfully turn this term into a valid rewrite rule:

                                          In [7]:
                                          lemma mem_subset x y z =
                                            List.mem x y && (subset y z [@trigger rw]) ==> List.mem x z
                                          [@@auto] [@@rewrite]
                                          
                                          Out[7]:
                                          val mem_subset : 'a -> 'a list -> 'a list -> bool = <fun>
                                          Goal:
                                          
                                          List.mem x y && subset y z ==> List.mem x z.
                                          
                                          1 nontautological subgoal.
                                          
                                          Subgoal 1:
                                          
                                           H0. List.mem x y
                                           H1. subset y z
                                          |---------------------------------------------------------------------------
                                           List.mem x z
                                          
                                          
                                          Must try induction.
                                          
                                          The recursive terms in the conjecture suggest 3 inductions.
                                          Subsumption and merging reduces this to 2.
                                          
                                          However, scheme scoring gives us a clear winner.
                                          We shall induct according to a scheme derived from List.mem.
                                          
                                          Induction scheme:
                                          
                                           (y = [] ==> φ z y x) && (not (y = []) && φ z (List.tl y) x ==> φ z y x).
                                          
                                          2 nontautological subgoals.
                                          
                                          Subgoal 1.2:
                                          
                                           H0. y = []
                                           H1. List.mem x y
                                           H2. subset y z
                                          |---------------------------------------------------------------------------
                                           List.mem x z
                                          
                                          But simplification reduces this to true, using the definitions of List.mem
                                          and subset.
                                          
                                          Subgoal 1.1:
                                          
                                           H0. not (y = [])
                                           H1. List.mem x (List.tl y) && subset (List.tl y) z ==> List.mem x z
                                           H2. List.mem x y
                                           H3. subset y z
                                          |---------------------------------------------------------------------------
                                           List.mem x z
                                          
                                          But simplification reduces this to true, using the definitions of List.mem
                                          and subset.
                                          
                                           Rules:
                                              (:def List.mem)
                                              (:def subset)
                                              (:induct List.mem)
                                          
                                          
                                          Proved
                                          proof
                                          ground_instances0
                                          definitions4
                                          inductions1
                                          search_time
                                          0.306s
                                          Expand
                                          • start[0.306s, "Goal"]
                                              List.mem :var_0: :var_1: && subset :var_1: :var_2:
                                              ==> List.mem :var_0: :var_2:
                                          • subproof

                                            (not (List.mem x y) || not (subset y z)) || List.mem x z
                                            • start[0.306s, "1"] (not (List.mem x y) || not (subset y z)) || List.mem x z
                                            • induction on (functional )
                                              :scheme (y = [] ==> φ z y x)
                                                      && (not (y = []) && φ z (List.tl y) x ==> φ z y x)
                                            • Split ((((not (y = []) || not (List.mem x y)) || not (subset y z))
                                                      || List.mem x z)
                                                     && (((not
                                                           (not (y = [])
                                                            && ((not (List.mem x (List.tl y)) || not (subset (List.tl y) z))
                                                                || List.mem x z))
                                                           || not (List.mem x y))
                                                          || not (subset y z))
                                                         || List.mem x z)
                                                     :cases [((not (y = []) || not (List.mem x y)) || not (subset y z))
                                                             || List.mem x z;
                                                             (((y = []
                                                                || not
                                                                   (not (List.mem x (List.tl y) && subset (List.tl y) z)
                                                                    || List.mem x z))
                                                               || not (List.mem x y))
                                                              || not (subset y z))
                                                             || List.mem x z])
                                              • subproof
                                                (((y = [] || not (not (List.mem x (List.tl y) && subset (List.tl y) z) || List.mem x z)) || not (List.mem x y)) || not (subset y z)) || List.mem x z
                                                • start[0.201s, "1.1"]
                                                    (((y = []
                                                       || not
                                                          (not (List.mem x (List.tl y) && subset (List.tl y) z) || List.mem x z))
                                                      || not (List.mem x y))
                                                     || not (subset y z))
                                                    || List.mem x z
                                                • simplify
                                                  into
                                                  true
                                                  expansions
                                                  [List.mem, subset]
                                                  rewrite_steps
                                                    forward_chaining
                                                  • subproof
                                                    ((not (y = []) || not (List.mem x y)) || not (subset y z)) || List.mem x z
                                                    • start[0.201s, "1.2"]
                                                        ((not (y = []) || not (List.mem x y)) || not (subset y z)) || List.mem x z
                                                    • simplify
                                                      into
                                                      true
                                                      expansions
                                                      [List.mem, subset]
                                                      rewrite_steps
                                                        forward_chaining

                                                  And finally, let's verify that the rewrite rule can indeed match as we expect:

                                                  In [8]:
                                                  verify (fun x y z -> subset x y && subset y z ==> subset x z) [@@auto]
                                                  
                                                  Out[8]:
                                                  - : 'a list -> 'a list -> 'a list -> bool = <fun>
                                                  Goal:
                                                  
                                                  subset x y && subset y z ==> subset x z.
                                                  
                                                  1 nontautological subgoal.
                                                  
                                                  Subgoal 1:
                                                  
                                                   H0. subset x y
                                                   H1. subset y z
                                                  |---------------------------------------------------------------------------
                                                   subset x 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 subset.
                                                  
                                                  Induction scheme:
                                                  
                                                   (not (List.mem (List.hd x) y && not (x = [])) ==> φ z y x)
                                                   && (not (x = []) && List.mem (List.hd x) y && φ z y (List.tl x)
                                                       ==> φ z y x).
                                                  
                                                  2 nontautological subgoals.
                                                  
                                                  Subgoal 1.2:
                                                  
                                                   H0. subset x y
                                                   H1. subset y z
                                                  |---------------------------------------------------------------------------
                                                   C0. List.mem (List.hd x) y && not (x = [])
                                                   C1. subset x z
                                                  
                                                  This simplifies, using the definition of subset to the following 2 subgoals:
                                                  
                                                  Subgoal 1.2.2:
                                                  
                                                   H0. x = []
                                                   H1. subset y z
                                                  |---------------------------------------------------------------------------
                                                   C0. List.mem (List.hd x) y
                                                   C1. subset x z
                                                  
                                                  But simplification reduces this to true, using the definition of subset.
                                                  
                                                  Subgoal 1.2.1:
                                                  
                                                   H0. subset y z
                                                   H1. x = []
                                                   H2. List.mem (List.hd x) y
                                                  |---------------------------------------------------------------------------
                                                   subset x z
                                                  
                                                  But simplification reduces this to true, using the definition of subset.
                                                  
                                                  Subgoal 1.1:
                                                  
                                                   H0. not (x = [])
                                                   H1. List.mem (List.hd x) y
                                                   H2. subset (List.tl x) y && subset y z ==> subset (List.tl x) z
                                                   H3. subset x y
                                                   H4. subset y z
                                                  |---------------------------------------------------------------------------
                                                   subset x z
                                                  
                                                  But simplification reduces this to true, using the definition of subset, and
                                                  the rewrite rule mem_subset.
                                                  
                                                   Rules:
                                                      (:def subset)
                                                      (:rw mem_subset)
                                                      (:induct subset)
                                                  
                                                  
                                                  Proved
                                                  proof
                                                  ground_instances0
                                                  definitions6
                                                  inductions1
                                                  search_time
                                                  0.477s
                                                  Expand
                                                  • start[0.477s, "Goal"]
                                                      subset :var_0: :var_1: && subset :var_1: :var_2: ==> subset :var_0: :var_2:
                                                  • subproof

                                                    (not (subset x y) || not (subset y z)) || subset x z
                                                    • start[0.477s, "1"] (not (subset x y) || not (subset y z)) || subset x z
                                                    • induction on (functional )
                                                      :scheme (not (List.mem (List.hd x) y && not (x = [])) ==> φ z y x)
                                                              && (not (x = []) && List.mem (List.hd x) y && φ z y (List.tl x)
                                                                  ==> φ z y x)
                                                    • Split ((((List.mem (List.hd x) y && not (x = []) || not (subset x y))
                                                               || not (subset y z))
                                                              || subset x z)
                                                             && (((not
                                                                   ((not (x = []) && List.mem (List.hd x) y)
                                                                    && ((not (subset (List.tl x) y) || not (subset y z))
                                                                        || subset (List.tl x) z))
                                                                   || not (subset x y))
                                                                  || not (subset y z))
                                                                 || subset x z)
                                                             :cases [((not (subset x y) || not (subset y z))
                                                                      || List.mem (List.hd x) y && not (x = []))
                                                                     || subset x z;
                                                                     ((((x = [] || not (List.mem (List.hd x) y))
                                                                        || not
                                                                           (not (subset (List.tl x) y && subset y z)
                                                                            || subset (List.tl x) z))
                                                                       || not (subset x y))
                                                                      || not (subset y z))
                                                                     || subset x z])
                                                      • subproof
                                                        ((((x = [] || not (List.mem (List.hd x) y)) || not (not (subset (List.tl x) y && subset y z) || subset (List.tl x) z)) || not (subset x y)) || not (subset y z)) || subset x z
                                                        • start[0.316s, "1.1"]
                                                            ((((x = [] || not (List.mem (List.hd x) y))
                                                               || not
                                                                  (not (subset (List.tl x) y && subset y z) || subset (List.tl x) z))
                                                              || not (subset x y))
                                                             || not (subset y z))
                                                            || subset x z
                                                        • simplify
                                                          into
                                                          true
                                                          expansions
                                                          [subset, subset]
                                                          rewrite_steps
                                                          mem_subset
                                                          forward_chaining
                                                        • subproof
                                                          ((not (subset x y) || not (subset y z)) || List.mem (List.hd x) y && not (x = [])) || subset x z
                                                          • start[0.316s, "1.2"]
                                                              ((not (subset x y) || not (subset y z))
                                                               || List.mem (List.hd x) y && not (x = []))
                                                              || subset x z
                                                          • simplify
                                                            into
                                                            (((not (x = []) || not (subset y z)) || List.mem (List.hd x) y) || subset x z)
                                                            && (((not (subset y z) || not (x = [])) || not (List.mem (List.hd x) y))
                                                                || subset x z)
                                                            expansions
                                                            [subset, subset]
                                                            rewrite_steps
                                                              forward_chaining
                                                                • Subproof
                                                                • Subproof

                                                        Permutative Restriction

                                                        The @@permutative annotation applies only to rewrite rules and is used to restrict the rule so that it will only apply if the instantiated rhs is lexicographically smaller than the matched lhs. This restriction can be particularly useful in order to break out of infinite rewrite loops while trying to "canonicalize" a form, for example distributing the "simplest" terms to the left.

                                                        Let's say we want to prove the commutativity of Peano_nat.plus and install it as a rewrite rule:

                                                        In [9]:
                                                        lemma comm_plus x y =
                                                          Peano_nat.(plus x y = plus y x)
                                                         [@@auto] [@@rw] [@@permutative]
                                                        
                                                        Out[9]:
                                                        val comm_plus : Peano_nat.t -> Peano_nat.t -> bool = <fun>
                                                        Goal:
                                                        
                                                        Peano_nat.= (Peano_nat.plus x y) (Peano_nat.plus y x).
                                                        
                                                        1 nontautological subgoal.
                                                        
                                                        Subgoal 1:
                                                        
                                                        |---------------------------------------------------------------------------
                                                         Peano_nat.plus x y = Peano_nat.plus y x
                                                        
                                                        
                                                        Must try induction.
                                                        
                                                        The recursive terms in the conjecture suggest 2 inductions.
                                                        
                                                        We shall break ties using a complexity heuristic.
                                                        We shall induct according to a scheme derived from Peano_nat.plus.
                                                        
                                                        Induction scheme:
                                                        
                                                         (y = Peano_nat.Z ==> φ y x)
                                                         && (not (y = Peano_nat.Z) && φ (Destruct(Peano_nat.S, 0, y)) x ==> φ y x).
                                                        
                                                        2 nontautological subgoals.
                                                        
                                                        Subgoal 1.2:
                                                        
                                                         H0. y = Peano_nat.Z
                                                        |---------------------------------------------------------------------------
                                                         Peano_nat.plus x y = Peano_nat.plus y x
                                                        
                                                        This simplifies, using the definition of Peano_nat.plus to:
                                                        
                                                        Subgoal 1.2':
                                                        
                                                        |---------------------------------------------------------------------------
                                                         Peano_nat.plus x Peano_nat.Z = x
                                                        
                                                        
                                                        Must try induction.
                                                        
                                                        We shall induct according to a scheme derived from Peano_nat.plus.
                                                        
                                                        Induction scheme:
                                                        
                                                         (x = Peano_nat.Z ==> φ x)
                                                         && (not (x = Peano_nat.Z) && φ (Destruct(Peano_nat.S, 0, x)) ==> φ x).
                                                        
                                                        2 nontautological subgoals.
                                                        
                                                        Subgoal 1.2'.2:
                                                        
                                                         H0. x = Peano_nat.Z
                                                        |---------------------------------------------------------------------------
                                                         Peano_nat.plus x Peano_nat.Z = x
                                                        
                                                        But simplification reduces this to true, using the definition of
                                                        Peano_nat.plus.
                                                        
                                                        Subgoal 1.2'.1:
                                                        
                                                         H0. not (x = Peano_nat.Z)
                                                         H1. Peano_nat.plus (Destruct(Peano_nat.S, 0, x)) Peano_nat.Z =
                                                             Destruct(Peano_nat.S, 0, x)
                                                        |---------------------------------------------------------------------------
                                                         Peano_nat.plus x Peano_nat.Z = x
                                                        
                                                        But simplification reduces this to true, using the definition of
                                                        Peano_nat.plus.
                                                        
                                                        Subgoal 1.1:
                                                        
                                                         H0. not (y = Peano_nat.Z)
                                                         H1. Peano_nat.plus x (Destruct(Peano_nat.S, 0, y)) =
                                                             Peano_nat.plus (Destruct(Peano_nat.S, 0, y)) x
                                                        |---------------------------------------------------------------------------
                                                         Peano_nat.plus x y = Peano_nat.plus y x
                                                        
                                                        This simplifies, using the definition of Peano_nat.plus to:
                                                        
                                                        Subgoal 1.1':
                                                        
                                                         H0. Peano_nat.plus x (Destruct(Peano_nat.S, 0, y)) =
                                                             Peano_nat.plus (Destruct(Peano_nat.S, 0, y)) x
                                                        |---------------------------------------------------------------------------
                                                         C0. y = Peano_nat.Z
                                                         C1. Peano_nat.plus x y =
                                                             Peano_nat.S (Peano_nat.plus (Destruct(Peano_nat.S, 0, y)) x)
                                                        
                                                        
                                                        We can eliminate destructors by the following
                                                        substitution:
                                                         y -> Peano_nat.S y1
                                                        
                                                        This produces the modified subgoal:
                                                        
                                                        Subgoal 1.1'':
                                                        
                                                         H0. Peano_nat.plus x y1 = Peano_nat.plus y1 x
                                                        |---------------------------------------------------------------------------
                                                         Peano_nat.plus x (Peano_nat.S y1) = Peano_nat.S (Peano_nat.plus y1 x)
                                                        
                                                        
                                                        Cross-fertilizing with:
                                                        
                                                         Peano_nat.plus x y1 = Peano_nat.plus y1 x
                                                        
                                                        This produces the modified subgoal:
                                                        
                                                        Subgoal 1.1''':
                                                        
                                                        |---------------------------------------------------------------------------
                                                         Peano_nat.plus x (Peano_nat.S y1) = Peano_nat.S (Peano_nat.plus x y1)
                                                        
                                                        
                                                        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 Peano_nat.plus.
                                                        
                                                        Induction scheme:
                                                        
                                                         (x = Peano_nat.Z ==> φ x y1)
                                                         && (not (x = Peano_nat.Z) && φ (Destruct(Peano_nat.S, 0, x)) y1 ==> φ x y1).
                                                        
                                                        2 nontautological subgoals.
                                                        
                                                        Subgoal 1.1'''.2:
                                                        
                                                         H0. x = Peano_nat.Z
                                                        |---------------------------------------------------------------------------
                                                         Peano_nat.plus x (Peano_nat.S y1) = Peano_nat.S (Peano_nat.plus x y1)
                                                        
                                                        But simplification reduces this to true, using the definition of
                                                        Peano_nat.plus.
                                                        
                                                        Subgoal 1.1'''.1:
                                                        
                                                         H0. not (x = Peano_nat.Z)
                                                         H1. Peano_nat.plus (Destruct(Peano_nat.S, 0, x)) (Peano_nat.S y1) =
                                                             Peano_nat.S (Peano_nat.plus (Destruct(Peano_nat.S, 0, x)) y1)
                                                        |---------------------------------------------------------------------------
                                                         Peano_nat.plus x (Peano_nat.S y1) = Peano_nat.S (Peano_nat.plus x y1)
                                                        
                                                        But simplification reduces this to true, using the definition of
                                                        Peano_nat.plus.
                                                        
                                                         Rules:
                                                            (:def Peano_nat.plus)
                                                            (:induct Peano_nat.plus)
                                                        
                                                        
                                                        Proved
                                                        proof
                                                        ground_instances0
                                                        definitions8
                                                        inductions3
                                                        search_time
                                                        0.632s
                                                        Expand
                                                        • start[0.632s, "Goal"]
                                                            Peano_nat.plus :var_0: :var_1: = Peano_nat.plus :var_1: :var_0:
                                                        • subproof

                                                          Peano_nat.plus x y = Peano_nat.plus y x
                                                          • start[0.631s, "1"] Peano_nat.plus x y = Peano_nat.plus y x
                                                          • induction on (functional )
                                                            :scheme (y = Peano_nat.Z ==> φ y x)
                                                                    && (not (y = Peano_nat.Z) && φ (Destruct(Peano_nat.S, 0, y)) x
                                                                        ==> φ y x)
                                                          • Split ((not (y = Peano_nat.Z) || Peano_nat.plus x y = Peano_nat.plus y x)
                                                                   && (not
                                                                       (not (y = Peano_nat.Z)
                                                                        && Peano_nat.plus x (Destruct(Peano_nat.S, 0, y)) =
                                                                           Peano_nat.plus (Destruct(Peano_nat.S, 0, y)) x)
                                                                       || Peano_nat.plus x y = Peano_nat.plus y x)
                                                                   :cases [not (y = Peano_nat.Z)
                                                                           || Peano_nat.plus x y = Peano_nat.plus y x;
                                                                           (y = Peano_nat.Z
                                                                            || not
                                                                               (Peano_nat.plus x (Destruct(Peano_nat.S, 0, y)) =
                                                                                Peano_nat.plus (Destruct(Peano_nat.S, 0, y)) x))
                                                                           || Peano_nat.plus x y = Peano_nat.plus y x])
                                                            • subproof
                                                              (y = Peano_nat.Z || not (Peano_nat.plus x (Destruct(Peano_nat.S, 0, y)) = Peano_nat.plus (Destruct(Peano_nat.S, 0, y)) x)) || Peano_nat.plus x y = Peano_nat.plus y x
                                                              • start[0.532s, "1.1"]
                                                                  (y = Peano_nat.Z
                                                                   || not
                                                                      (Peano_nat.plus x (Destruct(Peano_nat.S, 0, y)) =
                                                                       Peano_nat.plus (Destruct(Peano_nat.S, 0, y)) x))
                                                                  || Peano_nat.plus x y = Peano_nat.plus y x
                                                              • simplify
                                                                into
                                                                (y = Peano_nat.Z
                                                                 || not
                                                                    (Peano_nat.plus x (Destruct(Peano_nat.S, 0, y)) =
                                                                     Peano_nat.plus (Destruct(Peano_nat.S, 0, y)) x))
                                                                || Peano_nat.plus x y =
                                                                   Peano_nat.S (Peano_nat.plus (Destruct(Peano_nat.S, 0, y)) x)
                                                                expansions
                                                                Peano_nat.plus
                                                                rewrite_steps
                                                                  forward_chaining
                                                                  • Elim_destructor (:cstor Peano_nat.S :replace Peano_nat.S y1 :context [])
                                                                  • induction on (functional )
                                                                    :scheme (x = Peano_nat.Z ==> φ x y1)
                                                                            && (not (x = Peano_nat.Z) && φ (Destruct(Peano_nat.S, 0, x)) y1
                                                                                ==> φ x y1)
                                                                  • Split ((not (x = Peano_nat.Z)
                                                                            || Peano_nat.plus x (Peano_nat.S y1) =
                                                                               Peano_nat.S (Peano_nat.plus x y1))
                                                                           && (not
                                                                               (not (x = Peano_nat.Z)
                                                                                && Peano_nat.plus (Destruct(Peano_nat.S, 0, x)) (Peano_nat.S y1)
                                                                                   =
                                                                                   Peano_nat.S (Peano_nat.plus (Destruct(Peano_nat.S, 0, x)) y1))
                                                                               || Peano_nat.plus x (Peano_nat.S y1) =
                                                                                  Peano_nat.S (Peano_nat.plus x y1))
                                                                           :cases [not (x = Peano_nat.Z)
                                                                                   || Peano_nat.plus x (Peano_nat.S y1) =
                                                                                      Peano_nat.S (Peano_nat.plus x y1);
                                                                                   (x = Peano_nat.Z
                                                                                    || not
                                                                                       (Peano_nat.plus (Destruct(Peano_nat.S, 0, x))
                                                                                        (Peano_nat.S y1) =
                                                                                        Peano_nat.S
                                                                                        (Peano_nat.plus (Destruct(Peano_nat.S, 0, x)) y1)))
                                                                                   || Peano_nat.plus x (Peano_nat.S y1) =
                                                                                      Peano_nat.S (Peano_nat.plus x y1)])
                                                                    • Subproof
                                                                    • Subproof
                                                                • subproof
                                                                  not (y = Peano_nat.Z) || Peano_nat.plus x y = Peano_nat.plus y x
                                                                  • start[0.532s, "1.2"]
                                                                      not (y = Peano_nat.Z) || Peano_nat.plus x y = Peano_nat.plus y x
                                                                  • simplify
                                                                    into
                                                                    Peano_nat.plus x Peano_nat.Z = x
                                                                    expansions
                                                                    Peano_nat.plus
                                                                    rewrite_steps
                                                                      forward_chaining
                                                                      • induction on (functional )
                                                                        :scheme (x = Peano_nat.Z ==> φ x)
                                                                                && (not (x = Peano_nat.Z) && φ (Destruct(Peano_nat.S, 0, x))
                                                                                    ==> φ x)
                                                                      • Split ((not (x = Peano_nat.Z) || Peano_nat.plus x Peano_nat.Z = x)
                                                                               && (not
                                                                                   (not (x = Peano_nat.Z)
                                                                                    && Peano_nat.plus (Destruct(Peano_nat.S, 0, x)) Peano_nat.Z =
                                                                                       Destruct(Peano_nat.S, 0, x))
                                                                                   || Peano_nat.plus x Peano_nat.Z = x)
                                                                               :cases [not (x = Peano_nat.Z) || Peano_nat.plus x Peano_nat.Z = x;
                                                                                       (x = Peano_nat.Z
                                                                                        || not
                                                                                           (Peano_nat.plus (Destruct(Peano_nat.S, 0, x)) Peano_nat.Z
                                                                                            = Destruct(Peano_nat.S, 0, x)))
                                                                                       || Peano_nat.plus x Peano_nat.Z = x])
                                                                        • Subproof
                                                                        • Subproof

                                                                Had we not restricted comm_plus as a permutative rule, the simplifier would have entered a rewrite loop every time it encountered a term matching plus <x> <y>, while with the permutative restriction in place, this has the effect of directing all the "simplest" terms to the left of plus, which will help with making further rewrite rules applicable and with simplification in general.

                                                                Forward-chaining Rules

                                                                Forward chaining is the second type of rule that Imandra allows us to register and participate automatically in proofs.

                                                                A forward chaining rule is a theorem containing a collection of trigger terms which must include all free variables of the theorem. If Imandra can appropriately match the triggers with terms in the goal, then an instantiation of the rule is added to the context. The context of a goal is not displayed in the goal itself (i.e., when the goal is printed), but is rather used in the background to aid the simplifier in closing branches, relieving hypotheses of rewrite rules during backchaining, and so on.

                                                                For example, let us prove the following theorem and install it as a forward-chaining rule:

                                                                In [10]:
                                                                lemma len_nonnegative x =
                                                                  List.length x [@trigger] >= 0
                                                                [@@simp] [@@fc]
                                                                
                                                                Out[10]:
                                                                val len_nonnegative : 'a list -> bool = <fun>
                                                                
                                                                Proved
                                                                proof
                                                                ground_instances0
                                                                definitions0
                                                                inductions0
                                                                search_time
                                                                0.164s
                                                                details
                                                                Expand
                                                                smt_stats
                                                                rlimit count229
                                                                mk bool var5
                                                                memory23.650000
                                                                max memory53.880000
                                                                num allocs14911132350.000000
                                                                Expand
                                                                • start[0.164s] List.length :var_0: >= 0
                                                                • simplify

                                                                  into
                                                                  true
                                                                  expansions
                                                                  []
                                                                  rewrite_steps
                                                                    forward_chaining
                                                                    List.len_nonnegative
                                                                  • unsat

                                                                    (mp (asserted (not true)) (rewrite (= (not true) false)) false)

                                                                  Now when Imandra encounters a term of the form List.length <term>, the formula List.length <term> >= 0 will be added to the context of the goal under focus. In other words, a forward chaining rule allows Imandra to extend the database of background logical facts it knows about a goal. These facts are made available to the simplifier, and can thus be used to enhance simplification by closing branches and relieving hypotheses of conditional rewrite rules.

                                                                  A forward chaining rule can contain multiple disjoint triggers. In this case, if either of the triggers matches, the forward chaining rule fires. For example, the following forward chaining version of the rev_len rewrite rule we added above will fire if either List.length x or List.length (List.rev x) matches.

                                                                  In [11]:
                                                                  lemma rev_len_fc x =
                                                                     List.length x [@trigger] = List.length (List.rev x) [@trigger]
                                                                  [@@auto] [@@fc]
                                                                  
                                                                  Out[11]:
                                                                  val rev_len_fc : 'a list -> bool = <fun>
                                                                  Goal:
                                                                  
                                                                  List.length x = List.length (List.rev x).
                                                                  
                                                                  1 nontautological subgoal.
                                                                  
                                                                  Subgoal 1:
                                                                  
                                                                  |---------------------------------------------------------------------------
                                                                   List.length x = List.length (List.rev x)
                                                                  
                                                                  But simplification reduces this to true, using the rewrite rule rev_len.
                                                                  
                                                                   Rules:
                                                                      (:rw rev_len)
                                                                      (:fc List.len_nonnegative)
                                                                      (:fc len_nonnegative)
                                                                  
                                                                  
                                                                  Proved
                                                                  proof
                                                                  ground_instances0
                                                                  definitions0
                                                                  inductions0
                                                                  search_time
                                                                  0.065s
                                                                  Expand
                                                                  • start[0.065s, "Goal"] List.length :var_0: = List.length (List.rev :var_0:)
                                                                  • subproof

                                                                    List.length x = List.length (List.rev x)
                                                                    • start[0.065s, "1"] List.length x = List.length (List.rev x)
                                                                    • simplify
                                                                      into
                                                                      true
                                                                      expansions
                                                                      []
                                                                      rewrite_steps
                                                                      rev_len
                                                                      forward_chaining
                                                                      • List.len_nonnegative
                                                                      • len_nonnegative
                                                                      • List.len_nonnegative
                                                                      • len_nonnegative

                                                                  Additionally, a forward chaining rule can contain multiple conjoined triggers, forming a trigger cluster. In this case, all the triggers must match in order for the forward chaining rule to apply.

                                                                  To create a trigger cluster multiple terms must be annotated with [@trigger <x>i], where <x> is a numeric identifier common to all the triggers in the cluster. For example:

                                                                  In [12]:
                                                                  theorem subset_trans l1 l2 l3 =
                                                                    (subset l1 l2 [@trigger 0i]) && (subset l2 l3 [@trigger 0i])
                                                                    ==>
                                                                    subset l1 l3
                                                                   [@@auto] [@@forward_chaining]
                                                                  
                                                                  Out[12]:
                                                                  val subset_trans : 'a list -> 'a list -> 'a list -> bool = <fun>
                                                                  Goal:
                                                                  
                                                                  subset l1 l2 && subset l2 l3 ==> subset l1 l3.
                                                                  
                                                                  1 nontautological subgoal.
                                                                  
                                                                  Subgoal 1:
                                                                  
                                                                   H0. subset l1 l2
                                                                   H1. subset l2 l3
                                                                  |---------------------------------------------------------------------------
                                                                   subset l1 l3
                                                                  
                                                                  
                                                                  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 subset.
                                                                  
                                                                  Induction scheme:
                                                                  
                                                                   (not (List.mem (List.hd l1) l2 && not (l1 = [])) ==> φ l3 l2 l1)
                                                                   && (not (l1 = []) && List.mem (List.hd l1) l2 && φ l3 l2 (List.tl l1)
                                                                       ==> φ l3 l2 l1).
                                                                  
                                                                  2 nontautological subgoals.
                                                                  
                                                                  Subgoal 1.2:
                                                                  
                                                                   H0. subset l1 l2
                                                                   H1. subset l2 l3
                                                                  |---------------------------------------------------------------------------
                                                                   C0. List.mem (List.hd l1) l2 && not (l1 = [])
                                                                   C1. subset l1 l3
                                                                  
                                                                  This simplifies, using the definition of subset to the following 2 subgoals:
                                                                  
                                                                  Subgoal 1.2.2:
                                                                  
                                                                   H0. l1 = []
                                                                   H1. subset l2 l3
                                                                  |---------------------------------------------------------------------------
                                                                   C0. List.mem (List.hd l1) l2
                                                                   C1. subset l1 l3
                                                                  
                                                                  But simplification reduces this to true, using the definition of subset.
                                                                  
                                                                  Subgoal 1.2.1:
                                                                  
                                                                   H0. subset l2 l3
                                                                   H1. l1 = []
                                                                   H2. List.mem (List.hd l1) l2
                                                                  |---------------------------------------------------------------------------
                                                                   subset l1 l3
                                                                  
                                                                  But simplification reduces this to true, using the definition of subset.
                                                                  
                                                                  Subgoal 1.1:
                                                                  
                                                                   H0. not (l1 = [])
                                                                   H1. List.mem (List.hd l1) l2
                                                                   H2. subset (List.tl l1) l2 && subset l2 l3 ==> subset (List.tl l1) l3
                                                                   H3. subset l1 l2
                                                                   H4. subset l2 l3
                                                                  |---------------------------------------------------------------------------
                                                                   subset l1 l3
                                                                  
                                                                  But simplification reduces this to true, using the definition of subset, and
                                                                  the rewrite rule mem_subset.
                                                                  
                                                                   Rules:
                                                                      (:def subset)
                                                                      (:rw mem_subset)
                                                                      (:induct subset)
                                                                  
                                                                  
                                                                  Proved
                                                                  proof
                                                                  ground_instances0
                                                                  definitions6
                                                                  inductions1
                                                                  search_time
                                                                  0.804s
                                                                  Expand
                                                                  • start[0.804s, "Goal"]
                                                                      subset :var_0: :var_1: && subset :var_1: :var_2: ==> subset :var_0: :var_2:
                                                                  • subproof

                                                                    (not (subset l1 l2) || not (subset l2 l3)) || subset l1 l3
                                                                    • start[0.801s, "1"] (not (subset l1 l2) || not (subset l2 l3)) || subset l1 l3
                                                                    • induction on (functional )
                                                                      :scheme (not (List.mem (List.hd l1) l2 && not (l1 = [])) ==> φ l3 l2 l1)
                                                                              && (not (l1 = [])
                                                                                  && List.mem (List.hd l1) l2 && φ l3 l2 (List.tl l1)
                                                                                  ==> φ l3 l2 l1)
                                                                    • Split ((((List.mem (List.hd l1) l2 && not (l1 = []) || not (subset l1 l2))
                                                                               || not (subset l2 l3))
                                                                              || subset l1 l3)
                                                                             && (((not
                                                                                   ((not (l1 = []) && List.mem (List.hd l1) l2)
                                                                                    && ((not (subset (List.tl l1) l2) || not (subset l2 l3))
                                                                                        || subset (List.tl l1) l3))
                                                                                   || not (subset l1 l2))
                                                                                  || not (subset l2 l3))
                                                                                 || subset l1 l3)
                                                                             :cases [((not (subset l1 l2) || not (subset l2 l3))
                                                                                      || List.mem (List.hd l1) l2 && not (l1 = []))
                                                                                     || subset l1 l3;
                                                                                     ((((l1 = [] || not (List.mem (List.hd l1) l2))
                                                                                        || not
                                                                                           (not (subset (List.tl l1) l2 && subset l2 l3)
                                                                                            || subset (List.tl l1) l3))
                                                                                       || not (subset l1 l2))
                                                                                      || not (subset l2 l3))
                                                                                     || subset l1 l3])
                                                                      • subproof
                                                                        ((((l1 = [] || not (List.mem (List.hd l1) l2)) || not (not (subset (List.tl l1) l2 && subset l2 l3) || subset (List.tl l1) l3)) || not (subset l1 l2)) || not (subset l2 l3)) || subset l1 l3
                                                                        • start[0.509s, "1.1"]
                                                                            ((((l1 = [] || not (List.mem (List.hd l1) l2))
                                                                               || not
                                                                                  (not (subset (List.tl l1) l2 && subset l2 l3)
                                                                                   || subset (List.tl l1) l3))
                                                                              || not (subset l1 l2))
                                                                             || not (subset l2 l3))
                                                                            || subset l1 l3
                                                                        • simplify
                                                                          into
                                                                          true
                                                                          expansions
                                                                          [subset, subset]
                                                                          rewrite_steps
                                                                          mem_subset
                                                                          forward_chaining
                                                                        • subproof
                                                                          ((not (subset l1 l2) || not (subset l2 l3)) || List.mem (List.hd l1) l2 && not (l1 = [])) || subset l1 l3
                                                                          • start[0.509s, "1.2"]
                                                                              ((not (subset l1 l2) || not (subset l2 l3))
                                                                               || List.mem (List.hd l1) l2 && not (l1 = []))
                                                                              || subset l1 l3
                                                                          • simplify
                                                                            into
                                                                            (((not (l1 = []) || not (subset l2 l3)) || List.mem (List.hd l1) l2)
                                                                             || subset l1 l3)
                                                                            && (((not (subset l2 l3) || not (l1 = [])) || not (List.mem (List.hd l1) l2))
                                                                                || subset l1 l3)
                                                                            expansions
                                                                            [subset, subset]
                                                                            rewrite_steps
                                                                              forward_chaining
                                                                                • Subproof
                                                                                • Subproof

                                                                        This forward chaining rule will match only if a goal contains terms that match both subset l1 l2 and subset l2 l3.

                                                                        It should be noted that Imandra supports automatic trigger selection, meaning it's often not necessary to annotate the trigger terms manually. Imandra can typically infer for us both simple triggers and trigger clusters. In fact for both the single trigger examples above, we could have omitted the trigger annotations altogether, and Imandra would have found some for us automatically.