Last active
January 29, 2022 18:25
-
-
Save gernst/c39cd33beb23f5e9a993d32576c97aee to your computer and use it in GitHub Desktop.
Proof that multiplication is commutative; following Rustan's proof in the Dafny demo at POPL 2022 virtual workshop
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
begin | |
fun mult :: "nat ⇒ nat ⇒ nat" where | |
"mult x 0 = 0" | | |
"mult x y = x + mult x (y - 1)" | |
lemma mult_rec[simp]: | |
"y ≠ 0 ⟹ mult x y = x + mult x (y - 1)" | |
by (cases y) auto | |
(* this is probably somewhere in the standard library *) | |
lemma nat_lex_induct: | |
fixes x :: nat and y :: nat | |
assumes "⋀ x y. (⋀ x' y'. x' < x ⟹ P x' y') ⟹ (⋀ y'. y' < y ⟹ P x y') ⟹ P x y" | |
shows "P x y" | |
sorry | |
lemma mult_com: | |
shows "mult x y = mult y x" | |
proof (induction x y rule: nat_lex_induct) | |
case (1 x y) | |
(* set up four cases that are proven to be exhaustive *) | |
consider (a) "x = y" | (b) "x ≠ y" "x = 0" | (c) "y < x" "x ≠ 0" | (d) "x-1 < x" "x < y" "x ≠ 0" "y ≠ 0" | |
by linarith | |
then show ?case | |
proof cases | |
case a | |
then show ?thesis | |
by simp | |
next | |
case b | |
with 1 show ?thesis | |
by auto | |
next | |
case c | |
with 1 show ?thesis | |
by metis | |
next | |
case d | |
have "mult x y = x + mult x (y-1)" | |
using d by simp | |
also have "... = x + mult (y-1) x" | |
using `x < y` 1 by auto | |
also have "... = x + y - 1 + mult (y-1) (x-1)" | |
using d by simp | |
also have "... = x + y - 1 + mult (x-1) (y-1)" | |
using d 1 by metis | |
also have "... = y + mult (x-1) y" | |
using d by simp | |
also have "... = y + mult y (x-1)" | |
using `x-1 < x` 1 by simp | |
finally show ?thesis | |
using d by simp | |
qed | |
qed | |
(* standard proof *) | |
lemma mult_com': | |
shows "mult x y = mult y x" | |
proof - | |
have "⋀ y. mult 0 y = 0" | |
proof - | |
fix y | |
show "mult 0 y = 0" | |
by (induction y) auto | |
qed | |
moreover have "⋀ x y. y ≠ 0 ⟹ mult y x = x + mult (y - 1) x" | |
proof - | |
fix x y :: nat | |
assume "y ≠ 0" | |
then show "mult y x = x + mult (y - 1) x" | |
by (induction x) auto | |
qed | |
ultimately show ?thesis | |
by (induction x) auto | |
qed |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment