logic.bend source
logic.bend on the hub · documented module
import Base# Logic.bend — propositional connectives, proven Bool laws, order lemmas.## This is the "everyday proof kit": small connectives plus the handful of# rewrite lemmas used constantly (De Morgan, double negation, commutativity,# Nat order reflexivity). Every law here is proven inline by case analysis# ({==} after match) or structural induction — the four everyday tactics:# intro : x => body (prove A -> B by assuming x : A)# split : match on a parameter (prove per-case, each {==})# induct : recurse on a subterm (the recursive call is the IH)# rewrite: %e : P turns the goal, then {==}# See nat.bend for rewrite-heavy examples.# --- extra connectives (straight-line over Base and/or/not) ---def imp(a: Bool, b: Bool) -> Bool: Bool.or(Bool.not(a), b)def iff(a: Bool, b: Bool) -> Bool: Bool.not(Bool.xor(a, b))def nand(a: Bool, b: Bool) -> Bool: Bool.not(Bool.and(a, b))def nor(a: Bool, b: Bool) -> Bool: Bool.not(Bool.or(a, b))# --- proven Bool laws (split on both args, each case definitional) ---law demorgan_and: for a: Bool for b: Bool {Bool.not(Bool.and(a, b)) == Bool.or(Bool.not(a), Bool.not(b)) : Bool}def demorgan_and(a, b): match a b: case False{} False{}: {==} case False{} True{}: {==} case True{} False{}: {==} case True{} True{}: {==}law demorgan_or: for a: Bool for b: Bool {Bool.not(Bool.or(a, b)) == Bool.and(Bool.not(a), Bool.not(b)) : Bool}def demorgan_or(a, b): match a b: case False{} False{}: {==} case False{} True{}: {==} case True{} False{}: {==} case True{} True{}: {==}law double_neg: for a: Bool {Bool.not(Bool.not(a)) == a : Bool}def double_neg(a): match a: case False{}: {==} case True{}: {==}law and_comm: for a: Bool for b: Bool {Bool.and(a, b) == Bool.and(b, a) : Bool}def and_comm(a, b): match a b: case False{} False{}: {==} case False{} True{}: {==} case True{} False{}: {==} case True{} True{}: {==}law or_comm: for a: Bool for b: Bool {Bool.or(a, b) == Bool.or(b, a) : Bool}def or_comm(a, b): match a b: case False{} False{}: {==} case False{} True{}: {==} case True{} False{}: {==} case True{} True{}: {==}law and_idem: for a: Bool {Bool.and(a, a) == a : Bool}def and_idem(a): match a: case False{}: {==} case True{}: {==}law or_idem: for a: Bool {Bool.or(a, a) == a : Bool}def or_idem(a): match a: case False{}: {==} case True{}: {==}# imp unfolds to its definition: one {==}, no split needed.law imp_eq: for a: Bool for b: Bool {imp(a, b) == Bool.or(Bool.not(a), b) : Bool}def imp_eq(a, b): {==}# Distributivity (8-case splits, all definitional).law and_distr_or: for a: Bool for b: Bool for c: Bool {Bool.and(a, Bool.or(b, c)) == Bool.or(Bool.and(a, b), Bool.and(a, c)) : Bool}def and_distr_or(a, b, c): match a b c: case False{} False{} False{}: {==} case False{} False{} True{}: {==} case False{} True{} False{}: {==} case False{} True{} True{}: {==} case True{} False{} False{}: {==} case True{} False{} True{}: {==} case True{} True{} False{}: {==} case True{} True{} True{}: {==}law or_distr_and: for a: Bool for b: Bool for c: Bool {Bool.or(a, Bool.and(b, c)) == Bool.and(Bool.or(a, b), Bool.or(a, c)) : Bool}def or_distr_and(a, b, c): match a b c: case False{} False{} False{}: {==} case False{} False{} True{}: {==} case False{} True{} False{}: {==} case False{} True{} True{}: {==} case True{} False{} False{}: {==} case True{} False{} True{}: {==} case True{} True{} False{}: {==} case True{} True{} True{}: {==}# xor is associative + absorption (8-case and 4-case splits).law xor_assoc: for a: Bool for b: Bool for c: Bool {Bool.xor(Bool.xor(a, b), c) == Bool.xor(a, Bool.xor(b, c)) : Bool}def xor_assoc(a, b, c): match a b c: case False{} False{} False{}: {==} case False{} False{} True{}: {==} case False{} True{} False{}: {==} case False{} True{} True{}: {==} case True{} False{} False{}: {==} case True{} False{} True{}: {==} case True{} True{} False{}: {==} case True{} True{} True{}: {==}law and_absorb: for a: Bool for b: Bool {Bool.and(a, Bool.or(a, b)) == a : Bool}def and_absorb(a, b): match a b: case False{} False{}: {==} case False{} True{}: {==} case True{} False{}: {==} case True{} True{}: {==}law or_absorb: for a: Bool for b: Bool {Bool.or(a, Bool.and(a, b)) == a : Bool}def or_absorb(a, b): match a b: case False{} False{}: {==} case False{} True{}: {==} case True{} False{}: {==} case True{} True{}: {==}# xor_self: b ^ b == False.law xor_self: for b: Bool {Bool.xor(b, b) == False{} : Bool}def xor_self(b): match b: case False{}: {==} case True{}: {==}# bool_cmp_refl: cmp(b, b) == EQ.law bool_cmp_refl: for b: Bool {Bool.cmp(b, b) == EQ{} : Cmp}def bool_cmp_refl(b): match b: case False{}: {==} case True{}: {==}# --- Nat order / equality reflexivity (induction, mirror of Base ge_refl) ---law le_refl: for a: Nat {Nat.is_le(a, a) == True{} : Bool}def le_refl(a): match a: case 0n: {==} case 1n+p: le_refl(p)law lt_succ: for a: Nat {Nat.is_lt(a, 1n+a) == True{} : Bool}def lt_succ(a): match a: case 0n: {==} case 1n+p: lt_succ(p)law eq_nat_refl: for a: Nat {Nat.is_eq(a, a) == True{} : Bool}def eq_nat_refl(a): match a: case 0n: {==} case 1n+p: eq_nat_refl(p)# le_total: trichotomy-lite (one side always holds), double induction.law le_total: for a: Nat for b: Nat {Bool.or(Nat.is_le(a, b), Nat.is_le(b, a)) == True{} : Bool}def le_total(a, b): match a b: case 0n 0n: {==} case 0n 1n+q: {==} case 1n+p 0n: {==} case 1n+p 1n+q: le_total(p, q)# --- reflexivity witness: {x == x} on demand ---def erefl(-A: Type, -x: A) -> {x == x : A}: {==}