Attributes

Attributes can be used to give Imandra verification hints, and to instruct Imandra how it should use a proved theorem in subsequent verification efforts, via the installation of a theorem as a "rule".

Verification Hints

  • [@@auto]: apply Imandra's inductive waterfall proof strategy, which combines simplification (including automatic subgoaling, conditional rewriting and forward-chaining using previously proved lemmas, decision procedures for datatypes and arithmetic, etc.), and may decide to do induction. This is the most common way to prove a theorem in Imandra.

  • [@@induct <flag?>]: apply Imandra's inductive waterfall proof strategy, but control the top-level induction. The <flag?> can be one of:

    • functional <func_name> - perform functional induction using an induction scheme derived from <func_name>
    • structural <args?> - perform structural induction on the arguments <args?> if given, else on a heuristically chosen collection of variables. The types of the induction variables must be algebraic datatypes / variant types. An additive approach (linear in the total number of constructors) is taken for combining the schemes of individual variables into a composite induction scheme.
    • structural_mult <args?> - like structural, except uses a "multiplicative" scheme, rather than an additive one
    • structural_add <args?> - a synonym for structural
  • [@@simp] or [@@simplify]: apply simplification to the goal before unrolling.

  • [@@disable <f_1>,...,<f_k>]: If f_i is a rule, instructs Imandra to ignore f_i during the proof attempt. If f_i is a function, instructs Imandra to leave the function definition unexpanded during the proof attempt. This is especially useful in the presence of rewrite rules about non-recursive functions, as such rules will typically not apply unless the relevant non-recursive function is disabled. Imandra might choose to ignore this hint if ignoring it leads to immediate closure of the goal, or to the construction of a valid counterexample. Note that rules and functions can be globally disabled, using the #disable directive.

  • [@@enable <f_1>,...,<f_k>]: The dual of @@disable. Note that rules and functions can be globally enabled, using the #enable directive.

  • [@@apply <thm <arg_1> ... <arg_k>>]: instantiate thm with the given arguments and add its instantiation to the hypotheses of the goal. This is especially useful when thm is not naturally useable as a @@rewrite or @@forward-chaining rule, but is nevertheless needed (in an instantiated form) to prove a given theorem.

  • [@@blast]: apply Imandra's blast procedure, which combines symbolic execution and SAT-based bit-blasting. This is useful for difficult combinatorial problems, and problems involving nontrivial (i.e., nonlinear) arithmetic over bounded discrete domains.

Rule Classes

Theorems may be installed as rules, which instructs Imandra to apply them in certain ways during subsequent proof attempts. The development of an appropriate collection of rules can be used to "teach" Imandra how to reason in a new domain.

Examples

In [1]:
verify (fun x y -> List.length (x@y) = List.length x + List.length y) [@@auto]
Out[1]:
- : 'a list -> 'a list -> bool = <fun>
Goal:

List.length (x @ y) = List.length x + List.length y.

1 nontautological subgoal.

Subgoal 1:

|---------------------------------------------------------------------------
 List.length (List.append x y) = List.length x + List.length y


Must try induction.

The recursive terms in the conjecture suggest 3 inductions.
Subsumption and merging reduces this to 2.

Only 1 of those schemes are unflawed.
We shall induct according to a scheme derived from List.append.

Induction scheme:

 (x = [] ==> φ y x) && (not (x = []) && φ y (List.tl x) ==> φ y x).

2 nontautological subgoals.

Subgoal 1.2:

 H0. x = []
|---------------------------------------------------------------------------
 List.length (List.append x y) = List.length x + List.length y

But simplification reduces this to true, using the definitions of List.append
and List.length.

Subgoal 1.1:

 H0. not (x = [])
 H1. List.length (List.append (List.tl x) y) =
     List.length (List.tl x) + List.length y
|---------------------------------------------------------------------------
 List.length (List.append x y) = List.length x + List.length y

But simplification reduces this to true, using the definitions of List.append
and List.length.

 Rules:
    (:def List.append)
    (:def List.length)
    (:fc List.len_nonnegative)
    (:induct List.append)

Proved
proof
ground_instances0
definitions5
inductions1
search_time
0.083s
Expand
  • start[0.083s, "Goal"]
      List.length (List.append :var_0: :var_1:) =
      List.length :var_0: + List.length :var_1:
  • subproof

    List.length (List.append x y) = List.length x + List.length y
    • start[0.083s, "1"]
        List.length (List.append x y) = List.length x + List.length y
    • induction on (functional )
      :scheme (x = [] ==> φ y x) && (not (x = []) && φ y (List.tl x) ==> φ y x)
    • Split ((not (x = [])
              || List.length (List.append x y) = List.length x + List.length y)
             && (not
                 (not (x = [])
                  && List.length (List.append (List.tl x) y) =
                     List.length (List.tl x) + List.length y)
                 || List.length (List.append x y) = List.length x + List.length y)
             :cases [not (x = [])
                     || List.length (List.append x y) =
                        List.length x + List.length y;
                     (x = []
                      || not
                         (List.length (List.append (List.tl x) y) =
                          List.length (List.tl x) + List.length y))
                     || List.length (List.append x y) =
                        List.length x + List.length y])
      • subproof
        (x = [] || not (List.length (List.append (List.tl x) y) = List.length (List.tl x) + List.length y)) || List.length (List.append x y) = List.length x + List.length y
        • start[0.031s, "1.1"]
            (x = []
             || not
                (List.length (List.append (List.tl x) y) =
                 List.length (List.tl x) + List.length y))
            || List.length (List.append x y) = List.length x + List.length y
        • simplify
          into
          true
          expansions
          [List.length, List.length, List.append]
          rewrite_steps
            forward_chaining
            • List.len_nonnegative
            • List.len_nonnegative
            • List.len_nonnegative
            • List.len_nonnegative
            • List.len_nonnegative
        • subproof
          not (x = []) || List.length (List.append x y) = List.length x + List.length y
          • start[0.031s, "1.2"]
              not (x = [])
              || List.length (List.append x y) = List.length x + List.length y
          • simplify
            into
            true
            expansions
            [List.length, List.append]
            rewrite_steps
              forward_chaining
              • List.len_nonnegative
              • List.len_nonnegative
              • List.len_nonnegative
      In [2]:
      verify (fun x -> x @ [] @ x = x @ x) [@@simp]
      
      Out[2]:
      - : 'a list -> bool = <fun>
      
      Proved
      proof
      ground_instances0
      definitions1
      inductions0
      search_time
      0.060s
      details
      Expand
      smt_stats
      rlimit count225
      mk bool var5
      num allocs32577163
      memory8.860000
      max memory12.060000
      Expand
      • start[0.060s]
          List.append :var_0: (List.append [] :var_0:) = List.append :var_0: :var_0:
      • simplify

        into
        true
        expansions
        List.append
        rewrite_steps
          forward_chaining
          • unsat

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

            List.length (List.append x y) = List.length x + List.length y
            • start[0.076s, "1"]
                List.length (List.append x y) = List.length x + List.length y
            • induction on (functional )
              :scheme (x = [] ==> φ y x) && (not (x = []) && φ y (List.tl x) ==> φ y x)
            • Split ((not (x = [])
                      || List.length (List.append x y) = List.length x + List.length y)
                     && (not
                         (not (x = [])
                          && List.length (List.append (List.tl x) y) =
                             List.length (List.tl x) + List.length y)
                         || List.length (List.append x y) = List.length x + List.length y)
                     :cases [not (x = [])
                             || List.length (List.append x y) =
                                List.length x + List.length y;
                             (x = []
                              || not
                                 (List.length (List.append (List.tl x) y) =
                                  List.length (List.tl x) + List.length y))
                             || List.length (List.append x y) =
                                List.length x + List.length y])
              • subproof
                (x = [] || not (List.length (List.append (List.tl x) y) = List.length (List.tl x) + List.length y)) || List.length (List.append x y) = List.length x + List.length y
                • start[0.033s, "1.1"]
                    (x = []
                     || not
                        (List.length (List.append (List.tl x) y) =
                         List.length (List.tl x) + List.length y))
                    || List.length (List.append x y) = List.length x + List.length y
                • simplify
                  into
                  true
                  expansions
                  [List.length, List.length, List.append]
                  rewrite_steps
                    forward_chaining
                    • List.len_nonnegative
                    • List.len_nonnegative
                    • List.len_nonnegative
                    • List.len_nonnegative
                    • List.len_nonnegative
                • subproof
                  not (x = []) || List.length (List.append x y) = List.length x + List.length y
                  • start[0.033s, "1.2"]
                      not (x = [])
                      || List.length (List.append x y) = List.length x + List.length y
                  • simplify
                    into
                    true
                    expansions
                    [List.length, List.append]
                    rewrite_steps
                      forward_chaining
                      • List.len_nonnegative
                      • List.len_nonnegative
                      • List.len_nonnegative
              In [4]:
              theorem len_non_neg x = (List.length x) [@trigger] >= 0 [@@simp] [@@fc]
              
              Out[4]:
              val len_non_neg : 'a list -> bool = <fun>
              
              Proved
              proof
              ground_instances0
              definitions0
              inductions0
              search_time
              0.040s
              details
              Expand
              smt_stats
              rlimit count229
              mk bool var5
              num allocs126815297
              memory12.540000
              max memory15.560000
              Expand
              • start[0.040s] 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)
                In [5]:
                lemma foo = (fun x -> x @ [] = x) [@@induct x] [@@disable List.append_to_nil]
                
                Out[5]:
                val foo : 'a list -> bool = <fun>
                Goal:
                
                x @ [] = x.
                
                1 nontautological subgoal.
                
                Induction scheme:
                
                 φ [] && (x <> [] && φ (List.tl x) ==> φ x).
                
                2 nontautological subgoals.
                
                Subgoal 2:
                
                |---------------------------------------------------------------------------
                 List.append [] [] = []
                
                But simplification reduces this to true, using the definition of List.append.
                
                Subgoal 1:
                
                 H0. x <> []
                 H1. List.append (List.tl x) [] = List.tl x
                |---------------------------------------------------------------------------
                 List.append x [] = x
                
                But simplification reduces this to true, using the definition of List.append.
                
                 Rules:
                    (:def List.append)
                    (:induct struct list)
                
                
                Proved
                proof
                ground_instances0
                definitions2
                inductions1
                search_time
                0.016s
                Expand
                • start[0.016s, "Goal"] List.append :var_0: [] = :var_0:
                • subproof

                  List.append x [] = x
                  • start[0.016s, "1"] List.append x [] = x
                  • induction on (structural+ x)
                    :scheme φ [] && (x <> [] && φ (List.tl x) ==> φ x)
                  • Split (List.append [] [] = []
                           && (not (x <> [] && List.append (List.tl x) [] = List.tl x)
                               || List.append x [] = x)
                           :cases [List.append [] [] = [];
                                   (not (x <> []) || not (List.append (List.tl x) [] = List.tl x))
                                   || List.append x [] = x])
                    • subproof
                      (not (x <> []) || not (List.append (List.tl x) [] = List.tl x)) || List.append x [] = x
                      • start[0.015s, "1"]
                          (not (x <> []) || not (List.append (List.tl x) [] = List.tl x))
                          || List.append x [] = x
                      • simplify
                        into
                        true
                        expansions
                        List.append
                        rewrite_steps
                          forward_chaining
                        • subproof
                          List.append [] [] = []
                          • start[0.015s, "2"] List.append [] [] = []
                          • simplify
                            into
                            true
                            expansions
                            List.append
                            rewrite_steps
                              forward_chaining