module Idris08 import Syntax.PreorderReasoning -- Start with definition of Is. data Is : Bool -> Type where OK : Is True -- We can define unit tests checked by the compiler. additionWorks : Is (3 + 4 == 7) additionWorks = OK reverse_test1 : Is (reverse [1,2,3] == [3,2,1]) reverse_test1 = OK mutual even : Nat -> Bool even Z = True even (S k) = odd k odd : Nat -> Bool odd Z = False odd (S k) = even k odd17 : Is (odd 17) odd17 = OK -- Inductive evidence. -- Even n is a *proof*/*evidence* that n is -- even. data Even : Nat -> Type where ZEven : Even 0 SSEven : Even n -> Even (S (S n)) -- It is possible to create a term of type -- Even n if and only if n is even. -- Let's prove that 6 is even. sixIsEven : Even 6 sixIsEven = SSEven (SSEven (SSEven ZEven)) -- use auto! sixIsEven' : Even 6 sixIsEven' = SSEven (SSEven (SSEven ZEven)) -- not possible! -- sevenIsEven : Even 7 -- sevenIsEven = SSEven (SSEven (SSEven ?rhs)) total plusEven : Even m -> Even n -> Even (m + n) plusEven ZEven y = y plusEven (SSEven x) y = SSEven (plusEven x y) nm2Even : Even (S (S n)) -> Even n nm2Even (SSEven x) = x -- Implicit parameters / forall / dependent functions nm2Even' : (n : Nat) -> Even (S (S n)) -> Even n nm2Even' Z x = ZEven nm2Even' (S Z) (SSEven ZEven) impossible nm2Even' (S Z) (SSEven (SSEven _)) impossible nm2Even' (S (S k)) (SSEven x) = x {- implication functions AND pairs forall dependent functions exists dependent pairs -} -- Dependent pairs -- Pairs where the *type* of the second -- component can depend on the *value* -- of the first. four : (n ** Even n) four = (4 ** SSEven (SSEven ZEven)) EvenNat : Type EvenNat = (n ** Even n) plus : EvenNat -> EvenNat -> EvenNat plus (m ** em) (n ** en) = (m + n ** plusEven em en) data ListN : Nat -> Type -> Type where Nil : ListN 0 a (::) : a -> ListN n a -> ListN (S n) a filter : (a -> Bool) -> ListN n a -> (m ** (ListN m a , LTE m n)) filter f [] = (0 ** ([], LTEZero)) filter f (x :: xs) with (filter f xs) filter f (x :: xs) | (m ** (xs' , mLTEn)) = if (f x) then (S m ** (x :: xs', (LTESucc mLTEn))) else (m ** (xs' , lteSuccRight mLTEn)) -- Equality -- data (=) : A -> B -> Type where -- Refl : x = x onePlusOne : (1 + 1 = 2) onePlusOne = Refl -- sym : (x = y) -> (y = x) -- sym Refl = Refl -- trans : (x = y) -> (y = z) -> (x = z) -- trans Refl Refl = Refl -- cong : (A , B : Type) -> (x , y : A) -> (f : A -> B) -> (x = y) -> (f x = f y) -- cong A B x x f Refl = Refl -- [C-c RET i -- show implicits] -- [C-c RET h -- hide implicits] -- prove symmetry, transitivity, congruence (then show std) -- plusZn plusnZ : (n : Nat) -> n + 0 = n plusnZ Z = Refl plusnZ (S k) = cong {f = S} (plusnZ k) plusnZ2 : (n : Nat) -> n + 0 = n plusnZ2 Z = Refl plusnZ2 (S k) = let IH = plusnZ2 k in rewrite IH in Refl plus_assoc : (x , y , z : Nat) -> (x + (y + z)) = ((x + y) + z) plus_assoc Z y z = Refl plus_assoc (S k) y z = cong (plus_assoc k y z) -- import Syntax.PreorderReasoning -- show definitions -- prove map (f . g) xs = (map f . map g) xs mapComp : (xs : List a) -> map (f . g) xs = (map f . map g) xs mapComp [] = Refl mapComp {f} {g} (x :: xs) = (map (f . g) (x :: xs)) ={ Refl }= ((f . g) x :: map (f . g) xs) ={ Refl }= (f (g x) :: map (f . g) xs) ={ cong (mapComp xs) }= (f (g x) :: (map f . map g) xs) ={ Refl }= (f (g x) :: map f (map g xs)) ={ Refl }= (map f (g x :: map g xs)) ={ Refl }= (map f (map g (x :: xs))) ={ Refl }= ((map f . map g) (x :: xs)) QED mapComp2 : (xs : List a) -> map (f . g) xs = (map f . map g) xs mapComp2 [] = Refl mapComp2 (x :: xs) = cong (mapComp xs) -- Nat fold. -- Dependent version. -- Same for lists.