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