nat.bend source
nat.bend on the hub · documented module
import Base# Nat.bend — Nat addition/multiplication laws, proven by induction+rewriting.## Proof pattern (see guide add_zero): match on the induction variable to# refine the goal, call yourself for the IH, rewrite with %e : P where P is# the goal with _ marking the rewritten side, close with {==}.# Rewrites compose with Equal.sym / Equal.cong / Equal.trans from Base when# the goal faces the "wrong" direction.# add_zero_r: x + 0 == x.law add_zero_r: for x: Nat {Nat.add(x, 0n) == x : Nat}def add_zero_r(x): match x: case 0n: {==} case 1n+p: %add_zero_r(p) : {1n+Nat.add(p, 0n) == 1n+_ : Nat} {==}# add_succ_r: x + (1 + y) == 1 + (x + y).law add_succ_r: for x: Nat for y: Nat {Nat.add(x, 1n+y) == 1n+Nat.add(x, y) : Nat}def add_succ_r(x, y): match x: case 0n: {==} case 1n+p: %add_succ_r(p, y) : {1n+Nat.add(p, 1n+y) == 1n+_ : Nat} {==}# add_comm: x + y == y + x. Base case flips with sym; step chains the# ornamented IH (cong) with the flipped succ lemma (trans).law add_comm: for x: Nat for +y: Nat {Nat.add(x, y) == Nat.add(y, x) : Nat}def add_comm(x, y): match x: case 0n: Equal.sym(Nat, Nat.add(y, 0n), y, add_zero_r(y)) case 1n++p: Equal.trans(Nat, 1n+Nat.add(p, y), 1n+Nat.add(y, p), Nat.add(y, 1n+p), Equal.cong(Nat, Nat, w => (1n+w : Nat), Nat.add(p, y), Nat.add(y, p), add_comm(p, y)), Equal.sym(Nat, Nat.add(y, 1n+p), 1n+Nat.add(y, p), add_succ_r(y, p)))# add_assoc: (x + y) + z == x + (y + z).law add_assoc: for x: Nat for +y: Nat for +z: Nat {Nat.add(Nat.add(x, y), z) == Nat.add(x, Nat.add(y, z)) : Nat}def add_assoc(x, y, z): match x: case 0n: {==} case 1n++p: Equal.trans(Nat, Nat.add(Nat.add(1n+p, y), z), 1n+Nat.add(Nat.add(p, y), z), Nat.add(1n+p, Nat.add(y, z)), {==}, Equal.cong(Nat, Nat, w => (1n+w : Nat), Nat.add(Nat.add(p, y), z), Nat.add(p, Nat.add(y, z)), add_assoc(p, y, z)))# add_shuffle: (a+b)+(c+d) == (a+c)+(b+d). Base is a 3-step trans;# step is one cong (double unfolding aligns both sides with the IH).law add_shuffle: for a: Nat for +b: Nat for +c: Nat for +d: Nat {Nat.add(Nat.add(a, b), Nat.add(c, d)) == Nat.add(Nat.add(a, c), Nat.add(b, d)) : Nat}def add_shuffle(a, b, c, d): match a: case 0n: Equal.trans(Nat, Nat.add(b, Nat.add(c, d)), Nat.add(Nat.add(b, c), d), Nat.add(c, Nat.add(b, d)), Equal.sym(Nat, Nat.add(Nat.add(b, c), d), Nat.add(b, Nat.add(c, d)), add_assoc(b, c, d)), Equal.trans(Nat, Nat.add(Nat.add(b, c), d), Nat.add(Nat.add(c, b), d), Nat.add(c, Nat.add(b, d)), Equal.cong(Nat, Nat, w => Nat.add(w, d), Nat.add(b, c), Nat.add(c, b), add_comm(b, c)), add_assoc(c, b, d))) case 1n+p: Equal.cong(Nat, Nat, w => (1n+w : Nat), Nat.add(Nat.add(p, b), Nat.add(c, d)), Nat.add(Nat.add(p, c), Nat.add(b, d)), add_shuffle(p, b, c, d))# mul_add_distr: x * (b + c) == x * b + x * c.law mul_add_distr: for x: Nat for +b: Nat for +c: Nat {Nat.mul(x, Nat.add(b, c)) == Nat.add(Nat.mul(x, b), Nat.mul(x, c)) : Nat}def mul_add_distr(x, b, c): match x: case 0n: {==} case 1n++p: Equal.trans(Nat, Nat.add(Nat.add(b, c), Nat.mul(p, Nat.add(b, c))), Nat.add(Nat.add(b, c), Nat.add(Nat.mul(p, b), Nat.mul(p, c))), Nat.add(Nat.add(b, Nat.mul(p, b)), Nat.add(c, Nat.mul(p, c))), Equal.cong(Nat, Nat, w => Nat.add(Nat.add(b, c), w), Nat.mul(p, Nat.add(b, c)), Nat.add(Nat.mul(p, b), Nat.mul(p, c)), mul_add_distr(p, b, c)), add_shuffle(b, c, Nat.mul(p, b), Nat.mul(p, c)))# mul_zero_r: x * 0 == 0 (both sides unfold to mul(p, 0); IH fits directly).law mul_zero_r: for x: Nat {Nat.mul(x, 0n) == 0n : Nat}def mul_zero_r(x): match x: case 0n: {==} case 1n+p: mul_zero_r(p)# sub_refl: x - x == 0.law sub_refl: for a: Nat {Nat.sub(a, a) == 0n : Nat}def sub_refl(a): match a: case 0n: {==} case 1n+p: sub_refl(p)# cmp_refl: cmp(x, x) == EQ.law cmp_refl: for a: Nat {Nat.cmp(a, a) == EQ{} : Cmp}def cmp_refl(a): match a: case 0n: {==} case 1n+p: cmp_refl(p)# cmp_sym_refl: EQ == cmp(x, x) (flipped, for % rewriting).law cmp_sym_refl: for a: Nat {EQ{} == Nat.cmp(a, a) : Cmp}def cmp_sym_refl(a): Equal.sym(Cmp, Nat.cmp(a, a), EQ{}, cmp_refl(a))# mul_one_r: x * 1 == x.law mul_one_r: for x: Nat {Nat.mul(x, 1n) == x : Nat}def mul_one_r(x): match x: case 0n: {==} case 1n+p: Equal.trans(Nat, 1n+Nat.mul(p, 1n), 1n+p, 1n+p, Equal.cong(Nat, Nat, w => (1n+w : Nat), Nat.mul(p, 1n), p, mul_one_r(p)), {==})# mul_1p_1: (1 + p) * 1 == 1 + p. Isolates the one_r cong step.law mul_1p_1: for p: Nat {Nat.mul(1n+p, 1n) == 1n+p : Nat}def mul_1p_1(p): Equal.cong(Nat, Nat, w => Nat.add(1n, w), Nat.mul(p, 1n), p, mul_one_r(p))# mul_succ_r: x * (1 + y) == x * y + x, via distr + one + comm.law mul_succ_r: for x: Nat for +y: Nat {Nat.mul(x, 1n+y) == Nat.add(Nat.mul(x, y), x) : Nat}def mul_succ_r(x, y): match x: case 0n: {==} case 1n++p: Equal.trans(Nat, Nat.mul(1n+p, 1n+y), Nat.add(Nat.mul(1n+p, 1n), Nat.mul(1n+p, y)), Nat.add(Nat.mul(1n+p, y), 1n+p), mul_add_distr(1n+p, 1n, y), Equal.trans(Nat, Nat.add(Nat.mul(1n+p, 1n), Nat.mul(1n+p, y)), Nat.add(1n+p, Nat.mul(1n+p, y)), Nat.add(Nat.mul(1n+p, y), 1n+p), Equal.cong(Nat, Nat, w => Nat.add(w, Nat.mul(1n+p, y)), Nat.mul(1n+p, 1n), 1n+p, mul_1p_1(p)), Equal.sym(Nat, Nat.add(Nat.mul(1n+p, y), 1n+p), Nat.add(1n+p, Nat.mul(1n+p, y)), add_comm(Nat.mul(1n+p, y), 1n+p))))# mul_comm: x * y == y * x.law mul_comm: for x: Nat for +y: Nat {Nat.mul(x, y) == Nat.mul(y, x) : Nat}def mul_comm(x, y): match x: case 0n: Equal.sym(Nat, Nat.mul(y, 0n), 0n, mul_zero_r(y)) case 1n++p: Equal.trans(Nat, Nat.add(y, Nat.mul(p, y)), Nat.add(Nat.mul(y, p), y), Nat.mul(y, 1n+p), Equal.trans(Nat, Nat.add(y, Nat.mul(p, y)), Nat.add(y, Nat.mul(y, p)), Nat.add(Nat.mul(y, p), y), Equal.cong(Nat, Nat, w => Nat.add(y, w), Nat.mul(p, y), Nat.mul(y, p), mul_comm(p, y)), add_comm(y, Nat.mul(y, p))), Equal.sym(Nat, Nat.mul(y, 1n+p), Nat.add(Nat.mul(y, p), y), mul_succ_r(y, p)))# add_le_mono: is_le(a+c, b+c) == is_le(a, b). Induct on c; base rewrites# both adds with add_zero_r (nested congs, mul_succ_r shape); step rewrites# both adds with add_succ_r, then Succ/Succ cmp cancels definitionally.law add_le_mono: for +a: Nat for +b: Nat for +c: Nat {Nat.is_le(Nat.add(a, c), Nat.add(b, c)) == Nat.is_le(a, b) : Bool}def add_le_mono(a, b, c): match c: case 0n: Equal.trans(Bool, Nat.is_le(Nat.add(a, 0n), Nat.add(b, 0n)), Nat.is_le(a, Nat.add(b, 0n)), Nat.is_le(a, b), Equal.cong(Nat, Bool, w => Nat.is_le(w, Nat.add(b, 0n)), Nat.add(a, 0n), a, add_zero_r(a)), Equal.cong(Nat, Bool, w => Nat.is_le(a, w), Nat.add(b, 0n), b, add_zero_r(b))) case 1n++q: Equal.trans(Bool, Nat.is_le(Nat.add(a, 1n+q), Nat.add(b, 1n+q)), Nat.is_le(1n+Nat.add(a, q), 1n+Nat.add(b, q)), Nat.is_le(a, b), Equal.trans(Bool, Nat.is_le(Nat.add(a, 1n+q), Nat.add(b, 1n+q)), Nat.is_le(1n+Nat.add(a, q), Nat.add(b, 1n+q)), Nat.is_le(1n+Nat.add(a, q), 1n+Nat.add(b, q)), Equal.cong(Nat, Bool, w => Nat.is_le(w, Nat.add(b, 1n+q)), Nat.add(a, 1n+q), 1n+Nat.add(a, q), add_succ_r(a, q)), Equal.cong(Nat, Bool, w => Nat.is_le(1n+Nat.add(a, q), w), Nat.add(b, 1n+q), 1n+Nat.add(b, q), add_succ_r(b, q))), Equal.trans(Bool, Nat.is_le(1n+Nat.add(a, q), 1n+Nat.add(b, q)), Nat.is_le(Nat.add(a, q), Nat.add(b, q)), Nat.is_le(a, b), {==}, add_le_mono(a, b, q)))