Mini project about yet another mystery function

The ostensible goal of this mini-project is to elucidate which function satisfies the following specification:

Definition specification_of_a_mystery_function (mf : nat -> nat -> nat) :=
  (forall i : nat,
      mf (S i) 1 = i)
  /\
  (forall j : nat,
      mf 1 (S j) = j)
  /\
  (forall i j1 j2 : nat,
      mf (S i) (S j1 + S j2) = S (mf (S i) (S j1) + mf (S i) (S j2)))
  /\
  (forall i1 i2 j : nat,
      mf (S i1 + S i2) (S j) = S (mf (S i1) (S j) + mf (S i2) (S j))).

Anton: The ostensible goal, eh.

Alfrothul: The actual goal, of course...

Dana: ...is to practice induction proofs.

Resources

• The .v file for the present lecture note (latest version: 08 Jul 2025).

Task 1

The goal of this task is to prove that the mystery function is commutative:

Property the_mystery_function_is_commutative :
  forall mf : nat -> nat -> nat,
    specification_of_the_mystery_function mf ->
    forall x y : nat,
      mf (S x) (S y) = mf (S y) (S x).

1. Prove this property using two nested mathematical inductions.
2. Prove this property using (one instance of) course-of-value induction.
3. Prove this property using (one instance of) strong induction.

Task 2

The following lemma comes handy when using course-of-values induction and strong induction:

Lemma all_nats_are_expressible_as_a_sum :
  forall n : nat,
    exists n1 n2 : nat,
      n1 <= n /\ n2 <= n /\ n1 + n2 = n.

Prove this lemma very simply.

Task 3

The goal of this task is to prove the following characteristic property of the mystery function:

Proposition a_characteristic_property_of_the_mystery_function :
  forall mf : nat -> nat -> nat,
    specification_of_a_mystery_function mf ->
    forall i j : nat,
      S (mf (S i) (S j)) = S i * S j.

1. Prove this property using strong induction over i.
2. Prove this property using strong induction over j instead of over i.
3. Prove this property using course-of-values induction.
4. Prove this property using mathematical induction.

Partial solution for Task 3a

The base case is simple to prove, so let us focus on its induction step:

Proof.
  unfold specification_of_a_mystery_function.
  intros mf [H_mf_1_r [H_mf_1_l [H_mf_plus_r H_mf_plus_l]]].
  intros i j.
  induction i as [ | i' IHi'] using nat_ind_strong.
  - rewrite -> H_mf_1_l.
    exact (eq_sym (Nat.mul_1_l (S j))).
  -

The *goals* window reads:

mf : nat -> nat -> nat
H_mf_1_r : forall i : nat, mf (S i) 1 = i
H_mf_1_l : forall j : nat, mf 1 (S j) = j
H_mf_plus_r : forall i j1 j2 : nat, mf (S i) (S j1 + S j2) = S (mf (S i) (S j1) + mf (S i) (S j2))
H_mf_plus_l : forall i1 i2 j : nat, mf (S i1 + S i2) (S j) = S (mf (S i1) (S j) + mf (S i2) (S j))
i', j : nat
IHi' : forall i : nat, i <= i' -> S (mf (S i) (S j)) = S i * S j
============================
S (mf (S (S i')) (S j)) = S (S i') * S j

We first decompose i' as the sum of two natural numbers:

- destruct (all_nats_are_expressible_as_a_sum  i') as [i1' [i2' [H_i1' [H_i2' H_i1'_i2']]]].
  rewrite <- H_i1'_i2'.

The *goals* window reads:

mf : nat -> nat -> nat
H_mf_1_r : forall i : nat, mf (S i) 1 = i
H_mf_1_l : forall j : nat, mf 1 (S j) = j
H_mf_plus_r : forall i j1 j2 : nat, mf (S i) (S j1 + S j2) = S (mf (S i) (S j1) + mf (S i) (S j2))
H_mf_plus_l : forall i1 i2 j : nat, mf (S i1 + S i2) (S j) = S (mf (S i1) (S j) + mf (S i2) (S j))
i', j : nat
IHi' : forall i : nat, i <= i' -> S (mf (S i) (S j)) = S i * S j
i1', i2' : nat
H_i1' : i1' <= i'
H_i2' : i2' <= i'
H_i1'_i2' : i1' + i2' = i'
============================
S (mf (S (S (i1' + i2'))) (S j)) = S (S (i1' + i2')) * S j

To be in position to invoke H_mf_plus_l, we first need to rewrite S (S (i1' + i2')) into S i1' + S i2':

rewrite -> (plus_n_Sm i1' i2').
rewrite <- (plus_Sn_m i1' (S i2')).
rewrite -> H_mf_plus_l.

The *goals* window reads:

mf : nat -> nat -> nat
H_mf_1_r : forall i : nat, mf (S i) 1 = i
H_mf_1_l : forall j : nat, mf 1 (S j) = j
H_mf_plus_r : forall i j1 j2 : nat, mf (S i) (S j1 + S j2) = S (mf (S i) (S j1) + mf (S i) (S j2))
H_mf_plus_l : forall i1 i2 j : nat, mf (S i1 + S i2) (S j) = S (mf (S i1) (S j) + mf (S i2) (S j))
i', j : nat
IHi' : forall i : nat, i <= i' -> S (mf (S i) (S j)) = S i * S j
i1', i2' : nat
H_i1' : i1' <= i'
H_i2' : i2' <= i'
H_i1'_i2' : i1' + i2' = i'
============================
S (S (mf (S i1') (S j) + mf (S i2') (S j))) = (S i1' + S i2') * S j

To be in position to invoke the induction hypothesis on i1' and on i2', we first need to rewrite S (S (mf (S i1') (S j) + mf (S i2') (S j))) into S (mf (S i1') (S j)) + S (mf (S i2') (S j)):

rewrite -> plus_n_Sm.
rewrite <- plus_Sn_m.
rewrite -> (IHi' i1' H_i1').
rewrite -> (IHi' i2' H_i2').

The *goals* window reads:

mf : nat -> nat -> nat
H_mf_1_r : forall i : nat, mf (S i) 1 = i
H_mf_1_l : forall j : nat, mf 1 (S j) = j
H_mf_plus_r : forall i j1 j2 : nat, mf (S i) (S j1 + S j2) = S (mf (S i) (S j1) + mf (S i) (S j2))
H_mf_plus_l : forall i1 i2 j : nat, mf (S i1 + S i2) (S j) = S (mf (S i1) (S j) + mf (S i2) (S j))
i', j : nat
IHi' : forall i : nat, i <= i' -> S (mf (S i) (S j)) = S i * S j
i1', i2' : nat
H_i1' : i1' <= i'
H_i2' : i2' <= i'
H_i1'_i2' : i1' + i2' = i'
============================
S i1' * S j + S i2' * S j = (S i1' + S i2') * S j

The goal is then proved using the distributivity property of multiplication over addition.

Task 4

Implement the mystery function and verify that it satisfies its specification.

Hint: The following lemma should prove handy:

Lemma yeah_yeah :
  forall i j : nat,
    pred (S i * S j) = i * S j + j.

Food for thought

In how many ways can we break a chocolate tablet into 1*1 squares?

Resources

• The .v file for the present lecture note (latest version: 08 Jul 2025).

Version

Created [08 Jul 2025]