def dot_vadd

bendtorch@1.3.0.0 · PROOF.bend:16

import Base
import bendtorch@1.3.0.0/spec.bend as Spec
import bend-ml-nat-lemmas@0.1.2.0/main.bend as NL

16# dot(a + b, v) == dot(a, v) + dot(b, v): induction on the three vectors; at each entry (x + y)·z splits into x·z + y·z
17# (distributivity) and add4 regroups the four terms
18def dot_vadd(a: List<&2, Nat>, b: List<&2, Nat>, v: List<&2, Nat>) -> {Spec.dotn(Spec.vadd(a, b), v) == Nat.add(Spec.dotn(a, v), Spec.dotn(b, v)) : Nat}:
19  match a b v:
20    case Nil{} _ _:
21      {==}
22    case Con{+x, +xt} Nil{} +v:
23      Equal.sym(Nat, Nat.add(Spec.dotn(Con{x, xt}, v), 0n), Spec.dotn(Con{x, xt}, v), NL.add_zero(Spec.dotn(Con{x, xt}, v)))
24    case Con{x, xt} Con{y, yt} Nil{}:
25      {==}
26    case Con{+x, +xt} Con{+y, +yt} Con{+z, +zt}:
27      +xz = Nat.mul(x, z)
28      +yz = Nat.mul(y, z)
29      +pa = Spec.dotn(xt, zt)
30      +pb = Spec.dotn(yt, zt)
31      Equal.trans(Nat, Nat.add(Nat.mul(Nat.add(x, y), z), Spec.dotn(Spec.vadd(xt, yt), zt)), Nat.add(Nat.mul(Nat.add(x, y), z), Nat.add(pa, pb)), Nat.add(Nat.add(xz, pa), Nat.add(yz, pb)),
32        Equal.cong(Nat, Nat, s => Nat.add(Nat.mul(Nat.add(x, y), z), s), Spec.dotn(Spec.vadd(xt, yt), zt), Nat.add(pa, pb), dot_vadd(xt, yt, zt)),
33        Equal.trans(Nat, Nat.add(Nat.mul(Nat.add(x, y), z), Nat.add(pa, pb)), Nat.add(Nat.add(xz, yz), Nat.add(pa, pb)), Nat.add(Nat.add(xz, pa), Nat.add(yz, pb)),
34          Equal.cong(Nat, Nat, s => Nat.add(s, Nat.add(pa, pb)), Nat.mul(Nat.add(x, y), z), Nat.add(xz, yz), Equal.sym(Nat, Nat.add(xz, yz), Nat.mul(Nat.add(x, y), z), NL.mul_dist(x, y, z))),
35          NL.add4(xz, yz, pa, pb)))