时间戳

首页 > 解决方案 > coq - 将归纳假设应用于 eqb_list_true_iff 中的假设

coq - coq - 将归纳假设应用于 eqb_list_true_iff 中的假设

问题描述

我在空闲时间研究软件基础书籍，这个问题对我来说特别具有挑战性。这是卡住的地方：


Fixpoint eqb_list {A : Type} (eqb : A -> A -> bool)
                  (l1 l2 : list A) : bool :=
  match l1, l2 with
  | [], [] => true
  | [], _ => false
  | _, [] => false
  | (l1' :: l1s'), (l2' :: l2s') => (eqb l1' l2') && (eqb_list eqb l1s' l2s')
  end.

Lemma eqb_list_true_iff :
  forall A (eqb : A -> A -> bool),
    (forall a1 a2, eqb a1 a2 = true <-> a1 = a2) ->
    forall l1 l2, eqb_list eqb l1 l2 = true <-> l1 = l2.
Proof.
  intros. split.
  - intro. induction l1 as [|l1' l1s' IHl'].
  + destruct l2. { reflexivity. } { simpl in H0. discriminate H0. }
  + induction l2 as [|l2' l2s' Il2h']. { simpl in H0. discriminate. } { simpl in H0. }
Abort.

这是证明状态......

1 subgoal
A : Type
eqb : A -> A -> bool
H : forall a1 a2 : A, eqb a1 a2 = true <-> a1 = a2
l1' : A
l1s' : list A
x : A
l2 : list A
H0 : eqb l1' x && eqb_list eqb l1s' l2 = true
IHl' : eqb_list eqb l1s' (x :: l2) = true ->
       l1s' = x :: l2
______________________________________(1/1)
l1' :: l1s' = x :: l2

我可以轻松地隔离eqb l1' x并在下面进行一些重写以使列表的头部（l1'和x）相等，但是尾部（l1s和l2）正在杀死我。我的直觉告诉我，通过某种方式申请IHl'，H0我可以继续前进，但我无法找到一种普遍认可归纳假设的方法，也无法找到一种按摩H0方法使其相似IHl'。任何帮助，将不胜感激！

标签： coqproofcoq-tactic

解决方案

归纳假设太弱了。非正式地，你可以期望证明的那部分是这样的：

我们想证明l1 :: l1s = x :: l2'，因为它足以证明：

  1. l1 = x（使用对eqb参数的假设），以及
  2. l1s = l2'.

后一种说法应该以某种方式从归纳假设得出。因此，归纳假设应该说明比较l1s和l2'。但是IHl'，您当前的目标是l1s与x :: l2'.

问题是第一个induction l1是在目标“ l1 = l2”上完成的：在那个点l2是固定的，所以在归纳的情况下，归纳假设将比较 与 的尾部l1，l2而不是与 的尾部l2。

简而言之，目标过于具体，无法通过归纳法直接证明。首先必须概括。Software Foundations的 Tactics 章节（改变归纳假设）解释了如何解决这个问题。

（我故意不放弃实际的解决方案，因为这是一个家庭作业问题，但请随时要求进一步澄清。）

推荐阅读