Я застрял, чтобы доказать следующую допущенную лемму. Пожалуйста, помогите мне, как действовать.
Функция sumoneseq добавляет и возвращает список повторений 'true' в обратном порядке. Дано [ верно ; ложно; правда; правда ; ложь; true; true; true ] возвращает [3; 2; 1]. Функция sumones добавляет значения в список nat. Учитывая [3; 2; 1], он возвращает 6.
Notation "x :: l" := (cons x l) (at level 60, right associativity).
Notation "[ ]" := nil.
Notation "[ x ; .. ; y ]" := (cons x .. (cons y nil) ..).
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_l: forall lb ln,
sumones (sumoneseq lb ln) = sumones ln + sumones (sumoneseq lb []).
Proof.
induction ln.
+ simpl. auto.
+ simpl.
Admitted.
Всего 1 ответ
Две вещи:
f
с помощью прямой индукции выберите параметр, для которого f
структурно рекурсивна. Так что в вашем примере с sumoneseq
по lb
вместо ln
поскольку sumoneseq
структурно рекурсивен по sumoneseq
f
которой один или несколько ее аргументов фиксируются на определенных значениях (например, sumoneseq
с его вторым аргументом, являющимся []
), посредством прямой индукции почти гарантированно завершится неудачей, поскольку значение этого аргумента варьируется между рекурсивными вызовами f
, что означает, что вы не сможете применить индуктивную гипотезу в вашем индуктивном случае. В этом случае вам необходимо вручную обобщить гипотезу об индукции, найдя более общее свойство для f
, причем каждый из ее аргументов является достаточно общим. Например, вместо того, чтобы доказать, что все forall lb ln, sumones (sumoneseq lb ln) = sumones ln + sumones (sumoneseq lb [])
напрямую по индукции, попробуйте обобщить его на что-то вроде forall lb ln ln', sumones (sumoneseq lb (ln ++ ln')) = sumones ln + sumones (sumoneseq lb ln')
и докажите это прямой индукцией. Ваш желаемый результат следует как следствие этого более общего результата. Вы можете узнать больше об обобщении гипотезы индукции в блоге Джеймса Уилкокса, который щедро включает в себя 8 упражнений возрастающей сложности при выполнении именно этого.
Теперь попробуйте доказать свою лемму с учетом этих двух моментов. Подсказка: при доказательстве более общего утверждения о sumoneseq
помощью прямой индукции вы также можете найти полезную лемму о некотором свойстве sumones
.
Если вы попробовали еще раз, но безрезультатно, полное решение предоставляется ниже горизонтального правила ( предупреждение о спойлере! ).
Здесь идет полное решение. Как вы, вероятно, можете видеть, требуется много анализа кейсов поверх основной индукции (вероятно, из-за вашей оптимизации в sumoneseq
отбрасывания 0
с из ln
), и причины для многих из этих случаев на самом деле очень похожи и повторяются. Я мог бы, вероятно, еще больше сократить сценарий проверки с помощью небольшого количества Ltac
программ, ищущих похожие шаблоны в различных случаях, но я не стал беспокоиться об этом, так как просто взломал его сразу.
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.