Is there a tactic to help resolving existential quantifiers in Coq? I am working on Software Foundations Volume 1 on my own it is its 2019 version by the way, and I have reached to its lesson Inductively Defined Propositions, and there, for almost one month I have been stuck on an exercise re_not_empty expressed like this in Coq (the exercise itself begins at Fixpoint):
Inductive reg_exp {T : Type} : Type :=
  | EmptySet
  | EmptyStr
  | Char (t : T)
  | App (r1 r2 : reg_exp)
  | Union (r1 r2 : reg_exp)
  | Star (r : reg_exp).

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

Notation &quot;s =~ re&quot; := (exp_match s re) (at level 80).

Fixpoint re_not_empty {T : Type} (re : @reg_exp T) : bool Admitted.

Lemma re_not_empty_correct : ∀T (re : @reg_exp T),
  (∃s, s =~ re) ↔ re_not_empty re = true.
Proof. Admitted.

Although I am obliged not to tell anything about solutions but to get help I have to say at least about Fixpoint that is defined like this:
Fixpoint re_not_empty {T : Type} (re : @reg_exp T) : bool :=
  match re with
  | EmptySet =&gt; false
  | EmptyStr | Char _ =&gt; true
  | App re1 re2 =&gt; re_not_empty re1 &amp;&amp; re_not_empty re2
  | Union re1 re2 =&gt; re_not_empty re1 || re_not_empty re2
  | Star re =&gt; re_not_empty re
  end.

I could prove the backward case easily. For the forward case I stuck at Star re there is a ∃ s, s =~ Star re in the evidences or context and a ∃ s', s' =~ re in the goals. The most probable thing to pass it is using inversion on that evidence but how to tell Coq with destruct to put s1 ++ s2 instead of s and put the results in the context instead of in the goals?
I was similarly stuck on this problem. I believe your Fixpoint for Star re should just be true. In regular expressions, the empty string is always accepted under star.