# Need guidance on proving a lemma

**URL:** <https://discourse.rocq-prover.org/t/need-guidance-on-proving-a-lemma/846>\
**Category:** Using Rocq\
**Tags:** software-foundations\
**Created:** [May 19, 2020, 3:45am UTC](https://discourse.rocq-prover.org/t/need-guidance-on-proving-a-lemma/846 "2020-05-19T03:45:49Z")\
**Posts on this page:** 3\
**Page:** 1

<div class="post-metadata">

**Author:** ![jeffhappily](https://avatars.discourse-cdn.com/v4/letter/j/85e7bf/32.png) [@jeffhappily](https://discourse.rocq-prover.org/u/jeffhappily)\
**Post date:** [May 19, 2020, 3:45am UTC](https://discourse.rocq-prover.org/t/need-guidance-on-proving-a-lemma/846/1 "2020-05-19T03:45:49Z")

</div>

I’m currently reading the book Logical Foundation in Software Foundation. I got stuck proving the lemma `match_eps_refl` so I need some help, here’s the link [https://softwarefoundations.cis.upenn.edu/lf-current/IndProp.html](https://softwarefoundations.cis.upenn.edu/lf-current/IndProp.html).

Given that

```auto
Definition refl_matches_eps m :=
  forall re : @reg_exp ascii, reflect ([] =~ re) (m re).

Fixpoint match_eps (re: @reg_exp ascii) : bool :=
  match re with
  | EmptySet => false
  | EmptyStr => true
  | Char _ => false
  | App r1 r2 => (match_eps r1) && (match_eps r2)
  | Union r1 r2 => (match_eps r1) || (match_eps r2)
  | Star r => match_eps r
  end.

Lemma nil_app_nil : forall (X: Type) (l1 l2: list X),
  l1 ++ l2 = [] -> l1 = [] /\ l2 = [].
Proof.
  intros. destruct l1.
  - simpl in H. split.
    + reflexivity.
    + apply H.
  - discriminate H. Qed.

```

I have to proof that

```auto
Lemma match_eps_refl : refl_matches_eps match_eps.

```

and here’s what I got

```auto
Proof.
  unfold refl_matches_eps. intros.
  induction re.
  - simpl. apply ReflectF. unfold not. intros. inversion H.
  - simpl. apply ReflectT. apply MEmpty.
  - simpl. apply ReflectF. unfold not. intros. inversion H.
  - simpl.
    inversion IHre1.
      + inversion IHre2.
        * simpl. apply ReflectT. apply (MApp [] _ []).
          apply H0. apply H2.
        * simpl. apply ReflectF. unfold not.
          intros. unfold not in H2. inversion H3.
          apply nil_app_nil in H4. destruct H4 as [_ H4]. apply H2.
          rewrite H4 in H8. apply H8.
      + simpl. apply ReflectF.
        unfold not. intros. inversion H1.
        apply nil_app_nil in H2. destruct H2 as [H2 _]. apply H0.
        rewrite H2 in H5. apply H5.
  - simpl. inversion IHre1.
    + simpl. apply ReflectT. apply MUnionL. apply H0.
    + simpl. inversion IHre2.
      * apply ReflectT. apply MUnionR. apply H2.
      * apply ReflectF. unfold not. intros.
        inversion H3.
        { apply H0. apply H6. }
        { apply H2. apply H6. }
  - simpl. inversion IHre.
    + apply ReflectT. apply MStar0.
    + apply ReflectF. unfold not. intros.

```

I’m stuck at the `Star` case and I don’t know how can I continue from there. Hope someone can guide me on this. Thanks!

---

<div class="post-metadata">

**Author:** ![RandomActsOfGrammar](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/randomactsofgrammar/32/326_2.png) [@RandomActsOfGrammar](https://discourse.rocq-prover.org/u/RandomActsOfGrammar)\
**Post date:** [May 19, 2020, 2:13pm UTC](https://discourse.rocq-prover.org/t/need-guidance-on-proving-a-lemma/846/2 "2020-05-19T14:13:49Z")

</div>

Look at your definition of `match_eps` again (the `Star` case in particular) and what its result is supposed to mean. Once you fix that, your final case will be simple.

---

<div class="post-metadata">

**Author:** ![jeffhappily](https://avatars.discourse-cdn.com/v4/letter/j/85e7bf/32.png) [@jeffhappily](https://discourse.rocq-prover.org/u/jeffhappily)\
**Post date:** [May 20, 2020, 1:50am UTC](https://discourse.rocq-prover.org/t/need-guidance-on-proving-a-lemma/846/3 "2020-05-20T01:50:04Z")

</div>

Thanks! I got it working by updating the `Star` case in `match_eps` to just return `true`.