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
|
module Funcs
use option.Option
use Functions.Func
(* Abstraction definition axiom :
constant some : 'a -> (option 'a) = (\ x:'a. Some x) *)
constant some : 'a -> (option 'a)
axiom some_def : forall x:'a. some x = Some x
(* Abstraction definition axiom :
constant ocase (f:'a -> 'b) (d:'b) : (option 'a) -> 'b =
(\ x:'a. match x with None -> d | Some x -> f x end) *)
function ocase (f:'a -> 'b) (d:'b) : (option 'a) -> 'b
axiom ocase_def : forall f:'a -> 'b,d:'b,x:option 'a.
ocase f d x = match x with None -> d | Some x -> f x end
lemma ocase_some : forall f:'a -> 'b,d:'b,x:'a.
ocase f d (Some x) = f x
lemma ocase_none : forall f:'a -> 'b,d:'b.
ocase f d None = d
let lemma compose_ocase_some (f:'a -> 'b) (d:'b) : unit
ensures { rcompose some (ocase f d) = f }
=
assert { extensionalEqual (rcompose some (ocase f d)) f }
function omap (f:'a -> 'b) (x:option 'a) : option 'b = match x with
| None -> None
| Some x -> Some (f x)
end
function olift (f:'a -> 'b) : (option 'a) -> (option 'b) = ocase (compose some f) None
lemma olift_def : forall f:'a -> 'b,x:option 'a. olift f x = omap f x
lemma olift_none : forall f:'a -> 'b. olift f None = None
lemma olift_some : forall f:'a -> 'b,x:'a. olift f (Some x) = Some (f x)
lemma olift_none_inversion : forall f:'a -> 'b,x:option 'a. olift f x = None <-> x = None
let lemma olift_some_inversion (f:'a -> 'b) (x:option 'a) (y:'b) : unit
ensures { olift f x = Some y <->
match x with None -> false | Some x' -> f x' = y end }
=
match x with
| None -> ()
| Some _x' -> ()
end
let lemma olift_identity (_:'a) : unit
ensures { olift (identity:'a -> 'a) = identity }
=
assert { extensionalEqual (olift (identity:'a -> 'a)) identity }
let lemma olift_composition (g:'b-> 'c) (f:'a -> 'b) : unit
ensures { compose (olift g) (olift f) = olift (compose g f) }
=
assert { extensionalEqual (compose (olift g) (olift f)) (olift (compose g f)) }
lemma olift_some_commutation : forall f:'a -> 'b.
compose some f = compose (olift f) some
let lemma olift_update (f:'a -> 'b) (x:'a) (y:'b) : unit
ensures { olift (f[x<-y]) = (olift f)[Some x <- Some y] }
=
assert { extensionalEqual (olift (f[x <- y])) ((olift f)[Some x <- Some y]) }
end
|
