~/bend-docscommunity

nat.bend checks

raw source on the hub · import 0x4c3090ea8722081700f9d99ea7503e43/nat.bend as MNat

1 import
import Base

Laws

law add_zero_r proved

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

source · line 12 · raw

@x:Nat -> {Nat.add(x, 0n) == x : Nat}

add_zero_r: x + 0 == x.

law add_succ_r proved

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

source · line 25 · raw

@x:Nat -> @y:Nat -> {Nat.add(x, 1n+y) == 1n+Nat.add(x, y) : Nat}

add_succ_r: x + (1 + y) == 1 + (x + y).

law add_comm proved

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

source · line 40 · raw

@x:Nat -> @+y:Nat -> {Nat.add(x, y) == Nat.add(y, x) : 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_assoc proved

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

source · line 57 · raw

@x:Nat -> @+y:Nat -> @+z:Nat -> {Nat.add(Nat.add(x, y), z) == Nat.add(x, Nat.add(y, z)) : Nat}

add_assoc: (x + y) + z == x + (y + z).

law add_shuffle proved

Also proved in bend-mathlib as algebra.nat_add_four: import bend-mathlib@0.7.2.0/algebra.bend as Algebra, then Algebra.nat_add_four.

source · line 79 · raw

@a:Nat -> @+b:Nat -> @+c:Nat -> @+d:Nat -> {Nat.add(Nat.add(a, b), Nat.add(c, d)) == Nat.add(Nat.add(a, c), Nat.add(b, d)) : Nat}

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 mul_add_distr proved

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

source · line 110 · raw

@x:Nat -> @+b:Nat -> @+c:Nat -> {Nat.mul(x, Nat.add(b, c)) == Nat.add(Nat.mul(x, b), Nat.mul(x, c)) : Nat}

mul_add_distr: x * (b + c) == x * b + x * c.

law mul_zero_r proved

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

source · line 133 · raw

@x:Nat -> {Nat.mul(x, 0n) == 0n : Nat}

mul_zero_r: x * 0 == 0 (both sides unfold to mul(p, 0); IH fits directly).

law sub_refl proved

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

source · line 145 · raw

@a:Nat -> {Nat.sub(a, a) == 0n : Nat}

sub_refl: x - x == 0.

law cmp_refl provedsource · line 157 · raw

@a:Nat -> {Nat.cmp(a, a) == EQ{} : Cmp}

cmp_refl: cmp(x, x) == EQ.

law cmp_sym_refl provedsource · line 169 · raw

@a:Nat -> {EQ{} == Nat.cmp(a, a) : Cmp}

cmp_sym_refl: EQ == cmp(x, x) (flipped, for % rewriting).

law mul_one_r proved

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

source · line 177 · raw

@x:Nat -> {Nat.mul(x, 1n) == x : Nat}

mul_one_r: x * 1 == x.

law mul_1p_1 provedsource · line 195 · raw

@p:Nat -> {Nat.mul(1n+p, 1n) == 1n+p : Nat}

mul_1p_1: (1 + p) * 1 == 1 + p. Isolates the one_r cong step.

law mul_succ_r proved

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

source · line 204 · raw

@x:Nat -> @+y:Nat -> {Nat.mul(x, 1n+y) == Nat.add(Nat.mul(x, y), x) : Nat}

mul_succ_r: x * (1 + y) == x * y + x, via distr + one + comm.

law mul_comm proved

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

source · line 231 · raw

@x:Nat -> @+y:Nat -> {Nat.mul(x, y) == Nat.mul(y, x) : Nat}

mul_comm: x * y == y * x.

law add_le_mono provedsource · line 258 · raw

@+a:Nat -> @+b:Nat -> @+c:Nat -> {Nat.is_le(Nat.add(a, c), Nat.add(b, c)) == Nat.is_le(a, b) : Bool}

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.