## Stream: Coq users

### Topic: ✔ beginners question on induction

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

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.

Now I am left with:

1 goal (ID 13)

• n : nat
• IHn : n = length (iota n)
============================
S n = length (iota (S n))

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):

A small step of computation is needed. How does `simpl` change the goal ?

It does nothing.

#### 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 `iota`is 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):

With high-powered tools, here is how I prove the lemma:

``````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):

Robert Hoedicke said:

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?

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):

Ok, I see more clearly now. Thanks again.

#### 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):

or

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

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

or building the list in opposite order and using a reverse on top of it

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

I would assume that if the induction hypothesis holds for an arbitrary n, it also holds for (S n).

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):

Robert Hoedicke said:

It does nothing.

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.
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'.
Qed.

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

Theorem iota_len (n : nat) : length (iota n) = n.
Proof.
unfold iota.
apply iota_len_subproof.
Qed.
``````

A solution with your original iota goes the following way :

• change n into n + length nil
• unfold iota and say to coq : I want to prove it for a general list l instead of nil
``````Require Import List.
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'.
Qed.
``````

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

Thanks again for the detailed answers.

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

Robert Hoedicke has marked this topic as resolved.

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

Paolo Giarrusso said:

I would assume that if the induction hypothesis holds for an arbitrary n, it also holds for (S n).

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`.

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).

#### Paolo Giarrusso (Nov 29 2022 at 13:32):

Oh dear, I never meant embarrassment, only to clarify (if necessary) :-|

Last updated: Dec 05 2023 at 06:01 UTC