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?
A small step of computation is needed. How does simpl
change the goal ?
It does nothing.
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.
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?
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.
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.
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.
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.
Ok, I see more clearly now. Thanks again.
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.
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.
or
Fixpoint iota n :=
match n with
| 0 => nil
| S n' => iota n' ++ (n' :: nil)
end.
or building the list in opposite order and using a reverse on top of it
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
.
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.
Thanks again for the detailed answers.
Robert Hoedicke has marked this topic as resolved.
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 specificP
, you must proveP (S n)
assuming onlyP n
, and the only way to do that is by using the properties of your specificP
.
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).
Oh dear, I never meant embarrassment, only to clarify (if necessary) :-|
Last updated: Dec 05 2023 at 06:01 UTC