例: 乗法の交換法則

乗法の交換法則は次の等式を意味しています:

m * n = n * m

このとき m と n は整数の範囲を持ちます。この等式を直接エンコードすると次のような (証明の) 関数インターフェイスが得られます:

// prfun mul_commute{m,n:int}{p:int}(MUL(m, n, p)): MUL(n, m, p) //

mul_commute の実装は次のようになります:

primplmnt mul_commute {m,n}{p}(pf0) = let // prfun auxnat {m:nat} {p:int} .<m>. ( pf: MUL(m, n, p) ) : MUL(n, m, p) = ( case+ pf of | MULbas() => mul_nx0_0{n}() | MULind(pf1) => mul_distribute(auxnat(pf1), mul_nx1_n{n}()) // end of [MULind] ) (* end of [auxnat] *) // in // sif m >= 0 then auxnat(pf0) else let prval MULneg(pf1) = pf0 in mul_neg_2(auxnat(pf1)) end // end of [else] // end // end of [mul_commute]

このとき、次の証明関数が使われています:

// prfun mul_nx0_0{n:int}(): MUL(n, 0, 0) // n * 0 = 0 // prfun mul_nx1_n{n:int}(): MUL(n, 1, n) // n * 1 = n // prfun mul_neg_2 {m,n:int}{p:int}(MUL(m,n,p)): MUL(m,~n,~p) // m*(~n) = ~(m*n) //

内部の関数 auxnat は次の等式を満たす数学的帰納法の証明を素直にエンコードしています:

m * n = n * m

このとき m は自然数の範囲を、n は整数の範囲を取ります。関数 mul_commuteauxnat を使ってすぐに実装できるでしょう。