lightning.idr

%default total
-- What's Idris?
-- * Dependently typed
-- * purely functional
-- * haskell-like syntax
-- Looks like this:

bottles : Nat -> String
bottles    Z    = "Buy more beer!"
bottles n@(S k) = show n ++
                  " bottles of beer on the wall, " ++
                  show n ++
                  " bottles of beer.\nTake one down, pass it around, " ++
                  show k ++
                  " bottles of beer on the wall.\n" ++
                  bottles k

-- Can prove theorems as well as write programs.
-- Theorems in general math and more to the point, about programs.

-- Equality!
data MyEq : {A, B : Type} -> (x : A) -> (y : B) -> Type where
  myRefl : MyEq x x

-- This is built in as =

fivePlusFiveIsTen : 5 + 5 `MyEq` 10
fivePlusFiveIsTen = myRefl

plusZeroIsIdentity : plus x 0 = x
plusZeroIsIdentity {x =  Z   } = Refl
plusZeroIsIdentity {x = (S k)} = eqSucc (plus k 0) k plusZeroIsIdentity

succPlusXYIsPlusXSuccY : S (plus x y) = plus x (S y)
succPlusXYIsPlusXSuccY {x = Z  } {y} = Refl
succPlusXYIsPlusXSuccY {x = S x} {y} = eqSucc _ _ succPlusXYIsPlusXSuccY

additionIsCommutative : plus x y = plus y x
additionIsCommutative {x = Z  } {y} = sym plusZeroIsIdentity
additionIsCommutative {x = S x} {y} = -- ?oqwieuc
     rewrite additionIsCommutative {x = x} {y = y} in succPlusXYIsPlusXSuccY

-- The actual bug I promised to talk about:
proofOfVoid : Void
proofOfVoid = (\Refl impossible) $ cong {f = (>0) . (1/)} $ the (-0.0 = 0.0) Refl

-- broken down:
zeroIsNegativeZero : 0.0 = -0.0
zeroIsNegativeZero = Refl

trueIsFalse : True = False
trueIsFalse = cong {f = (>0) . (1/)} zeroIsNegativeZero

trueIsFalseImpliesAnything : {a : Type} -> True = False -> a
trueIsFalseImpliesAnything Refl impossible

anything : {a : Type} -> a
anything = trueIsFalseImpliesAnything trueIsFalse

proofOfVoid' : Void
proofOfVoid' = anything

tenLTZero : LT 10 0
tenLTZero = anything

data Direction = Up | Down
data Color = Black | White

upIsDown : Up = Down
upIsDown = anything

blackIsWhite : Black = White
blackIsWhite = anything