~/bend-docscommunity

proofs/boolean_logic.bend checks

raw source on the hub · import stelliferous@0.0.2.0/proofs/boolean_logic.bend as Boolean_logic

Fold a sequence of conditions and recover any member by one induction.

3 imports
import Base
import ./storage_shape.bend as Shape
import ./word_encoding.bend as WordEncoding

Laws

law every_condition_holds provedsource · line 60 · raw

@+conditions:List<&2, Bool> -> @+index:Nat -> @truth:{all(conditions) == True{} : Bool} -> {condition_at(conditions, index) == True{} : Bool}

Definitions

def When source · line 7 · raw

@enabled:Bool -> @Property:Data -> Data

Evidence is required only for an enabled branch.

def choose_matching source · line 12 · raw

@-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, Bool.or(first, rest), wanted, old) : Element}

def left source · line 21 · raw

@+first:Bool -> @+second:Bool -> @truth:{Bool.and(first, second) == True{} : Bool} -> {first == True{} : Bool}

def all source · line 32 · raw

@conditions:List<&2, Bool> -> Bool

Stored in reverse evaluation order so all preserves left-associated &&.

def Holds source · line 38 · raw

@conditions:List<&2, Bool> -> Data

Evidence for every condition, in the same reverse order as all.

def all_hold source · line 43 · raw

@+conditions:List<&2, Bool> -> @+holds:Holds(conditions) -> {all(conditions) == True{} : Bool}

def condition_at source · line 52 · raw

@conditions:List<&2, Bool> -> @index:Nat -> Bool

A missing condition is True, the neutral element, not an array read.

def or_true_right source · line 76 · raw

@+value:Bool -> {Bool.or(value, True{}) == True{} : Bool}

Disjunction identities shared by coverage proofs.

def or_false_left source · line 81 · raw

@+first:Bool -> @+second:Bool -> @proof:{Bool.or(first, second) == False{} : Bool} -> {first == False{} : Bool}

def or_false_right source · line 86 · raw

@+first:Bool -> @+second:Bool -> @proof:{Bool.or(first, second) == False{} : Bool} -> {second == False{} : Bool}

def or_associative source · line 91 · raw

@+first:Bool -> @+second:Bool -> @+third:Bool -> {Bool.or(first, Bool.or(second, third)) == Bool.or(Bool.or(first, second), third) : Bool}