# Need guidance on proving a lemma

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.

Given that

``````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

``````Lemma match_eps_refl : refl_matches_eps match_eps.
``````

and here’s what I got

``````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!

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.

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

1 Like