~/bend-docscommunity

logic.bend checks

raw source on the hub · import 0x4c3090ea8722081700f9d99ea7503e43/logic.bend as Logic

1 import
import Base

Laws

law demorgan_and proved

Also proved in bend-mathlib as bool.de_morgan_and: import bend-mathlib@0.7.2.0/bool.bend as MBool, then MBool.de_morgan_and.

source · line 31 · raw

@a:Bool -> @b:Bool -> {Bool.not(Bool.and(a, b)) == Bool.or(Bool.not(a), Bool.not(b)) : Bool}

law demorgan_or proved

Also proved in bend-mathlib as bool.de_morgan_or: import bend-mathlib@0.7.2.0/bool.bend as MBool, then MBool.de_morgan_or.

source · line 47 · raw

@a:Bool -> @b:Bool -> {Bool.not(Bool.or(a, b)) == Bool.and(Bool.not(a), Bool.not(b)) : Bool}

law double_neg proved

Also proved in bend-mathlib as bool.not_not: import bend-mathlib@0.7.2.0/bool.bend as MBool, then MBool.not_not.

source · line 63 · raw

@a:Bool -> {Bool.not(Bool.not(a)) == a : Bool}

law and_comm proved

Also proved in bend-mathlib as bool.and_comm: import bend-mathlib@0.7.2.0/bool.bend as MBool, then MBool.and_comm.

source · line 74 · raw

@a:Bool -> @b:Bool -> {Bool.and(a, b) == Bool.and(b, a) : Bool}

law or_comm proved

Also proved in bend-mathlib as bool.or_comm: import bend-mathlib@0.7.2.0/bool.bend as MBool, then MBool.or_comm.

source · line 90 · raw

@a:Bool -> @b:Bool -> {Bool.or(a, b) == Bool.or(b, a) : Bool}

law and_idem proved

Also proved in bend-mathlib as bool.and_self: import bend-mathlib@0.7.2.0/bool.bend as MBool, then MBool.and_self.

source · line 106 · raw

@a:Bool -> {Bool.and(a, a) == a : Bool}

law or_idem proved

Also proved in bend-mathlib as bool.or_self: import bend-mathlib@0.7.2.0/bool.bend as MBool, then MBool.or_self.

source · line 117 · raw

@a:Bool -> {Bool.or(a, a) == a : Bool}

law imp_eq provedsource · line 129 · raw

@a:Bool -> @b:Bool -> {imp(a, b) == Bool.or(Bool.not(a), b) : Bool}

imp unfolds to its definition: one {==}, no split needed.

law and_distr_or proved

Also proved in bend-mathlib as bool.and_or_distrib_left: import bend-mathlib@0.7.2.0/bool.bend as MBool, then MBool.and_or_distrib_left.

source · line 138 · raw

@a:Bool -> @b:Bool -> @c:Bool -> {Bool.and(a, Bool.or(b, c)) == Bool.or(Bool.and(a, b), Bool.and(a, c)) : Bool}

Distributivity (8-case splits, all definitional).

law or_distr_and proved

Also proved in bend-mathlib as bool.or_and_distrib_left: import bend-mathlib@0.7.2.0/bool.bend as MBool, then MBool.or_and_distrib_left.

source · line 164 · raw

@a:Bool -> @b:Bool -> @c:Bool -> {Bool.or(a, Bool.and(b, c)) == Bool.and(Bool.or(a, b), Bool.or(a, c)) : Bool}

law xor_assoc proved

Also proved in bend-mathlib as bool.xor_assoc: import bend-mathlib@0.7.2.0/bool.bend as MBool, then MBool.xor_assoc.

source · line 191 · raw

@a:Bool -> @b:Bool -> @c:Bool -> {Bool.xor(Bool.xor(a, b), c) == Bool.xor(a, Bool.xor(b, c)) : Bool}

xor is associative + absorption (8-case and 4-case splits).

law and_absorb proved

Also proved in bend-mathlib as bool.and_or_absorb: import bend-mathlib@0.7.2.0/bool.bend as MBool, then MBool.and_or_absorb.

source · line 216 · raw

@a:Bool -> @b:Bool -> {Bool.and(a, Bool.or(a, b)) == a : Bool}

law or_absorb proved

Also proved in bend-mathlib as bool.or_and_absorb: import bend-mathlib@0.7.2.0/bool.bend as MBool, then MBool.or_and_absorb.

source · line 232 · raw

@a:Bool -> @b:Bool -> {Bool.or(a, Bool.and(a, b)) == a : Bool}

law xor_self proved

Also proved in bend-mathlib as bool.xor_self: import bend-mathlib@0.7.2.0/bool.bend as MBool, then MBool.xor_self.

source · line 249 · raw

@b:Bool -> {Bool.xor(b, b) == False{} : Bool}

xor_self: b ^ b == False.

law bool_cmp_refl proved

Also proved in bend-mathlib as bool.cmp_refl: import bend-mathlib@0.7.2.0/bool.bend as MBool, then MBool.cmp_refl.

source · line 261 · raw

@b:Bool -> {Bool.cmp(b, b) == EQ{} : Cmp}

bool_cmp_refl: cmp(b, b) == EQ.

law le_refl provedsource · line 274 · raw

@a:Nat -> {Nat.is_le(a, a) == True{} : Bool}

law lt_succ provedsource · line 285 · raw

@a:Nat -> {Nat.is_lt(a, 1n+a) == True{} : Bool}

law eq_nat_refl proved

Also proved in bend-mathlib as nat.is_eq_refl: import bend-mathlib@0.7.2.0/nat.bend as MNat, then MNat.is_eq_refl.

source · line 296 · raw

@a:Nat -> {Nat.is_eq(a, a) == True{} : Bool}

law le_total provedsource · line 308 · raw

@a:Nat -> @b:Nat -> {Bool.or(Nat.is_le(a, b), Nat.is_le(b, a)) == True{} : Bool}

le_total: trichotomy-lite (one side always holds), double induction.

Definitions

def imp source · line 17 · raw

@a:Bool -> @b:Bool -> Bool

def iff source · line 20 · raw

@a:Bool -> @b:Bool -> Bool

def nand source · line 23 · raw

@a:Bool -> @b:Bool -> Bool

def nor source · line 26 · raw

@a:Bool -> @b:Bool -> Bool

def erefl source · line 326 · raw

@-A:Type -> @-x:A -> {x == x : A}