Need guidance on proving a lemma

Using Coq
1

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!

2

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.

3

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

1 Like