# 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 "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.


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?

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.

• That sounds reasonable, but I'm very tired now. I will check it out tomorrow. Oct 6 '20 at 19:53
• It worked but what about such tactics? Oct 8 '20 at 8:04

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.