纠结于一个简单引理的证明:我应该用哪个归纳法?

Question

我有以下结构:

Inductive instr : Set :=
| Select    : nat -> instr
| Backspace : instr.
Definition prog := list instr.

和以下功能:

Fixpoint Forward (input output: list nat) : option prog :=
match input with
| nil => match output with
| nil => Some nil
| y::r => None
end
| x::rest => match output with
| nil => match rest with
| nil => None   
| xx::rrest => match (Forward rrest nil) with
| Some pp => Some ((Select x) :: Backspace :: pp)
| None => None
end
end
| y::r => if ( beq_nat x y ) then match (Forward rest r) with
| Some pp => Some ((Select x) :: pp)
| None => None 
end
else match rest with
| nil => None
| xx::rrest => match (Forward rrest output) with
     | Some pp => Some ((Select x) :: Backspace :: pp)
     | None => None                                                                          
end
end
end
end.

现在我想证明这个简单引理:

Lemma app_forward :
forall (p p':prog) (input1 input2 output:list nat),
Forward input1 output = Some p ->
Forward input2 nil = Some p' ->
Forward (input1 ++ input2) output = Some (p++p').

注意:如下面的答案所述，引理的更一般形式为假:

Lemma not_app_forward :
forall (p p':prog) (input1 input2 output1 output2:list nat),
Forward input1 output1 = Some p ->
Forward input2 output2 = Some p' ->
Forward (input1 ++ input2) (output1 ++ output2) = Some (p++p').

不管我用什么归纳法，我都卡住了。

例如，我尝试了这个归纳模式:

Definition list_pair_induction {A : Type} :
forall (P : list A -> Prop),
P nil ->
(forall a, P (a :: nil)) ->
(forall a b tl, P tl -> P (a :: b :: tl)) ->
forall l, P l.
Proof.
intros P Pn P1 Prec.
fix tsli 1.
intros [ | x l].
exact Pn.
generalize (tsli l).
destruct l as [ | y tl]; intros Pl.
exact (P1 x).
apply Prec. exact (tsli tl).
Defined.

但我没能完成证明。肯定有什么明显的东西我没看到。谁能帮我证明一下吗?

谢谢!!

Answer 1

你的问题有两个问题。第一个是你要证明的命题是假的，这里有一个反例的证明。

Lemma not_app_forward :
not
(forall (p p':prog) (input1 input2 output1 output2:list nat),
Forward input1 output1 = Some p ->
Forward input2 output2 = Some p' ->
Forward (input1 ++ input2) (output1 ++ output2) = Some (p++p')).
Proof. 
intros abs.
assert (tmp := abs (Select 1 :: Backspace :: nil) (Select 1 :: Select 2 :: nil)
(1 :: 2 :: nil) (1 :: 2 :: nil) nil (1 :: 2 :: nil) refl_equal refl_equal).
compute in tmp.
discriminate.
Qed.

所以，与你的说法相反，这不是一个简单的引理。

第二个问题是函数形状复杂，归纳证明难以组织。我将在下面讨论这方面。

从函数Forward的结构来看，很自然地，您应该对input参数进行归纳法证明，因为它是递归调用发生在子项上的参数。然而，递归调用不仅发生在直接子项上(如Forward rest ...)，而且发生在子项的子项上(如Forward rrest ...)，这一事实使证明变得复杂。

有几种方法可以解决这个困难，但都需要一定程度的解释或学习。

1 -一种方法是使用Equations插件来Coq并使用Equations重新定义Forward函数。然后你可以使用函数归纳法来解决你的问题:这将使用一个专门针对你的问题的归纳法原则。

2 -第二种方法是手工构建定制的归纳原理。这是一个尝试。

Definition two_step_list_induction {A : Type} :
forall (P : list A -> Prop),
P nil ->
(forall a, P (a :: nil)) ->
(forall a b tl, 
P (b :: tl) -> P tl -> P (a :: b :: tl)) ->
forall l, P l.
Proof.
intros P Pn P1 Prec.
fix tsli 1.
intros [ | x l].
exact Pn.
generalize (tsli l).
destruct l as [ | y tl]; intros Pl.
exact (P1 x).
apply Prec;[assumption | exact (tsli tl)].
Defined.

然后你可以用下面的命令开始你的证明:

Lemma app_forward :
forall (p p':prog) (input1 input2 output1 output2:list nat),
Forward input1 output1 = Some p ->
Forward input2 output2 = Some p' ->
Forward (input1 ++ input2) (output1 ++ output2) = Some (p++p').
Proof.
intros p p' input1; revert p; induction input1 as [ | a | a b tl Ih1 Ih2]
using two_step_list_induction.

但是，正如我已经说过的，你想要证明的引理实际上是假的，所以这个证明是不可能成立的，我也不能说明所提出的方法是有效的。

编辑:既然原来的问题已经被更正了，下面是对原来问题的完整更正:

Lemma app_forward : forall (p p':prog) (input1 input2 output:list nat),
Forward input1 output = Some p ->
Forward input2 nil = Some p' ->
Forward (input1 ++ input2) output = Some (p++p').
Proof.
intros p p' input1; revert p; induction input1 as [ | x | x xx rrest Ih1 Ih2]
using two_step_list_induction.
simpl.
* intros p input2 [ | no1 output].
+ intros [= p_is_nil ]; rewrite <- p_is_nil; simpl; auto.
+ discriminate.
* simpl.
destruct output as [ | y r]; simpl; try discriminate.
destruct (x =? y); try discriminate.
destruct r as [ | no12 output1]; simpl; try discriminate.
now intros [= pval] v2; rewrite <- pval, v2; simpl.
* intros p input2 output.
destruct output as [ | y r].
simpl (Forward (x :: xx :: rrest) nil).
destruct (Forward rrest nil) as [v | ] eqn:vtl; try discriminate.
intros [= pval] p'val.
assert(tmp := Ih2 _ _ _ vtl p'val).
simpl.
rewrite tmp, <- pval.
easy.
change (Forward (x :: xx :: rrest) (y :: r)) with
(if x =? y then match Forward (xx :: rrest) r with
| Some pp => Some (Select x :: pp)
| None => None end
else match Forward rrest (y :: r) with
| Some pp => Some (Select x :: Backspace :: pp)
| None => None
end).
destruct (Forward (xx :: rrest) r) as [vrest | ] eqn:eqnrest.
destruct (x =? y) eqn:xeqy.
intros [= vp ] v2; rewrite <- vp; clear vp.
generalize (Ih1 _ _ _ eqnrest v2); simpl.
rewrite xeqy; intros it; rewrite it.
easy.
destruct (Forward rrest (y :: r)) as [v | ] eqn:eqnrrest; try discriminate.
intros [= vp] v2; rewrite <- vp; clear vp.
simpl; rewrite xeqy, (Ih2 _ _ _ eqnrrest v2).
easy.
destruct (x =? y) eqn:xeqy; try discriminate.
destruct (Forward rrest (y :: r)) as [v | ] eqn:eqnrrest; try discriminate.
intros [= vp] v2; rewrite <- vp; clear vp.
simpl.
rewrite xeqy, (Ih2 _ _ _ eqnrrest v2).
easy.
Qed.

关于这个解决方案的一些注释:

• 原始函数中发布的代码包含3个递归调用，其中一个参数是直接子列表(rest)，第二个参数是第二个子列表(rest)。前者由归纳假设Ih1处理，后者由归纳假设Ih2处理。由于我没有时间研究的原因，我的证明需要使用4个归纳假设，而不是3个。这意味着可能存在一些重复。
有时候，simpl策略太急于展开递归定义，直到它不能再做任何事情。为了平衡simpl策略的这种偏差，我必须手动执行展开步骤之一，而不依赖simpl。这个展开步骤由出现在脚本中间的change策略调用执行。
• 每次在函数中有递归调用时，结果稍后由match结构分析。为了解释这一点，证明对递归调用的结果进行案例分析，并使用destruct策略的destruct ... eqn:...变体来执行此分析。
• 除了这些先进的技术，证明只是通过与Coq的交互来指导。

使用coq-8.15验证此证明脚本，并导入List和ZArith模块。

3 -您可以通过依赖更强大的有充分根据的归纳来避免构建量身定制的归纳原理。这将为您提供一个更一般的归纳假设，它可以用于更广泛的递归参数集(甚至不是初始第一个列表的结构子项的参数)。以下是完整的脚本:

Require Import Wellfounded.
Lemma app_forward2 : forall (p p':prog) (input1 input2 output:list nat),
Forward input1 output = Some p ->
Forward input2 nil = Some p' ->
Forward (input1 ++ input2) output = Some (p++p').
Proof.
intros p p' input1; revert p.
induction input1 as [input1 Ih] using
(well_founded_ind
(wf_inverse_image (list nat) nat lt (@length nat) lt_wf)).
destruct input1 as [ | x [ | xx rrest]] eqn:input1eq.                 
* intros p input2 [ | no1 output].
+ intros [= p_is_nil ]; rewrite <- p_is_nil; simpl; auto.
+ discriminate.
* simpl.
destruct output as [ | y r]; simpl; try discriminate.
destruct (x =? y); try discriminate.
destruct r as [ | no12 output1]; simpl; try discriminate.
now intros [= pval] v2; rewrite <- pval, v2; simpl.
* intros p input2 output.
assert (rrestlt : length rrest < length (x :: xx :: rrest)).
now simpl; auto with arith.
assert (restlt : length (xx :: rrest) < length (x :: xx :: rrest)).
now simpl; auto with arith.
destruct output as [ | y r].
simpl (Forward (x :: xx :: rrest) nil).
destruct (Forward rrest nil) as [v | ] eqn:vtl; try discriminate.
intros [= pval] p'val.
assert (tmp := Ih _ rrestlt _ _ _ vtl p'val).
simpl.
rewrite tmp, <- pval.
easy.
change (Forward (x :: xx :: rrest) (y :: r)) with
(if x =? y then match Forward (xx :: rrest) r with
| Some pp => Some (Select x :: pp)
| None => None end
else match Forward rrest (y :: r) with
| Some pp => Some (Select x :: Backspace :: pp)
| None => None
end).
destruct (Forward (xx :: rrest) r) as [vrest | ] eqn:eqnrest.
destruct (x =? y) eqn:xeqy.
intros [= vp ] v2; rewrite <- vp; clear vp.
generalize (Ih _ restlt _ _ _ eqnrest v2); simpl.
rewrite xeqy; intros it; rewrite it.
easy.
destruct (Forward rrest (y :: r)) as [v | ] eqn:eqnrrest; try discriminate.
intros [= vp] v2; rewrite <- vp; clear vp.
simpl; rewrite xeqy, (Ih _ rrestlt _ _ _ eqnrrest v2).
easy.
destruct (x =? y) eqn:xeqy; try discriminate.
destruct (Forward rrest (y :: r)) as [v | ] eqn:eqnrrest; try discriminate.
intros [= vp] v2; rewrite <- vp; clear vp.
simpl.
rewrite xeqy, (Ih _ rrestlt _ _ _ eqnrrest v2).
easy.
Qed.

仔细检查引理app_forward2的脚本可以发现，该脚本与app_forward的脚本几乎相同。三个主要提示:

• well_founded_induction结合wf_inverse_image、length和lt_wf给出了一个一般归纳假设，该假设可用于input1被替换为长度较短的列表的任何情况。

• destruct input1用各种情况替换input1的每个实例，包括在归纳假设中出现的实例。

• 在之前的解决方案中，所有对归纳假设Ih1和Ih2的调用都被简单地替换为对Ih的调用，使用假设restlt和rrestlt来保证长度的减少。