1
$\begingroup$

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?

$\endgroup$
1
$\begingroup$

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.

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

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.