Is there a tactic to help resolving existential quantifiers in Coq?

Question

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 "s =~ re" := (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 => false
  | EmptyStr | Char _ => true
  | App re1 re2 => re_not_empty re1 && re_not_empty re2
  | Union re1 re2 => re_not_empty re1 || re_not_empty re2
  | Star re => 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?

Answer 1

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.

Answer 2

Maybe you can consider changing your definition of re_not_empty.

My definition is shown below.

Fixpoint re_not_empty {T : Type} (re : @reg_exp T) : bool :=
  match re with
  | EmptySet => false
  | EmptyStr | Char _ => true
  | App re1 re2 => re_not_empty re1 && re_not_empty re2
  | Union re1 re2 => re_not_empty re1 || re_not_empty re2
  | Star re => true
  end.

According to my definition, the s ~= Star re situation can be proved easily.

But the problem is, why does re_not_empty Star re is always true? You can look up the definition of exp_match, then you will find that forall re, [] =~ (Star re). So no matter what exactly re is, even it is EmptySet, there always be a [] to match it.

I was also stuck on this problem for a long time. Wish my answer can help you.