Two things:
- When proving a property of some function
f
using a direct induction, choose the parameter on which f
is structurally recursive on. So in your example involving sumoneseq
, induct on lb
instead of ln
since sumoneseq
is structurally recursive on lb
.
- Proving a property of some function
f
where one or more of its arguments are fixed to specific values (e.g. sumoneseq
with its second argument being []
) by direct induction is almost guaranteed to fail, since the value of that argument varies between recursive calls of f
, meaning that you would not be able to apply the induction hypothesis in your inductive case. In that case, you need to manually generalize the induction hypothesis by finding a more general property on which f
holds, with each of its arguments being sufficiently general. For example, instead of proving forall lb ln, sumones (sumoneseq lb ln) = sumones ln + sumones (sumoneseq lb [])
directly by induction, try generalizing it to something like forall lb ln ln', sumones (sumoneseq lb (ln ++ ln')) = sumones ln + sumones (sumoneseq lb ln')
instead and prove that by direct induction. Your desired result then follows as a corollary of that more general result.
You can learn more about generalizing the induction hypothesis in James Wilcox's blog post which generously includes 8 exercises of increasing difficulty on doing just that.
Now try to prove your lemma with these two points in mind. Hint: when proving your more general statement about sumoneseq
by direct induction, you may also find it helpful to extract out a suitable lemma on a certain property of sumones
.
If you've tried again to no avail then the full solution is provided below the horizontal rule (spoiler alert!).
Here goes the full solution. As you can probably see, a lot of case analysis is required on top of the main induction (likely due to your optimization in sumoneseq
of discarding 0
s from ln
) and the reasoning for many of these cases are actually very similar and repetitive. I could've probably further shortened the proof script with a bit of Ltac
programming looking for similar patterns in the various cases but I haven't bothered doing so since I just hacked it up straight away.
From Coq Require Import List Lia.
Import ListNotations.
Fixpoint sumoneseq (lb: list bool) (ln: list nat)
: list nat :=
match lb, ln with
| nil, 0::tl'' => tl''
| nil, _ => ln
| true::tl', nil => sumoneseq tl' (1::nil)
| true::tl', h::tl'' => sumoneseq tl' (S h::tl'')
| false::tl', 0::tl'' => sumoneseq tl' ln
| false::tl', _ => sumoneseq tl' (0::ln)
end.
Fixpoint sumones (ln: list nat) : nat :=
match ln with
| nil => 0
| r::tl => r + (sumones tl)
end.
Lemma sumones_app_plus_distr : forall l l',
sumones (l ++ l') = sumones l + sumones l'.
Proof.
induction l; simpl; intros; auto.
rewrite IHl; lia.
Qed.
Lemma sumones_l' : forall lb ln ln',
sumones (sumoneseq lb (ln ++ ln')) =
sumones ln + sumones (sumoneseq lb ln').
Proof.
induction lb; simpl; intros.
- destruct ln, ln'; simpl; auto.
+ destruct n; rewrite app_nil_r; simpl; auto.
+ destruct n, n0; simpl; rewrite sumones_app_plus_distr;
simpl; lia.
- destruct a, ln, ln'; simpl; auto.
+ replace (S n :: ln ++ []) with ((S n :: ln) ++ [])
by reflexivity.
replace [1] with ([1] ++ []) by now rewrite app_nil_r.
repeat rewrite IHlb; simpl; lia.
+ replace (S n :: ln ++ n0 :: ln')
with ((S n :: ln ++ [n0]) ++ ln')
by (simpl; now rewrite <- app_assoc).
replace (S n0 :: ln') with ([S n0] ++ ln')
by reflexivity.
repeat rewrite IHlb.
replace (S n :: ln ++ [n0])
with ((S n :: ln) ++ [n0])
by reflexivity.
repeat rewrite sumones_app_plus_distr; simpl; lia.
+ destruct n.
* replace (0 :: ln ++ []) with ((0 :: ln) ++ [])
by reflexivity.
replace [0] with ([0] ++ [])
by now rewrite app_nil_r.
repeat rewrite IHlb; simpl; lia.
* replace (0 :: S n :: ln ++ [])
with ((0 :: S n :: ln) ++ []) by reflexivity.
replace [0] with ([0] ++ [])
by now rewrite app_nil_r.
repeat rewrite IHlb; simpl; lia.
+ destruct n, n0.
* replace (0 :: ln ++ 0 :: ln')
with ((0 :: ln ++ [0]) ++ ln')
by (simpl; now rewrite <- app_assoc).
replace (0 :: ln') with ([0] ++ ln') by reflexivity.
repeat rewrite IHlb.
repeat (repeat rewrite sumones_app_plus_distr;
simpl); lia.
* replace (0 :: ln ++ S n0 :: ln')
with ((0 :: ln ++ [S n0]) ++ ln')
by (simpl; now rewrite <- app_assoc).
replace (0 :: S n0 :: ln') with ([0; S n0] ++ ln')
by reflexivity.
repeat rewrite IHlb.
repeat (repeat rewrite sumones_app_plus_distr;
simpl); lia.
* replace (0 :: S n :: ln ++ 0 :: ln')
with ((0 :: S n :: ln ++ [0]) ++ ln')
by (simpl; now rewrite <- app_assoc).
replace (0 :: ln') with ([0] ++ ln')
by reflexivity.
repeat rewrite IHlb.
repeat (repeat rewrite sumones_app_plus_distr;
simpl); lia.
* replace (0 :: S n :: ln ++ S n0 :: ln')
with ((0 :: S n :: ln ++ [S n0]) ++ ln')
by (simpl; now rewrite <- app_assoc).
replace (0 :: S n0 :: ln') with ([0; S n0] ++ ln')
by reflexivity.
repeat rewrite IHlb.
repeat (repeat rewrite sumones_app_plus_distr;
simpl); lia.
Qed.
Lemma sumones_l: forall lb ln,
sumones (sumoneseq lb ln) =
sumones ln + sumones (sumoneseq lb []).
Proof.
intros; replace (sumoneseq lb ln)
with (sumoneseq lb (ln ++ []))
by (now rewrite app_nil_r); apply sumones_l'.
Qed.