Mini project about fourth-order induction

This mini-project is a spinoff of Exercise 12 in Chapter Induction principles: from first-order to higher-order induction, in Week 11 (Task 1 below). The goal of Task 0 to Task 4 is to study a sequence of properties, and the goal of Task 5 is to generalize these properties.

Resources

• The .v file for the present mini-project (latest version: 04 Jun 2025).

Task 0

Prove the following property using fourth-order induction:

Property fours_and_threes :
  forall n : nat,
  exists a b : nat,
    6 + n = 4 * a + 3 * b.

Does your proof need the full power of nat_ind4 or would a tailored version of it suffice?

Task 1

Prove the following property using fourth-order induction:

Property fours_and_fives :
  forall n : nat,
  exists a b : nat,
    12 + n = 4 * a + 5 * b.

Task 2

Prove the following property using fourth-order induction:

Property fours_and_sevens :
  forall n : nat,
  exists a b : nat,
    18 + n = 4 * a + 7 * b.

How does your proof, in this task, compare to the proofs in Task 0 and in Task 1?

If your three proofs are not aligned, revisit them and align them.

Task 3

Based on the alignment that was identified in Task 2, write an aligned proof the following property:

Property fours_and_nines :
  forall n : nat,
  exists a b : nat,
    24 + n = 4 * a + 9 * b.

Task 4

Just to make sure, and based on the previous tasks, complete the statement of the following property and prove it in a aligned way:

Property fours_and_elevens :
  forall n : nat,
  exists a b : nat,
    ?? + n = 4 * a + 11 * b.

Task 5

The goal of this task is to generalize the previous properties, based on the observation that the second factor is an odd number that is larger than 1:

Property fours_and_an_odd_number_that_is_larger_than_1 :
  forall m n : nat,
  exists a b : nat,
    ?? + n = 4 * a + S (2 * S m) * b.

1. Complete the statement in a way that is compatible with the statements in the previous tasks.

2. Verify that your completed statement is compatible with the previous proofs by completing the following proof:

   Proof.
     intros [ | [ | [ | [ | [ | m']]]]] n.
     - simpl (...).
       simpl (S (2 * 1)).
       exact (fours_and_threes n).
     - simpl (...).
       simpl (S (2 * 2)).
       exact (fours_and_fives n).
     - simpl (...).
       simpl (S (2 * 3)).
       exact (fours_and_sevens n).
     - simpl (...).
       simpl (S (2 * 4)).
       exact (fours_and_nines n).
     - simpl (...).
       simpl (S (2 * 5)).
       exact (fours_and_elevens n).
     -
   

3. Prove Property fours_and_an_odd_number_that_is_larger_than_1 by mathematical induction over m. In the induction step, conduct a fourth-order induction over n:

   1. Start by admitting the four base cases, and prove the induction step in a way that is aligned with the previous tasks.
   2. Answer the following four questions in any order:
      1. Analyze the first base cases in the proofs of Task 0 to Task 4 to find some inspiration to prove the first base case of your fourth-order induction proof.
      2. Analyze the second base cases in the proofs of Task 0 to Task 4 to find some inspiration to prove the second base case of your fourth-order induction proof.
      3. Analyze the third base cases in the proofs of Task 0 to Task 4 to find some inspiration to prove the third base case of your fourth-order induction proof.
      4. Analyze the fourth base cases in the proofs of Task 0 to Task 4 to find some inspiration to prove the fourth base case of your fourth-order induction proof.

To answer the questions in Task 5.3.b, you might want to first state and prove some more properties in the sequence:

Property fours_and_thirteens :
  forall n : nat,
  exists a b : nat,
    ?? + n = 4 * a + 13 * b.

Property fours_and_fifteens :
  forall n : nat,
  exists a b : nat,
    ?? + n = 4 * a + 15 * b.

Property fours_and_seventeens :
  forall n : nat,
  exists a b : nat,
    ?? + n = 4 * a + 17 * b.

Property fours_and_nineteens :
  forall n : nat,
  exists a b : nat,
    ?? + n = 4 * a + 19 * b.

Resources

• The .v file for the present mini-project (latest version: 04 Jun 2025).

Version

Created [04 Jun 2025]