Mutual induction and recursion

The goal of this lecture note is to study mutually recursive functions in tCPA and how to reason about them.

Resources

• The .v file for the present lecture note (latest version: 05 Apr 2024).

Evenness and oddness, together

The two predicates evenp and oddp are so intertwined that they are often defined together:

Fixpoint evenp (n : nat) : bool :=
  match n with
  | 0 =>
    true
  | S n' =>
    oddp n'
  end
with oddp (n : nat) : bool :=
       match n with
       | 0 =>
         false
       | S n' =>
         evenp n'
       end.

Their soundness and completeness can be proved separately, in the comfort of nat_ind2:

Theorem soundness_and_completeness_of_evenp :
  forall n : nat,
    evenp n = true <-> exists m : nat, n = 2 * m.
Proof.
  intro n.
  induction n as [ | | n' [IHn'_sound IHn'_complete] [IHSn'_sound IHSn'_complete]] using nat_ind2.
  [...]

Theorem soundness_and_completeness_of_oddp :
  forall n : nat,
    oddp n = true <-> exists m : nat, n = S (2 * m).
Proof.
  intro n.
  induction n as [ | | n' [IHn'_sound IHn'_complete] [IHSn'_sound IHSn'_complete]] using nat_ind2.
  [...]

On the other hand, why should they? Since they are defined together, their soundness and completeness can be proved together... in the comfort of mathematical induction:

Theorem soundness_and_completeness_of_evenp_and_of_oddp :
  forall n : nat,
    (evenp n = true <-> exists m : nat, n = 2 * m)
    /\
    (oddp n = true <-> exists m : nat, n = S (2 * m)).
Proof.
  intro n.
  induction n as [ | n' [[IHn'_esound IHn'_ecomplete] [IHn'_osound IHn'_ocomplete]]].
  [...]

Exercise 20

Complete the proofs above.

Pre-ternary, ternary, or post-ternary?

Likewise, predicates testing whether a number is divisible by 3 or not can be defined independently of each other:

Fixpoint independent_pre_ternaryp (n : nat) : bool :=
  match n with
  | 0 =>
    false
  | 1 =>
    false
  | 2 =>
    true
  | S (S (S n')) =>
    independent_pre_ternaryp n'
  end.

Fixpoint independent_ternaryp (n : nat) : bool :=
  match n with
  | 0 =>
    true
  | 1 =>
    false
  | 2 =>
    false
  | S (S (S n')) =>
    independent_ternaryp n'
  end.

Fixpoint independent_post_ternaryp (n : nat) : bool :=
  match n with
  | 0 =>
    false
  | 1 =>
    true
  | 2 =>
    false
  | S (S (S n')) =>
    independent_post_ternaryp n'
  end.

Or they can be defined together:

Fixpoint pre_ternaryp (n : nat) : bool :=
   match n with
   | 0 =>
     false
   | S n' =>
     post_ternaryp n'
   end
with ternaryp (n : nat) : bool :=
      match n with
      | 0 =>
        true
      | S n' =>
        pre_ternaryp n'
      end
with post_ternaryp (n : nat) : bool :=
       match n with
       | 0 =>
         false
       | S n' =>
         ternaryp n'
       end.

Likewise, their soundness and completeness can be proved independently (using nat_ind3 for comfort):

Theorem soundness_and_completeness_of_ternaryp :
  forall n : nat,
    ternaryp n = true <-> exists m : nat, n = 3 * m.
Proof.
  intro n.
  induction n as [ | | | n' [IHn'_sound IHn'_complete] [IHSn'_sound IHSn'_complete] [IHSSn'_sound IHSSn'_complete]] using nat_ind3.
  [...]

Theorem soundness_and_completeness_of_post_ternaryp :
  forall n : nat,
    post_ternaryp n = true <-> exists m : nat, n = S (3 * m).
Proof.
  intro n.
  induction n as [ | | | n' [IHn'_sound IHn'_complete] [IHSn'_sound IHSn'_complete] [IHSSn'_sound IHSSn'_complete]] using nat_ind3.
  [...]

Theorem soundness_and_completeness_of_pre_ternaryp :
  forall n : nat,
    pre_ternaryp n = true <-> exists m : nat, n = S (S (3 * m)).
Proof.
  intro n.
  induction n as [ | | | n' [IHn'_sound IHn'_complete] [IHSn'_sound IHSn'_complete] [IHSSn'_sound IHSSn'_complete]] using nat_ind3.
  [...]

Or they can be proved together, using ordinary mathematical induction:

Theorem soundness_and_completeness_of_ternaryp_and_friends :
  forall n : nat,
    (pre_ternaryp n = true <-> exists m : nat, n = S (S (3 * m)))
    /\
    (ternaryp n = true <-> exists m : nat, n = 3 * m)
    /\
    (post_ternaryp n = true <-> exists m : nat, n = S (3 * m)).
Proof.
  intro n.
  induction n as [ | n' [[IHn'_presound IHn'_precomplete] [[IHn'_tsound IHn'_tcomplete] [IHn'_postsound IHn'_postcomplete]]]].
  [...]

Exercise 21

Complete the proofs above.

Resources

• The .v file for the present lecture note (latest version: 05 Apr 2024).

Version

Created [05 Apr 2024]