✔ beginners question on induction · Coq users

While working through "Coq in a Hurry" I tried to proove forall n : nat, n = length (iota n), iota being the function that generates a list of natural numbers from zero to n - 1. The base case was simple.

Require Import List.
Definition iota (n : nat) :=
let fix i (n : nat) (a : list nat) : list nat :=
match n with
| 0 => a
| S n' => i n' (n' :: a)
end
in i n nil.

Lemma iota_len : forall n : nat, n = length (iota n).
Proof.
induction n.
unfold iota.
compute.
reflexivity.

At this point I would assume that I can finish the proof by applying the
induction hypothesis, but I can not get this to work. Do I need a forall
in the hypothesis, and if so, how can I get it?

Pierre Rousselin (Nov 28 2022 at 15:28):

Robert Hoedicke (Nov 28 2022 at 15:30):

Olivier Laurent (Nov 28 2022 at 15:39):

A good question is how would you do on paper? It seems you need to prove something more general about the length of the output of the internal function i. And then instantiate it in the case of i n nil: following the way iotais defined.

Robert Hoedicke (Nov 28 2022 at 15:41):

I would assume that if the induction hypothesis holds for an arbitrary n, it also holds for (S n).
Why would I need to get into the implementation details of iota?

Huỳnh Trần Khanh (Nov 28 2022 at 15:41):

Require Import List.
From Equations Require Import Equations.
Require Import Lia.

Equations iota_aux (n : nat) (a : list nat) : list nat :=
| 0, a := a
| (S n), a := iota_aux n (n :: a).

Definition iota (n : nat) := iota_aux n nil.

Lemma iota_aux_len (n : nat) : forall a : list nat, n + length a = length (iota_aux n a).
Proof.
  induction n.
  - easy.
  - intro a.
    simp iota_aux.
    pose proof (IHn (n :: a)) as H.
    simpl in H.
    lia.
Qed.

Lemma iota_len (n : nat) : n = length (iota n).
Proof.
  unfold iota.
  pose proof (iota_aux_len n nil) as H.
  simpl in H.
  lia.
Qed.

As my Coq skills aren't good yet, I don't know how to do this proof with fixpoints. But the idea is to split the definition into two parts and prove a more general property about the auxiliary recursive function.

Huỳnh Trần Khanh (Nov 28 2022 at 15:42):

In fact, you really need to get into the "implementation details" about iota. Without this, there is no way you can reason about the list argument of the inner fixpoint.

Robert Hoedicke (Nov 28 2022 at 15:45):

I am glad to see that there is a proof. But I still don't get the requirement about the internals.
Thanks a lot to all of you for your time.

Olivier Laurent (Nov 28 2022 at 15:46):

The problem is that (using i for the internal fixpoint): iota (S n) = i n (n :: a) which you cannot directly link to iota n to apply the induction hypothesis.

Robert Hoedicke (Nov 28 2022 at 15:50):

Olivier Laurent (Nov 28 2022 at 15:52):

If you want the proof to be by a direct induction on n, a way is to have iota also defined by direct induction on n. For example:

Fixpoint iota n :=
match n with
| 0 => nil
| S n' => 0 :: map S (iota n')
end.

Robert Hoedicke (Nov 28 2022 at 15:55):

I guess I was trying to be overly clever with my linear time implementation of iota.
The text actually hints at the usage of map.

Olivier Laurent (Nov 28 2022 at 15:55):

Fixpoint iota n :=
match n with
| 0 => nil
| S n' => iota n' ++ (n' :: nil)
end.

Olivier Laurent (Nov 28 2022 at 15:56):

Paolo Giarrusso (Nov 28 2022 at 19:53):

Maybe that's clear by now, but that is never something you can assume: when proving ∀ n, P n by induction for some specific P, you must prove P (S n) assuming only P n, and the only way to do that is by using the properties of your specific P.

Pierre Rousselin (Nov 29 2022 at 08:25):

Yes you are right, sorry I replied too fast. Here is a backward-style solution without lia. The important part, as @Huỳnh Trần Khanh said is that you need to keep your list general in the subproof about the auxiliary function. If you want to hide the auxiliary functions and theorems from Search, you may name them with _subterm or _subproof. Also, by default rewrite uses equalities left to right so you may want to reverse your equalities for further use.

Require Import List.
(* For add_succ_r and add_0_r: *)
Require Import PeanoNat.
Import Nat.

Fixpoint iota_subterm (n : nat) (l : list nat) : list nat :=
  match n with
    0 => l
  | S n' => iota_subterm n' (n' :: l)
  end.

Theorem iota_len_subproof (n : nat) :
  forall (l : list nat), length (iota_subterm n l) = n + length l.
Proof.
  (* l has to stay general *)
  induction n as [|n' IHn'].
  - intros l. reflexivity.
  - intros l. simpl. rewrite IHn'.
    simpl. rewrite add_succ_r. reflexivity.
Qed.

Definition iota (n : nat) := iota_subterm n nil.

Theorem iota_len (n : nat) : length (iota n) = n.
Proof.
  unfold iota.
  rewrite <-(add_0_r n) at 2.
  apply iota_len_subproof.
Qed.

Require Import List.
(* For add_succ_r and add_0_r: *)
Require Import PeanoNat.
Import Nat.

Definition iota (n : nat) :=
  let fix i (n : nat) (a : list nat) : list nat :=
  match n with
  | 0 => a
  | S n' => i n' (n' :: a)
  end
in i n nil.

Lemma iota_len : forall n : nat, n = length (iota n).
Proof.
  intros n. rewrite <-(add_0_r) at 1.
  replace 0 with (length (@nil nat)) by reflexivity.
  unfold iota.
  generalize (@nil nat) as l.
  induction n as [|n' IHn'].
  - intros n. reflexivity.
  - intros l. rewrite <-IHn'.
    simpl. rewrite add_succ_r. reflexivity.
Qed.

Robert Hoedicke (Nov 29 2022 at 11:02):

Notification Bot (Nov 29 2022 at 11:02):

Robert Hoedicke (Nov 29 2022 at 13:23):

You found me out. This is really quite embarrassing. I am glad that the answers to my stupid question yielded much deeper insights (at least for me).

Stream: Coq users

Topic: ✔ beginners question on induction

Robert Hoedicke (Nov 28 2022 at 15:12):