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

Question

我正在尝试将上下文无关语法在练习任务中的应用形式化。我在证明一个引理时遇到问题。我试图简化我的上下文来概述问题，但它仍然有点麻烦。

所以我定义了乔姆斯基范式中的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.

此构造生成 3 个子目标，第 1 个和第 2 个我已分别通过应用 Der_eps 和 Der_ter 构造函数证明。但是第三个子目标中的上下文与证明我的目标无关，它有:

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，但它并没有让我开心。

Answer 1

看来你的归纳假设还不够强。如果您对一个更具多态性的目标执行 induction pt，您将获得更有用的假设，而不是与您开始时的特定 l 相关。

你应该尝试:

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