main.bend checks

raw source on the hub · import bend-ml-nat-lemmas@0.1.0.0/main.bend as Main

bend-ml-nat-lemmas: lemas provados de Nat e List que a Base do Bend não tem.

import bend-ml-nat-lemmas@0.1.0/main.bend as NL NL.add_comm(a, b) NL.mul_assoc(a, b, c) NL.product_append(xs, ys) ...

Cada law afirma um fato; o def logo abaixo é a prova, checada pelo kernel. Como ler uma prova: ela é uma função cujo TIPO é a afirmação. - match faz análise de casos (o número é 0, ou é 1 + p). - Uma chamada da própria função é a hipótese de indução ("já sei que vale para p, então provo para 1 + p"). - %e : P reescreve o objetivo usando a igualdade e. - {==} fecha quando os dois lados já calculam para a mesma coisa. Um parâmetro leva + quando a prova o usa mais de uma vez.

1 import

import Base

Laws

law add_zero 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 27 · raw

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

law add_succ provedsource · line 41 · raw

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

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 55 · raw

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

law add_assoc provedsource · line 71 · raw

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

law mul_zero 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 86 · raw

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

law mul_succ provedsource · line 109 · raw

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

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 124 · raw

@+a:Nat -> @+b:Nat -> {Nat.mul(a, b) == Nat.mul(b, a) : Nat}

law mul_dist provedsource · line 140 · raw

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

law mul_assoc provedsource · line 156 · raw

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

law mul_one_l proved
Also proved in bend-mathlib as nat.one_mul: `import bend-mathlib@0.7.2.0/nat.bend as MNat`, then `MNat.one_mul`.
source · line 173 · raw

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

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 182 · raw

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

law append_nil provedsource · line 195 · raw

@-A:Data -> @xs:List<&2, A> -> {List.append(&2, A, xs, []) == xs : List<&2, A>}

law append_assoc provedsource · line 209 · raw

@-A:Data -> @xs:List<&2, A> -> @ys:List<&2, A> -> @zs:List<&2, A> -> {List.append(&2, A, List.append(&2, A, xs, ys), zs) == List.append(&2, A, xs, List.append(&2, A, ys, zs)) : List<&2, A>}

law length_append provedsource · line 225 · raw

@-A:Data -> @xs:List<&2, A> -> @ys:List<&2, A> -> {List.length(&2, A, List.append(&2, A, xs, ys)) == Nat.add(List.length(&2, A, xs), List.length(&2, A, ys)) : Nat}

law product_append provedsource · line 240 · raw

@+xs:List<&2, Nat> -> @+ys:List<&2, Nat> -> {product(List.append(&2, Nat, xs, ys)) == Nat.mul(product(xs), product(ys)) : Nat}

Definitions

def product source · line 19 · raw

@xs:List<&2, Nat> -> Nat

Produto dos elementos de uma lista de Nat; a lista vazia vale 1. É o "número de elementos" de um tensor cuja shape é a lista.

def add_swap source · line 100 · raw

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

x + (y + z) == y + (x + z): troca os termos do meio de uma soma tripla. (Lema auxiliar; não é uma lei publicada.)