fabian/veribase-idr2 - Change Z5TGJFFAN7TRV2SXI3RK2E6FL4XHGE4UDRCKNCNJ45KSCNXE6KUAC

AVLTree work

Created by fabian on June 24, 2021

Z5TGJFFAN7TRV2SXI3RK2E6FL4XHGE4UDRCKNCNJ45KSCNXE6KUAC

Dependencies

In channels

main

Change contents

Insertion in src/Data/Natural/ExtraOperations.idr at line 17 [2.6751]

[2.7080]

export
proofDiffGTEThenMinus : (x, y : Natural) -> x `GTE` y -> diff x y = minus x y
proofDiffGTEThenMinus x Zero _ = case x of
  Zero          => Refl
  (Succesor x') => Refl
proofDiffGTEThenMinus (Succesor x) (Succesor y) (SuccesorLTE p) =
  rewrite proofDiffGTEThenMinus x y p in Refl

Replacement in src/Data/AVLTree.idr at line 33 [4.160]

B:BD[4.1263] → [3.519:579]

  IsNode : {leftTree : AVLTree t leftHeight leftBounds {o}}

[4.1263]

[3.579]

  IsNode : {leftHeight, rightHeight : Natural}
         -> {leftTree : AVLTree t leftHeight leftBounds {o}}

Replacement in src/Data/AVLTree.idr at line 40 [4.160]

B:BD[3.930] → [3.930:1010]

         -> NonEmpty (Node leftTree pivot rightTree {leftHeight} {rightHeight})

[3.930]

[5.197]

         -> NonEmpty (Node leftTree pivot rightTree {leftHeight=leftHeight} {rightHeight=rightHeight})

Replacement in src/Data/AVLTree.idr at line 47 [4.160]

B:BD[5.337] → [3.1011:1080]

  IsRotatableLeft : {leftTree : AVLTree t leftHeight leftBounds {o}}

[5.337]

[3.1080]

  IsRotatableLeft : {leftHeight, rightHeight : Natural}
                  -> {leftTree : AVLTree t leftHeight leftBounds {o}}

Insertion in src/Data/AVLTree.idr at line 52 [4.160]

[5.490]

[3.1187]

                  -> {auto balanceFactor : leftHeight `LT` rightHeight}

Replacement in src/Data/AVLTree.idr at line 56 [4.160]

B:BD[3.1477] → [3.1477:1571]

                  -> RotatableLeft (Node leftTree pivot rightTree {leftHeight} {rightHeight})

[3.1477]

[5.631]

                  -> RotatableLeft (Node leftTree pivot rightTree {leftHeight=leftHeight} {rightHeight=rightHeight})

Replacement in src/Data/AVLTree.idr at line 59 [4.160]

B:BD[5.686] → [3.1572:2194]

  IsRotatableRight : {leftTree : AVLTree t leftHeight leftBounds {o}}
                  -> {pivot : t}
                  -> {rightTree : AVLTree t rightHeight rightBounds {o}}
                  -> {auto leftNonEmpty : NonEmpty leftTree}
                  -> {auto leftBound : (optional leftBounds  ((\b => LT @{o} b pivot) . Builtin.snd) Unit)}
                  -> {auto rightBound : (optional rightBounds ((\b => GT @{o} b pivot) . Builtin.fst) Unit)}
                  -> {auto height : diff leftHeight rightHeight `LTE` 1}
                  -> RotatableRight (Node leftTree pivot rightTree {leftHeight} {rightHeight})

[5.686]

[5.1047]

  IsRotatableRight : {leftHeight, rightHeight : Natural}
                   -> {leftTree : AVLTree t leftHeight leftBounds {o}}
                   -> {pivot : t}
                   -> {rightTree : AVLTree t rightHeight rightBounds {o}}
                   -> {auto leftNonEmpty : NonEmpty leftTree}
                   -> {auto balanceFactor : rightHeight `LT` leftHeight}
                   -> {auto leftBound : (optional leftBounds  ((\b => LT @{o} b pivot) . Builtin.snd) Unit)}
                   -> {auto rightBound : (optional rightBounds ((\b => GT @{o} b pivot) . Builtin.fst) Unit)}
                   -> {auto height : diff leftHeight rightHeight `LTE` 1}
                   -> RotatableRight (Node leftTree pivot rightTree {leftHeight=leftHeight} {rightHeight=rightHeight})

Replacement in src/Data/AVLTree.idr at line 70 [4.160]

B:BD[5.1048] → [5.1048:1144]

rotateLeft : (tree : AVLTree t h b {o}) -> {auto ok: RotatableLeft tree} -> AVLTree t h' b' {o}

[5.1048]

[5.1144]

rotateLeft : (tree : AVLTree t h b {o}) -> {auto ok: RotatableLeft tree} -> AVLTree t ?holeHeight (Some ?holeBounds) {o}

Replacement in src/Data/AVLTree.idr at line 74 [4.160]

B:BD[5.1332] → [3.2195:2241]

  IsRotatableLeft {height} => ?holeRotateLeft

[5.1332]

[5.1383]

  IsRotatableLeft {balanceFactor=ZeroLTEAny} impossible
  IsRotatableLeft {leftHeight} {rightHeight=Succesor (max rightLeftHeight rightRightHeight)} {balanceFactor=SuccesorLTE p} =>
    ?holeRotateLeft -- Node (Node treeA pivot1 treeB) pivot2 treeC -- rewrite proofDiffGTEThenMinus rightHeight leftHeight balanceFactor in ?holeRotateLeft