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:

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

2 nontautological subgoals.

Subgoal 1.2:

|---------------------------------------------------------------------------
 C0. x <> []
 C1. 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. 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_instances:0
definitions:5
inductions:1
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 (not (x <> []) ==> φ x y)
              && (x <> [] && φ (List.tl x) y ==> φ x y)
    • Split (let (_x_0 : bool) = x <> [] in
             let (_x_1 : int) = List.length y in
             let (_x_2 : bool)
                 = List.length (List.append x y) = List.length x + _x_1
             in
             let (_x_3 : sko_ty_0 list) = List.tl x in
             (_x_0 || _x_2)
             && (not
                 (_x_0
                  && (List.length (List.append _x_3 y) = List.length _x_3 + _x_1))
                 || _x_2)
             :cases [x <> []
                     || (List.length (List.append x y)
                         = List.length x + List.length y);
                     let (_x_0 : sko_ty_0 list) = List.tl x in
                     let (_x_1 : int) = List.length y in
                     not (x <> [])
                     || not
                        (List.length (List.append _x_0 y) = List.length _x_0 + _x_1)
                     || (List.length (List.append x y) = List.length x + _x_1)])
      • subproof
        let (_x_0 : sko_ty_0 list) = List.tl x in let (_x_1 : int) = List.length y in not (x <> []) || not (List.length (List.append _x_0 y) = List.length _x_0 + _x_1) || (List.length (List.append x y) = List.length x + _x_1)
        • start[0.042s, "1.1"]
            let (_x_0 : sko_ty_0 list) = List.tl x in
            let (_x_1 : int) = List.length y in
            not (x <> [])
            || not (List.length (List.append _x_0 y) = List.length _x_0 + _x_1)
            || (List.length (List.append x y) = List.length x + _x_1)
        • 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
          x <> [] || (List.length (List.append x y) = List.length x + List.length y)
          • start[0.042s, "1.2"]
              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
              • 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_instances:0
      definitions:1
      inductions:0
      search_time:
      0.049s
      details:
      Expand
      smt_stats:
      rlimit count:430
      num allocs:54829479
      time:0.013000
      memory:15.510000
      max memory:15.980000
      Expand
      • start[0.049s]
          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
          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:
          
           (not (x <> []) ==> φ x y) && (x <> [] && φ (List.tl x) y ==> φ x y).
          
          2 nontautological subgoals.
          
          Subgoal 1.2:
          
          |---------------------------------------------------------------------------
           C0. x <> []
           C1. 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. 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_instances:0
          definitions:5
          inductions:1
          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 (not (x <> []) ==> φ x y)
                      && (x <> [] && φ (List.tl x) y ==> φ x y)
            • Split (let (_x_0 : bool) = x <> [] in
                     let (_x_1 : int) = List.length y in
                     let (_x_2 : bool)
                         = List.length (List.append x y) = List.length x + _x_1
                     in
                     let (_x_3 : sko_ty_0 list) = List.tl x in
                     (_x_0 || _x_2)
                     && (not
                         (_x_0
                          && (List.length (List.append _x_3 y) = List.length _x_3 + _x_1))
                         || _x_2)
                     :cases [x <> []
                             || (List.length (List.append x y)
                                 = List.length x + List.length y);
                             let (_x_0 : sko_ty_0 list) = List.tl x in
                             let (_x_1 : int) = List.length y in
                             not (x <> [])
                             || not
                                (List.length (List.append _x_0 y) = List.length _x_0 + _x_1)
                             || (List.length (List.append x y) = List.length x + _x_1)])
              • subproof
                let (_x_0 : sko_ty_0 list) = List.tl x in let (_x_1 : int) = List.length y in not (x <> []) || not (List.length (List.append _x_0 y) = List.length _x_0 + _x_1) || (List.length (List.append x y) = List.length x + _x_1)
                • start[0.040s, "1.1"]
                    let (_x_0 : sko_ty_0 list) = List.tl x in
                    let (_x_1 : int) = List.length y in
                    not (x <> [])
                    || not (List.length (List.append _x_0 y) = List.length _x_0 + _x_1)
                    || (List.length (List.append x y) = List.length x + _x_1)
                • 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
                  x <> [] || (List.length (List.append x y) = List.length x + List.length y)
                  • start[0.040s, "1.2"]
                      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
                      • 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_instances:0
              definitions:0
              inductions:0
              search_time:
              0.030s
              details:
              Expand
              smt_stats:
              rlimit count:514
              num allocs:174727728
              time:0.009000
              memory:16.080000
              max memory:16.570000
              Expand
              • start[0.030s] List.length ( :var_0: ) >= 0
              • simplify

                into:
                true
                expansions:
                []
                rewrite_steps:
                  forward_chaining:
                  List.len_nonnegative
                • Unsat
                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_instances:0
                definitions:2
                inductions:1
                search_time:
                0.013s
                Expand
                • start[0.013s, "Goal"] List.append ( :var_0: ) [] = ( :var_0: )
                • subproof

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