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?