blob: f3d1984834874b3956d6aa4c834bcb17738bcd26 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
|
module Theorems
import Data.Vect
%default total
fiveIsFive : 5 = 5
fiveIsFive = Refl
plusReduces : (n:Nat) -> plus Z n = n
plusReduces n = Refl
plusReducesZ : (n:Nat) -> plus n Z = n
plusReducesZ Z = Refl
plusReducesZ (S k) = cong (plusReducesZ k)
plus' : Nat -> Nat -> Nat
plus' Z m = m
plus' (S k) m = S (plus' k m)
plus_commutes_Z : m = plus' m 0
plus_commutes_Z {m = Z} = Refl
plus_commutes_Z {m = (S k)} = rewrite plus_commutes_Z {m=k} in Refl
plus_commutes_S : (k,m : Nat) -> S (plus m k) = plus m (S k)
plus_commutes_S k Z = Refl
plus_commutes_S k (S j) = rewrite plus_commutes_S k j in Refl
plus_commutes : (n, m : Nat) -> plus' n m = plus' m n
plus_commutes Z m = plus_commutes_Z
plus_commutes (S k) m = rewrite plus_commutes k m in plus_commutes_S k m
plus_assoc : (n, m, k : Nat) -> plus' n (plus' m k) = plus' (plus' n m) k
plus_assoc Z m k = Refl
plus_assoc (S j) m k = rewrite plus_assoc j m k in Refl
same_lists : {xs : List a} -> {ys : List a} -> x = y -> xs = ys
-> x :: xs = y :: ys
same_lists {x = x} {y = x} {xs = ys} {ys = ys} Refl Refl = Refl
data ThreeEq : (x, y, z : Nat) -> Type where
Equals : ThreeEq x x x
allSameS : (x, y, z : Nat) -> ThreeEq x y z -> ThreeEq (S x) (S y) (S z)
allSameS z z z Equals = Equals
plusCommutes2 : (n : Nat) -> (m : Nat) -> n + m = m + n
plusCommutes2 Z m = rewrite plusZeroRightNeutral m in Refl
plusCommutes2 (S k) m = rewrite plusCommutes2 k m in
plusSuccRightSucc m k
headUnequal : DecEq a => {xs : Vect n a} -> {ys : Vect n a} ->
(contra : (x = y) -> Void) -> (x :: xs = y :: ys) -> Void
headUnequal contra Refl = contra Refl
tailUnequal : DecEq a => {xs : Vect n a} -> {ys : Vect n a} ->
(contra : (xs = ys) -> Void) -> ((x :: xs) = (y :: ys)) -> Void
tailUnequal contra Refl = contra Refl
[myimpl] DecEq a => DecEq (Vect n a) where
decEq [] [] = Yes Refl
decEq (x :: xs) (y :: ys) = case decEq x y of
Yes Refl => case decEq xs ys of
Yes Refl => Yes Refl
No contra => No (tailUnequal contra)
No contra => No (headUnequal contra)
data Last : List a -> a -> Type where
LastOne : Last [value] value
LastCons : (prf : Last xs value) -> Last (x :: xs) value
notInNil : (Last [] value) -> Void
notInNil LastOne impossible
notInNil (LastCons _) impossible
lastDiff : (x = y -> Void) -> Last [x] y -> Void
lastDiff contra LastOne = contra Refl
lastDiff contra (LastCons prf) = notInNil prf
isLast : DecEq a => (xs : List a) -> (value : a) -> Dec (Last xs value)
isLast [] value = No notInNil
isLast [x] value = case decEq x value of
Yes Refl => Yes LastOne
No contra => No (lastDiff contra)
isLast (x :: x' :: xs) value = case isLast (x' :: xs) value of
Yes prf => Yes (LastCons prf)
No contra => No (\(LastCons prf) => contra prf)
|
