git.iko.soy/Idris-dev
on ef96397 help sign in
Idris-dev/tutorial/examples/theorems.idr
57 lines 1.1 kB history raw
2fiveIsFive : 5 = 5
3fiveIsFive = refl
5twoPlusTwo : 2 + 2 = 4
6twoPlusTwo = refl
8total disjoint : (n : Nat) -> O = S n -> _|_
9disjoint n p = replace {P = disjointTy} p ()
10 where
11 disjointTy : Nat -> Type
12 disjointTy O = ()
13 disjointTy (S k) = _|_
15total acyclic : (n : Nat) -> n = S n -> _|_
16acyclic O p = disjoint _ p
17acyclic (S k) p = acyclic k (succInjective _ _ p)
19empty1 : _|_
20empty1 = hd [] where
21 hd : List a -> a
22 hd (x :: xs) = x
24empty2 : _|_
25empty2 = empty2
27plusReduces : (n:Nat) -> plus O n = n
28plusReduces n = refl
30plusReducesO : (n:Nat) -> n = plus n O
31plusReducesO O = refl
32plusReducesO (S k) = cong (plusReducesO k)
34plusReducesS : (n:Nat) -> (m:Nat) -> S (plus n m) = plus n (S m)
35plusReducesS O m = refl
36plusReducesS (S k) m = cong (plusReducesS k m)
38plusReducesO' : (n:Nat) -> n = plus n O
39plusReducesO' O = ?plusredO_O
40plusReducesO' (S k) = let ih = plusReducesO' k in
41 ?plusredO_S
44---------- Proofs ----------
46plusredO_S = proof {
47 intro;
48 intro;
49 rewrite ih;
50 trivial;
53plusredO_O = proof {
54 compute;
55 trivial;