1

在逻辑基础关于归纳命题的章节中，练习exp_match_ex1涉及以下定义：

Inductive reg_exp (T : Type) : Type :=
  | EmptySet
  | EmptyStr
  | Char (t : T)
  | App (r1 r2 : reg_exp T)
  | Union (r1 r2 : reg_exp T)
  | Star (r : reg_exp T).

Arguments EmptySet {T}.
Arguments EmptyStr {T}.
Arguments Char {T} _.
Arguments App {T} _ _.
Arguments Union {T} _ _.
Arguments Star {T} _.

Inductive exp_match {T} : list T -> reg_exp T -> Prop :=
  | MEmpty : [] =~ EmptyStr
  | MChar x : [x] =~ (Char x)
  | MApp s1 re1 s2 re2
             (H1 : s1 =~ re1)
             (H2 : s2 =~ re2)
           : (s1 ++ s2) =~ (App re1 re2)
  | MUnionL s1 re1 re2
                (H1 : s1 =~ re1)
              : s1 =~ (Union re1 re2)
  | MUnionR re1 s2 re2
                (H2 : s2 =~ re2)
              : s2 =~ (Union re1 re2)
  | MStar0 re : [] =~ (Star re)
  | MStarApp s1 s2 re
                 (H1 : s1 =~ re)
                 (H2 : s2 =~ (Star re))
               : (s1 ++ s2) =~ (Star re)
  where "s =~ re" := (exp_match s re).

我一直试图证明以下引理：

Lemma MStar' : forall T (ss : list (list T)) (re : reg_exp T),
  (forall s, In s ss -> s =~ re) ->
  fold app ss [] =~ Star re.
Proof.
  intros. induction ss.
    - simpl. apply MStar0.
    - simpl. pose proof (H x). assert (Hx: In x (x :: ss)). {
        simpl. left. reflexivity.
    } pose proof (H0 Hx).
    (* stuck *)

结果是：

T: Type
x: list T
ss: list (list T)
re: reg_exp T
H: forall s : list T, In s (x :: ss) -> s =~ re
IHss: (forall s : list T, In s ss -> s =~ re) -> fold app ss [ ] =~ Star re
H0: In x (x :: ss) -> x =~ re
Hx: In x (x :: ss)
H1: x =~ re
====================================
1/1
x ++ fold app ss [ ] =~ Star re

最初看起来尝试通过归纳继续ss可以让我取得进展，但我找不到任何方法来转换假设forall s : list T, In s (x :: ss) -> s =~ re，以便我可以fold app ss [ ] =~ Star re从归纳假设中证明(forall s : list T, In s ss -> s =~ re) -> fold app ss [ ] =~ Star re。

4

1 回答 1

1

我认为问题是你还不需要应用归纳假设。当您遇到您描述的情况时，只需尝试再次查看您的构造函数（因此，就在您的 (* 卡住 *) 步骤上）。

于 2021-09-11T16:27:28.127 回答