proofs/boolean_logic.bend

stelliferous@0.0.2.0 · 95 lines · 13 definitions

1# Fold a sequence of conditions and recover any member by one induction.
2import Base
3import stelliferous@0.0.2.0/proofs/storage_shape.bend as Shape
4import stelliferous@0.0.2.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{}: {==}