/
partial.tt
56 lines (47 loc) · 964 Bytes
/
partial.tt
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
{- Uustalu, Altenkirch and Capretta's Partiality monad -}
Data Partial (A:*) : * = {- codata -}
Now : (a:A)Partial A
| Later : (p:Partial A)Partial A;
Declare never:(A:*)Partial A;
never = [A:*](Later _ (never A));
returnD = [A:*][a:A]Now _ a;
{- corecursive -}
Rec bindD : (A,B:*)(d:Partial A)(k:(a:A)(Partial B))Partial B;
intros;
case d;
intros;
fill k a;
intros;
fill Later _ (bindD _ _ p k);
Qed;
{- corecursive -}
Rec lfpAux : (A,B:*)(k:(a0:A)(Partial B))
(f:(fk:(a1:A)Partial B)(fa:A)Partial B)(a:A)Partial B;
intros;
case f k a;
intros;
fill Now _ a0;
intros;
fill Later _ (lfpAux _ _ (f k) f a);
Qed;
lfp = [A,B:*][f:(k:(a:A)Partial B)((a:A)Partial B)][a:A]
(lfpAux _ _ ([x:A]never B) f a);
Load "nat.tt";
Check lfp;
fact : (x:Nat)Partial Nat;
intros;
refine lfp;
fill Nat;
intro factfn arg;
case arg;
refine returnD;
fill (S O);
intros;
case (factfn k);
intros;
refine returnD;
fill (mult a (S k));
intros;
fill p;
fill x;
Qed;