@@ -0,0 +1,96 @@
1+module scg
2+
3+%default total
4+
5+data Ord = Zero | Suc Ord | Sup (Nat -> Ord)
6+
7+natElim : (n : Nat) -> (P : Nat -> Set) ->
8+ (P O) -> ((n : Nat) -> (P n) -> (P (S n))) -> (P n)
9+natElim O P mO mS = mO
10+natElim (S k) P mO mS = mS k (natElim k P mO mS)
11+
12+ordElim : (x : Ord) ->
13+ (P : Ord -> Set) ->
14+ (P Zero) ->
15+ ((x : Ord) -> P x -> P (Suc x)) ->
16+ ((f : Nat -> Ord) -> ((n : Nat) -> P (f n)) ->
17+ P (Sup f)) -> P x
18+ordElim Zero P mZ mSuc mSup = mZ
19+ordElim (Suc o) P mZ mSuc mSup = mSuc o (ordElim o P mZ mSuc mSup)
20+ordElim (Sup f) P mZ mSuc mSup =
21+ mSup f (\n => ordElim (f n) P mZ mSuc mSup)
22+
23+myplus' : Nat -> Nat -> Nat
24+myplus : Nat -> Nat -> Nat
25+
26+myplus O y = y
27+myplus (S k) y = S (myplus' k y)
28+
29+myplus' O y = y
30+myplus' (S k) y = S (myplus y k)
31+
32+mnubBy : (a -> a -> Bool) -> List a -> List a
33+mnubBy = nubBy' []
34+ where
35+ nubBy' : List a -> (a -> a -> Bool) -> List a -> List a
36+ nubBy' acc p [] = []
37+ nubBy' acc p (x::xs) =
38+ if elemBy p x acc then
39+ nubBy' acc p xs
40+ else
41+ x :: nubBy' (x::acc) p xs
42+
43+partial
44+vtrans : Vect a n -> Vect a n -> List a
45+vtrans [] _ = []
46+vtrans (x :: xs) ys = x :: vtrans ys ys
47+
48+even : Nat -> Bool
49+even O = True
50+even (S k) = odd k
51+ where
52+ odd : Nat -> Bool
53+ odd O = False
54+ odd (S k) = even k
55+
56+ack : Nat -> Nat -> Nat
57+ack O n = S n
58+ack (S m) O = ack m (S O)
59+ack (S m) (S n) = ack m (ack (S m) n)
60+
61+data Bin = eps | c0 Bin | c1 Bin
62+
63+foo : Bin -> Nat
64+foo eps = O
65+foo (c0 eps) = O
66+foo (c0 (c1 x)) = S (foo (c1 x))
67+foo (c0 (c0 x)) = foo (c0 x)
68+foo (c1 x) = S (foo x)
69+
70+bar : Nat -> Nat -> Nat
71+bar x y = mp x y where
72+ mp : Nat -> Nat -> Nat
73+ mp O y = y
74+ mp (S k) y = S (bar k y)
75+
76+total mfib : Nat -> Nat
77+mfib O = O
78+mfib (S O) = S O
79+mfib (S (S n)) = mfib (S n) + mfib n
80+
81+maxCommutative : (left : Nat) -> (right : Nat) ->
82+ maximum left right = maximum right left
83+maxCommutative O O = refl
84+maxCommutative (S left) O = refl
85+maxCommutative O (S right) = refl
86+maxCommutative (S left) (S right) =
87+ let inductiveHypothesis = maxCommutative left right in
88+ ?maxCommutativeStepCase
89+
90+maxCommutativeStepCase = proof {
91+ intros;
92+ rewrite (boolElimSuccSucc (lte left right) right left);
93+ rewrite (boolElimSuccSucc (lte right left) left right);
94+ rewrite inductiveHypothesis;
95+ trivial;
96+}