proofs/boolean_logic.bend
stelliferous@0.0.3.0 · 124 lines · 0 definitions
1# Fold a sequence of conditions and recover any member by one induction.
2import Base
3import stelliferous@0.0.3.0/proofs/storage_shape.bend as Shape
4import stelliferous@0.0.3.0/proofs/word_encoding.bend as WordEncoding
5
6# Evidence is required only for an enabled branch.
7def When(enabled: Bool,Property: Data) -> Data:
8 match enabled:
9 case False{}: Unit
10 case True{}: Property
11
12def choose_matching(-Element: Data,+first: Bool,+rest: Bool,+actual: Element,+wanted: Element,+old: Element,
13 correct: When(first,{actual == wanted : Element})) ->
14 {Bool.pick(Element,rest,wanted,Bool.pick(Element,first,actual,old)) == Bool.pick(Element,first || rest,wanted,old) : Element}:
15 match first rest:
16 case False{} False{}: {==}
17 case False{} True{}: {==}
18 case True{} False{}: correct
19 case True{} True{}: {==}
20
21def left(+first: Bool,+second: Bool,truth: {Bool.and(first,second) == True{} : Bool}) -> {first == True{} : Bool}:
22 match first:
23 case False{}: Empty.absurd({False{} == True{} : Bool},WordEncoding.false_true(truth))
24 case True{}: {==}
25
26def right(+first: Bool,+second: Bool,truth: {Bool.and(first,second) == True{} : Bool}) -> {second == True{} : Bool}:
27 match first:
28 case False{}: Empty.absurd({second == True{} : Bool},WordEncoding.false_true(truth))
29 case True{}: truth
30
31# Stored in reverse evaluation order so all preserves left-associated &&.
32def all(conditions: List<&2,Bool>) -> Bool:
33 match conditions:
34 case Nil{}: True{}
35 case last <> prefix: Bool.and(all(prefix),last)
36
37# Evidence for every condition, in the same reverse order as all.
38def Holds(conditions: List<&2,Bool>) -> Data:
39 match conditions:
40 case Nil{}: Unit
41 case last <> prefix: Shape.Both<{last == True{} : Bool},Holds(prefix)>
42
43def all_hold(+conditions: List<&2,Bool>,+holds: Holds(conditions)) -> {all(conditions) == True{} : Bool}:
44 match conditions:
45 case Nil{}: {==}
46 case +last <> +prefix:
47 Shape.Both{+here,+rest} = holds
48 %Equal.sym(Bool,all(prefix),True{},all_hold(prefix,rest)) : {Bool.and(_,last) == True{} : Bool}
49 here
50
51# A missing condition is True, the neutral element, not an array read.
52def condition_at(conditions: List<&2,Bool>,index: Nat) -> Bool:
53 match conditions:
54 case Nil{}: True{}
55 case last <> prefix:
56 match index:
57 case 0n: last
58 case 1n+previous: condition_at(prefix,previous)
59
60law every_condition_holds:
61 for +conditions: List<&2,Bool>
62 for +index: Nat
63 for truth: {all(conditions) == True{} : Bool}
64 {condition_at(conditions,index) == True{} : Bool}
65
66def every_condition_holds(conditions,index,truth):
67 match conditions:
68 case Nil{}: {==}
69 case +last <> +prefix:
70 match index:
71 case 0n: right(all(prefix),last,truth)
72 case 1n+previous:
73 every_condition_holds(prefix,previous,left(all(prefix),last,truth))
74
75# Disjunction identities shared by coverage proofs.
76def or_true_right(+value: Bool) -> {value || True{} == True{} : Bool}:
77 match value:
78 case False{}: {==}
79 case True{}: {==}
80
81def or_false_left(+first: Bool,+second: Bool,proof: {first || second == False{} : Bool}) -> {first == False{} : Bool}:
82 match first:
83 case False{}: {==}
84 case True{}: Empty.absurd({True{} == False{} : Bool},WordEncoding.false_true(Equal.sym(Bool,True{},False{},proof)))
85
86def or_false_right(+first: Bool,+second: Bool,proof: {first || second == False{} : Bool}) -> {second == False{} : Bool}:
87 match first:
88 case False{}: proof
89 case True{}: Empty.absurd({second == False{} : Bool},WordEncoding.false_true(Equal.sym(Bool,True{},False{},proof)))
90
91def or_associative(+first: Bool,+second: Bool,+third: Bool) ->
92 {first || (second || third) == (first || second) || third : Bool}:
93 match first:
94 case False{}: {==}
95 case True{}: {==}
96
97# Boolean predicates agree when each truth witness implies the other.
98def equivalent(+first: Bool,+second: Bool,
99 forward: {first == True{} : Bool} -> {second == True{} : Bool},
100 backward: {second == True{} : Bool} -> {first == True{} : Bool}) -> {first == second : Bool}:
101 match first second:
102 case False{} False{}: {==}
103 case True{} True{}: {==}
104 case True{} False{}: Empty.absurd({True{} == False{} : Bool},WordEncoding.false_true(forward({==})))
105 case False{} True{}: Empty.absurd({False{} == True{} : Bool},WordEncoding.false_true(backward({==})))
106
107def and_associative(+first: Bool,+second: Bool,+third: Bool) -> {(first && second) && third == first && (second && third) : Bool}:
108 match first:
109 case False{}: {==}
110 case True{}: {==}
111
112def and_true(+a: Bool,+b: Bool,ha: {a == True{} : Bool},hb: {b == True{} : Bool}) -> {a && b == True{} : Bool}:
113 %Equal.sym(Bool,a,True{},ha) : {_ && b == True{} : Bool}
114 hb
115
116def not_true(value: Bool,evidence: {Bool.not(value) == True{} : Bool}) -> {value == False{} : Bool}:
117 match value:
118 case False{}: {==}
119 case True{}: Empty.absurd({True{} == False{} : Bool},WordEncoding.false_true(evidence))
120
121def and_false_right(+left: Bool) -> {left && False{} == False{} : Bool}:
122 match left:
123 case True{}: {==}
124 case False{}: {==}