# Using Imandra Discover¶

Imandra Discover is a tool for theory exploration and producing conjectures. Sometimes, it is not entirely clear what lemmas are necessary for a proof to succeed, or what the properties of a program are. Discover intends to help with this problem, giving the user potential properties to be proved and themselves used as lemmas.

## Balanced Binary Trees¶

In this example, we will define a type of binary trees, and a function that creates a balanced binary tree of a given number of nodes. Balanced binary trees are trees where the subtrees to the left and right of the root have either the same number of nodes, or differ by one. We will then demonstrate how to use Discover for the discovery of properties of these functions.

# Demonstration¶

You may need to #require the Discover bridge. This may not be necessary if you are using Try Imandra or Imandra through a Docker image. The command is commented out here for reference so that you can easily use it if needed.

In :
(* #require "imandra-discover-bridge";; *)
open Imandra_discover_bridge.User_level;;

Out:

It is common to restrict induction used by Imandra using #max_induct.

In :
#max_induct 1;;
#induct_unroll 20;;

Out:

This is our type of binary trees. The content of the binary trees is immaterial.

Keep in mind that Discover instantiates polymorphic types with int. This means that if this was a polymorphic binary tree whose values were of 'a, Discover would replace the type variable 'a with int. If Discover gives you unexpected output or seems to lack things that it should have, take a look at the signature used by Discover. You can specify the types of your functions to prevent this.

In :
type bt = | Empty
| Branch of
{value : int;
left : bt;
right : bt;};;

Out:
type bt = Empty | Branch of { value : Z.t; left : bt; right : bt; }


Let's define some functions that we will use in the construction of balanced binary trees.

In :
let lhs_split n = n/2;;
let rhs_split n = n - lhs_split n;;

Out:
val lhs_split : Z.t -> Z.t = <fun>
val rhs_split : Z.t -> Z.t = <fun>


What are some properties that hold of these functions? We should ask Discover to suggest some things. We invoke Discover with the events database db and pass it a list of the string function names we would like Discover to investigate.

In :
discover db ~iterations:2i ["+";"lhs_split";"rhs_split"];;

Out:
 <===DISCOVER===================================>
We are running Discover on the following signature:

+:int->int->int
lhs_split:int->int
rhs_split:int->int

We are running Discover with this inferred constant type:
type nonrec discover_type = | Bool of discover_bool
| Int of discover_int
<==============================================>
Running Discover on: discover_run
<===DISCOVER RESULTS===========================>
The below laws are the result of the condition: No condition. These are the 6 amazing conjectures suggested by Discover for discover_run.
fun x -> (lhs_split (x + x)) = x
fun x -> (rhs_split (x + x)) = x
fun x -> ((lhs_split x) + (rhs_split x)) = x
fun x y -> (y + x) = (x + y)
fun x y z -> (y + (x + z)) = (x + (y + z))
fun x y z -> ((x + y) + z) = (x + (y + z))
These are SUBSUMED laws that may be interesting to the user.
No subsumed conjectures.
<==============================================>
A string list discover_result with the conjectures before filtering has been defined.
A string list discover_result_simplified contains the conjectures after simplification by Imandra.
- : unit = ()


Discover finishes after running for a few seconds and gives us some conjectures we could try to prove. One of them states that the sum of the lhs_split and rhs_split of some x0 is equal to x0. Great, we can ask Imandra to prove it for us.

In :
lemma discover__2 x0 = ((lhs_split x0) + (rhs_split x0)) = x0 [@@rewrite]  [@@auto];;

Out:
val discover__2 : discover_int -> discover_bool = <fun>
Goal:

lhs_split x0 + rhs_split x0 = x0.

1 tautological subgoal.

Subgoal 1:

|---------------------------------------------------------------------------
true

But this is obviously true.


Proved
proof
 ground_instances: 0 definitions: 0 inductions: 0 search_time: 0.000s
Expand
• start[0.000s, "Goal"]
let (_x_0 : int) = ( :var_0: ) / 2 in
_x_0 + (( :var_0: ) - _x_0) = ( :var_0: )
• #### subproof

true
• start[0.000s, "1"] true
• ##### simplify
 into: true expansions: [] rewrite_steps: forward_chaining:

#### Warning

Pattern will match only if lhs_split is disabled
(non-recursive function)
See https://docs.imandra.ai/imandra-docs/notebooks/verification-simplification

#### Warning

Pattern will match only if rhs_split is disabled
(non-recursive function)
See https://docs.imandra.ai/imandra-docs/notebooks/verification-simplification

Now, we will make a function that should return a balanced binary tree with n nodes, given n.

In :
let rec cbal n =
if n < 0 then Empty else
match n with
| 0 -> Empty
| 1 -> Branch {value=1; left = Empty; right = Empty}
| _ -> let left_split = lhs_split (n-1) in
let right_split = rhs_split (n-1) in
let left = cbal left_split in
let right = cbal right_split in
Branch {value=1; left; right};;

Out:
val cbal : discover_int -> bt = <fun>

termination proof

### Termination proof

call cbal (lhs_split (n - 1)) from cbal n
original:cbal n
sub:cbal (lhs_split (n - 1))
original ordinal:Ordinal.Int (_cnt n)
sub ordinal:Ordinal.Int (_cnt (lhs_split (n - 1)))
path:[not (1 = n) && not (0 = n) && not (n < 0)]
proof:
detailed proof
ground_instances:1
definitions:0
inductions:0
search_time:
0.009s
details:
Expand
smt_stats:
 num checks: 3 arith assert lower: 10 arith tableau max rows: 4 arith tableau max columns: 11 arith pivots: 1 rlimit count: 3038 mk clause: 11 datatype occurs check: 2 mk bool var: 23 arith assert upper: 3 arith row summations: 4 propagations: 5 conflicts: 2 arith fixed eqs: 1 datatype accessor ax: 2 arith conflicts: 1 arith num rows: 4 arith assert diseq: 6 num allocs: 2.346e+08 final checks: 1 added eqs: 9 del clause: 11 arith eq adapter: 5 memory: 22.63 max memory: 22.63
Expand
• start[0.009s]
let (_x_0 : int) = if n >= 0 then n else 0 in
let (_x_1 : int) = (n - 1) / 2 in
let (_x_2 : int) = if _x_1 >= 0 then _x_1 else 0 in
let (_x_3 : bool)
= not (not (1 = _x_1) && (not (0 = _x_1) && not (_x_1 < 0)))
in
not (1 = n)
&& (not (0 = n) && (not (n < 0) && ((_x_0 >= 0) && (_x_2 >= 0))))
==> (_x_3 && _x_3) || Ordinal.( << ) (Ordinal.Int _x_2) (Ordinal.Int _x_0)
• ###### simplify
 into: let (_x_0 : int) = ((-1) + n) / 2 in not (not (1 = _x_0) && not (0 = _x_0) && (0 <= _x_0)) || Ordinal.( << ) (Ordinal.Int (if _x_0 >= 0 then _x_0 else 0)) (Ordinal.Int (if n >= 0 then n else 0)) || not (not (1 = n) && not (0 = n) && (0 <= n)) expansions: [] rewrite_steps: forward_chaining:
• unroll
 expr: (let ((a!1 (ite (>= (div (+ (- 1) n_448/server) 2) 0) (div (+ (- 1) n_448/server) 2)… expansions:
• Unsat
call cbal (rhs_split (n - 1)) from cbal n
original:cbal n
sub:cbal (rhs_split (n - 1))
original ordinal:Ordinal.Int (_cnt n)
sub ordinal:Ordinal.Int (_cnt (rhs_split (n - 1)))
path:[not (1 = n) && not (0 = n) && not (n < 0)]
proof:
detailed proof
ground_instances:1
definitions:0
inductions:0
search_time:
0.010s
details:
Expand
smt_stats:
 num checks: 3 arith assert lower: 10 arith tableau max rows: 5 arith tableau max columns: 12 arith pivots: 3 rlimit count: 1634 mk clause: 16 datatype occurs check: 2 mk bool var: 23 arith assert upper: 3 arith row summations: 9 propagations: 6 conflicts: 2 arith fixed eqs: 1 datatype accessor ax: 2 arith conflicts: 1 arith num rows: 5 arith assert diseq: 4 num allocs: 2.07036e+08 final checks: 1 added eqs: 9 del clause: 16 arith eq adapter: 5 memory: 22.6 max memory: 22.6
Expand
• start[0.010s]
let (_x_0 : int) = if n >= 0 then n else 0 in
let (_x_1 : int) = n - 1 in
let (_x_2 : int) = _x_1 - _x_1 / 2 in
let (_x_3 : int) = if _x_2 >= 0 then _x_2 else 0 in
let (_x_4 : bool)
= not (not (1 = _x_2) && (not (0 = _x_2) && not (_x_2 < 0)))
in
not (1 = n)
&& (not (0 = n) && (not (n < 0) && ((_x_0 >= 0) && (_x_3 >= 0))))
==> (_x_4 && _x_4) || Ordinal.( << ) (Ordinal.Int _x_3) (Ordinal.Int _x_0)
• ###### simplify
 into: let (_x_0 : int) = (-1) + n in let (_x_1 : int) = (-1) * (_x_0 / 2) in let (_x_2 : int) = n + _x_1 in not (not (2 = _x_2) && not (1 = _x_2) && (1 <= _x_2)) || Ordinal.( << ) (Ordinal.Int (if _x_2 >= 1 then _x_0 + _x_1 else 0)) (Ordinal.Int (if n >= 0 then n else 0)) || not (not (1 = n) && not (0 = n) && (0 <= n)) expansions: [] rewrite_steps: forward_chaining:
• unroll
 expr: (let ((a!1 (+ n_448/server (* (- 1) (div (+ (- 1) n_448/server) 2)))) (a!2 (+ (- 1) n_448/serv… expansions:
• Unsat

This is simply the size of the tree.

In :
let rec nodes tree =
match tree with
| Empty -> 0
| Branch {left; right; _} -> 1 + (nodes left) + (nodes right);;

Out:
val nodes : bt -> discover_int = <fun>

termination proof

### Termination proof

call nodes (Destruct(Branch, 1, tree)) from nodes tree
original:nodes tree
sub:nodes (Destruct(Branch, 1, tree))
original ordinal:Ordinal.Int (_cnt tree)
sub ordinal:Ordinal.Int (_cnt (Destruct(Branch, 1, tree)))
path:[Is_a(Branch, tree)]
proof:
detailed proof
ground_instances:3
definitions:0
inductions:0
search_time:
0.010s
details:
Expand
smt_stats:
 num checks: 8 arith assert lower: 28 arith tableau max rows: 8 arith tableau max columns: 23 arith pivots: 23 rlimit count: 7130 mk clause: 50 datatype occurs check: 20 mk bool var: 149 arith assert upper: 37 datatype splits: 5 decisions: 59 arith row summations: 44 propagations: 68 conflicts: 15 arith fixed eqs: 10 datatype accessor ax: 11 arith conflicts: 4 arith num rows: 8 arith assert diseq: 4 datatype constructor ax: 28 num allocs: 2.95125e+08 final checks: 5 added eqs: 126 del clause: 25 arith eq adapter: 29 memory: 22.95 max memory: 22.97
Expand
• start[0.010s]
let (_x_0 : int) = count.bt tree in
let (_x_1 : bt) = Destruct(Branch, 1, tree) in
let (_x_2 : int) = count.bt _x_1 in
let (_x_3 : bool) = not Is_a(Branch, _x_1) in
Is_a(Branch, tree) && ((_x_0 >= 0) && (_x_2 >= 0))
==> (_x_3 && _x_3) || Ordinal.( << ) (Ordinal.Int _x_2) (Ordinal.Int _x_0)
• ###### simplify
 into: let (_x_0 : int) = count.bt tree in let (_x_1 : bt) = Destruct(Branch, 1, tree) in let (_x_2 : int) = count.bt _x_1 in not (Is_a(Branch, tree) && (_x_0 >= 0) && (_x_2 >= 0)) || not Is_a(Branch, _x_1) || Ordinal.( << ) (Ordinal.Int _x_2) (Ordinal.Int _x_0) expansions: [] rewrite_steps: forward_chaining:
• unroll
 expr: (|Ordinal.<<| (|Ordinal.Int_79/boot| (|count.bt_1257/client| (|get… expansions:
• unroll
 expr: (|count.bt_1257/client| (|get.Branch.left_518/server| tree_520/server)) expansions:
• unroll
 expr: (|count.bt_1257/client| tree_520/server) expansions:
• Unsat
call nodes (Destruct(Branch, 2, tree)) from nodes tree
original:nodes tree
sub:nodes (Destruct(Branch, 2, tree))
original ordinal:Ordinal.Int (_cnt tree)
sub ordinal:Ordinal.Int (_cnt (Destruct(Branch, 2, tree)))
path:[Is_a(Branch, tree)]
proof:
detailed proof
ground_instances:3
definitions:0
inductions:0
search_time:
0.011s
details:
Expand
smt_stats:
 num checks: 8 arith assert lower: 22 arith tableau max rows: 7 arith tableau max columns: 22 arith pivots: 16 rlimit count: 3045 mk clause: 35 datatype occurs check: 14 mk bool var: 105 arith assert upper: 25 datatype splits: 3 decisions: 27 arith row summations: 25 propagations: 35 conflicts: 13 arith fixed eqs: 8 datatype accessor ax: 8 minimized lits: 1 arith conflicts: 4 arith num rows: 7 arith assert diseq: 1 datatype constructor ax: 15 num allocs: 2.65424e+08 final checks: 4 added eqs: 71 del clause: 26 arith eq adapter: 19 memory: 22.97 max memory: 22.97
Expand
• start[0.011s]
let (_x_0 : int) = count.bt tree in
let (_x_1 : bt) = Destruct(Branch, 2, tree) in
let (_x_2 : int) = count.bt _x_1 in
let (_x_3 : bool) = not Is_a(Branch, _x_1) in
Is_a(Branch, tree) && ((_x_0 >= 0) && (_x_2 >= 0))
==> (_x_3 && _x_3) || Ordinal.( << ) (Ordinal.Int _x_2) (Ordinal.Int _x_0)
• ###### simplify
 into: let (_x_0 : bt) = Destruct(Branch, 2, tree) in let (_x_1 : int) = count.bt _x_0 in let (_x_2 : int) = count.bt tree in not Is_a(Branch, _x_0) || Ordinal.( << ) (Ordinal.Int _x_1) (Ordinal.Int _x_2) || not (Is_a(Branch, tree) && (_x_2 >= 0) && (_x_1 >= 0)) expansions: [] rewrite_steps: forward_chaining:
• unroll
 expr: (|Ordinal.<<| (|Ordinal.Int_79/boot| (|count.bt_1257/client| (|get… expansions:
• unroll
 expr: (|count.bt_1257/client| (|get.Branch.right_519/server| tree_520/server)) expansions:
• unroll
 expr: (|count.bt_1257/client| tree_520/server) expansions:
• Unsat

In our function cbal, we always return Empty if n < 0. This suggests that we will want to have a predicate capturing the interesting case where the input to cbal is nonnegative, and a predicate for the zero or negative case.

In :
let nonnegative x = x >= 0;;
let leq_zero x = x <= 0;;

Out:
val nonnegative : discover_int -> discover_bool = <fun>
val leq_zero : discover_int -> discover_bool = <fun>


Now that we have the functions nodes and cbal, we should ask Discover to find some properties that may hold. Since cbal is only really interesting if the input is nonnegative, we invoke Discover with the labeled argument ~condition set to the string literal "nonnegative". This string argument lets Discover know to always instantiate a fixed variable with values satisfying the predicate we just defined. We specify nodes and cbal for investigation.

In :
discover db ~condition:"nonnegative" ["nodes";"cbal"];;

Out:
 <===DISCOVER===================================>
We are running Discover on the following signature:

mk_Empty:bt
mk_Branch:int->bt->bt->bt
nodes:bt->int
cbal:int->bt

We are running Discover with this inferred constant type:
type nonrec discover_type =
| Bool of discover_bool
| Int of discover_int
| Bt of discover_bt
<==============================================>
Running Discover on: discover_run
<===DISCOVER RESULTS===========================>
The below laws are the result of the condition: nonnegative x0
These are the 4 amazing conjectures suggested by Discover for discover_run.
fun x -> (nonnegative x) ==> (cbal (nodes mk_Empty)) = mk_Empty
fun x -> (nonnegative x) ==> (nodes (cbal x)) = x
fun x y z -> (nonnegative x) ==> (nodes (mk_Branch x z y)) = (nodes (mk_Branch x y z))
fun u x y z -> (nonnegative x) ==> (nodes (mk_Branch (nodes u) y z)) = (nodes (mk_Branch x y z))
These are SUBSUMED laws that may be interesting to the user.
No subsumed conjectures.
<==============================================>
A string list discover_result with the conjectures before filtering has been defined.
A string list discover_result_simplified contains the conjectures after simplification by Imandra.
- : unit = ()


Great, Discover suggests that the balanced binary trees produced by cbal have the correct number of nodes! It's often helpful to tweak the lemmas suggested by Discover. In this case we'll replace the predicate condition with its body. Let's have Imandra prove it.

In :
lemma discover__0 x0 = x0 >= 0 ==> (nodes (cbal x0)) = x0   [@@auto];;

Out:
val discover__0 : discover_int -> discover_bool = <fun>
Goal:

x0 >= 0 ==> nodes (cbal x0) = x0.

1 nontautological subgoal.

Subgoal 1:

H0. x0 >= 0
|---------------------------------------------------------------------------
nodes (cbal x0) = x0

Must try induction.

We shall induct according to a scheme derived from cbal.

Induction scheme:

(not (not (1 = x0) && (not (0 = x0) && not (x0 < 0))) ==> φ x0)
&& (not (x0 < 0)
&& (not (0 = x0)
&& (not (1 = x0)
&& (φ (rhs_split (x0 - 1)) && φ (lhs_split (x0 - 1)))))
==> φ x0).

2 nontautological subgoals.

Subgoal 1.2:

H0. x0 >= 0
|---------------------------------------------------------------------------
C0. not (1 = x0) && not (0 = x0) && (0 <= x0)
C1. nodes (cbal x0) = x0

But simplification reduces this to true, using the definitions of cbal and
nodes.

Subgoal 1.1:

H0. 0 <= x0
H1. not (0 = x0)
H2. not (1 = x0)
H3. x0 + (-1) * (((-1) + x0) / 2) >= 1
==> nodes (cbal ((-1) + x0 + (-1) * (((-1) + x0) / 2)))
= (-1) + x0 + (-1) * (((-1) + x0) / 2)
H4. ((-1) + x0) / 2 >= 0
==> nodes (cbal (((-1) + x0) / 2)) = ((-1) + x0) / 2
H5. x0 >= 0
|---------------------------------------------------------------------------
nodes (cbal x0) = x0

But simplification reduces this to true, using the definitions of cbal and
nodes.

ⓘ  Rules:
(:def cbal)
(:def nodes)
(:induct cbal)


Proved
proof
 ground_instances: 0 definitions: 6 inductions: 1 search_time: 0.350s
Expand
• start[0.350s, "Goal"]
( :var_0: ) >= 0 ==> nodes (cbal ( :var_0: )) = ( :var_0: )
• #### subproof

not (x0 >= 0) || (nodes (cbal x0) = x0)
• start[0.350s, "1"] not (x0 >= 0) || (nodes (cbal x0) = x0)
• induction on (functional ?)
:scheme (not (not (1 = x0) && (not (0 = x0) && not (x0 < 0))) ==> φ x0)
&& (not (x0 < 0)
&& (not (0 = x0)
&& (not (1 = x0)
&& (φ (rhs_split (x0 - 1)) && φ (lhs_split (x0 - 1)))))
==> φ x0)
• Split (let (_x_0 : bool) = not (1 = x0) in
let (_x_1 : bool) = not (0 = x0) in
let (_x_2 : bool) = 0 <= x0 in
let (_x_3 : bool) = nodes (cbal x0) = x0 in
let (_x_4 : bool) = not (x0 >= 0) in
let (_x_5 : int) = (-1) + x0 in
let (_x_6 : int) = _x_5 / 2 in
let (_x_7 : int) = (-1) * _x_6 in
let (_x_8 : int) = _x_5 + _x_7 in
((_x_0 && _x_1 && _x_2) || _x_3 || _x_4)
&& (not
(_x_2 && _x_1 && _x_0
&& (not (x0 + _x_7 >= 1) || (nodes (cbal _x_8) = _x_8))
&& (not (_x_6 >= 0) || (nodes (cbal _x_6) = _x_6)))
|| _x_3 || _x_4)
:cases [not (x0 >= 0) || (not (1 = x0) && not (0 = x0) && (0 <= x0))
|| (nodes (cbal x0) = x0);
let (_x_0 : int) = (-1) + x0 in
let (_x_1 : int) = _x_0 / 2 in
let (_x_2 : int) = (-1) * _x_1 in
let (_x_3 : int) = _x_0 + _x_2 in
not (0 <= x0) || (0 = x0) || (1 = x0)
|| not (x0 + _x_2 >= 1 ==> nodes (cbal _x_3) = _x_3)
|| not (_x_1 >= 0 ==> nodes (cbal _x_1) = _x_1)
|| not (x0 >= 0) || (nodes (cbal x0) = x0)])
• ##### subproof
let (_x_0 : int) = (-1) + x0 in let (_x_1 : int) = _x_0 / 2 in let (_x_2 : int) = (-1) * _x_1 in let (_x_3 : int) = _x_0 + _x_2 in not (0 <= x0) || (0 = x0) || (1 = x0) || not (x0 + _x_2 >= 1 ==> nodes (cbal _x_3) = _x_3) || not (_x_1 >= 0 ==> nodes (cbal _x_1) = _x_1) || not (x0 >= 0) || (nodes (cbal x0) = x0)
• start[0.109s, "1.1"]
let (_x_0 : int) = (-1) + x0 in
let (_x_1 : int) = _x_0 / 2 in
let (_x_2 : int) = (-1) * _x_1 in
let (_x_3 : int) = _x_0 + _x_2 in
not (0 <= x0) || (0 = x0) || (1 = x0)
|| not (x0 + _x_2 >= 1 ==> nodes (cbal _x_3) = _x_3)
|| not (_x_1 >= 0 ==> nodes (cbal _x_1) = _x_1) || not (x0 >= 0)
|| (nodes (cbal x0) = x0)
• ###### simplify
 into: true expansions: [nodes, cbal] rewrite_steps: forward_chaining:
• ##### subproof
not (x0 >= 0) || (not (1 = x0) && not (0 = x0) && (0 <= x0)) || (nodes (cbal x0) = x0)
• start[0.109s, "1.2"]
not (x0 >= 0) || (not (1 = x0) && not (0 = x0) && (0 <= x0))
|| (nodes (cbal x0) = x0)
• ###### simplify
 into: true expansions: [nodes, nodes, nodes, cbal] rewrite_steps: forward_chaining:

What about the zero or negative case?

In :
discover db ~condition:"leq_zero" ["nodes";"cbal";"Empty"];;

Out:
 <===DISCOVER===================================>
We are running Discover on the following signature:

Empty:bt
mk_Empty:bt
mk_Branch:int->bt->bt->bt
nodes:bt->int
cbal:int->bt

We are running Discover with this inferred constant type:
type nonrec discover_type =
| Bool of discover_bool
| Int of discover_int
| Bt of discover_bt
<==============================================>
Running Discover on: discover_run
<===DISCOVER RESULTS===========================>
The below laws are the result of the condition: leq_zero x0
These are the 5 amazing conjectures suggested by Discover for discover_run.
fun x -> (leq_zero x) ==> mk_Empty = Empty
fun x -> (leq_zero x) ==> (cbal x) = Empty
fun x y -> (leq_zero x) ==> (nodes (mk_Branch y Empty Empty)) = (nodes (mk_Branch x Empty Empty))
fun x y z -> (leq_zero x) ==> (nodes (mk_Branch x z y)) = (nodes (mk_Branch x y z))
fun u x y z -> (leq_zero x) ==> (nodes (mk_Branch (nodes u) y z)) = (nodes (mk_Branch x y z))
These are SUBSUMED laws that may be interesting to the user.
No subsumed conjectures.
<==============================================>
A string list discover_result with the conjectures before filtering has been defined.
A string list discover_result_simplified contains the conjectures after simplification by Imandra.
- : unit = ()


Discover suggests exactly what cbal does in the less than or equal to zero case, so we can have Imandra prove this as well.

In :
lemma discover__0_neg x0 = x0 <= 0 ==> (cbal x0) = Empty [@@auto];;

Out:
val discover__0_neg : discover_int -> discover_bool = <fun>
Goal:

x0 <= 0 ==> cbal x0 = Empty.

1 nontautological subgoal.

Subgoal 1:

H0. x0 <= 0
|---------------------------------------------------------------------------
cbal x0 = Empty

But simplification reduces this to true, using the definition of cbal.

ⓘ  Rules:
(:def cbal)


Proved
proof
 ground_instances: 0 definitions: 1 inductions: 0 search_time: 0.014s
Expand
• start[0.014s, "Goal"] ( :var_0: ) <= 0 ==> cbal ( :var_0: ) = Empty
• #### subproof

not (x0 <= 0) || (cbal x0 = Empty)
• start[0.013s, "1"] not (x0 <= 0) || (cbal x0 = Empty)
• ##### simplify
 into: true expansions: cbal rewrite_steps: forward_chaining:

We were interested in verifying that the trees produced by cbal are actually balanced, so here is a predicate capturing that idea.

In :
let is_balanced tree =
match tree with
| Empty -> true
| Branch {left; right; _} ->
let lnodes = nodes left in
let rnodes = nodes right in
rnodes = lnodes || rnodes - lnodes = 1;;

Out:
val is_balanced : discover_bt -> discover_bool = <fun>


Now we can ask Discover to find a relationship between is_balanced, cbal, and true. We include true so that Discover can suggest predicates as equations. Similarly, you can include false to find things that don't hold.

In :
discover db ["is_balanced";"cbal";"true"];;

Out:
 <===DISCOVER===================================>
We are running Discover on the following signature:

true:bool
mk_Empty:bt
mk_Branch:int->bt->bt->bt
is_balanced:bt->bool
cbal:int->bt

We are running Discover with this inferred constant type:
type nonrec discover_type =
| Bool of discover_bool
| Int of discover_int
| Bt of discover_bt
<==============================================>
Running Discover on: discover_run
<===DISCOVER RESULTS===========================>
The below laws are the result of the condition: No condition. These are the 3 amazing conjectures suggested by Discover for discover_run.
(is_balanced mk_Empty) = true
fun x -> (is_balanced (cbal x)) = true
fun x y -> (is_balanced (mk_Branch x y y)) = true
These are SUBSUMED laws that may be interesting to the user.
No subsumed conjectures.
<==============================================>
A string list discover_result with the conjectures before filtering has been defined.
A string list discover_result_simplified contains the conjectures after simplification by Imandra.
- : unit = ()


Discover suggests that every tree produced by cbal is balanced. We can prove this too!

In :
lemma discover_cbal_balanced_0 x0 = x0 >= 0 ==> (is_balanced (cbal x0)) [@@auto];;

Out:
val discover_cbal_balanced_0 : discover_int -> discover_bool = <fun>
Goal:

x0 >= 0 ==> is_balanced (cbal x0).

1 nontautological subgoal.

Subgoal 1:

H0. Is_a(Branch, cbal x0)
H1. x0 >= 0
|---------------------------------------------------------------------------
C0. nodes (Destruct(Branch, 2, cbal x0))
= nodes (Destruct(Branch, 1, cbal x0))
C1. nodes (Destruct(Branch, 2, cbal x0))
+ (-1) * nodes (Destruct(Branch, 1, cbal x0)) = 1

Must try induction.

We shall induct according to a scheme derived from cbal.

Induction scheme:

(not (not (1 = x0) && (not (0 = x0) && not (x0 < 0))) ==> φ x0)
&& (not (x0 < 0)
&& (not (0 = x0)
&& (not (1 = x0)
&& (φ (rhs_split (x0 - 1)) && φ (lhs_split (x0 - 1)))))
==> φ x0).

2 nontautological subgoals.

Subgoal 1.2:

H0. x0 >= 0
H1. Is_a(Branch, cbal x0)
|---------------------------------------------------------------------------
C0. not (1 = x0) && not (0 = x0) && (0 <= x0)
C1. nodes (Destruct(Branch, 2, cbal x0))
= nodes (Destruct(Branch, 1, cbal x0))
C2. nodes (Destruct(Branch, 2, cbal x0))
+ (-1) * nodes (Destruct(Branch, 1, cbal x0)) = 1

But simplification reduces this to true, using the definitions of cbal and
nodes.

Subgoal 1.1:

H0. 0 <= x0
H1. not (0 = x0)
H2. not (1 = x0)
H3. not (x0 + (-1) * (((-1) + x0) / 2) >= 1)
|| (nodes
(Destruct(Branch, 2, cbal ((-1) + x0 + (-1) * (((-1) + x0) / 2))))
= nodes
(Destruct(Branch, 1, cbal ((-1) + x0 + (-1) * (((-1) + x0) / 2)))))
|| not Is_a(Branch, cbal ((-1) + x0 + (-1) * (((-1) + x0) / 2)))
|| (nodes
(Destruct(Branch, 2, cbal ((-1) + x0 + (-1) * (((-1) + x0) / 2))))
+ (-1)
* nodes
(Destruct(Branch, 1, cbal ((-1) + x0 + (-1) * (((-1) + x0) / 2))))
= 1)
H4. not Is_a(Branch, cbal (((-1) + x0) / 2))
|| (nodes (Destruct(Branch, 2, cbal (((-1) + x0) / 2)))
= nodes (Destruct(Branch, 1, cbal (((-1) + x0) / 2))))
|| not (((-1) + x0) / 2 >= 0)
|| (nodes (Destruct(Branch, 2, cbal (((-1) + x0) / 2)))
+ (-1) * nodes (Destruct(Branch, 1, cbal (((-1) + x0) / 2))) = 1)
H5. x0 >= 0
H6. Is_a(Branch, cbal x0)
|---------------------------------------------------------------------------
C0. nodes (Destruct(Branch, 2, cbal x0))
= nodes (Destruct(Branch, 1, cbal x0))
C1. nodes (Destruct(Branch, 2, cbal x0))
+ (-1) * nodes (Destruct(Branch, 1, cbal x0)) = 1

This simplifies, using the definitions of cbal and nodes to the following 8
subgoals:

Subgoal 1.1.8:

H0. Is_a(Branch, cbal (((-1) + x0) / 2))
H1. 0 <= x0
H2. nodes (Destruct(Branch, 2, cbal (((-1) + x0) / 2)))
+ (-1) * nodes (Destruct(Branch, 1, cbal (((-1) + x0) / 2))) = 1
|---------------------------------------------------------------------------
C0. (-1)
= nodes (Destruct(Branch, 1, cbal (((-1) + x0) / 2)))
+ nodes (Destruct(Branch, 2, cbal (((-1) + x0) / 2)))
C1. nodes (Destruct(Branch, 2, cbal (((-1) + x0) / 2)))
= nodes (Destruct(Branch, 1, cbal (((-1) + x0) / 2)))
C2. Is_a(Branch, cbal ((-1) + x0 + (-1) * (((-1) + x0) / 2)))
C3. (-1) * nodes (Destruct(Branch, 1, cbal (((-1) + x0) / 2)))
+ (-1) * nodes (Destruct(Branch, 2, cbal (((-1) + x0) / 2))) = 2
C4. 0 = x0
C5. 1 = x0

This simplifies to:

Subgoal 1.1.8':

H0. Is_a(Branch, cbal (((-1) + x0) / 2))
H1. 0 <= x0
H2. nodes (Destruct(Branch, 2, cbal (((-1) + x0) / 2)))
+ (-1) * nodes (Destruct(Branch, 1, cbal (((-1) + x0) / 2))) = 1
|---------------------------------------------------------------------------
C0. (-1)
= nodes (Destruct(Branch, 1, cbal (((-1) + x0) / 2)))
+ nodes (Destruct(Branch, 2, cbal (((-1) + x0) / 2)))
C1. Is_a(Branch, cbal ((-1) + x0 + (-1) * (((-1) + x0) / 2)))
C2. 0 = x0

But we verify Subgoal 1.1.8' by recursive unrolling.

Subgoal 1.1.7:

H0. Is_a(Branch, cbal (((-1) + x0) / 2))
H1. 0 <= x0
H2. nodes (Destruct(Branch, 2, cbal (((-1) + x0) / 2)))
= nodes (Destruct(Branch, 1, cbal (((-1) + x0) / 2)))
|---------------------------------------------------------------------------
C0. (-1)
= nodes (Destruct(Branch, 1, cbal (((-1) + x0) / 2)))
+ nodes (Destruct(Branch, 2, cbal (((-1) + x0) / 2)))
C1. Is_a(Branch, cbal ((-1) + x0 + (-1) * (((-1) + x0) / 2)))
C2. (-1) * nodes (Destruct(Branch, 1, cbal (((-1) + x0) / 2)))
+ (-1) * nodes (Destruct(Branch, 2, cbal (((-1) + x0) / 2))) = 2
C3. 0 = x0
C4. 1 = x0

This simplifies to:

Subgoal 1.1.7':

H0. Is_a(Branch, cbal (((-1) + x0) / 2))
H1. 0 <= x0
H2. nodes (Destruct(Branch, 2, cbal (((-1) + x0) / 2)))
= nodes (Destruct(Branch, 1, cbal (((-1) + x0) / 2)))
|---------------------------------------------------------------------------
C0. Is_a(Branch, cbal ((-1) + x0 + (-1) * (((-1) + x0) / 2)))
C1. (-1) * nodes (Destruct(Branch, 1, cbal (((-1) + x0) / 2)))
+ (-1) * nodes (Destruct(Branch, 2, cbal (((-1) + x0) / 2))) = 2
C2. 0 = x0

But we verify Subgoal 1.1.7' by recursive unrolling.

Subgoal 1.1.6:

H0. nodes (Destruct(Branch, 2, cbal ((-1) + x0 + (-1) * (((-1) + x0) / 2))))
+ (-1)
* nodes
(Destruct(Branch, 1, cbal ((-1) + x0 + (-1) * (((-1) + x0) / 2))))
= 1
H1. 0 <= x0
H2. Is_a(Branch, cbal ((-1) + x0 + (-1) * (((-1) + x0) / 2)))
|---------------------------------------------------------------------------
C0. nodes (Destruct(Branch, 1, cbal ((-1) + x0 + (-1) * (((-1) + x0) / 2))))
+ nodes
(Destruct(Branch, 2, cbal ((-1) + x0 + (-1) * (((-1) + x0) / 2))))
= 0
C1. Is_a(Branch, cbal (((-1) + x0) / 2))
C2. nodes (Destruct(Branch, 1, cbal ((-1) + x0 + (-1) * (((-1) + x0) / 2))))
+ nodes
(Destruct(Branch, 2, cbal ((-1) + x0 + (-1) * (((-1) + x0) / 2))))
= (-1)
C3. nodes (Destruct(Branch, 2, cbal ((-1) + x0 + (-1) * (((-1) + x0) / 2))))
= nodes
(Destruct(Branch, 1, cbal ((-1) + x0 + (-1) * (((-1) + x0) / 2))))
C4. 0 = x0
C5. 1 = x0

This simplifies to:

Subgoal 1.1.6':

H0. nodes (Destruct(Branch, 2, cbal ((-1) + x0 + (-1) * (((-1) + x0) / 2))))
+ (-1)
* nodes
(Destruct(Branch, 1, cbal ((-1) + x0 + (-1) * (((-1) + x0) / 2))))
= 1
H1. 0 <= x0
H2. Is_a(Branch, cbal ((-1) + x0 + (-1) * (((-1) + x0) / 2)))
|---------------------------------------------------------------------------
C0. Is_a(Branch, cbal (((-1) + x0) / 2))
C1. nodes (Destruct(Branch, 1, cbal ((-1) + x0 + (-1) * (((-1) + x0) / 2))))
+ nodes
(Destruct(Branch, 2, cbal ((-1) + x0 + (-1) * (((-1) + x0) / 2))))
= (-1)
C2. 0 = x0

But we verify Subgoal 1.1.6' by recursive unrolling.

Subgoal 1.1.5:

H0. 0 <= x0
H1. Is_a(Branch, cbal ((-1) + x0 + (-1) * (((-1) + x0) / 2)))
H2. nodes (Destruct(Branch, 2, cbal ((-1) + x0 + (-1) * (((-1) + x0) / 2))))
= nodes
(Destruct(Branch, 1, cbal ((-1) + x0 + (-1) * (((-1) + x0) / 2))))
|---------------------------------------------------------------------------
C0. nodes (Destruct(Branch, 1, cbal ((-1) + x0 + (-1) * (((-1) + x0) / 2))))
+ nodes
(Destruct(Branch, 2, cbal ((-1) + x0 + (-1) * (((-1) + x0) / 2))))
= 0
C1. Is_a(Branch, cbal (((-1) + x0) / 2))
C2. nodes (Destruct(Branch, 1, cbal ((-1) + x0 + (-1) * (((-1) + x0) / 2))))
+ nodes
(Destruct(Branch, 2, cbal ((-1) + x0 + (-1) * (((-1) + x0) / 2))))
= (-1)
C3. 0 = x0
C4. 1 = x0

This simplifies to:

Subgoal 1.1.5':

H0. 0 <= x0
H1. Is_a(Branch, cbal ((-1) + x0 + (-1) * (((-1) + x0) / 2)))
H2. nodes (Destruct(Branch, 2, cbal ((-1) + x0 + (-1) * (((-1) + x0) / 2))))
= nodes
(Destruct(Branch, 1, cbal ((-1) + x0 + (-1) * (((-1) + x0) / 2))))
|---------------------------------------------------------------------------
C0. nodes (Destruct(Branch, 1, cbal ((-1) + x0 + (-1) * (((-1) + x0) / 2))))
+ nodes
(Destruct(Branch, 2, cbal ((-1) + x0 + (-1) * (((-1) + x0) / 2))))
= 0
C1. Is_a(Branch, cbal (((-1) + x0) / 2))
C2. 0 = x0

But we verify Subgoal 1.1.5' by recursive unrolling.

Subgoal 1.1.4:

H0. Is_a(Branch, cbal (((-1) + x0) / 2))
H1. nodes (Destruct(Branch, 2, cbal ((-1) + x0 + (-1) * (((-1) + x0) / 2))))
+ (-1)
* nodes
(Destruct(Branch, 1, cbal ((-1) + x0 + (-1) * (((-1) + x0) / 2))))
= 1
H2. 0 <= x0
H3. Is_a(Branch, cbal ((-1) + x0 + (-1) * (((-1) + x0) / 2)))
H4. nodes (Destruct(Branch, 2, cbal (((-1) + x0) / 2)))
+ (-1) * nodes (Destruct(Branch, 1, cbal (((-1) + x0) / 2))) = 1
|---------------------------------------------------------------------------
C0. nodes (Destruct(Branch, 1, cbal ((-1) + x0 + (-1) * (((-1) + x0) / 2))))
+ nodes
(Destruct(Branch, 2, cbal ((-1) + x0 + (-1) * (((-1) + x0) / 2))))
= nodes (Destruct(Branch, 1, cbal (((-1) + x0) / 2)))
+ nodes (Destruct(Branch, 2, cbal (((-1) + x0) / 2)))
C1. nodes (Destruct(Branch, 2, cbal (((-1) + x0) / 2)))
= nodes (Destruct(Branch, 1, cbal (((-1) + x0) / 2)))
C2. nodes (Destruct(Branch, 1, cbal ((-1) + x0 + (-1) * (((-1) + x0) / 2))))
+ nodes
(Destruct(Branch, 2, cbal ((-1) + x0 + (-1) * (((-1) + x0) / 2))))
+ (-1) * nodes (Destruct(Branch, 1, cbal (((-1) + x0) / 2)))
+ (-1) * nodes (Destruct(Branch, 2, cbal (((-1) + x0) / 2))) = 1
C3. nodes (Destruct(Branch, 2, cbal ((-1) + x0 + (-1) * (((-1) + x0) / 2))))
= nodes
(Destruct(Branch, 1, cbal ((-1) + x0 + (-1) * (((-1) + x0) / 2))))
C4. 0 = x0
C5. 1 = x0

This simplifies to:

Subgoal 1.1.4':

H0. Is_a(Branch, cbal (((-1) + x0) / 2))
H1. nodes (Destruct(Branch, 2, cbal ((-1) + x0 + (-1) * (((-1) + x0) / 2))))
+ (-1)
* nodes
(Destruct(Branch, 1, cbal ((-1) + x0 + (-1) * (((-1) + x0) / 2))))
= 1
H2. 0 <= x0
H3. Is_a(Branch, cbal ((-1) + x0 + (-1) * (((-1) + x0) / 2)))
H4. nodes (Destruct(Branch, 2, cbal (((-1) + x0) / 2)))
+ (-1) * nodes (Destruct(Branch, 1, cbal (((-1) + x0) / 2))) = 1
|---------------------------------------------------------------------------
C0. nodes (Destruct(Branch, 1, cbal ((-1) + x0 + (-1) * (((-1) + x0) / 2))))
+ nodes
(Destruct(Branch, 2, cbal ((-1) + x0 + (-1) * (((-1) + x0) / 2))))
= nodes (Destruct(Branch, 1, cbal (((-1) + x0) / 2)))
+ nodes (Destruct(Branch, 2, cbal (((-1) + x0) / 2)))
C1. 0 = x0

But we verify Subgoal 1.1.4' by recursive unrolling.

Subgoal 1.1.3:

H0. Is_a(Branch, cbal (((-1) + x0) / 2))
H1. nodes (Destruct(Branch, 2, cbal ((-1) + x0 + (-1) * (((-1) + x0) / 2))))
+ (-1)
* nodes
(Destruct(Branch, 1, cbal ((-1) + x0 + (-1) * (((-1) + x0) / 2))))
= 1
H2. 0 <= x0
H3. nodes (Destruct(Branch, 2, cbal (((-1) + x0) / 2)))
= nodes (Destruct(Branch, 1, cbal (((-1) + x0) / 2)))
H4. Is_a(Branch, cbal ((-1) + x0 + (-1) * (((-1) + x0) / 2)))
|---------------------------------------------------------------------------
C0. nodes (Destruct(Branch, 1, cbal ((-1) + x0 + (-1) * (((-1) + x0) / 2))))
+ nodes
(Destruct(Branch, 2, cbal ((-1) + x0 + (-1) * (((-1) + x0) / 2))))
= nodes (Destruct(Branch, 1, cbal (((-1) + x0) / 2)))
+ nodes (Destruct(Branch, 2, cbal (((-1) + x0) / 2)))
C1. nodes (Destruct(Branch, 1, cbal ((-1) + x0 + (-1) * (((-1) + x0) / 2))))
+ nodes
(Destruct(Branch, 2, cbal ((-1) + x0 + (-1) * (((-1) + x0) / 2))))
+ (-1) * nodes (Destruct(Branch, 1, cbal (((-1) + x0) / 2)))
+ (-1) * nodes (Destruct(Branch, 2, cbal (((-1) + x0) / 2))) = 1
C2. nodes (Destruct(Branch, 2, cbal ((-1) + x0 + (-1) * (((-1) + x0) / 2))))
= nodes
(Destruct(Branch, 1, cbal ((-1) + x0 + (-1) * (((-1) + x0) / 2))))
C3. 0 = x0
C4. 1 = x0

This simplifies to:

Subgoal 1.1.3':

H0. Is_a(Branch, cbal (((-1) + x0) / 2))
H1. nodes (Destruct(Branch, 2, cbal ((-1) + x0 + (-1) * (((-1) + x0) / 2))))
+ (-1)
* nodes
(Destruct(Branch, 1, cbal ((-1) + x0 + (-1) * (((-1) + x0) / 2))))
= 1
H2. 0 <= x0
H3. nodes (Destruct(Branch, 2, cbal (((-1) + x0) / 2)))
= nodes (Destruct(Branch, 1, cbal (((-1) + x0) / 2)))
H4. Is_a(Branch, cbal ((-1) + x0 + (-1) * (((-1) + x0) / 2)))
|---------------------------------------------------------------------------
C0. nodes (Destruct(Branch, 1, cbal ((-1) + x0 + (-1) * (((-1) + x0) / 2))))
+ nodes
(Destruct(Branch, 2, cbal ((-1) + x0 + (-1) * (((-1) + x0) / 2))))
+ (-1) * nodes (Destruct(Branch, 1, cbal (((-1) + x0) / 2)))
+ (-1) * nodes (Destruct(Branch, 2, cbal (((-1) + x0) / 2))) = 1
C1. 0 = x0

But we verify Subgoal 1.1.3' by recursive unrolling.

Subgoal 1.1.2:

H0. Is_a(Branch, cbal (((-1) + x0) / 2))
H1. 0 <= x0
H2. Is_a(Branch, cbal ((-1) + x0 + (-1) * (((-1) + x0) / 2)))
H3. nodes (Destruct(Branch, 2, cbal (((-1) + x0) / 2)))
+ (-1) * nodes (Destruct(Branch, 1, cbal (((-1) + x0) / 2))) = 1
H4. nodes (Destruct(Branch, 2, cbal ((-1) + x0 + (-1) * (((-1) + x0) / 2))))
= nodes
(Destruct(Branch, 1, cbal ((-1) + x0 + (-1) * (((-1) + x0) / 2))))
|---------------------------------------------------------------------------
C0. nodes (Destruct(Branch, 1, cbal ((-1) + x0 + (-1) * (((-1) + x0) / 2))))
+ nodes
(Destruct(Branch, 2, cbal ((-1) + x0 + (-1) * (((-1) + x0) / 2))))
= nodes (Destruct(Branch, 1, cbal (((-1) + x0) / 2)))
+ nodes (Destruct(Branch, 2, cbal (((-1) + x0) / 2)))
C1. nodes (Destruct(Branch, 2, cbal (((-1) + x0) / 2)))
= nodes (Destruct(Branch, 1, cbal (((-1) + x0) / 2)))
C2. nodes (Destruct(Branch, 1, cbal ((-1) + x0 + (-1) * (((-1) + x0) / 2))))
+ nodes
(Destruct(Branch, 2, cbal ((-1) + x0 + (-1) * (((-1) + x0) / 2))))
+ (-1) * nodes (Destruct(Branch, 1, cbal (((-1) + x0) / 2)))
+ (-1) * nodes (Destruct(Branch, 2, cbal (((-1) + x0) / 2))) = 1
C3. 0 = x0
C4. 1 = x0

This simplifies to:

Subgoal 1.1.2':

H0. Is_a(Branch, cbal (((-1) + x0) / 2))
H1. 0 <= x0
H2. Is_a(Branch, cbal ((-1) + x0 + (-1) * (((-1) + x0) / 2)))
H3. nodes (Destruct(Branch, 2, cbal (((-1) + x0) / 2)))
+ (-1) * nodes (Destruct(Branch, 1, cbal (((-1) + x0) / 2))) = 1
H4. nodes (Destruct(Branch, 2, cbal ((-1) + x0 + (-1) * (((-1) + x0) / 2))))
= nodes
(Destruct(Branch, 1, cbal ((-1) + x0 + (-1) * (((-1) + x0) / 2))))
|---------------------------------------------------------------------------
C0. nodes (Destruct(Branch, 1, cbal ((-1) + x0 + (-1) * (((-1) + x0) / 2))))
+ nodes
(Destruct(Branch, 2, cbal ((-1) + x0 + (-1) * (((-1) + x0) / 2))))
+ (-1) * nodes (Destruct(Branch, 1, cbal (((-1) + x0) / 2)))
+ (-1) * nodes (Destruct(Branch, 2, cbal (((-1) + x0) / 2))) = 1
C1. 0 = x0

But we verify Subgoal 1.1.2' by recursive unrolling.

Subgoal 1.1.1:

H0. Is_a(Branch, cbal (((-1) + x0) / 2))
H1. 0 <= x0
H2. nodes (Destruct(Branch, 2, cbal (((-1) + x0) / 2)))
= nodes (Destruct(Branch, 1, cbal (((-1) + x0) / 2)))
H3. Is_a(Branch, cbal ((-1) + x0 + (-1) * (((-1) + x0) / 2)))
H4. nodes (Destruct(Branch, 2, cbal ((-1) + x0 + (-1) * (((-1) + x0) / 2))))
= nodes
(Destruct(Branch, 1, cbal ((-1) + x0 + (-1) * (((-1) + x0) / 2))))
|---------------------------------------------------------------------------
C0. nodes (Destruct(Branch, 1, cbal ((-1) + x0 + (-1) * (((-1) + x0) / 2))))
+ nodes
(Destruct(Branch, 2, cbal ((-1) + x0 + (-1) * (((-1) + x0) / 2))))
= nodes (Destruct(Branch, 1, cbal (((-1) + x0) / 2)))
+ nodes (Destruct(Branch, 2, cbal (((-1) + x0) / 2)))
C1. nodes (Destruct(Branch, 1, cbal ((-1) + x0 + (-1) * (((-1) + x0) / 2))))
+ nodes
(Destruct(Branch, 2, cbal ((-1) + x0 + (-1) * (((-1) + x0) / 2))))
+ (-1) * nodes (Destruct(Branch, 1, cbal (((-1) + x0) / 2)))
+ (-1) * nodes (Destruct(Branch, 2, cbal (((-1) + x0) / 2))) = 1
C2. 0 = x0
C3. 1 = x0

This simplifies to:

Subgoal 1.1.1':

H0. Is_a(Branch, cbal (((-1) + x0) / 2))
H1. 0 <= x0
H2. nodes (Destruct(Branch, 2, cbal (((-1) + x0) / 2)))
= nodes (Destruct(Branch, 1, cbal (((-1) + x0) / 2)))
H3. Is_a(Branch, cbal ((-1) + x0 + (-1) * (((-1) + x0) / 2)))
H4. nodes (Destruct(Branch, 2, cbal ((-1) + x0 + (-1) * (((-1) + x0) / 2))))
= nodes
(Destruct(Branch, 1, cbal ((-1) + x0 + (-1) * (((-1) + x0) / 2))))
|---------------------------------------------------------------------------
C0. nodes (Destruct(Branch, 1, cbal ((-1) + x0 + (-1) * (((-1) + x0) / 2))))
+ nodes
(Destruct(Branch, 2, cbal ((-1) + x0 + (-1) * (((-1) + x0) / 2))))
= nodes (Destruct(Branch, 1, cbal (((-1) + x0) / 2)))
+ nodes (Destruct(Branch, 2, cbal (((-1) + x0) / 2)))
C1. 0 = x0

But we verify Subgoal 1.1.1' by recursive unrolling.

ⓘ  Rules:
(:def cbal)
(:def nodes)
(:induct cbal)


Proved
proof
ground_instances:44
definitions:23
inductions:1
search_time:
4.134s
details:
Expand
smt_stats:
 arith-assume-eqs: 23 arith-make-feasible: 373 arith-max-columns: 107 arith-conflicts: 20 arith-gcd-calls: 4 datatype occurs check: 310 arith-lower: 593 arith-diseq: 335 datatype splits: 153 arith-propagations: 265 arith-patches-success: 3 propagations: 2584 arith-patches: 4 interface eqs: 23 arith-bound-propagations-cheap: 265 conflicts: 105 datatype constructor ax: 290 final checks: 68 added eqs: 4110 del clause: 1841 arith-branch: 1 num checks: 26 rlimit count: 1.10198e+06 arith-cheap-eqs: 659 mk clause: 2456 mk bool var: 2539 decisions: 1117 arith-max-rows: 65 datatype accessor ax: 97 minimized lits: 28 arith-bound-propagations-lp: 62 arith eq adapter: 381 arith-upper: 609 time: 0.001 memory: 54.5 max memory: 54.5 num allocs: 6.27923e+10
Expand
• start[4.134s, "Goal"]
let (_x_0 : bt) = cbal ( :var_0: ) in
let (_x_1 : int) = nodes (Destruct(Branch, 2, _x_0)) in
let (_x_2 : int) = nodes (Destruct(Branch, 1, _x_0)) in
( :var_0: ) >= 0
==> (if Is_a(Branch, _x_0) then (_x_1 = _x_2) || (_x_1 - _x_2 = 1)
else true)
• #### subproof

let (_x_0 : bt) = cbal x0 in let (_x_1 : int) = nodes (Destruct(Branch, 2, _x_0)) in let (_x_2 : int) = nodes (Destruct(Branch, 1, _x_0)) in not Is_a(Branch, _x_0) || not (x0 >= 0) || (_x_1 = _x_2) || (_x_1 + (-1) * _x_2 = 1)
• start[4.133s, "1"]
let (_x_0 : bt) = cbal x0 in
let (_x_1 : int) = nodes (Destruct(Branch, 2, _x_0)) in
let (_x_2 : int) = nodes (Destruct(Branch, 1, _x_0)) in
not Is_a(Branch, _x_0) || not (x0 >= 0) || (_x_1 = _x_2)
|| (_x_1 + (-1) * _x_2 = 1)
• induction on (functional ?)
:scheme (not (not (1 = x0) && (not (0 = x0) && not (x0 < 0))) ==> φ x0)
&& (not (x0 < 0)
&& (not (0 = x0)
&& (not (1 = x0)
&& (φ (rhs_split (x0 - 1)) && φ (lhs_split (x0 - 1)))))
==> φ x0)
• Split (let (_x_0 : bool) = not (1 = x0) in
let (_x_1 : bool) = not (0 = x0) in
let (_x_2 : bool) = 0 <= x0 in
let (_x_3 : bt) = cbal x0 in
let (_x_4 : int) = nodes (Destruct(Branch, 2, _x_3)) in
let (_x_5 : int) = nodes (Destruct(Branch, 1, _x_3)) in
let (_x_6 : bool) = _x_4 = _x_5 in
let (_x_7 : bool) = _x_4 + (-1) * _x_5 = 1 in
let (_x_8 : bool) = not (x0 >= 0) in
let (_x_9 : bool) = not Is_a(Branch, _x_3) in
let (_x_10 : int) = (-1) + x0 in
let (_x_11 : int) = _x_10 / 2 in
let (_x_12 : int) = (-1) * _x_11 in
let (_x_13 : bt) = cbal (_x_10 + _x_12) in
let (_x_14 : int) = nodes (Destruct(Branch, 2, _x_13)) in
let (_x_15 : int) = nodes (Destruct(Branch, 1, _x_13)) in
let (_x_16 : bt) = cbal _x_11 in
let (_x_17 : int) = nodes (Destruct(Branch, 2, _x_16)) in
let (_x_18 : int) = nodes (Destruct(Branch, 1, _x_16)) in
((_x_0 && _x_1 && _x_2) || _x_6 || _x_7 || _x_8 || _x_9)
&& (not
(_x_2 && _x_1 && _x_0
&& (not (x0 + _x_12 >= 1) || (_x_14 = _x_15)
|| not Is_a(Branch, _x_13) || (_x_14 + (-1) * _x_15 = 1))
&& (not Is_a(Branch, _x_16) || (_x_17 = _x_18)
|| not (_x_11 >= 0) || (_x_17 + (-1) * _x_18 = 1)))
|| _x_6 || _x_7 || _x_8 || _x_9)
:cases [let (_x_0 : bt) = cbal x0 in
let (_x_1 : int) = nodes (Destruct(Branch, 2, _x_0)) in
let (_x_2 : int) = nodes (Destruct(Branch, 1, _x_0)) in
not (x0 >= 0) || not Is_a(Branch, _x_0)
|| (not (1 = x0) && not (0 = x0) && (0 <= x0))
|| (_x_1 = _x_2) || (_x_1 + (-1) * _x_2 = 1);
let (_x_0 : int) = (-1) + x0 in
let (_x_1 : int) = _x_0 / 2 in
let (_x_2 : int) = (-1) * _x_1 in
let (_x_3 : bt) = cbal (_x_0 + _x_2) in
let (_x_4 : int) = nodes (Destruct(Branch, 2, _x_3)) in
let (_x_5 : int) = nodes (Destruct(Branch, 1, _x_3)) in
let (_x_6 : bt) = cbal _x_1 in
let (_x_7 : int) = nodes (Destruct(Branch, 2, _x_6)) in
let (_x_8 : int) = nodes (Destruct(Branch, 1, _x_6)) in
let (_x_9 : bt) = cbal x0 in
let (_x_10 : int) = nodes (Destruct(Branch, 2, _x_9)) in
let (_x_11 : int) = nodes (Destruct(Branch, 1, _x_9)) in
not (0 <= x0) || (0 = x0) || (1 = x0)
|| not
(not (x0 + _x_2 >= 1) || (_x_4 = _x_5)
|| not Is_a(Branch, _x_3) || (_x_4 + (-1) * _x_5 = 1))
|| not
(not Is_a(Branch, _x_6) || (_x_7 = _x_8) || not (_x_1 >= 0)
|| (_x_7 + (-1) * _x_8 = 1))
|| not (x0 >= 0) || not Is_a(Branch, _x_9) || (_x_10 = _x_11)
|| (_x_10 + (-1) * _x_11 = 1)])
• ##### subproof
let (_x_0 : int) = (-1) + x0 in let (_x_1 : int) = _x_0 / 2 in let (_x_2 : int) = (-1) * _x_1 in let (_x_3 : bt) = cbal (_x_0 + _x_2) in let (_x_4 : int) = nodes (Destruct(Branch, 2, _x_3)) in let (_x_5 : int) = nodes (Destruct(Branch, 1, _x_3)) in let (_x_6 : bt) = cbal _x_1 in let (_x_7 : int) = nodes (Destruct(Branch, 2, _x_6)) in let (_x_8 : int) = nodes (Destruct(Branch, 1, _x_6)) in let (_x_9 : bt) = cbal x0 in let (_x_10 : int) = nodes (Destruct(Branch, 2, _x_9)) in let (_x_11 : int) = nodes (Destruct(Branch, 1, _x_9)) in not (0 <= x0) || (0 = x0) || (1 = x0) || not (not (x0 + _x_2 >= 1) || (_x_4 = _x_5) || not Is_a(Branch, _x_3) || (_x_4 + (-1) * _x_5 = 1)) || not (not Is_a(Branch, _x_6) || (_x_7 = _x_8) || not (_x_1 >= 0) || (_x_7 + (-1) * _x_8 = 1)) || not (x0 >= 0) || not Is_a(Branch, _x_9) || (_x_10 = _x_11) || (_x_10 + (-1) * _x_11 = 1)
• start[3.848s, "1.1"]
let (_x_0 : int) = (-1) + x0 in
let (_x_1 : int) = _x_0 / 2 in
let (_x_2 : int) = (-1) * _x_1 in
let (_x_3 : bt) = cbal (_x_0 + _x_2) in
let (_x_4 : int) = nodes (Destruct(Branch, 2, _x_3)) in
let (_x_5 : int) = nodes (Destruct(Branch, 1, _x_3)) in
let (_x_6 : bt) = cbal _x_1 in
let (_x_7 : int) = nodes (Destruct(Branch, 2, _x_6)) in
let (_x_8 : int) = nodes (Destruct(Branch, 1, _x_6)) in
let (_x_9 : bt) = cbal x0 in
let (_x_10 : int) = nodes (Destruct(Branch, 2, _x_9)) in
let (_x_11 : int) = nodes (Destruct(Branch, 1, _x_9)) in
not (0 <= x0) || (0 = x0) || (1 = x0)
|| not
(not (x0 + _x_2 >= 1) || (_x_4 = _x_5) || not Is_a(Branch, _x_3)
|| (_x_4 + (-1) * _x_5 = 1))
|| not
(not Is_a(Branch, _x_6) || (_x_7 = _x_8) || not (_x_1 >= 0)
|| (_x_7 + (-1) * _x_8 = 1))
|| not (x0 >= 0) || not Is_a(Branch, _x_9) || (_x_10 = _x_11)
|| (_x_10 + (-1) * _x_11 = 1)
• ###### simplify
 into: let (_x_0 : int) = (-1) + x0 in let (_x_1 : int) = _x_0 / 2 in let (_x_2 : bt) = cbal _x_1 in let (_x_3 : bool) = Is_a(Branch, _x_2) in let (_x_4 : bool) = not _x_3 in let (_x_5 : int) = nodes (Destruct(Branch, 1, _x_2)) in let (_x_6 : int) = nodes (Destruct(Branch, 2, _x_2)) in let (_x_7 : int) = _x_5 + _x_6 in let (_x_8 : bool) = not (0 <= x0) in let (_x_9 : bool) = _x_4 || ((-1) = _x_7) || _x_8 in let (_x_10 : bool) = _x_6 = _x_5 in let (_x_11 : bt) = cbal (_x_0 + (-1) * _x_1) in let (_x_12 : bool) = Is_a(Branch, _x_11) in let (_x_13 : int) = (-1) * _x_5 in let (_x_14 : bool) = not (_x_6 + _x_13 = 1) in let (_x_15 : int) = (-1) * _x_6 in let (_x_16 : bool) = _x_13 + _x_15 = 2 in let (_x_17 : bool) = 0 = x0 in let (_x_18 : bool) = 1 = x0 in let (_x_19 : bool) = not _x_10 in let (_x_20 : int) = nodes (Destruct(Branch, 1, _x_11)) in let (_x_21 : int) = nodes (Destruct(Branch, 2, _x_11)) in let (_x_22 : int) = _x_20 + _x_21 in let (_x_23 : bool) = (_x_22 = 0) || _x_3 in let (_x_24 : bool) = not (_x_21 + (-1) * _x_20 = 1) in let (_x_25 : bool) = _x_22 = (-1) in let (_x_26 : bool) = _x_21 = _x_20 in let (_x_27 : bool) = not _x_12 in let (_x_28 : bool) = not _x_26 in let (_x_29 : bool) = _x_4 || _x_24 || _x_8 in let (_x_30 : bool) = _x_22 = _x_7 in let (_x_31 : bool) = _x_22 + _x_13 + _x_15 = 1 in let (_x_32 : bool) = _x_4 || _x_8 in (_x_9 || _x_10 || _x_12 || _x_14 || _x_16 || _x_17 || _x_18) && (_x_9 || _x_19 || _x_12 || _x_16 || _x_17 || _x_18) && (_x_23 || _x_24 || _x_8 || _x_25 || _x_26 || _x_27 || _x_17 || _x_18) && (_x_23 || _x_8 || _x_25 || _x_27 || _x_28 || _x_17 || _x_18) && (_x_29 || _x_30 || _x_10 || _x_31 || _x_26 || _x_27 || _x_14 || _x_17 || _x_18) && (_x_29 || _x_19 || _x_30 || _x_31 || _x_26 || _x_27 || _x_17 || _x_18) && (_x_32 || _x_30 || _x_10 || _x_31 || _x_27 || _x_14 || _x_28 || _x_17 || _x_18) && (_x_32 || _x_19 || _x_30 || _x_31 || _x_27 || _x_28 || _x_17 || _x_18) expansions: [nodes, nodes, cbal, nodes, nodes, cbal, nodes, nodes, cbal, nodes, nodes, cbal, nodes, nodes, cbal, cbal] rewrite_steps: forward_chaining:
• Subproof
• Subproof
• Subproof
• Subproof
• Subproof
• Subproof
• Subproof
• Subproof
• ##### subproof
let (_x_0 : bt) = cbal x0 in let (_x_1 : int) = nodes (Destruct(Branch, 2, _x_0)) in let (_x_2 : int) = nodes (Destruct(Branch, 1, _x_0)) in not (x0 >= 0) || not Is_a(Branch, _x_0) || (not (1 = x0) && not (0 = x0) && (0 <= x0)) || (_x_1 = _x_2) || (_x_1 + (-1) * _x_2 = 1)
• start[3.848s, "1.2"]
let (_x_0 : bt) = cbal x0 in
let (_x_1 : int) = nodes (Destruct(Branch, 2, _x_0)) in
let (_x_2 : int) = nodes (Destruct(Branch, 1, _x_0)) in
not (x0 >= 0) || not Is_a(Branch, _x_0)
|| (not (1 = x0) && not (0 = x0) && (0 <= x0)) || (_x_1 = _x_2)
|| (_x_1 + (-1) * _x_2 = 1)
• ###### simplify
 into: true expansions: [nodes, nodes, cbal, nodes, nodes, cbal, cbal] rewrite_steps: forward_chaining:

In this demonstration we used Discover to suggest conjectures and lemmas used in the verification of some properties of balanced binary trees. We also showed examples of using conditions with Discover and some basic pointers on its use.