[balanced_bst] AVL_treeTheory and fibonacciTheory (+fibmod3)

[binghe]

Hi,

This PR contains a slightly modified version of the AVL tree formalisation, by our student (Sineeha Kodwani) in the last year.

AVL tree is another balanced bst (binary search tree), perhaps nowadays is less famous than red-black trees. A valid AVL tree is a (finite) binary tree structure (defined by a datatype with constructors Tip and Bin) whose children heights differ by at most one:

[avl_def]
⊢ (avl Tip ⇔ T) ∧
  ∀bf k v l r.
    avl (Bin bf k v l r) ⇔
    (height l = height r ∨ height l = height r + 1 ∨ height r = height l + 1) ∧
    bf = &height r − &height l ∧ avl l ∧ avl r

It's not obvious from this definition that the height of AVL trees is logarithm to the number of nodes in it (for optimal searching performance), but if we define a function N(k) as the minimal number of nodes of all AVL trees whose height is k:

[N_def]
⊢ ∀k. N k = MIN_SET (IMAGE node_count {x | height x = k ∧ avl x})

Then we can prove the following recursive relation between different N(k) values and a elegant connection to the Fibonacci numbers:

[N_k]
⊢ ∀k. N (k + 2) = N (k + 1) + N k + 1

[N_fibonacci_relation]
⊢ ∀k. N k = fib (k + 2) − 1

It's known (but the proof is not mechanised here) that the Fibonacci numbers has the exponential upper/lower bounds [1,2], and thus the height of AVL trees is indeed logarithm to the number of nodes.

The work also correctly defines insert and delete operations to AVL tree, and have some test theorems showing the correctness on concrete AVL trees, but the correctness of these operations is not fully formalised. (The overall code quality is medium but the finished parts are all correct.)

I extracted from the original work all proofs about the Fibonacci number itself and created a dedicated fibonacciTheory, also under exampels/balanced_bst. It's not putting into arithmeticTheory or numberTheory because I also merged the existing small fibmod3Theory from examples/misc but the proof depends on intLib. I plan to formalise the exponential upper/lower bounds, but then real numbers will also involve. Therefore it's better (for now) just have a dedicated
fibonacciTheory in examples.

--Chun

[1] https://proofwiki.org/wiki/Fibonacci_Number_greater_than_Golden_Section_to_Power_less_Two
[2] https://proofwiki.org/wiki/Fibonacci_Number_less_than_Golden_Section_to_Power_less_One

[binghe]

The fibonacciTheory contains some proofs ported from HOL-Light. The new tactic ASM_ARITH_TAC in intLib is like ASM_REAL_ARITH_TAC vs REAL_ARITH_TAC, also learnt from HOL-Light.

The following new theorem TRANSITIVE_STEPWISE_LE (in arithmeticTheory) is also learnt from HOL-Light (only the name and statements):

   [TRANSITIVE_STEPWISE_LE]  Theorem      
      ⊢ ∀R. (∀x. R x x) ∧ (∀x y z. R x y ∧ R y z ⇒ R x z) ∧
            (∀n. R n (SUC n)) ⇒
            ∀m n. m ≤ n ⇒ R m n

whose proof is based on the existing transitive_monotone.