PROOF.bend checks
raw source on the hub · import 0xe6b82fa6c4c459c7023adf4b12a3ac46/PROOF.bend as PROOF
PROOF.bend -- proofs of the laws in LAWS.bend. The gate: bend PROOF.bend => "All terms check."
Proof notes (learned on Bend 2.0.4):
- induction is a recursive call on a structurally smaller pattern variable
- %e : P rewrites the goal: P is the goal with _ marking the b-side of
e's equation, and the goal becomes P with a in that place
- evidence of Empty (clashes like 2n-vs-3n broadcast) is discharged by a
match with no cases
3 imports
import Base import ./tinygrad/shape.bend as Sh import ./LAWS.bend as Laws
Definitions
def max_comm source · line 17 · raw
@+a:Nat -> @+b:Nat -> {0xe6b82fa6c4c459c7023adf4b12a3ac46/tinygrad/shape.maxn(a, b) == 0xe6b82fa6c4c459c7023adf4b12a3ac46/tinygrad/shape.maxn(b, a) : Nat}
def max_bdim2 source · line 52 · raw
@d2:Nat -> @e2:Nat -> @ev:0xe6b82fa6c4c459c7023adf4b12a3ac46/tinygrad/shape.bdim2(d2, e2) -> {0xe6b82fa6c4c459c7023adf4b12a3ac46/tinygrad/shape.maxn(d2, e2) == e2 : Nat}a dominating dim yields the max
def max_bdim source · line 64 · raw
@d:Nat -> @e:Nat -> @ev:0xe6b82fa6c4c459c7023adf4b12a3ac46/tinygrad/shape.bdim(d, e) -> {0xe6b82fa6c4c459c7023adf4b12a3ac46/tinygrad/shape.maxn(d, e) == e : Nat}
def sub_diag source · line 100 · raw
@+a:Nat -> {Nat.sub(a, a) == 0n : Nat}
def add_zero_right source · line 108 · raw
@+a:Nat -> {Nat.add(a, 0n) == a : Nat}