mul.bend source

mul.bend on the hub · documented module

# mul.bend: laws of Base's Nat.mul. Kept apart from nat.bend because the# proofs use ac.bend, which imports nat.bend.import Baseimport ./nat.bend as Nimport ./ac.bend as Adef mul_add_r_rev(+a: Nat, +b: Nat, +x: Nat) -> {Nat.add(Nat.mul(a, x), Nat.mul(b, x)) == Nat.mul(Nat.add(a, b), x) : Nat}:  Equal.sym(Nat, Nat.mul(Nat.add(a, b), x), Nat.add(Nat.mul(a, x), Nat.mul(b, x)), N.mul_add_r(a, b, x))def mul_add_l(+x: Nat, +y: Nat, +z: Nat) -> {Nat.mul(x, Nat.add(y, z)) == Nat.add(Nat.mul(x, y), Nat.mul(x, z)) : Nat}:  match x:    case 0n:      {==}    case 1n++p:      %Equal.sym(Nat, Nat.mul(p, Nat.add(y, z)), Nat.add(Nat.mul(p, y), Nat.mul(p, z)), mul_add_l(p, y, z)) : {Nat.add(Nat.add(y, z), _) == Nat.add(Nat.add(y, Nat.mul(p, y)), Nat.add(z, Nat.mul(p, z))) : Nat}      A.ac([y, z, Nat.mul(p, y), Nat.mul(p, z)],        A.EAdd{A.EAdd{A.EAtom{0n}, A.EAtom{1n}}, A.EAdd{A.EAtom{2n}, A.EAtom{3n}}},        A.EAdd{A.EAdd{A.EAtom{0n}, A.EAtom{2n}}, A.EAdd{A.EAtom{1n}, A.EAtom{3n}}}, {==})def mul_assoc(+a: Nat, +b: Nat, +c: Nat) -> {Nat.mul(a, Nat.mul(b, c)) == Nat.mul(Nat.mul(a, b), c) : Nat}:  match a:    case 0n:      {==}    case 1n++p:      %mul_add_r_rev(b, Nat.mul(p, b), c) : {Nat.add(Nat.mul(b, c), Nat.mul(p, Nat.mul(b, c))) == _ : Nat}      %mul_assoc(p, b, c) : {Nat.add(Nat.mul(b, c), Nat.mul(p, Nat.mul(b, c))) == Nat.add(Nat.mul(b, c), _) : Nat}      {==}def mul_double_l(+x: Nat, +y: Nat) -> {Nat.double(Nat.mul(x, y)) == Nat.mul(Nat.double(x), y) : Nat}:  match x:    case 0n:      {==}    case 1n++p:      %mul_double_l(p, y) : {Nat.double(Nat.add(y, Nat.mul(p, y))) == Nat.add(y, Nat.add(y, _)) : Nat}      A.ac([y, Nat.mul(p, y)],        A.EDbl{A.EAdd{A.EAtom{0n}, A.EAtom{1n}}},        A.EAdd{A.EAtom{0n}, A.EAdd{A.EAtom{0n}, A.EDbl{A.EAtom{1n}}}}, {==})def mul_double_r(+x: Nat, +y: Nat) -> {Nat.double(Nat.mul(x, y)) == Nat.mul(x, Nat.double(y)) : Nat}:  match x:    case 0n:      {==}    case 1n++p:      %mul_double_r(p, y) : {Nat.double(Nat.add(y, Nat.mul(p, y))) == Nat.add(Nat.double(y), _) : Nat}      A.ac([y, Nat.mul(p, y)],        A.EDbl{A.EAdd{A.EAtom{0n}, A.EAtom{1n}}},        A.EAdd{A.EDbl{A.EAtom{0n}}, A.EDbl{A.EAtom{1n}}}, {==})def mul_zero(+a: Nat) -> {Nat.mul(a, 0n) == 0n : Nat}:  match a:    case 0n:      {==}    case 1n++p:      mul_zero(p)def mul_succ(+a: Nat, +b: Nat) -> {Nat.add(a, Nat.mul(a, b)) == Nat.mul(a, 1n+b) : Nat}:  match a:    case 0n:      {==}    case 1n++p:      %mul_succ(p, b) : {1n+Nat.add(p, Nat.add(b, Nat.mul(p, b))) == 1n+Nat.add(b, _) : Nat}      %N.add_swap(p, b, Nat.mul(p, b)) : {1n+Nat.add(p, Nat.add(b, Nat.mul(p, b))) == 1n+_ : Nat}      {==}def mul_comm(+a: Nat, +b: Nat) -> {Nat.mul(a, b) == Nat.mul(b, a) : Nat}:  match a:    case 0n:      %mul_zero(b) : {_ == Nat.mul(b, 0n) : Nat}      {==}    case 1n++p:      %mul_succ(b, p) : {Nat.add(b, Nat.mul(p, b)) == _ : Nat}      %mul_comm(p, b) : {Nat.add(b, Nat.mul(p, b)) == Nat.add(b, _) : Nat}      {==}