HandMul

Pierre Letouzey edited this page Oct 13, 2017 · 10 revisions

Here is a fun way to do multiplications by hand for numbers between 6 and 9.
Each hand represents a number. To represent six, we close all the fingers except the big one sixx. This is seven seven. This is eight eight. Finally this is nine nine.

Now we are ready to do 7 * 9, the left hand takes 7 the right one 9 seven rnine.
Now, the idea is simple, the sum of the fingers up gives the tens, and the product of the fingers down the units. On our example 7 * 9, how many fingers are up? 6 (2 on the left, 4 on the right). Now for the units, 3 fingers down for the left hand, one for the right, so 3 units (3 * 1). Putting tens and units together we get 63. Magic!

(* A magic way to do multiplication with hands *)
Inductive hand : Type := Hand6 | Hand7 | Hand8 | Hand9.
(* We can do any value from 6 to 9 with one hand. To do 8 we keep
   only three fingers up (so two fingers down) *)
Definition val_of h :=
match h with Hand6 => 6 | Hand7 => 7 | Hand8 => 8 | Hand9 => 9 end.
Coercion val_of : hand >-> nat.
(* Number of fingers up: to do 8 three fingers up *)
Definition up h :=
match h with Hand6 => 1 | Hand7 => 2 | Hand8 => 3 | Hand9 => 4 end.
(* Number of fingers up: to do 8 two fingers down *)
Definition down h :=
 match h with Hand6 => 4 | Hand7 => 3 | Hand8 => 2 | Hand9 => 1 end.
(* The left hand holds the first number, the right hand the second number,
   the production is composed
     for the tens by the sum of the fingers up and
     for the units by the product of the fingers down
 *)
Theorem hand_mult: forall (left right: hand),
  left * right = (up left + up right) * 10 + (down left * down right).
Proof.
intros left right; destruct left; destruct right; trivial.
Qed.
Clone this wiki locally
You can’t perform that action at this time.
You signed in with another tab or window. Reload to refresh your session. You signed out in another tab or window. Reload to refresh your session.
Press h to open a hovercard with more details.