Coq证明中如何加强归纳假设？

Question

我正在尝试将上下文无关文法的应用形式化为实践任务。我在证明一个引理时遇到了问题。我试图简化我的上下文以概述问题，但仍有些麻烦。

因此，我定义了Chomsky正规形式中的CFG和终端列表的可派生性如下：

Require Import List.
Import ListNotations.

Inductive ter : Type := T : nat -> ter.
Inductive var : Type := V : nat -> var.
Inductive eps : Type := E : eps.

Inductive rule : Type :=
  | Rt : var -> ter -> rule
  | Rv : var -> var -> var -> rule
  | Re : var -> eps -> rule.

Definition grammar := list rule.

Inductive der_ter_list : grammar -> var -> list ter -> Prop :=
  | Der_eps : forall (g : grammar) (v : var) (e : eps),
      In (Re v e) g -> der_ter_list g v []
  | Der_ter : forall (g : grammar) (v : var) (t : ter),
      In (Rt v t) g -> der_ter_list g v [t]
  | Der_var : forall (g : grammar) (v v1 v2 : var) (tl1 tl2 : list ter),
      In (Rv v v1 v2) g -> der_ter_list g v1 tl1 -> der_ter_list g v2 tl2 ->
        der_ter_list g v (tl1 ++ tl2).

我有一些存储终端和其他信息的对象，例如：

Inductive obj : Set := Get_obj : nat -> ter -> obj.

我尝试定义所有可能的对象列表，这些对象可以从给定的非终端派生出来（使用辅助函数）：

Fixpoint get_all_pairs (l1 l2 : list (list obj)) : list (list obj) := match l1 with
    | [] => []
    | l::t => (map (fun x => l ++ x) l2) ++ get_all_pairs t l2
  end.

Fixpoint getLabels (objs : list obj) : list ter := match objs with
    | [] => []
    | (Get_obj yy ter)::t => ter::(getLabels t)
  end.

Inductive paths : grammar -> var -> list (list obj) -> Prop :=
  | Empty_paths : forall (g : grammar) (v : var) (e : eps),
      In (Re v e) g -> paths g v [[]]
  | One_obj_path : forall (g : grammar) (v : var) (n : nat) (t : ter) (objs : list obj),
      In (Rt v t) g -> In (Get_obj n t) objs -> paths g v [[Get_obj n t]]
  | Combine_paths : forall (g : grammar) (v v1 v2 : var) (l1 l2 : list (list obj)),
      In (Rv v v1 v2) g -> paths g v1 l1 -> paths g v2 l2 -> paths g v (get_all_pairs l1 l2).

（paths的每个构造函数实际上对应于rule的构造函数）

现在我正在尝试通过归纳证明关于paths的事实，即paths中的每个元素都可以从非终端派生出来：

Theorem derives_all_path : forall (g: grammar) (v : var)
  (ll : list (list obj)) (pths : paths g v ll), forall (l : list obj),
        In l ll -> der_ter_list g v (getLabels l).
Proof.
  intros g v ll pt l contains.
  induction pt.

这段话的英译如下：

"This construction generates 3 subgoals, 1st and 2nd I've proved by applying Der_eps and Der_ter constructors respectively. But context in 3rd subgoal is not relevant to prove my goal, it has: "

contains : In l (get_all_pairs l1 l2)
IHpt1 : In l l1 -> der_ter_list g v1 (getLabels l)
IHpt2 : In l l2 -> der_ter_list g v2 (getLabels l)

“contains” 的意思是列表 “l” 是由列表 “l1” 和 “l2” 中的一些元素连接而成，但是在 “IHpt1” 和 “IHpt2” 中的前提条件只有当 “l2” 和 “l1” 都为空时才成立，这在一般情况下并不成立，所以使用这个上下文无法证明目标。

如果“contains”中的“l”、“IHpt1”和“IHpt2”是不同的列表，则问题可以得到解决，但不幸的是，我不知道如何向 Coq 解释这一点。是否有任何一种方法可以改变“IHpt1”和“IHpt2”来证明目标，或者有其他方法来证明整个事实？

我尝试查看了“paths_ind”，但结果并不令人满意。

- Roman Fedorov

---

欢迎来到Stackoverflow！ - Anton Trunov

Answer 1

看起来你的归纳假设不够强。如果你在一个更多态的目标上执行induction pt，你会得到更有用的假设，而不是与你开始的特定l相关的假设。

你应该尝试：

intros g v ll pt; induction pt; intros l contains.

- gallais