CODEWITHSUNDEEP
coqlogical-foundations
user4035
user4035

Reputation: 23729

IndProp: re_not_empty_correct

Lemma re_not_empty_correct : forall T (re : @reg_exp T),
  (exists s, s =~ re) <-> re_not_empty re = true.
Proof.
  split.
  - admit. (* I proved it myself *)
  - intros. induction re.
    + simpl in H. discriminate H.
    + exists []. apply MEmpty.
    + exists [t]. apply MChar.
    + simpl in H. rewrite -> andb_true_iff in H. destruct H as [H1 H2].
      apply IHre1 in H1. apply IHre2 in H2.

Here is what we've got so far:

1 subgoal (ID 505)

T : Type
re1, re2 : reg_exp
H1 : exists s : list T, s =~ re1
H2 : exists s : list T, s =~ re2
IHre1 : re_not_empty re1 = true -> exists s : list T, s =~ re1
IHre2 : re_not_empty re2 = true -> exists s : list T, s =~ re2
============================
exists s : list T, s =~ App re1 re2

Now I need either to combine H1 and H2 into exists s : list T, s =~ App re1 re2 or destruct the goal into 2 subgoals and prove them separately using H1 and H2. But I don't know, how to do it.

Upvotes: 1

Views: 335

Answers (1)

Bubbler
Bubbler

Reputation: 982

You can think of exists as a pair type which includes a value and its property. Just like an ordinary pair type, you can destruct it.

For example, destruct H1 as [s1 H1]. at that point gives

s1 : list T
H1 : s1 =~ re1

Given this, think about how to construct an s in the goal that satisfies s =~ App re1 re2. Then use the tactic exists (your answer). (which will change the goal to (your answer) =~ App re1 re2) and fill in the rest of the proof (it should be trivial if your s is correct).

Upvotes: 1

Related Questions