flip_tree_annotated.idr

module Tree

{-
background/why

goals:
    1. Given a tree, flip it horizontally
    2. prove flip (flip t) = t
        i.e. flip is its own inverse or that flip is an involution

given:
        1
       / \
      2   3
     / \
    4   5

return:
        1
       / \
      3   2
         / \
        5   4
-}

{-
the totality property:
    1. is important for proofs
    2. enforces program termination which means that
       a total language is not turing complete
    3. it means that every input has an output
-}
%default total

{-
A tree is made up of leaves and branches

1. A leaf doesn't contain any information.
2. A branch consists of a left tree, a value, and a right tree.

        branch
       /      \
    leaf      leaf
-}
data Tree : Type -> Type where
  Leaf : Tree a
  Branch : (ltree : Tree a) -> a -> (rtree : Tree a) -> Tree a

flip : Tree a -> Tree a
flip Leaf = Leaf
flip (Branch ltree x rtree) = Branch (flip rtree) x (flip ltree)

example : Tree Int
example = flip
    (Branch
        (Branch
            (Branch Leaf 4 Leaf)
            2
            (Branch Leaf 5 Leaf)
        )
        1
        (Branch Leaf 3 Leaf)
    )

||| Curry-Howard correspondence is an isomorphism between proofs and programs
||| 1. types are theorems (statements that are true)
||| 2. programs (function definitions) are proofs
|||
||| Full dependent types allow us to write types that depend on values
||| which are useful for proving properties.
flipFlip : (t : Tree a) -> flip (flip t) = t
-- leaf flipped twice is still a leaf
flipFlip Leaf = Refl
flipFlip (Branch ltree x rtree) =
  -- invoke the inductive hypothesis on ltree
  rewrite flipFlip ltree in
  -- invoke the IH on rtree
  rewrite flipFlip rtree in
          -- qed
          Refl

{-
some nice language features include

1. interactive theorem proving
2. given a type, give me a blank definition
3. given an empty definition, split the possible cases
4. given an empty definition, search for a proof (program) that inhabits the type
    - This means that you can have parts of your program generated for you!
5. write functions that take in a value (1) and return a type (String)

examples of cool things you can do
1. write a printf that is typesafe
    - e.g. printf("%s %s", "hi") will not compile
    - https://www.youtube.com/watch?v=fVBck2Zngjo
2. prove properties about distributed algorithms
    - https://news.ycombinator.com/item?id=10017549
    - Proof of linearizability in Raft using Coq
3. write proofs instead of tests
    - proofs prove a property and are stronger than a test
    - tests only show that certain cases work
4. [].first in ruby returns nil, you can make this a compile time error
5. when taking the ith element out of a list, you can make sure that the list
    has at least i elements in it, which removes (index out of bounds errors during runtime)
    and turning them into compile time errors
-}

{-
brew install ghc cabal-install
mkdir tree
cd tree
cabal update
cabal sandbox init
cabal install idris
.cabal-sandbox/bin/idris
-}