In Logical Foundations' chapter on Inductive Propositions, the exercise exp_match_ex1 involves the following definitions:
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).
I'm stuck trying to prove the following lemma:
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 *)
Which results in:
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
Initially it looked like trying to proceed by induction on ss would allow me to make progress but I can't find any way to transform the hypothesis forall s : list T, In s (x :: ss) -> s =~ re so that I can prove fold app ss [ ] =~ Star re from the inductive hypothesis (forall s : list T, In s ss -> s =~ re) -> fold app ss [ ] =~ Star re.
I think the thing is that you do not need to apply induction hypothesis yet. Just try to see again on your constructors right when you have situation you've described (so, right on your (* stuck *) step).