proofs/boolean_logic.bend source

proofs/boolean_logic.bend on the hub · documented module

# Fold a sequence of conditions and recover any member by one induction.import Baseimport ./storage_shape.bend as Shapeimport ./word_encoding.bend as WordEncoding# Evidence is required only for an enabled branch.def When(enabled: Bool,Property: Data) -> Data:  match enabled:    case False{}: Unit    case True{}: Propertydef choose_matching(-Element: Data,+first: Bool,+rest: Bool,+actual: Element,+wanted: Element,+old: Element,  correct: When(first,{actual == wanted : Element})) ->  {Bool.pick(Element,rest,wanted,Bool.pick(Element,first,actual,old)) == Bool.pick(Element,first || rest,wanted,old) : Element}:  match first rest:    case False{} False{}: {==}    case False{} True{}: {==}    case True{} False{}: correct    case True{} True{}: {==}def left(+first: Bool,+second: Bool,truth: {Bool.and(first,second) == True{} : Bool}) -> {first == True{} : Bool}:  match first:    case False{}: Empty.absurd({False{} == True{} : Bool},WordEncoding.false_true(truth))    case True{}: {==}def right(+first: Bool,+second: Bool,truth: {Bool.and(first,second) == True{} : Bool}) -> {second == True{} : Bool}:  match first:    case False{}: Empty.absurd({second == True{} : Bool},WordEncoding.false_true(truth))    case True{}: truth# Stored in reverse evaluation order so all preserves left-associated &&.def all(conditions: List<&2,Bool>) -> Bool:  match conditions:    case Nil{}: True{}    case last <> prefix: Bool.and(all(prefix),last)# Evidence for every condition, in the same reverse order as all.def Holds(conditions: List<&2,Bool>) -> Data:  match conditions:    case Nil{}: Unit    case last <> prefix: Shape.Both<{last == True{} : Bool},Holds(prefix)>def all_hold(+conditions: List<&2,Bool>,+holds: Holds(conditions)) -> {all(conditions) == True{} : Bool}:  match conditions:    case Nil{}: {==}    case +last <> +prefix:      Shape.Both{+here,+rest} = holds      %Equal.sym(Bool,all(prefix),True{},all_hold(prefix,rest)) : {Bool.and(_,last) == True{} : Bool}      here# A missing condition is True, the neutral element, not an array read.def condition_at(conditions: List<&2,Bool>,index: Nat) -> Bool:  match conditions:    case Nil{}: True{}    case last <> prefix:      match index:        case 0n: last        case 1n+previous: condition_at(prefix,previous)law every_condition_holds:  for +conditions: List<&2,Bool>  for +index: Nat  for truth: {all(conditions) == True{} : Bool}  {condition_at(conditions,index) == True{} : Bool}def every_condition_holds(conditions,index,truth):  match conditions:    case Nil{}: {==}    case +last <> +prefix:      match index:        case 0n: right(all(prefix),last,truth)        case 1n+previous:          every_condition_holds(prefix,previous,left(all(prefix),last,truth))# Disjunction identities shared by coverage proofs.def or_true_right(+value: Bool) -> {value || True{} == True{} : Bool}:  match value:    case False{}: {==}    case True{}: {==}def or_false_left(+first: Bool,+second: Bool,proof: {first || second == False{} : Bool}) -> {first == False{} : Bool}:  match first:    case False{}: {==}    case True{}: Empty.absurd({True{} == False{} : Bool},WordEncoding.false_true(Equal.sym(Bool,True{},False{},proof)))def or_false_right(+first: Bool,+second: Bool,proof: {first || second == False{} : Bool}) -> {second == False{} : Bool}:  match first:    case False{}: proof    case True{}: Empty.absurd({second == False{} : Bool},WordEncoding.false_true(Equal.sym(Bool,True{},False{},proof)))def or_associative(+first: Bool,+second: Bool,+third: Bool) ->  {first || (second || third) == (first || second) || third : Bool}:  match first:    case False{}: {==}    case True{}: {==}