proofs/lib/logic.bend
bend-collections-laws-crypto@1.0.0.0 · 125 lines · 24 definitions
1import Base
2
3
4
5def truth(b: Bool) -> Type:
6 match b:
7 case False{}:
8 Empty
9 case True{}:
10 Unit
11
12def false_true(e: {False{} == True{} : Bool}) -> Empty:
13 %Equal.sym(Bool, False{}, True{}, e) : truth(_)
14 Unit{}
15
16def true_false(e: {True{} == False{} : Bool}) -> Empty:
17 false_true(Equal.sym(Bool, True{}, False{}, e))
18
19def and_left(a: Bool, b: Bool, e: {Bool.and(a, b) == True{} : Bool}) -> {a == True{} : Bool}:
20 match a:
21 case False{}:
22 Empty.absurd({False{} == True{} : Bool}, false_true(e))
23 case True{}:
24 {==}
25
26def and_right(a: Bool, b: Bool, e: {Bool.and(a, b) == True{} : Bool}) -> {b == True{} : Bool}:
27 match a:
28 case False{}:
29 Empty.absurd({b == True{} : Bool}, false_true(e))
30 case True{}:
31 e
32
33def and_intro(a: Bool, b: Bool, ea: {a == True{} : Bool}, eb: {b == True{} : Bool}) -> {Bool.and(a, b) == True{} : Bool}:
34 %Equal.sym(Bool, a, True{}, ea) : {Bool.and(_, b) == True{} : Bool}
35 eb
36
37def not_true(b: Bool, e: {Bool.not(b) == True{} : Bool}) -> {b == False{} : Bool}:
38 match b:
39 case False{}:
40 {==}
41 case True{}:
42 Empty.absurd({True{} == False{} : Bool}, false_true(e))
43
44def not_false(b: Bool, e: {b == False{} : Bool}) -> {Bool.not(b) == True{} : Bool}:
45 %Equal.sym(Bool, b, False{}, e) : {Bool.not(_) == True{} : Bool}
46 {==}
47
48def bool_cases(b: Bool) -> Or({b == True{} : Bool}, {b == False{} : Bool}):
49 match b:
50 case True{}:
51 Inl{{==}}
52 case False{}:
53 Inr{{==}}
54
55def true_not_false(b: Bool, t: {b == True{} : Bool}, f: {b == False{} : Bool}) -> Empty:
56 false_true(Equal.trans(Bool, False{}, b, True{}, Equal.sym(Bool, b, False{}, f), t))
57
58
59def cmp_code(c: Cmp) -> Nat:
60 match c:
61 case LT{}:
62 0n
63 case EQ{}:
64 1n
65 case GT{}:
66 2n
67
68def cmp_lt_eq(e: {LT{} == EQ{} : Cmp}) -> Empty:
69 %e : truth(Cmp.is_lt(_))
70 Unit{}
71
72def cmp_lt_gt(e: {LT{} == GT{} : Cmp}) -> Empty:
73 %e : truth(Cmp.is_lt(_))
74 Unit{}
75
76def cmp_eq_gt(e: {EQ{} == GT{} : Cmp}) -> Empty:
77 %e : truth(Cmp.is_eq(_))
78 Unit{}
79
80
81def none_some(-A: Data, x: A, e: {None{} == Some{x} : Maybe<&2, A>}) -> Empty:
82 %Equal.sym(Maybe<&2, A>, None{}, Some{x}, e) : truth(Maybe.is_some(&2, A, _))
83 Unit{}
84
85def some_value(-A: Data, m: Maybe<&2, A>, d: A) -> A:
86 match m:
87 case None{}:
88 d
89 case Some{x}:
90 x
91
92def some_inj(-A: Data, x: A, y: A, e: {Some{x} == Some{y} : Maybe<&2, A>}) -> {x == y : A}:
93 Equal.cong(Maybe<&2, A>, A, m => some_value(A, m, x), Some{x}, Some{y}, e)
94
95def pair_fst(-A: Type, -B: Type, a: A, b: B, c: A, d: B, e: {(a, b) == (c, d) : A & B}) -> {a == c : A}:
96 Equal.cong(A & B, A, p => Pair.fst(A, B, p), (a, b), (c, d), e)
97
98def pair_snd(-A: Type, -B: Type, a: A, b: B, c: A, d: B, e: {(a, b) == (c, d) : A & B}) -> {b == d : B}:
99 Equal.cong(A & B, B, p => Pair.snd(A, B, p), (a, b), (c, d), e)
100
101def pair_eq(-A: Type, -B: Type, a: A, b: B, c: A, d: B, ea: {a == c : A}, eb: {b == d : B}) -> {(a, b) == (c, d) : A & B}:
102 %ea : {(a, b) == (_, d) : A & B}
103 %eb : {(a, b) == (a, _) : A & B}
104 {==}
105
106
107def subst(-A: Type, -P: A -> Type, -a: A, -b: A, e: {a == b : A}, pa: P(a)) -> P(b):
108 %e : P(_)
109 pa
110
111
112def sfst(-A: Type, -B: @-x: A -> Type, p: Sigma<&1, &1, A, B>) -> A:
113 match p:
114 case Tuple{a, b}:
115 a
116
117def ssnd(-A: Type, -B: @-x: A -> Type, p: Sigma<&1, &1, A, B>) -> B(sfst(A, B, p)):
118 match p:
119 case Tuple{a, b}:
120 b
121
122def pair_eta(-A: Type, -B: Type, p: A & B) -> {p == (Pair.fst(A, B, p), Pair.snd(A, B, p)) : A & B}:
123 match p:
124 case Tuple{a, b}:
125 {==}