Stream: Coq users

Topic: ✔ beginners question on induction


view this post on Zulip 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)

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?

view this post on Zulip Pierre Rousselin (Nov 28 2022 at 15:28):

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

view this post on Zulip Robert Hoedicke (Nov 28 2022 at 15:30):

It does nothing.

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Robert Hoedicke (Nov 28 2022 at 15:50):

Ok, I see more clearly now. Thanks again.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Olivier Laurent (Nov 28 2022 at 15:55):

or

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

view this post on Zulip Olivier Laurent (Nov 28 2022 at 15:56):

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

view this post on Zulip 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.

view this post on Zulip 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.
(* 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.

A solution with your original iota goes the following way :

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.

view this post on Zulip Robert Hoedicke (Nov 29 2022 at 11:02):

Thanks again for the detailed answers.

view this post on Zulip Notification Bot (Nov 29 2022 at 11:02):

Robert Hoedicke has marked this topic as resolved.

view this post on Zulip 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).

view this post on Zulip Paolo Giarrusso (Nov 29 2022 at 13:32):

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


Last updated: Jun 14 2024 at 19:02 UTC