在逻辑基础上证明 MStar' (IndProp.v)

Question

在逻辑基础的归纳命题一章中，练习 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.

Answer 1

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

在逻辑基础上证明 MStar' (IndProp.v)

Proving MStar' in Logical Foundations (IndProp.v)

coq

logical-foundations