65 lines
1.6 KiB
Plaintext
65 lines
1.6 KiB
Plaintext
function Mult(x: nat, y: nat): nat {
|
|
if y == 0 then 0 else x + Mult(x, y - 1)
|
|
}
|
|
|
|
lemma {:induction false} MultCommutative(x: nat, y: nat)
|
|
ensures Mult(x, y) == Mult(y, x)
|
|
{
|
|
if x == y {
|
|
} else if x == 0 {
|
|
MultCommutative(x, y - 1);
|
|
} else if y < x {
|
|
MultCommutative(y, x);
|
|
} else {
|
|
calc {
|
|
Mult(x, y);
|
|
== //Def. Mult
|
|
x + Mult(x, y - 1);
|
|
== {MultCommutative(x, y - 1);}
|
|
x + Mult(y - 1, x);
|
|
==
|
|
x + y - 1 + Mult(y - 1, x - 1);
|
|
==
|
|
x - 1 + y + Mult(y - 1, x - 1);
|
|
== {MultCommutative(x - 1, y - 1);}
|
|
x - 1 + y + Mult(x - 1, y - 1);
|
|
==
|
|
y + Mult(x - 1, y);
|
|
== {MultCommutative(x - 1, y);}
|
|
y + Mult(y, x - 1);
|
|
==
|
|
Mult(y, x);
|
|
|
|
}
|
|
}
|
|
}
|
|
|
|
lemma {:induction false} MultCommutative'(x: nat, y: nat)
|
|
ensures Mult(x, y) == Mult(y, x)
|
|
decreases x + y
|
|
{
|
|
if x == y {// Trivial
|
|
} else if x == 0 {
|
|
MultCommutative'(x, y - 1);
|
|
} else if y == 0 {
|
|
MultCommutative'(y, x - 1);
|
|
} else { // x < y
|
|
calc {
|
|
Mult(x, y);
|
|
== // def. Mult
|
|
x + Mult(x, y - 1);
|
|
== {MultCommutative'(y - 1, x);}
|
|
x + Mult(y - 1, x) ;
|
|
== // def. Mult
|
|
x + y - 1 + Mult(y - 1, x - 1);
|
|
== {MultCommutative'(y - 1, x -1);}
|
|
y + x - 1 + Mult(x - 1, y - 1);
|
|
== // def. Mult
|
|
y + Mult(x - 1, y);
|
|
== {MultCommutative'(x - 1, y);}
|
|
y + Mult(y, x - 1);
|
|
== // def. Mult
|
|
Mult(y, x);
|
|
}
|
|
}
|
|
} |