Page 316 - 《软件学报》2021年第6期

1890 Journal of Software 软件学报 Vol.32, No.6, June 2021

由于 l_mul_dl 函数定义在 product′函数之上,再次利用数学归纳法对二维表变量 b 和 c(图 9)进行归纳展开
时,当 b 的形式为 a3::b 且 c 的形式为 a4::c 时,会取出其二维表中的第一个子表,并拆分成含有 product′的形式,
如下所示.
product′ A Zero add mul a0 (list_each A add a3 a4)=
add (product′ A Zero add mul a0 a3) (product′ A Zero add mul a0 a4)

Fig.8 Right distributive law of two-dimensional list multiplication and two-dimensional list addition
图 8 dl_mul_dl 函数与二维表加法的右分配律

Fig.9 Right distributive law of list and two-dimensional list multiplication and two-dimensional list addition
图 9 表与二维表乘法与二维表加法的右分配律
这提示表与二维表乘法和二维表加法的右分配律定理的证明需要一个新定理的证明支持,即表内积函数
product′与加法 add 的右分配律.
Lemma product_distr_r: forall n (a b c:list A),
length a=n→length b=n→length c=n→
product′ A Zero add mul a (list_each A add b c)
=add (product′ A Zero add mul a b) (product′ A Zero add mul a c).
由于 product′函数定义在 mul 函数之上,利用数学归纳法对 a,b 和 c(图 10)进行归纳展开时,当 a 的形式为
a0::a,b 的形式为 a1::b 且 c 的形式为 a2::c 时,利用化简拆分成含有 mul 的形式,如下所示.
add (mul a (add a1 a2)) (product′ A Zero add mul a0 (list_each A add b c))=
add (add (mul a a1) (product′ A Zero add mul a0 b))